A machine-checked solution to the Jacobians challenge

12.5. MeromorphicTrace.TraceForm🔗

Jacobians.MeromorphicTrace.TraceForm — source

traceSummand

The covector at y = f x obtained by pulling back α x through the inverse of mfderiv f x. The summand of the fibre-sum trace.

Typed in the model fibre ℂ →L[ℂ] ℂ (definitionally equal to T_{f x} Y →L[ℂ] ℂ and to T_y Y →L[ℂ] ℂ, since TangentSpace 𝓘(ℂ) _ = ℂ reduces to ℂ). Working in the model fibre means the fibre sum requires no transport between cotangent spaces of different fibre points.

(NB: the form variable is α, not ω — in this codebase ω is the analytic smoothness exponent IsManifold 𝓘(ℂ) ω X.)

noncomputable def traceSummand {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [ChartedSpace ℂ Y] (f : X → Y) (α : HolomorphicOneForms X) (x : X) :
    ℂ →L[ℂ] ℂ

sheetPullback

Value of the single-section pullback covector (α (g y)) ∘ mfderiv g y at a point y, in the cotangent fibre at y. The per-sheet term of the local representation of the fibre-sum trace over a base neighborhood.

noncomputable def sheetPullback {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [ChartedSpace ℂ Y] (α : HolomorphicOneForms X) (g : Y → X) (y : Y) :
    TangentSpace 𝓘(ℂ) y →L[ℂ] ℂ

contMDiffAt_pullback_section

The hom-bundle section y ↦ (α (s y)) ∘ mfderiv s y is ContMDiffAt at y₀ (as a section into the cotangent bundle of Y) whenever s is ContMDiffAt at y₀. Pointwise version of pullbackForm's contMDiff_toFun proof: the global ContMDiff hypothesis there is only ever used at the single point x₀, so it weakens to ContMDiffAt. This is what allows pulling a form back along a *local* holomorphic section, which is only ContMDiffOn its domain.

theorem contMDiffAt_pullback_section {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (α : HolomorphicOneForms X) {s : Y → X} {y₀ : Y}
    (hs : ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) ω s y₀) :
    ContMDiffAt 𝓘(ℂ) (𝓘(ℂ).prod 𝓘(ℂ, ℂ →L[ℂ] ℂ)) ω
      (fun y : Y => Bundle.TotalSpace.mk'
        (E := fun y : Y => TangentSpace 𝓘(ℂ) y →L[ℂ] (Bundle.Trivial Y ℂ) y) (ℂ →L[ℂ] ℂ) y
        ((α.toFun (s y)).comp (mfderiv 𝓘(ℂ) 𝓘(ℂ) s y))) y₀

contMDiffAt_sheetPullback

sheetPullback α g is ContMDiffAt at y₀ whenever g is ContMDiffAt there. Restatement of contMDiffAt_pullback_section in terms of sheetPullback (as a section into the cotangent bundle of Y).

theorem contMDiffAt_sheetPullback {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (α : HolomorphicOneForms X) {g : Y → X} {y₀ : Y}
    (hg : ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) ω g y₀) :
    ContMDiffAt 𝓘(ℂ) (𝓘(ℂ).prod 𝓘(ℂ, ℂ →L[ℂ] ℂ)) ω
      (fun y : Y => Bundle.TotalSpace.mk'
        (E := fun y : Y => TangentSpace 𝓘(ℂ) y →L[ℂ] (Bundle.Trivial Y ℂ) y) (ℂ →L[ℂ] ℂ) y
        (sheetPullback α g y)) y₀

mfderiv_section_eq_inverse

For a two-sided local inverse pair (f, s) around (x₀, y₀) (i.e. f ∘ s = id near y₀ and s ∘ f = id near x₀, with s y₀ = x₀ and f x₀ = y₀), the derivative of the section is the ContinuousLinearMap.inverse of mfderiv f x₀. Chain rule (mfderiv_comp) on both local identities + mfderiv_id + ContinuousLinearMap.inverse_eq.

theorem mfderiv_section_eq_inverse {X Y : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {s : Y → X} {x₀ : X} {y₀ : Y}
    (hsx : s y₀ = x₀) (hfx : f x₀ = y₀)
    (hf_diff : MDifferentiableAt 𝓘(ℂ) 𝓘(ℂ) f x₀)
    (hs_diff : MDifferentiableAt 𝓘(ℂ) 𝓘(ℂ) s y₀)
    (hfs : (f ∘ s) =ᶠ[𝓝 y₀] id) (hsf : (s ∘ f) =ᶠ[𝓝 x₀] id) :
    mfderiv 𝓘(ℂ) 𝓘(ℂ) s y₀ = (mfderiv 𝓘(ℂ) 𝓘(ℂ) f x₀).inverse

exists_twoSided_localInverse

A C^ω two-sided local inverse g at a non-critical point x₀: an open V ∋ f x₀ with g (f x₀) = x₀, f ∘ g = id on V, g ∘ f = id near x₀, and g smooth on V.

theorem exists_twoSided_localInverse {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y] [T2Space Y]
    [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) {x₀ : X} (hxcrit : x₀ ∉ criticalSet f) :
    ∃ (g : Y → X) (V : Set Y), IsOpen V ∧ f x₀ ∈ V ∧ g (f x₀) = x₀ ∧
      (∀ y ∈ V, f (g y) = y) ∧ ContMDiffOn 𝓘(ℂ) 𝓘(ℂ) ω g V ∧
      ((g ∘ f) =ᶠ[𝓝 x₀] id)

traceSummand_eq_sheetPullback

Key value identity. At y₀ = f x₀, the trace summand traceSummand f α x₀ equals sheetPullback α g y₀ for any two-sided local section g through x₀. Combines g (f x₀) = x₀ with mfderiv g (f x₀) = (mfderiv f x₀).inverse (mfderiv_section_eq_inverse), so the off-branch fibre sum is, sheet by sheet, a holomorphic pullback.

theorem traceSummand_eq_sheetPullback {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {g : Y → X} {x₀ : X}
    (α : HolomorphicOneForms X) (hgfx : g (f x₀) = x₀)
    (hf_diff : MDifferentiableAt 𝓘(ℂ) 𝓘(ℂ) f x₀)
    (hg_diff : MDifferentiableAt 𝓘(ℂ) 𝓘(ℂ) g (f x₀))
    (hfs : (f ∘ g) =ᶠ[𝓝 (f x₀)] id) (hsf : (g ∘ f) =ᶠ[𝓝 x₀] id) :
    traceSummand f α x₀ = sheetPullback α g (f x₀)

traceSummand_add

traceSummand is additive in the form.

theorem traceSummand_add {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [ChartedSpace ℂ Y] (f : X → Y) (α β : HolomorphicOneForms X) (x : X) :
    traceSummand f (α + β) x = traceSummand f α x + traceSummand f β x

traceSummand_smul

traceSummand is ℂ-homogeneous in the form.

theorem traceSummand_smul {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [ChartedSpace ℂ Y] (f : X → Y) (c : ℂ) (α : HolomorphicOneForms X) (x : X) :
    traceSummand f (c • α) x = c • traceSummand f α x

traceSummandAt

Retyping of the trace summand to the cotangent fibre at y, given f x = y. Since TangentSpace 𝓘(ℂ) (f x) = TangentSpace 𝓘(ℂ) y definitionally collapses to ℂ, this is a transport along f x = y.

noncomputable def traceSummandAt {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [ChartedSpace ℂ Y] (f : X → Y) (α : HolomorphicOneForms X) (_y : Y) (x : X) :
    ℂ →L[ℂ] ℂ

traceFun

Trace value (fibre sum). The covector at y obtained by summing traceSummand f α x over the fibre f⁻¹{y}. Total via finsum (= 0 when the fibre is infinite); off the branch locus the fibre is finite and this is the genuine finite sum. Typed in the model fibre ℂ →L[ℂ] ℂ, which is definitionally the cotangent fibre T_y Y →L[ℂ] ℂ.

noncomputable def traceFun {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [ChartedSpace ℂ Y] (f : X → Y) (α : HolomorphicOneForms X) (y : Y) :
    ℂ →L[ℂ] ℂ

LocalSheetSystem

Local sheet system of a branched cover f over a base neighborhood V of y₀ (off the branch locus). Bundles the finitely many holomorphic sections whose images sweep out the entire fibre at each point of V. This is precisely the trivialization data of the covering isCoveringMapOn_compl_branchLocus, repackaged as sections (Forster §4.22).

structure LocalSheetSystem {X Y : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [TopologicalSpace Y] [ChartedSpace ℂ Y] (f : X → Y) (y₀ : Y) where

sheet_mdifferentiableAt

Each sheet is MDifferentiableAt at every point of V.

theorem sheet_mdifferentiableAt {X Y : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {y₀ : Y} (S : LocalSheetSystem f y₀)
    (i : Fin S.n) {y : Y} (hy : y ∈ S.V) :
    MDifferentiableAt 𝓘(ℂ) 𝓘(ℂ) (S.sheet i) y

traceSummandAt_sheet_eq

Per-sheet value identity. On V, the retyped fibre summand at the sheet point sheet i y equals sheetPullback α (sheet i) y.

theorem traceSummandAt_sheet_eq {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [ChartedSpace ℂ Y] {f : X → Y} {y₀ : Y} (S : LocalSheetSystem f y₀)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (α : HolomorphicOneForms X) (i : Fin S.n) {y : Y} (hy : y ∈ S.V) :
    traceSummandAt f α y (S.sheet i y) = sheetPullback α (S.sheet i) y

traceFun_eq_sum_sheetPullback

Local representation of the trace (off-branch core). Over the base neighborhood V, the fibre-sum trace is the finite sum of the per-sheet pullbacks: traceFun f α y = ∑ᵢ sheetPullback α (sheet i) y. The fibre f⁻¹{y} is the range of the injective sheet map (fibre_eq + sheet_inj), so the finsum over the fibre collapses to the finite sum over the n sheets (finsum_mem_range), each term identified by traceSummandAt_sheet_eq.

theorem traceFun_eq_sum_sheetPullback {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {y₀ : Y} (S : LocalSheetSystem f y₀)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (α : HolomorphicOneForms X) {y : Y} (hy : y ∈ S.V) :
    traceFun f α y = ∑ i, sheetPullback α (S.sheet i) y

contMDiffAt_traceFun

Off-branch holomorphicity. Given a local sheet system at y₀, the trace section y ↦ traceFun f α y is ContMDiffAt (analytic) at y₀ — i.e. the fibre-sum trace is a holomorphic one-form near y₀. Reduces, via the local representation traceFun = ∑ᵢ sheetPullback (sheet i) on V, to the per-sheet smoothness contMDiffAt_sheetPullback summed over the (finitely many) sheets (ContMDiffAt.sum_section).

theorem contMDiffAt_traceFun {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] {f : X → Y} {y₀ : Y} (S : LocalSheetSystem f y₀)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (α : HolomorphicOneForms X) :
    ContMDiffAt 𝓘(ℂ) (𝓘(ℂ).prod 𝓘(ℂ, ℂ →L[ℂ] ℂ)) ω
      (fun y : Y => Bundle.TotalSpace.mk'
        (E := fun y : Y => TangentSpace 𝓘(ℂ) y →L[ℂ] (Bundle.Trivial Y ℂ) y) (ℂ →L[ℂ] ℂ) y
        (traceFun f α y)) y₀

traceFun_add_of_notMem_branchLocus

Additivity of the fibre-sum trace off the branch locus.

theorem traceFun_add_of_notMem_branchLocus {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) (α β : HolomorphicOneForms X)
    {y : Y} (hy : y ∉ branchLocus f) :
    traceFun f (α + β) y = traceFun f α y + traceFun f β y

traceFun_smul_of_notMem_branchLocus

ℂ-homogeneity of the fibre-sum trace off the branch locus.

theorem traceFun_smul_of_notMem_branchLocus {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) (c : ℂ) (α : HolomorphicOneForms X)
    {y : Y} (hy : y ∉ branchLocus f) :
    traceFun f (c • α) y = c • traceFun f α y

exists_localSheetSystem

Off the branch locus a local sheet system exists (Forster §4.22).

Construction (no covering trivialization needed — assembled directly from the proven local pieces): the fibre f⁻¹{y₀} is finite (fiber_finite_off_branchLocus), enumerated as pt : Fin n → X via Fintype.equivFin. The pt i are pairwise distinct points off criticalSet, separated by pairwise-disjoint opens Sep i (X is T2, Set.Finite.t2_separation). At each pt i, exists_twoSided_localInverse gives a C^ω two-sided section g i on an open Vsec i ∋ y₀ (supplying sheet_smooth, sheet_section, and the sheet_leftInv content), and isLocalHomeoOffCritical gives an open injective neighborhood, shrunk into Sep i to make the sheets disjoint. Properness (properNbhd of isProperMap_of_contMDiff) shrinks the fibre's open cover ⋃ Uinj to a base Ubase ∋ y₀ with f⁻¹ Ubase ⊆ ⋃ Uinj. Over V := Ubase ∩ ⋂ i (Vsec i ∩ g i⁻¹ (Uinj i)) every preimage of y ∈ V lands in some Uinj j, where g j y is its unique preimage — giving fibre_eq; the disjoint Sep i give sheet_inj. With this, contMDiffAt_traceFun_of_notMem_branchLocus (off-branch holomorphicity of the trace) is unconditional.

theorem exists_localSheetSystem {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y] [T2Space Y]
    [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) {y₀ : Y} (hy₀ : y₀ ∉ branchLocus f) :
    Nonempty (LocalSheetSystem f y₀)

contMDiffAt_traceFun_of_notMem_branchLocus

Off-branch holomorphicity of the trace, top-level form. For y₀ off the branch locus, the fibre-sum trace y ↦ traceFun f α y is ContMDiffAt (a holomorphic one-form) at y₀. Combines exists_localSheetSystem (the isolated covering step) with the fully-proven LocalSheetSystem.contMDiffAt_traceFun.

theorem contMDiffAt_traceFun_of_notMem_branchLocus {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀)
    (α : HolomorphicOneForms X) {y₀ : Y} (hy₀ : y₀ ∉ branchLocus f) :
    ContMDiffAt 𝓘(ℂ) (𝓘(ℂ).prod 𝓘(ℂ, ℂ →L[ℂ] ℂ)) ω
      (fun y : Y => Bundle.TotalSpace.mk'
        (E := fun y : Y => TangentSpace 𝓘(ℂ) y →L[ℂ] (Bundle.Trivial Y ℂ) y) (ℂ →L[ℂ] ℂ) y
        (traceFun f α y)) y₀

traceTotalSpaceMk

The trace, packaged as a map into the total space of the cotangent bundle of Y (the shape consumed by ContMDiffAt/ContMDiffSection). coeff is the covector to place in the fibre at y — either the raw fibre sum traceFun f α y or its branch extension traceFunExt f α y.

noncomputable abbrev traceTotalSpaceMk {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    (coeff : Y → (ℂ →L[ℂ] ℂ)) (y : Y) :
    Bundle.TotalSpace (ℂ →L[ℂ] ℂ)
      (fun y : Y => TangentSpace 𝓘(ℂ) y →L[ℂ] (Bundle.Trivial Y ℂ) y)

traceLocalCoeff

Local coefficient of the trace. The coordinate of the (extended) trace section coeff read in the *fixed* hom-bundle trivialization at y₀, evaluated on the model basis vector 1 : ℂ. Concretely inCoordinates … y₀ y y₀ y (coeff y) (1 : ℂ) : ℂ. This is the continuous/holomorphic object (unlike the raw (coeff y) 1); the trace section is ContMDiffAt/ContinuousAt at y₀ iff this scalar is, by contMDiffAt_hom_bundle. We define it for an arbitrary coefficient so it can be applied to both traceFun and traceFunExt.

noncomputable def traceLocalCoeff {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (coeff : Y → (ℂ →L[ℂ] ℂ)) (y₀ y : Y) : ℂ

clm_eq_apply_one_smul_id

A ℂ →L[ℂ] ℂ operator is its value-at-1 times the identity: φ = (φ 1) • id. The elementary fact underlying the reconstruction of an operator-valued chart coordinate from its scalar coordinate.

theorem clm_eq_apply_one_smul_id (φ : ℂ →L[ℂ] ℂ) :
    φ = (φ (1 : ℂ)) • ContinuousLinearMap.id ℂ ℂ

tangent_continuousLinearMapAt_center

Tangent trivialization is the identity at its own center. The fixed y₀-tangent trivialization's fiber coordinate map continuousLinearMapAt … y₀ is id (the chart-transition derivative D(chart ∘ chart.symm) at the center is D id = id). This is the precise sense in which the *fixed* trivialization removes the chart-frame discontinuity at y₀.

theorem tangent_continuousLinearMapAt_center {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (y₀ : Y) :
    (trivializationAt ℂ (TangentSpace 𝓘(ℂ) (M := Y)) y₀).continuousLinearMapAt ℂ y₀
      = ContinuousLinearMap.id ℂ ℂ

tangent_symmL_center

The inverse tangent trivialization symmL … y₀ is also id at the center (inverse of tangent_continuousLinearMapAt_center).

theorem tangent_symmL_center {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (y₀ : Y) :
    (trivializationAt ℂ (TangentSpace 𝓘(ℂ) (M := Y)) y₀).symmL ℂ y₀
      = ContinuousLinearMap.id ℂ ℂ

inCoordinates_center_self

The fixed-frame coordinate change is the identity AT the center y₀. For the cotangent hom-bundle, inCoordinates … y₀ y₀ y₀ y₀ φ = φ: at the center both the source (tangent) and target (trivial) coordinate changes are id. Consequently the *local coefficient* read at the center recovers the raw value, traceLocalCoeff coeff y₀ y₀ = (coeff y₀) 1 (traceLocalCoeff_center). This is what makes the branch value L • id self-consistent: its local coefficient at y₀ is exactly L.

theorem inCoordinates_center_self {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (φ : ℂ →L[ℂ] ℂ) (y₀ : Y) :
    ContinuousLinearMap.inCoordinates ℂ (TangentSpace 𝓘(ℂ) (M := Y)) ℂ (Bundle.Trivial Y ℂ)
      y₀ y₀ y₀ y₀ φ = φ

traceLocalCoeff_center

Local coefficient at the center recovers the raw value-at-1. Immediate from inCoordinates_center_self.

theorem traceLocalCoeff_center {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (coeff : Y → (ℂ →L[ℂ] ℂ)) (y₀ : Y) :
    traceLocalCoeff coeff y₀ y₀ = (coeff y₀) (1 : ℂ)

inCoordinates_apply_one_add

inCoordinates of the cotangent hom-bundle, value-at-1, is additive in the operator. The target trivial-bundle coordinate continuousLinearMapAt is id, so inCoordinates … φ 1 reduces to φ (symmL … 1), additive in φ.

theorem inCoordinates_apply_one_add {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (φ ψ : ℂ →L[ℂ] ℂ) (y₀ y : Y) :
    ContinuousLinearMap.inCoordinates ℂ (TangentSpace 𝓘(ℂ) (M := Y)) ℂ (Bundle.Trivial Y ℂ)
        y₀ y y₀ y (φ + ψ) (1 : ℂ)
      = ContinuousLinearMap.inCoordinates ℂ (TangentSpace 𝓘(ℂ) (M := Y)) ℂ (Bundle.Trivial Y ℂ)
          y₀ y y₀ y φ (1 : ℂ)
        + ContinuousLinearMap.inCoordinates ℂ (TangentSpace 𝓘(ℂ) (M := Y)) ℂ (Bundle.Trivial Y ℂ)
          y₀ y y₀ y ψ (1 : ℂ)

inCoordinates_apply_one_smul

inCoordinates value-at-1 is ℂ-homogeneous in the operator. Companion to inCoordinates_apply_one_add.

theorem inCoordinates_apply_one_smul {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (a : ℂ) (φ : ℂ →L[ℂ] ℂ) (y₀ y : Y) :
    ContinuousLinearMap.inCoordinates ℂ (TangentSpace 𝓘(ℂ) (M := Y)) ℂ (Bundle.Trivial Y ℂ)
        y₀ y y₀ y (a • φ) (1 : ℂ)
      = a • ContinuousLinearMap.inCoordinates ℂ (TangentSpace 𝓘(ℂ) (M := Y)) ℂ (Bundle.Trivial Y ℂ)
          y₀ y y₀ y φ (1 : ℂ)

traceBranchValue

Branch value of the trace, in the fixed y₀-frame. At a branch point y₀ the operator traceFun f α y (read in the *varying* chart at y) is genuinely discontinuous as y → y₀ for a non-trivial tangent bundle (genus ≥ 2; the CotangentCoeff.lean obstruction), so the naive operator limUnder is junk. The geometrically-correct value is built from the local coefficient read in the FIXED y₀-chart: take its removable-singularity limit L (a scalar in ℂ, the chart-pullback limUnder of z ↦ traceLocalCoeff (traceFun f α) y₀ (chart⁻¹ z)) and package it as the operator L • id. By traceLocalCoeff_center, this operator's own local coefficient at y₀ is exactly L, so the extension is self-consistent and its section is the continuous bundle-extension.

noncomputable def traceBranchValue {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (α : HolomorphicOneForms X) (y₀ : Y) :
    ℂ →L[ℂ] ℂ

traceFunExt

Canonical branch extension of the trace coefficient. Equal to the fibre sum traceFun f α off the branch locus, and to the fixed-frame branch value traceBranchValue at each branch point (where the naive finsum is 0). At a branch point the branch value is read in the fixed y₀-trivialization (the local coefficient), NOT as the raw-operator limit — the latter is discontinuous for a non-trivial tangent bundle. The membership test is decidable via Classical.dec.

noncomputable def traceFunExt {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (α : HolomorphicOneForms X) (y : Y) :
    ℂ →L[ℂ] ℂ

traceFunExt_of_notMem_branchLocus

Off the branch locus, the extension is the raw fibre sum.

theorem traceFunExt_of_notMem_branchLocus {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y)
    (α : HolomorphicOneForms X)
    {y : Y} (hy : y ∉ branchLocus f) :
    traceFunExt f α y = traceFun f α y

traceFunExt_of_mem_branchLocus

At a branch point, the extension is the fixed-frame branch value.

theorem traceFunExt_of_mem_branchLocus {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y)
    (α : HolomorphicOneForms X)
    {y : Y} (hy : y ∈ branchLocus f) :
    traceFunExt f α y = traceBranchValue f α y

traceFunExt_branchPoint_eq_smul_id

At a branch point the extension operator is (local coefficient) • id. Since the branch value is L • id and traceLocalCoeff (L • id) y y = L (traceLocalCoeff_center), the operator traceFunExt f α y is recovered from its own (scalar, linear-in-α) local coefficient. This is the bridge that turns the ℂ-linearity of the *scalar* local coefficient into ℂ-linearity of the *operator* extension at branch points.

theorem traceFunExt_branchPoint_eq_smul_id {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y)
    (α : HolomorphicOneForms X)
    {y : Y} (hy : y ∈ branchLocus f) :
    traceFunExt f α y = (traceLocalCoeff (traceFunExt f α) y y) • ContinuousLinearMap.id ℂ ℂ

eventually_notMem_branchLocus

A punctured neighborhood of any point y₀ eventually avoids the branch locus: the branch locus is finite (hence branchLocus f \ {y₀} is closed), so its complement is a neighborhood of y₀, and a point there which is also ≠ y₀ is off-branch. This is the engine behind both the agreement lemma below and the linearity argument: on 𝓝[≠] y₀ the trace is genuinely the off-branch fibre sum.

theorem eventually_notMem_branchLocus {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) (y₀ : Y) :
    ∀ᶠ y in 𝓝[≠] y₀, y ∉ branchLocus f

contMDiffAt_traceSection_ext_of_notMem_branchLocus

The extended trace section is ContMDiffAt at every point off the branch locus, unconditionally (no analytic hypothesis): the extension agrees with the raw fibre sum on the open set (branchLocus f)ᶜ, where the fibre sum is holomorphic (contMDiffAt_traceFun_of_notMem_branchLocus).

theorem contMDiffAt_traceSection_ext_of_notMem_branchLocus {X Y : Type*} [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀)
    (α : HolomorphicOneForms X) {y₀ : Y} (hy₀ : y₀ ∉ branchLocus f) :
    ContMDiffAt 𝓘(ℂ) (𝓘(ℂ).prod 𝓘(ℂ, ℂ →L[ℂ] ℂ)) ω
      (traceTotalSpaceMk (traceFunExt f α)) y₀

neBot_nhdsWithin_compl_self

A connected complex 1-manifold has no isolated points: the punctured neighborhood filter 𝓝[≠] y₀ is NeBot. (Y is Infinite — infinite_of_chartedSpace_complex — hence Nontrivial; with T1Space + ConnectedSpace this gives PerfectSpace, hence NeBot (𝓝[≠] y₀).) This is what makes limits along punctured neighborhoods unique, the engine of the linearity argument below.

instance neBot_nhdsWithin_compl_self {Y : Type*} [TopologicalSpace Y] [T2Space Y] [ConnectedSpace Y]
    [ChartedSpace ℂ Y] (y₀ : Y) : (𝓝[≠] y₀).NeBot

exists_traceForm_of_branchExtension

Reduction lemma for the trace. Given the per-branch-point extension data hext (holomorphic-extension smoothness + fixed-frame local-coefficient continuity at each branch point, for every form), the trace f₊ : Ω¹(X) →ₗ[ℂ] Ω¹(Y) exists as a genuine holomorphic-one-form linear map agreeing with the off-branch fibre sum traceFun.

Everything here is proven outright:

  • Section assembly: traceFunExt f α is a global ContMDiffSection — off-branch from contMDiffAt_traceSection_ext_of_notMem_branchLocus, at branch points from hext.

  • Linearity: at a branch point the extension operator is (local coefficient) • id, and the *scalar* local coefficient is the *unique* fixed-frame limit of the raw trace's local coefficient along the punctured neighborhood (neBot_nhdsWithin_compl_self + tendsto_nhds_unique); limits respect +/• and the local coefficient is linear in the operator (inCoordinates_apply_one_add/smul); off-branch the fibre sum is already additive/homogeneous (traceFun_add_of_notMem_branchLocus, …_smul_…).

theorem exists_traceForm_of_branchExtension {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀)
    (hext : ∀ (α : HolomorphicOneForms X) (y₀ : Y), y₀ ∈ branchLocus f →
      ContMDiffAt 𝓘(ℂ) (𝓘(ℂ).prod 𝓘(ℂ, ℂ →L[ℂ] ℂ)) ω
          (traceTotalSpaceMk (traceFunExt f α)) y₀ ∧
        ContinuousAt (fun y => traceLocalCoeff (traceFunExt f α) y₀ y) y₀) :
    ∃ T : HolomorphicOneForms X →ₗ[ℂ] HolomorphicOneForms Y,
      ∀ (α : HolomorphicOneForms X) (y : Y), y ∉ branchLocus f →
        (T α).toFun y = traceFun f α y

contMDiffAt_traceTotalSpaceMk_of_localCoeff

Section lift from the local coefficient (the converse of continuousAt_inCoordinates). If the scalar local coefficient y ↦ traceLocalCoeff coeff y₀ y is ContMDiffAt at y₀, then the section traceTotalSpaceMk coeff is ContMDiffAt at y₀. This is the bundle- coordinate engine: by contMDiffAt_hom_bundle the section is smooth iff its inCoordinates operator is smooth into the fixed normed space ℂ →L[ℂ] ℂ; that operator equals (traceLocalCoeff coeff y₀ y) • id (clm_eq_apply_one_smul_id), a scalar multiple of a constant operator, hence smooth from the scalar's smoothness.

theorem contMDiffAt_traceTotalSpaceMk_of_localCoeff {Y : Type*} [TopologicalSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (coeff : Y → (ℂ →L[ℂ] ℂ)) {y₀ : Y}
    (hcoeff : ContMDiffAt 𝓘(ℂ) 𝓘(ℂ, ℂ) ω (fun y => traceLocalCoeff coeff y₀ y) y₀) :
    ContMDiffAt 𝓘(ℂ) (𝓘(ℂ).prod 𝓘(ℂ, ℂ →L[ℂ] ℂ)) ω (traceTotalSpaceMk coeff) y₀

contMDiffAt_traceLocalCoeff_of_notMem_branchLocus

Off-branch smoothness of the local coefficient. Wherever y₁ is off the branch locus *and* lies in the fixed chart source at y₀, the scalar local coefficient y ↦ traceLocalCoeff (traceFun f α) y₀ y is ContMDiffAt at y₁. Derived from the off-branch section smoothness contMDiffAt_traceFun_of_notMem_branchLocus read in the *fixed y₀-trivialization* (contMDiffAt_section_iff with the hom-bundle trivialization at y₀, whose coordinate is exactly inCoordinates … y₀ · y₀ · by hom_trivializationAt_apply), then evaluated on the model basis vector 1.

theorem contMDiffAt_traceLocalCoeff_of_notMem_branchLocus {X Y : Type*} [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀)
    (α : HolomorphicOneForms X) (y₀ : Y) {y₁ : Y} (hy₁ : y₁ ∉ branchLocus f)
    (hy₁src : y₁ ∈ (chartAt ℂ y₀).source) :
    ContMDiffAt 𝓘(ℂ) 𝓘(ℂ, ℂ) ω (fun y => traceLocalCoeff (traceFun f α) y₀ y) y₁

differentiableAt_chartPullback_of_contMDiffAt

Manifold smoothness ⟹ chart-pullback differentiability (scalar codomain). If g : Y → ℂ is ContMDiffAt … ω at y₁, its chart pullback g ∘ (chartAt ℂ y₀).symm is DifferentiableAt ℂ at (chartAt ℂ y₀) y₁, provided y₁ lies in the chart source. The chart inverse (chartAt ℂ y₀).symm : ℂ → Y is ContMDiffAt at (chartAt ℂ y₀) y₁ (contMDiffOn_chart_symm, since (chartAt ℂ y₀) y₁ ∈ target) and maps it to y₁, so the composite g ∘ (chartAt ℂ y₀).symm : ℂ → ℂ is ContMDiffAt, i.e. DifferentiableAt.

theorem differentiableAt_chartPullback_of_contMDiffAt {Y : Type*} [TopologicalSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] {g : Y → ℂ} {y₀ y₁ : Y}
    (hg : ContMDiffAt 𝓘(ℂ) 𝓘(ℂ, ℂ) ω g y₁) (hy₁ : y₁ ∈ (chartAt ℂ y₀).source) :
    DifferentiableAt ℂ (g ∘ (chartAt ℂ y₀).symm) ((chartAt ℂ y₀) y₁)

contMDiffAt_of_analyticAt_chartPullback

Chart-pullback analyticity ⟹ manifold smoothness (scalar codomain). Converse of differentiableAt_chartPullback_of_contMDiffAt at the basepoint: if g : Y → ℂ is ContinuousAt at y₀ and its chart pullback g ∘ (chartAt ℂ y₀).symm is AnalyticAt ℂ at (chartAt ℂ y₀) y₀, then g is ContMDiffAt … ω at y₀. This is the mpr of contMDiffAt_iff for a scalar target (the target chart is the identity, the source extended chart is chartAt ℂ y₀), feeding the removably-extended analytic local coefficient back into section smoothness.

theorem contMDiffAt_of_analyticAt_chartPullback {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    {g : Y → ℂ} {y₀ : Y}
    (hcont : ContinuousAt g y₀)
    (han : AnalyticAt ℂ (g ∘ (chartAt ℂ y₀).symm) ((chartAt ℂ y₀) y₀)) :
    ContMDiffAt 𝓘(ℂ) 𝓘(ℂ, ℂ) ω g y₀

sub_div_deriv_tendsto_zero

One-variable analytic heart. If F is analytic at w₀ with F w₀ = z₀ and is not eventually constant ≡ z₀, then (F w − z₀)/F'(w) → 0 as w → w₀ through w ≠ w₀. Proof: F − z₀ = (w − w₀)^(d+1) · g (g w₀ ≠ 0), so for w ≠ w₀ the ratio equals (w − w₀)·g/( (d+1)·g + (w − w₀)·g'), whose limit is 0/((d+1) g w₀) = 0.

theorem sub_div_deriv_tendsto_zero {F : ℂ → ℂ} {w₀ z₀ : ℂ}
    (hF : AnalyticAt ℂ F w₀) (hFw₀ : F w₀ = z₀)
    (hnc : ¬ ∀ᶠ w in 𝓝 w₀, F w = z₀) :
    Tendsto (fun w => (F w - z₀) / deriv F w) (𝓝[≠] w₀) (𝓝 0)

traceSummand_inCoordinates_apply_one_eq_ref

Exact per-preimage local coefficient. Off the critical set, the trace summand's y₀-fixed-frame local coefficient at x equals (α's local coefficient at x, read in the x₀-frame) / F'(chartAt x₀ x), where F = chartAt ℂ y₀ ∘ f ∘ (chartAt ℂ x₀).symm. The proof computes inCoordinates(…)(traceSummand) 1 = (α x)((mfderiv f x)⁻¹ (∂/∂z)) and pushes everything through the chartAt x₀ and chartAt y₀ frames: the trivialization coordinate maps are mfderiv of charts (TangentBundle.continuousLinearMapAt_trivializationAt / symmL_trivializationAt), the section (mfderiv f x)⁻¹ = mfderiv g (f x) (mfderiv_section_eq_inverse), and deriv (chart-section) = (F')⁻¹ since the chart-section is the local inverse of F.

theorem traceSummand_inCoordinates_apply_one_eq_ref {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) (α : HolomorphicOneForms X) (y₀ : Y) {x₀ x : X}
    (hxcrit : x ∉ criticalSet f) (hxsrc : x ∈ (chartAt ℂ x₀).source)
    (hfx : f x ∈ (chartAt ℂ y₀).source) :
    ContinuousLinearMap.inCoordinates ℂ (TangentSpace 𝓘(ℂ) (M := Y)) ℂ (Bundle.Trivial Y ℂ)
        y₀ (f x) y₀ (f x) (traceSummand f α x) (1 : ℂ)
      = (ContinuousLinearMap.inCoordinates ℂ (TangentSpace 𝓘(ℂ) (M := X)) ℂ (Bundle.Trivial X ℂ)
          x₀ x x₀ x (α.toFun x) (1 : ℂ))
        / deriv (chartAt ℂ y₀ ∘ f ∘ (chartAt ℂ x₀).symm) ((chartAt ℂ x₀) x)

traceSummand_localCoeff_mul_sub_tendsto

Per-preimage growth. For a preimage x₀ ∈ f⁻¹{y₀}, the scaled trace-summand local coefficient (c (f x) − c y₀) · inCoordinates(…)(traceSummand f α x) 1 tends to 0 as x → x₀ through off-critical x ≠ x₀. By the exact value it equals a₀(x) · (F(ψ x) − z₀)/F'(ψ x) with a₀ the (continuous) local coefficient of α, and (F(u) − z₀)/F'(u) → 0 (sub_div_deriv_tendsto_zero, F analytic, F(ψ x₀) = z₀, not locally constant).

theorem traceSummand_localCoeff_mul_sub_tendsto {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) (α : HolomorphicOneForms X) {y₀ : Y} {x₀ : X}
    (hfx₀ : f x₀ = y₀) :
    Tendsto (fun x => (chartAt ℂ y₀ (f x) - chartAt ℂ y₀ y₀)
        * ContinuousLinearMap.inCoordinates ℂ (TangentSpace 𝓘(ℂ) (M := Y)) ℂ (Bundle.Trivial Y ℂ)
            y₀ (f x) y₀ (f x) (traceSummand f α x) (1 : ℂ))
      (𝓝[(criticalSet f)ᶜ \ {x₀}] x₀) (𝓝 0)

localCoeffLin

The linear map φ ↦ inCoordinates … y₀ y y₀ y φ 1 (the local-coefficient functional).

noncomputable def localCoeffLin {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (y₀ y : Y) : (ℂ →L[ℂ] ℂ) →ₗ[ℂ] ℂ where

traceLocalCoeff_traceFun_eq_finsum

Additivity over the fibre. Off the branch locus the local coefficient of the fibre-sum trace is the fibre sum of the per-summand local coefficients.

theorem traceLocalCoeff_traceFun_eq_finsum {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) (α : HolomorphicOneForms X)
    (y₀ : Y) {y : Y} (hy : y ∉ branchLocus f) :
    traceLocalCoeff (traceFun f α) y₀ y
      = ∑ᶠ x ∈ f ⁻¹' {y}, localCoeffLin y₀ y (traceSummand f α x)

fibre_ncard_locally_const

Off-branch fibre cardinality is locally constant. For a regular value y₁ there is an open V ∋ y₁ on which every fibre has the same cardinality (f⁻¹{y₁}).ncard (from the local sheet system: the n injective holomorphic sheets sweep out each nearby fibre).

theorem fibre_ncard_locally_const {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y] [T2Space Y]
    [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) {y₁ : Y} (hy₁ : y₁ ∉ branchLocus f) :
    ∃ V : Set Y, IsOpen V ∧ y₁ ∈ V ∧
      ∀ y ∈ V, (f ⁻¹' {y}).ncard = (f ⁻¹' {y₁}).ncard

bigPhi

The scaled per-summand local coefficient Φ summed in the fibre-sum assembly.

noncomputable def bigPhi {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (α : HolomorphicOneForms X) (y₀ : Y)
    (x : X) : ℂ

fibre_ncard_bddAbove_near_branch

Uniform off-branch fibre-cardinality bound near a branch point (the classical "off-branch fibre cardinality = degree, hence locally bounded"). The fibre card is locally constant off the branch locus (fibre_ncard_locally_const), and on a preconnected punctured chart-ball c.symm '' (Metric.ball z₀ r \ Badℂ) — connected because a ball in ℂ ≅ ℝ² minus the finite set Badℂ = c '' (branchLocus f ∩ c.source) is path-connected (Set.Countable.isPathConnected_ball_diff_complex) — a locally-constant ℕ-valued function is globally constant (IsPreconnected.constant, ℕ discrete). This punctured nbhd is eventual in 𝓝[≠] y₀ (pushing Metric.ball z₀ r \ Badℂ ∈ 𝓝[≠] z₀ along c), giving the uniform bound.

theorem fibre_ncard_bddAbove_near_branch {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) {y₀ : Y} (_hy₀ : y₀ ∈ branchLocus f) :
    ∃ N : ℕ, ∀ᶠ y in 𝓝[≠] y₀, y ∉ branchLocus f → (f ⁻¹' {y}).ncard ≤ N

traceLocalCoeff_mul_sub_tendsto_zero_Y

The manifold side of the branch-point boundedness argument.

The Y-side of traceLocalCoeff_mul_sub_tendsto_zero: in the chart c := chartAt ℂ y₀, the scaled local coefficient (c y − c y₀) · traceLocalCoeff (traceFun f α) y₀ y → 0 as y → y₀ through y ≠ y₀. The headline then follows by composing with c.symm (which carries 𝓝[≠] (c y₀) to 𝓝[≠] y₀).

Note a naive bound ‖traceLocalCoeff coeff y₀ y‖ ≤ B·‖coeff y‖ with a uniform B would be *unsound*: for arbitrary operators it is equivalent to local boundedness of the bare-fibre coordinate symmL(tangentTriv y₀) y 1, which fails for genus ≥ 2 (CotangentCoeff.lean const_one_section_continuous_of_coordChange_fixes_one): the constant native-frame section is discontinuous and not locally bounded (no Riemannian metric is placed on TY, so no compactness rescue). One must therefore *not* peel the inCoordinates/symmL factor off the operator norm; the obstruction factors cancel only when the application inCoordinates(…)(traceSummand f α x) 1 is kept together and evaluated in one chart:

  1. *Exact per-preimage local coefficient.* Off-branch traceLocalCoeff (traceFun f α) y₀ y = ∑_{x ∈ f⁻¹ y} inCoordinates(…)(traceSummand f α x) 1 (finite; inCoordinates-apply-1 is additive over the fibre sum). Each term is the local coefficient of a section-pullback and computes exactly to a(w) · S'(z), where S := chart_X ∘ s ∘ c.symm is the local section read in charts, z = c y, w = S(z), and a is α's coefficient in chart_X. Since S = F⁻¹ for F := c ∘ f ∘ chart_X.symm, we get S'(z) = 1/F'(w), so the term is a(w)/F'(w) — *no* symmL factor (the (mfderiv f x)⁻¹ and e.symmL chart factors cancel in the common chart_X frame), via the operator identity inside contMDiffAt_pullback_section (inCoordinates(sheetPullback) = inCoordinates_X(α) ∘ inCoordinates(mfderiv s)), evaluated at 1. Then (z − c y₀)·a(w)/F'(w) = a(w)·(F(w) − c y₀)/F'(w) → 0 by sub_div_deriv_tendsto_zero, a bounded.

  2. *Assembly.* Properness (X compact ⟹ f⁻¹ W ⊆ ⋃_j U_j for small W ∋ y₀) + the uniform off-branch fibre cardinality reduce the finite fibre sum to a finite sum of terms each → 0.

(Forster §10; Griffiths–Harris Ch. 2 §2.7.)

theorem traceLocalCoeff_mul_sub_tendsto_zero_Y {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) (α : HolomorphicOneForms X)
    {y₀ : Y} (hy₀ : y₀ ∈ branchLocus f) :
    Tendsto (fun y => ((chartAt ℂ y₀) y - (chartAt ℂ y₀) y₀)
        * traceLocalCoeff (traceFun f α) y₀ y) (𝓝[≠] y₀) (𝓝 0)

traceLocalCoeff_mul_sub_tendsto_zero

[THE TRACE'S ANALYTIC CRUX — local boundedness at a branch point, little-o form]

The single genuinely-analytic input. In the fixed chart c := chartAt ℂ y₀, the trace's *local coefficient* G z := traceLocalCoeff (traceFun f α) y₀ (c.symm z) satisfies the local little-o bound (z - c y₀) · G z → 0 as z → c y₀ (through the punctured neighborhood). Equivalently G =o[𝓝[≠] (c y₀)] (· - c y₀)⁻¹: the trace one-form traceFun f α on Y ∖ branchLocus f, read in the y₀-chart, has at worst a *removable* singularity at the branch point (no genuine pole).

This is exactly the hypothesis of Mathlib's little-o removable-singularity theorem Complex.differentiableOn_update_limUnder_insert_of_isLittleO, and it is the only fact the whole trace construction is missing.

Why the little-o (not global BddAbove). Global boundedness over the whole chart target is *false* in general (the chart codomain need not be relatively compact). The geometrically correct — and provable — statement is the *local* one at y₀, and the little-o form is strictly weaker than local boundedness yet still suffices for removability.

Proof strategy (no roots-of-unity / Puiseux needed). ‖traceFun f α y‖ is bounded by the fibre sum ∑_{x ∈ f⁻¹ y} ‖α x‖ · ‖(mfderiv f x)⁻¹‖. Near each branch preimage x_j ∈ f⁻¹ y₀ the map f has, in coordinates, an analytic normal form F with F(0) = c y₀ and a finite-order zero of F - c y₀; then the crude per-sheet estimate |z - c y₀| · ‖(mfderiv f x)⁻¹‖ = |F(w) - c y₀| / |F'(w)| → 0 (because F - c y₀ = wᵉ · g with g(0) ≠ 0, so the ratio is w · g/(e g + w g') → 0). Summing the finitely many sheets over the finite fibre gives (z - c y₀) · G z → 0 — no symmetric-function cancellation, just the triangle inequality. Holomorphy of G on the punctured disk is *not* used here; it is supplied separately in traceExtendsAt_branchPoint.

theorem traceLocalCoeff_mul_sub_tendsto_zero {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) (α : HolomorphicOneForms X)
    {y₀ : Y} (hy₀ : y₀ ∈ branchLocus f) :
    Tendsto
      (fun z : ℂ => (z - (chartAt ℂ y₀) y₀)
        * traceLocalCoeff (traceFun f α) y₀ ((chartAt ℂ y₀).symm z))
      (𝓝[≠] ((chartAt ℂ y₀) y₀)) (𝓝 0)

traceFunExt_branchValue_correct

Branch-value local-coefficient matching. With the refactored traceFunExt, the branch value traceFunExt f α y₀ = traceBranchValue f α y₀ is the operator L • id, where L is the chart-pullback removable-singularity limit of the *local coefficient* of the raw trace. The local coefficient of the extended trace at the center y₀ recovers exactly L: traceLocalCoeff (traceFunExt f α) y₀ y₀ = L = limUnder (𝓝\[≠\] (c y₀)) (z ↦ traceLocalCoeff (traceFun f α) y₀ (c⁻¹ z)).

This is precisely the "local-coefficient matching" the section-smoothness bridge needs at the puncture, and it is now a definitional consequence of the center-frame identity traceLocalCoeff_center (traceLocalCoeff (L • id) y₀ y₀ = (L • id) 1 = L) — it requires *no* boundedness/analytic input. (The old, design-flawed "raw convergence" conjunct — ContinuousAt of the raw operator in the model fibre — was *provably false* for a non-trivial tangent bundle, genus ≥ 2; it has been removed, and traceExtendsAt_branchPoint now expresses continuity in the geometrically-correct *fixed frame*, see its statement.)

theorem traceFunExt_branchValue_correct {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y)
    (α : HolomorphicOneForms X) {y₀ : Y} (hy₀ : y₀ ∈ branchLocus f) :
    traceLocalCoeff (traceFunExt f α) y₀ y₀ =
        limUnder (𝓝[≠] ((chartAt ℂ y₀) y₀))
          (fun z => traceLocalCoeff (traceFun f α) y₀ ((chartAt ℂ y₀).symm z))

traceExtendsAt_branchPoint

Via the analytic kernel traceLocalCoeff_mul_sub_tendsto_zero:

For every form α and every branch point y₀ ∈ branchLocus f, the canonical branch extension traceFunExt f α is, at y₀:

  • ContMDiffAt as a section of the cotangent bundle (the *holomorphic* extension), and

  • ContinuousAt in the fixed y₀-frame, i.e. the local coefficient y ↦ traceLocalCoeff (traceFunExt f α) y₀ y is ContinuousAt y₀.

Why the second conjunct is the *local coefficient*, not the raw operator. The naive "ContinuousAt (traceFunExt f α) y₀" — continuity of the operator read in the *model fibre* ℂ →L[ℂ] ℂ — is provably false for a non-trivial tangent bundle (genus ≥ 2): the raw operator traceFun f α y is inCoordinates(…) ∘ clmAt(tangentTriv y₀) y, whose chart-transition factor is discontinuous (the CotangentCoeff.lean obstruction). The geometrically-correct continuity statement is continuity of the section *in the bundle*, equivalently continuity of its coordinate in the fixed y₀-trivialization — the local coefficient. (This is also exactly the *shadow* of the first conjunct: section ContMDiffAt ⟹ local-coeff ContMDiffAt ⟹ ContinuousAt. The reduction lemma exists_traceForm_of_branchExtension consumes this fixed-frame continuity soundly; see its htendsto argument, which is now phrased in local coordinates.)

Bridge structure. The whole proof is the single fact: the *local coefficient* read in the y₀-chart is ContMDiffAt y₀. It is holomorphic off y₀ (off-branch section smoothness contMDiffAt_traceLocalCoeff_of_notMem_branchLocus + the scalar chart bridges) and bounded there, and has at worst a removable singularity (traceLocalCoeff_mul_sub_tendsto_zero: (z - z₀)·G z → 0), so by Mathlib's little-o removable singularity theorem (Complex.differentiableOn_update_limUnder_insert_of_isLittleO, DifferentiableOn.analyticAt) it extends analytically across y₀; its value at y₀ matches traceLocalCoeff (traceFunExt f α) y₀ y₀ by traceFunExt\_branchValue\_correct. Then:

  • conjunct 1 lifts it to the section via contMDiffAt_traceTotalSpaceMk_of_localCoeff;

  • conjunct 2 is its .continuousAt.

Everything *downstream* — the global ContMDiffSection regluing and the full ℂ-linearity of the trace — is proven unconditionally in exists_traceForm_of_branchExtension.

theorem traceExtendsAt_branchPoint {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y] [T2Space Y]
    [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) (α : HolomorphicOneForms X)
    {y₀ : Y} (hy₀ : y₀ ∈ branchLocus f) :
    ContMDiffAt 𝓘(ℂ) (𝓘(ℂ).prod 𝓘(ℂ, ℂ →L[ℂ] ℂ)) ω
        (traceTotalSpaceMk (traceFunExt f α)) y₀ ∧
      ContinuousAt (fun y => traceLocalCoeff (traceFunExt f α) y₀ y) y₀

exists_traceForm

Existence of the trace f₊ : Ω¹(X) →ₗ[ℂ] Ω¹(Y) as a genuine holomorphic one-form linear map agreeing with the off-branch fibre sum traceFun. Now a one-line consequence of the fully-proven reduction exists_traceForm_of_branchExtension and the isolated per-branch-point analytic input traceExtendsAt_branchPoint. Sound (classically true; Forster §10, Griffiths–Harris Ch. 2 §2.7).

theorem exists_traceForm {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y] [T2Space Y]
    [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) :
    ∃ T : HolomorphicOneForms X →ₗ[ℂ] HolomorphicOneForms Y,
      ∀ (α : HolomorphicOneForms X) (y : Y), y ∉ branchLocus f →
        (T α).toFun y = traceFun f α y

traceForm

Trace (pushforward) of holomorphic one-forms, f₊ : Ω¹(X) →ₗ[ℂ] Ω¹(Y), extracted from exists_traceForm. Off the branch locus it is the holomorphic fibre sum traceFun; across the (finite) branch locus it is the removable-singularity extension.

noncomputable def traceForm {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y] [T2Space Y]
    [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) :
    HolomorphicOneForms X →ₗ[ℂ] HolomorphicOneForms Y

traceForm_toFun_of_notMem_branchLocus

traceForm agrees with the fibre-sum traceFun off the branch locus.

theorem traceForm_toFun_of_notMem_branchLocus {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) (α : HolomorphicOneForms X)
    {y : Y} (hy : y ∉ branchLocus f) :
    (traceForm f hf hnonconst α).toFun y = traceFun f α y

traceForm_id

f₊(id) = id — the identity map is a one-sheeted unbranched cover, so its trace is the identity. Honest gap: classically true (Forster §10), but in this formalization traceForm is the removable-singularity extension of the off-branch fibre sum, and proving the extension of the (single-sheet) fibre sum for id equals id on *all* of X is the identity-theorem upgrade of the off-branch agreement — the same analytic status as traceExtendsAt_branchPoint.

theorem traceForm_id {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (hnonconst : ¬ ∃ x₀ : X, ∀ x, (id : X → X) x = x₀) :
    traceForm (id : X → X) contMDiff_id hnonconst =
      LinearMap.id (R := ℂ) (M := HolomorphicOneForms X)

contMDiffAt_localCoeff_section

Local coefficient of an arbitrary smooth section is ContMDiffAt. Generalizes contMDiffAt_traceLocalCoeff_of_notMem_branchLocus from traceFun f α to any smooth section s : HolomorphicOneForms Y: read in the FIXED y₀-hom-trivialization the section's coordinate is ContMDiffAt, hence the scalar local coefficient (its value on 1) is too. (No branch-locus hypothesis — s is globally smooth.)

theorem contMDiffAt_localCoeff_section {Y : Type*} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y]
    [ConnectedSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (s : HolomorphicOneForms Y) (y₀ : Y)
    {y₁ : Y}
    (hy₁src : y₁ ∈ (chartAt ℂ y₀).source) :
    ContMDiffAt 𝓘(ℂ) 𝓘(ℂ, ℂ) ω (fun y => traceLocalCoeff (s.toFun) y₀ y) y₁

isInvertible_mfderiv_of_notMem_criticalSet

Off the critical set, mfderiv g y is invertible (it has a two-sided local-inverse section).

theorem isInvertible_mfderiv_of_notMem_criticalSet {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (g : Y → X) (hg : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω g)
    (hgnc : ¬ ∃ x₀ : X, ∀ y, g y = x₀) {y : Y} (hy : y ∉ criticalSet g) :
    (mfderiv 𝓘(ℂ) 𝓘(ℂ) g y).IsInvertible

traceForm_comp

Covariance of the trace: (g ∘ f)₊ = g₊ ∘ f₊ (Griffiths–Harris Ch. 2 §2.7). Both sides are smooth forms; their fixed-frame local coefficients (not the discontinuous raw fibre components — the genus≥2 CotangentCoeff obstruction) agree off the finite bad set B = branchLocus (g∘f) ∪ branchLocus g ∪ g '' branchLocus f via the off-branch fibre factorization traceFun (g∘f) α z = traceFun g (traceForm f α) z (partition (g∘f)⁻¹{z} = ⊔_{y∈g⁻¹z} f⁻¹{y} + chain rule (mfderiv (g∘f))⁻¹ = (mfderiv f)⁻¹∘(mfderiv g)⁻¹ + pulling the common right-comp out of the inner finsum). The local coefficients are ContinuousOn the chart source (contMDiffAt_localCoeff_section), Bᶜ is dense (finite B, perfect space), so they agree everywhere; evaluating at the chart center (traceLocalCoeff_center) gives the operator equality.

theorem traceForm_comp {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y] [T2Space Y]
    [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] {Z : Type*}
    [TopologicalSpace Z] [T2Space Z] [CompactSpace Z]
    [ConnectedSpace Z] [Nonempty Z] [ChartedSpace ℂ Z] [IsManifold 𝓘(ℂ) ω Z]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (hfnc : ¬ ∃ y₀ : Y, ∀ x, f x = y₀)
    (g : Y → Z) (hg : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω g) (hgnc : ¬ ∃ z₀ : Z, ∀ y, g y = z₀)
    (hgf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω (g ∘ f)) (hgfnc : ¬ ∃ z₀ : Z, ∀ x, (g ∘ f) x = z₀) :
    traceForm (g ∘ f) hgf hgfnc =
      (traceForm g hg hgnc).comp (traceForm f hf hfnc)

traceFormTotal

Total trace f₊ : Ω¹(X) →ₗ[ℂ] Ω¹(Y), defined for every holomorphic f: the genuine traceForm when f is non-constant, and 0 when f is constant (degree 0). This is the object the ambient coordinate layer dualizes.

noncomputable def traceFormTotal {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y] [T2Space Y]
    [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] (f : X → Y)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) :
    HolomorphicOneForms X →ₗ[ℂ] HolomorphicOneForms Y

traceFormTotal_eq_zero_of_const

Total trace of a constant map is zero (degree 0, no sheets to sum over). Drop-in replacement for pushforwardForm_eq_zero_of_const.

theorem traceFormTotal_eq_zero_of_const {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hconst : ∃ y₀ : Y, ∀ x, f x = y₀) :
    traceFormTotal f hf = 0

traceFormTotal_of_nonconstant

Off-constant, the total trace is the genuine trace.

theorem traceFormTotal_of_nonconstant {X Y : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) :
    traceFormTotal f hf = traceForm f hf hnonconst

traceFormTotal_id

traceFormTotal id = id — for an infinite X the identity is non-constant, so traceFormTotal id = traceForm id, which is the identity by traceForm_id. Drop-in replacement for pushforwardForm_id.

theorem traceFormTotal_id {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] :
    traceFormTotal (id : X → X) contMDiff_id =
    LinearMap.id (R := ℂ) (M := HolomorphicOneForms X)

traceFormTotal_comp

Covariance traceFormTotal (g ∘ f) = traceFormTotal g ∘ₗ traceFormTotal f. Case-splits on constancy: if f or g is constant the composite is constant and both sides collapse to 0 (composition with the zero map); otherwise f is surjective, so g ∘ f non-constant follows from g non-constant, and the law is traceForm_comp. Drop-in replacement for pushforwardForm_comp.

theorem traceFormTotal_comp {X Y : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] [TopologicalSpace Y] [T2Space Y]
    [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] {Z : Type*}
    [TopologicalSpace Z] [T2Space Z] [CompactSpace Z]
    [ConnectedSpace Z] [Nonempty Z] [ChartedSpace ℂ Z] [IsManifold 𝓘(ℂ) ω Z]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (g : Y → Z) (hg : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω g)
    (hgf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω (g ∘ f)) :
    traceFormTotal (g ∘ f) hgf =
      (traceFormTotal g hg).comp (traceFormTotal f hf)