Form1.trace — the fibrewise trace of a holomorphic 1-form (jacobian-functoriality §6)

Unit: jacobian-functoriality. For a nonconstant holomorphic f : X → Y between Riemann surfaces (X compact connected), the trace Tr_f η ∈ Form1 Y of η ∈ Form1 X: in the target chart at y, its coefficient is the sum over the fibre stack at y of the repaired Jacobian-weighted planar traces (RS.traceCoeff, TraceCoeff.lean) of η's chart coefficients, transported by the branch/chart transition derivatives.

Main declarations:

• RS.stackAt/RS.traceChart/RS.branchTrans/RS.traceCoeffFun — the coefficient data over the chart family ι := Y (preferred charts restricted to the stack neighborhoods S.V).
• RS.qCoeff f η e₀ x = (deriv (e₀ ∘ f ∘ (chartAt x).symm))⁻¹ * coeffAt x η — the canonical (stack-free) per-fibre-point coefficient of the trace; RS.traceCoeffFun_eq_qSum identifies the defining coefficient with ∑ᶠ x ∈ f⁻¹{yhat}, qCoeff … away from the chart center (well- definedness), and RS.qSum_trans is its chart-transition law — together these give compat on a dense subset of each chart overlap, extended to the whole overlap by continuity (ContinuousOn.eqOn_of_subset_closure, Density.lean).
• RS.traceForm hf hne η : Form1 Y (via Form1.ofCoeffs) and the challenge-facing RS.Form1.trace (f : X → Y) (hf) : Form1 X →ₗ[ℂ] Form1 Y (zero for constant f).
• RS.coeffAt_traceForm (the preferred-chart evaluation) and RS.coeffAt_traceForm_of_isRegularValue (the regular-value formula, feed for the projection formula / functoriality laws / the trace–period relation).

Planar helper: congruence of traceZk on the root set

theorem RS.MTrace.traceZk_congr_root {g g' : ℂ → ℂ} {k : ℕ} {w : ℂ} (h : ∀ (v : ℂ), v ^ k = w → g v = g' v) : traceZk g k w = traceZk g' k w

Generic chart helpers

theorem RS.deriv_eq_of_eventuallyEq_comp' {g h k : ℂ → ℂ} {z : ℂ} (hg : DifferentiableAt ℂ g (h z)) (hh : DifferentiableAt ℂ h z) (heq : k =ᶠ[nhds z] g ∘ h) : deriv k z = deriv g (h z) * deriv h z

