20.6. CanonicalForms.FormRemovableSingularity🔗

Jacobians.CanonicalForms.FormRemovableSingularity — source

contMDiffOn_scalar_of_pullback_analyticOn

Scalar smoothness from chart-pullback analyticity on an open subset S of the chart source. If the chart pullback is analytic on chart x₀ '' S, then the scalar y ↦ L y (e.symmL ℂ y 1) is ContMDiffOn ω on S. The inverse of localRep_analyticOn_chartTarget; the argument is Montel.contMDiffOn_limit_inner with S in place of innerChartOpen.

theorem contMDiffOn_scalar_of_pullback_analyticOn {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
        (L : (y : X) → TangentSpace 𝓘(ℂ, ℂ) y →L[ℂ] (Bundle.Trivial X ℂ) y) (x₀ : X)
    {S : Set X} (hSopen : IsOpen S) (hSsub : S ⊆ (chartAt ℂ x₀).source)
    (hAn : letI e := trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀
      AnalyticOn ℂ
        (fun z : ℂ => L ((chartAt ℂ x₀).symm z) (e.symmL ℂ ((chartAt ℂ x₀).symm z) 1))
        ((chartAt ℂ x₀) '' S)) :
    letI e

contMDiffOn_totalSpaceMk_of_pullback_analyticOn

Section smoothness from chart-pullback analyticity on an open subset S of the chart source. The bundle-section y ↦ (y, L y) is ContMDiffOn ω on S. This is Montel.contMDiffOn_totalSpaceMk_L_inner re-derived on an arbitrary open S ⊆ (chart x₀).source.

theorem contMDiffOn_totalSpaceMk_of_pullback_analyticOn {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
        (L : (y : X) → TangentSpace 𝓘(ℂ, ℂ) y →L[ℂ] (Bundle.Trivial X ℂ) y) (x₀ : X)
    {S : Set X} (hSopen : IsOpen S) (hSsub : S ⊆ (chartAt ℂ x₀).source)
    (hAn : letI e := trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀
      AnalyticOn ℂ
        (fun z : ℂ => L ((chartAt ℂ x₀).symm z) (e.symmL ℂ ((chartAt ℂ x₀).symm z) 1))
        ((chartAt ℂ x₀) '' S)) :
    ContMDiffOn 𝓘(ℂ, ℂ) (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ →L[ℂ] ℂ)) ω
      (fun y : X => Bundle.TotalSpace.mk' (ℂ →L[ℂ] ℂ)
        (E := fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x)
        y (L y))
      S

holOfLocalRepAnalyticAt

The section-assembly lemma, local form. A bundle section L whose chart pullback in *each point's own chart* is AnalyticAt the chart centre is ContMDiff, hence a HolomorphicOneForms X. Smoothness at y is read in y's own chart: AnalyticAt gives analyticity on an open neighbourhood of chart y y, whose chart-preimage is an open neighbourhood of y.

noncomputable def holOfLocalRepAnalyticAt
    (L : (y : X) → TangentSpace 𝓘(ℂ, ℂ) y →L[ℂ] (Bundle.Trivial X ℂ) y)
    (hAn : ∀ x₀ : X,
      letI e := trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀
      AnalyticAt ℂ
        (fun z : ℂ => L ((chartAt ℂ x₀).symm z) (e.symmL ℂ ((chartAt ℂ x₀).symm z) 1))
        ((chartAt ℂ x₀) x₀)) :
    HolomorphicOneForms X where

formCoeff_sub

formCoeff subtracts (combining formCoeff_add and formCoeff_neg).

theorem formCoeff_sub {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (σ τ : ∀ x, FormFiber X x) (x : X) :
    formCoeff (σ - τ) x = formCoeff σ x - formCoeff τ x

frameCovector

The frame covector at y from the canonical tangent trivialisation: φ_y : T_y X →L[ℂ] ℂ.

noncomputable def frameCovector (y : X) : TangentSpace 𝓘(ℂ, ℂ) y →L[ℂ] ℂ

frameCovector_symmL_self

φ_y (e_y.symmL ℂ y 1) = 1: the frame covector evaluated on the canonical frame vector.

theorem frameCovector_symmL_self {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (y : X) :
    letI e

repVal

The repaired chart value of α at y: the normal-form value of the chart coefficient at the chart centre — the removable-singularity limit lim_{z → chart y y} formCoeff α.toFun y (z).

noncomputable def repVal (α : MeromorphicOneForm X) (y : X) : ℂ

analyticAt_repairedCoeff

The repaired chart coefficient toMeromorphicNFAt (formCoeff α.toFun y) (chart y y) is AnalyticAt (chart y y) when α ∈ omegaD 0 (order ≥ 0 ⟹ removable singularity). Reuses the repo's exists_analyticAt_eventuallyEq_of_meromorphicOrderAt_nonneg.

theorem analyticAt_repairedCoeff {α : MeromorphicOneForm X} (hα : α ∈ omegaD (X := X) 0) (y : X) :
    AnalyticAt ℂ (toMeromorphicNFAt (formCoeff α.toFun y) ((chartAt ℂ y) y)) ((chartAt ℂ y) y)

rawLocalRep

The bare chart representative of a section σ in the x₀-trivialisation.

noncomputable def rawLocalRep (σ : ∀ x, FormFiber X x) (x₀ y : X) : ℂ

formCoeff_eq_rawLocalRep

theorem formCoeff_eq_rawLocalRep {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (σ : ∀ x, FormFiber X x) (x : X) (z : ℂ) :
    formCoeff σ x z = rawLocalRep σ x ((chartAt ℂ x).symm z)

rawLocalRep_self_eq_formCoeff

rawLocalRep σ y y = formCoeff σ y (chart y y): the chart-centre value.

theorem rawLocalRep_self_eq_formCoeff {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (σ : ∀ x, FormFiber X x) (y : X) :
    rawLocalRep σ y y = formCoeff σ y ((chartAt ℂ y) y)

rawLocalRep_chart_transition

Chart-transition for rawLocalRep (raw analogue of Montel.localRep_chart_transition): rawLocalRep σ x₀' y = chartTransitionFactor x₀ x₀' y · rawLocalRep σ x₀ y for y in both base sets. The proof reuses the trivialisation identity symmL_apply_chartTransitionFactor.

theorem rawLocalRep_chart_transition {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (σ : ∀ x, FormFiber X x) (x₀ x₀' y : X)
    (hy₀' : y ∈ (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀').baseSet)
    (hy₀ : y ∈ (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀).baseSet) :
    rawLocalRep σ x₀' y = chartTransitionFactor (X := X) x₀ x₀' y * rawLocalRep σ x₀ y

section_eq_rawLocalRep_smul_frame

Self-frame reconstruction (raw analogue of Montel.toFun_eq_localRep_smul at x₀ = y): σ y = rawLocalRep σ y y • φ_y where φ_y = frameCovector y. In particular σ y (e_{x₀}.symmL ℂ y 1) = rawLocalRep σ y y · φ_y (e_{x₀}.symmL ℂ y 1).

theorem section_eq_rawLocalRep_smul_frame {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (σ : ∀ x, FormFiber X x) (y : X) :
    σ y = (rawLocalRep σ y y) • frameCovector y

eventually_analyticAt_formCoeff

formCoeff α.toFun x₀ is analytic at chart x₀ w, for w in a punctured neighbourhood of x₀ (pull MeromorphicAt.eventually_analyticAt back through the chart).

theorem eventually_analyticAt_formCoeff (α : MeromorphicOneForm X) (x₀ : X) :
    ∀ᶠ w in 𝓝[≠] x₀, AnalyticAt ℂ (formCoeff α.toFun x₀) ((chartAt ℂ x₀) w)

eventually_repVal_eq

The junk-free key step. For w in a punctured neighbourhood of x₀, the repaired value at w equals the actual chart-centre value: repVal α w = rawLocalRep α.toFun w w. Hence α.toFun carries no removable-singularity junk away from chart centres.

theorem eventually_repVal_eq (α : MeromorphicOneForm X) (x₀ : X) :
    ∀ᶠ w in 𝓝[≠] x₀, repVal α w = rawLocalRep α.toFun w w

repairedSection

The repaired section of an order-≥ 0 meromorphic 1-form: the per-point normal-form value times the canonical frame covector. A bare cotangent-bundle section.

noncomputable def repairedSection (α : MeromorphicOneForm X) : ∀ y, FormFiber X y

rawLocalRep_repairedSection_self

theorem rawLocalRep_repairedSection_self (α : MeromorphicOneForm X) (y : X) :
    rawLocalRep (repairedSection α) y y = repVal α y

formCoeff_repairedSection_eventuallyEq

The repaired section germ-matches α off every centre. In chart x₀, the chart coefficient of repairedSection α agrees on a punctured neighbourhood of the centre with formCoeff α.toFun x₀ (the junk-free key step + self-frame reconstruction). This drives both the analyticity of the repaired section and the germ-equality holToMero (repaired) ≡ α.

theorem formCoeff_repairedSection_eventuallyEq (α : MeromorphicOneForm X) (x₀ : X) :
    formCoeff (repairedSection α) x₀ =ᶠ[𝓝[≠] ((chartAt ℂ x₀) x₀)] formCoeff α.toFun x₀

analyticAt_pullback_repairedSection

The repaired section's chart pullback is analytic at every centre. In chart x₀, the pullback agrees off the centre with formCoeff α.toFun x₀ (the junk-free hypothesis + self-frame), and at the centre takes the normal-form value, so it equals the analytic normal-form repair of formCoeff α.toFun x₀ near the centre.

theorem analyticAt_pullback_repairedSection {α : MeromorphicOneForm X}
    (hα : α ∈ omegaD (X := X) 0) (x₀ : X) :
    letI e

repairedHOF

The repaired holomorphic 1-form of an order-≥ 0 meromorphic 1-form.

noncomputable def repairedHOF {α : MeromorphicOneForm X} (hα : α ∈ omegaD (X := X) 0) :
    HolomorphicOneForms X

repairedHOF_toFun

@[simp] theorem repairedHOF_toFun {α : MeromorphicOneForm X} (hα : α ∈ omegaD (X := X) 0) :
    (repairedHOF hα).toFun = repairedSection α

exists_holomorphic_germEq_of_mem_omegaD_zero

Every order-≥ 0 meromorphic 1-form is holomorphic modulo germ-junk. There is a holomorphic 1-form β (the repaired section) with holToMero β − α germ-zero everywhere (order ⊤ at every centre): their chart coefficients agree on a punctured neighbourhood of each centre. Packaging it as an existence keeps the large repairedHOF proof term out of downstream goals.

theorem exists_holomorphic_germEq_of_mem_omegaD_zero {α : MeromorphicOneForm X}
    (hα : α ∈ omegaD (X := X) 0) :
    ∃ β : HolomorphicOneForms X, holToMero β - α ∈ formGermZeroSubmodule (X := X)

holToOmega0Module_surjective

holToOmega0Module is surjective: every class [α] ∈ omegaDModule 0 is the image of a holomorphic form (the removable-singularity repair, which differs from α by germ-zero junk).

theorem holToOmega0Module_surjective {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    :
    Function.Surjective (holToOmega0Module (X := X))

holOmega0Equiv

Ω_0 ≅ HolomorphicOneForms (Forster §17.4 at D = 0): the holomorphic-to-meromorphic-1-form map is a linear isomorphism HolomorphicOneForms X ≃ₗ[ℂ] omegaDModule 0 (injective from holToOmega0Module_injective, surjective from the removable-singularity repair).

noncomputable def holOmega0Equiv : HolomorphicOneForms X ≃ₗ[ℂ] omegaDModule (X := X) 0

omegaDim_zero_eq_genus

omegaDim 0 = genus X (Forster §17.4 at D = 0), UNCONDITIONAL: the isomorphism Ω_0 ≅ HolomorphicOneForms X preserves finrank, and genus X = finrank ℂ (HolomorphicOneForms X) by definition.

theorem omegaDim_zero_eq_genus {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    : omegaDim (X := X) 0 = genus X

omegaDim_zero_le_genus

The reverse bound omegaDim 0 ≤ genus X (the removable-singularity direction).

theorem omegaDim_zero_le_genus {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    : omegaDim (X := X) 0 ≤ genus X

CanonicalForm17Data.hKgenus_unconditional

Unconditional hKgenus for a given §17.4 datum: lDim data.K = genus X, with the two removable-singularity inputs (Ω_0 finite-dimensional and omegaDim 0 ≤ genus X) now discharged.

theorem CanonicalForm17Data.hKgenus_unconditional (data : CanonicalForm17Data X) :
    lDim (X := X) data.K = genus X