Chain rule for deriv through an eventual factorization (local copy of Pullback.lean's private helper).

theorem RS.deriv_transition_mul {M : Type u_1} [TopologicalSpace M] [ChartedSpace ℂ M] {e e' : OpenPartialHomeomorph M ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ M) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ M) {q : M} (hq : q ∈ e.source) (hq' : q ∈ e'.source) : deriv (↑e' ∘ ↑e.symm) (↑e q) * deriv (↑e ∘ ↑e'.symm) (↑e' q) = 1

The two transition derivatives between overlapping maximal-atlas charts are mutually inverse.

theorem RS.open_subset_closure_diff {U : Set ℂ} (hU : IsOpen U) {s : Set ℂ} (hs : s.Finite) : U ⊆ closure (U \ s)

A nonempty open planar set is inside the closure of its complement of any finite set.

The trace coefficient data

noncomputable def RS.stackAt {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (y : Y) : FiberStack f y

The canonical fibre stack at y (a fixed choice, shared by every construction below).

Equations

• RS.stackAt hf hne y = ⋯.some

noncomputable def RS.traceChart {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (y : Y) : OpenPartialHomeomorph Y ℂ

The chart of the trace's coefficient data at index y: the preferred chart at y, restricted to the stack neighborhood (stackAt hf hne y).V.

Equations

• RS.traceChart hf hne y = (chartAt ℂ y).restr (RS.stackAt hf hne y).V

@[simp]

theorem RS.traceChart_coe {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (y : Y) : ↑(traceChart hf hne y) = ↑(chartAt ℂ y)

@[simp]

theorem RS.traceChart_symm_coe {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (y : Y) : ↑(traceChart hf hne y).symm = ↑(chartAt ℂ y).symm

theorem RS.traceChart_source {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (y : Y) : (traceChart hf hne y).source = (chartAt ℂ y).source ∩ (stackAt hf hne y).V

theorem RS.traceChart_target_eq {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (y : Y) : (traceChart hf hne y).target = (chartAt ℂ y).target ∩ ↑(chartAt ℂ y).symm ⁻¹' (stackAt hf hne y).V

theorem RS.mem_traceChart_source_self {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (y : Y) : y ∈ (traceChart hf hne y).source

theorem RS.traceChart_mem_maximalAtlas {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (y : Y) : traceChart hf hne y ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ Y

noncomputable def RS.branchTrans {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (y : Y) (i : Fin (stackAt hf hne y).n) : ℂ → ℂ

The transition from the preferred chart's coordinate at y to the i-th branch's target chart coordinate.

Equations

• RS.branchTrans hf hne y i = ↑((RS.stackAt hf hne y).A i).e' ∘ ↑(chartAt ℂ y).symm

theorem RS.analyticAt_branchTrans {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (y : Y) {w : ℂ} (hw : w ∈ (traceChart hf hne y).target) (i : Fin (stackAt hf hne y).n) : AnalyticAt ℂ (branchTrans hf hne y i) w

theorem RS.branchTrans_mem_ball {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (y : Y) {w : ℂ} (hw : w ∈ (traceChart hf hne y).target) (i : Fin (stackAt hf hne y).n) : branchTrans hf hne y i w ∈ Metric.ball 0 (((stackAt hf hne y).A i).radius ^ multiplicity f ((stackAt hf hne y).pt i))

noncomputable def RS.traceCoeffFun {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (η : Form1 X) (y : Y) : ℂ → ℂ

The coefficient of the trace in the chart at index y: the branch-transported sum of the repaired planar trace coefficients of η's stack-chart coefficients.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.analyticAt_coeffIn_stack_zero {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (η : Form1 X) (y : Y) (i : Fin (stackAt hf hne y).n) : AnalyticAt ℂ (coeffIn ((stackAt hf hne y).A i).e η) 0

theorem RS.analyticOnNhd_traceCoeffFun {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (η : Form1 X) (y : Y) : AnalyticOnNhd ℂ (traceCoeffFun hf hne η y) (traceChart hf hne y).target

Analyticity of the trace coefficient on the whole (restricted) chart target — including across branch points (the previous builder's blocker, discharged by RS.analyticOnNhd_traceCoeff).

The canonical per-fibre-point coefficient qCoeff

noncomputable def RS.qCoeff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] (f : X → Y) (η : Form1 X) (e₀ : OpenPartialHomeomorph Y ℂ) (x : X) : ℂ

The canonical (stack-independent) contribution of a fibre point x to the trace's coefficient in a target chart e₀: the coefficient of η at x, divided by the chart derivative of f. (Junk 0 at ramified x, where the chart derivative vanishes.)

Equations

• RS.qCoeff f η e₀ x = (deriv (↑e₀ ∘ f ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x))⁻¹ * RS.coeffAt x η

theorem RS.deriv_chartRead_eq_of_adapted {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {x₀ : X} {k : ℕ} (A : AdaptedChartsAt f x₀ k) {e₀ : OpenPartialHomeomorph Y ℂ} (he₀ : e₀ ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ Y) {x : X} (hx : x ∈ A.e.source) (hfx : f x ∈ e₀.source) : deriv (↑e₀ ∘ f ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x) = deriv (↑e₀ ∘ ↑A.e'.symm) (↑A.e' (f x)) * (↑k * ↑A.e x ^ (k - 1)) * deriv (↑A.e ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x)

Factorization of the chart derivative of f through a pair of adapted charts: d(f-in-charts) = d(target transition) · (k·v^(k-1)) · d(source transition).

theorem RS.qCoeff_eq_branch_term {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {y : Y} (S : FiberStack f y) (i : Fin S.n) {e₀ : OpenPartialHomeomorph Y ℂ} (he₀ : e₀ ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ Y) {x : X} (hx : x ∈ (S.A i).e.source) (hfx : f x ∈ e₀.source) (η : Form1 X) : qCoeff f η e₀ x = deriv (↑(S.A i).e' ∘ ↑e₀.symm) (↑e₀ (f x)) * (coeffIn (S.A i).e η (↑(S.A i).e x) * (↑(multiplicity f (S.pt i)) * ↑(S.A i).e x ^ (↑(multiplicity f (S.pt i)) - 1))⁻¹)

The per-fibre-point identity: qCoeff computed through the i-th branch of a fibre stack is exactly the branch-transported, Jacobian-divided coefficient of η (the integrand of traceZkForm). Holds at ramified points too (both sides junk to 0).

theorem RS.traceCoeffFun_eq_qSum {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (η : Form1 X) {y yhat : Y} (hyhat : yhat ∈ (traceChart hf hne y).source) (hyhatne : yhat ≠ y) : traceCoeffFun hf hne η y (↑(chartAt ℂ y) yhat) = ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {yhat}), qCoeff f η (chartAt ℂ y) x

Well-definedness at non-center points: the defining coefficient of the trace at yhat ≠ y (in the chart at index y) is the canonical qCoeff fibre sum over f⁻¹{yhat}.

theorem RS.qSum_trans {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (η : Form1 X) {yhat : Y} {e₀ e₁ : OpenPartialHomeomorph Y ℂ} (he₀ : e₀ ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ Y) (he₁ : e₁ ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ Y) (hyhat₀ : yhat ∈ e₀.source) (hyhat₁ : yhat ∈ e₁.source) : ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {yhat}), qCoeff f η e₁ x = deriv (↑e₀ ∘ ↑e₁.symm) (↑e₁ yhat) * ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {yhat}), qCoeff f η e₀ x

The chart-transition law for the canonical fibre sum.

theorem RS.traceCoeffFun_compat {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (η : Form1 X) (y y' p : Y) (hp : p ∈ (traceChart hf hne y).source ∩ (traceChart hf hne y').source) : traceCoeffFun hf hne η y' (↑(traceChart hf hne y') p) = deriv (↑(traceChart hf hne y) ∘ ↑(traceChart hf hne y').symm) (↑(traceChart hf hne y') p) * traceCoeffFun hf hne η y (↑(traceChart hf hne y) p)

The chart-compatibility law (CC1) of the trace's coefficient data: proved on the dense subset of the overlap avoiding the two chart centers via traceCoeffFun_eq_qSum/qSum_trans, and extended to the whole overlap by continuity.

Assembly: traceForm and Form1.trace

noncomputable def RS.traceData {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (η : Form1 X) : Form1CoeffData Y Y

The trace's coefficient data over the chart family ι := Y.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.traceForm {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (η : Form1 X) : Form1 Y

The trace of a holomorphic 1-form along a nonconstant holomorphic map, as a raw Form1 Y.

Equations

• RS.traceForm hf hne η = RS.Form1.ofCoeffs (RS.traceData hf hne η)

theorem RS.coeffIn_traceChart_traceForm {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (η : Form1 X) (y : Y) {w : ℂ} (hw : w ∈ (traceChart hf hne y).target) : coeffIn (traceChart hf hne y) (traceForm hf hne η) w = traceCoeffFun hf hne η y w

theorem RS.coeffAt_traceForm {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (η : Form1 X) (yhat : Y) : coeffAt yhat (traceForm hf hne η) = traceCoeffFun hf hne η yhat (↑(chartAt ℂ yhat) yhat)

Preferred-chart evaluation of the trace: the chart at index yhat restricts the preferred chart at yhat, so the transition factor is 1.

theorem RS.traceCoeffFun_add {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (η η' : Form1 X) (y : Y) (w : ℂ) : traceCoeffFun hf hne (η + η') y w = traceCoeffFun hf hne η y w + traceCoeffFun hf hne η' y w

Pointwise additivity of the trace coefficient in η.

theorem RS.traceCoeffFun_smul {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (c : ℂ) (η : Form1 X) (y : Y) (w : ℂ) : traceCoeffFun hf hne (c • η) y w = c * traceCoeffFun hf hne η y w

Pointwise ℂ-homogeneity of the trace coefficient in η.

theorem RS.traceForm_add {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (η η' : Form1 X) : traceForm hf hne (η + η') = traceForm hf hne η + traceForm hf hne η'

theorem RS.traceForm_smul {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (c : ℂ) (η : Form1 X) : traceForm hf hne (c • η) = c • traceForm hf hne η

noncomputable def RS.Form1.trace {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] (f : X → Y) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) : Form1 X →ₗ[ℂ] Form1 Y

Form1.trace (§6.1): the fibrewise trace of holomorphic 1-forms along a holomorphic f : X → Y, as a ℂ-linear map Form1 X →ₗ[ℂ] Form1 Y. The zero map for constant f (matching the gist's pullback convention on Jacobians).

Equations

• RS.Form1.trace f hf = if hne : ∃ (c : Y), ∀ (x : X), f x = c then 0 else { toFun := RS.traceForm hf hne, map_add' := ⋯, map_smul' := ⋯ }

theorem RS.Form1.trace_apply {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (η : Form1 X) : (trace f hf) η = traceForm hf hne η

theorem RS.Form1.trace_of_forall_eq {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hc : ∃ (c : Y), ∀ (x : X), f x = c) : trace f hf = 0

The regular-value formula

theorem RS.traceCoeff_eq_of_eq_one {h : ℂ → ℂ} {k : ℕ} (hk : k = 1) (hh : AnalyticAt ℂ h 0) : traceCoeff h k = h

traceCoeff at an unramified branch (k = 1, hypothesis form usable under type-dependent k).

theorem RS.coeffAt_traceForm_of_isRegularValue {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (hne : ¬∃ (c : Y), ∀ (x : X), f x = c) (η : Form1 X) {yhat : Y} (hyhat : IsRegularValue f yhat) : coeffAt yhat (traceForm hf hne η) = ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {yhat}), qCoeff f η (chartAt ℂ yhat) x

Regular-value evaluation of the trace: at a regular value yhat, the preferred-chart coefficient of traceForm η is the canonical fibre sum of qCoeff (every branch is unramified there, so the repaired coefficient evaluates literally).