19.18. Finiteness.CechModelManifold🔗

Jacobians.Finiteness.CechModelManifold — source

transition_analyticAt_of_mem

The chart transition chartAt z ∘ (chartAt y).symm is analytic at chartAt y x for any point x in the overlap of the two chart sources (generalizes transition_analyticAt, which is the case x = z = chart centre). Chart and inverse-chart are C^ω, composition C^ω, C^ω = analytic.

theorem transition_analyticAt_of_mem {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {y z x : X}
    (hxy : x ∈ (chartAt (H := ℂ) y).source) (hxz : x ∈ (chartAt (H := ℂ) z).source) :
    AnalyticAt ℂ ((chartAt (H := ℂ) z) ∘ (chartAt (H := ℂ) y).symm) ((chartAt (H := ℂ) y) x)

transition_deriv_ne_zero

The chart transition chartAt z ∘ (chartAt y).symm has nonvanishing derivative at chartAt y x for any point x in the overlap of the two chart sources. The transition is a biholomorphism: its inverse chartAt y ∘ (chartAt z).symm (analytic by transition_analyticAt_of_mem) composes with it to the identity near chartAt y x, so the chain rule forces the derivative to be nonzero. Companion to transition_analyticAt_of_mem; the pair is exactly the hypothesis bundle of Mathlib's meromorphicOrderAt_comp_of_deriv_ne_zero.

theorem transition_deriv_ne_zero {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {y z x : X}
    (hxy : x ∈ (chartAt (H := ℂ) y).source) (hxz : x ∈ (chartAt (H := ℂ) z).source) :
    deriv ((chartAt (H := ℂ) z) ∘ (chartAt (H := ℂ) y).symm) ((chartAt (H := ℂ) y) x) ≠ 0

analyticAt_chart_change_to

Own-chart → cover-chart analyticity. If h read in its *own* chart at x is analytic, then h read in the cover-chart y is analytic at chartAt y x (for x in that chart's source). The reverse of CechH0.analyticAt_chart_change, at a general point.

theorem analyticAt_chart_change_to {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {h : X → ℂ} {y x : X}
    (hxy : x ∈ (chartAt (H := ℂ) y).source)
    (ha : AnalyticAt ℂ (h ∘ (chartAt (H := ℂ) x).symm) ((chartAt (H := ℂ) x) x)) :
    AnalyticAt ℂ (h ∘ (chartAt (H := ℂ) y).symm) ((chartAt (H := ℂ) y) x)

analyticOn_pullback_of_holo

The chart-pullback of a holomorphic section is AnalyticOn the chart-image. If h is holomorphic on V ⊆ (chartAt y).source (analytic in each point's own chart), then h ∘ (chartAt y).symm is analytic on (chartAt y) '' V. This is the analyticity input to BddHol.ofAnalyticOn.

theorem analyticOn_pullback_of_holo {y : X} {V : Set X} (hV : V ⊆ (chartAt (H := ℂ) y).source)
    {h : X → ℂ}
    (hh : ∀ x ∈ V, AnalyticAt ℂ (h ∘ (chartAt (H := ℂ) x).symm) ((chartAt (H := ℂ) x) x)) :
    AnalyticOn ℂ (h ∘ (chartAt (H := ℂ) y).symm) ((chartAt (H := ℂ) y) '' V)

holoSectionToBddHol

The single-section K-bridge. A holomorphic 𝒪₀ section h on V ⊆ (chartAt y).source, read through the cover-chart y and restricted to a relatively-compact open U' ⋐ (chartAt y) '' V, is a BddHol U' element (analytic via analyticOn_pullback_of_holo, bounded via the relatively-compact shrinking). The value is the section's chart-pullback h ∘ (chartAt y).symm. This is the per-overlap building block of the germ→BddHol cochain map (exists_cechModel).

noncomputable def holoSectionToBddHol {y : X} {V : Set X} (hV : V ⊆ (chartAt (H := ℂ) y).source)
    {h : X → ℂ}
    (hh : ∀ x ∈ V, AnalyticAt ℂ (h ∘ (chartAt (H := ℂ) x).symm) ((chartAt (H := ℂ) x) x))
    {U' : Set ℂ} (hsub : closure U' ⊆ (chartAt (H := ℂ) y) '' V) (hcpt : IsCompact (closure U')) :
    BddHol U'

holoSectionToBddHol_toFun_of_mem

@[simp] theorem holoSectionToBddHol_toFun_of_mem {y : X} {V : Set X}
    (hV : V ⊆ (chartAt (H := ℂ) y).source) {h : X → ℂ}
    (hh : ∀ x ∈ V, AnalyticAt ℂ (h ∘ (chartAt (H := ℂ) x).symm) ((chartAt (H := ℂ) x) x))
    {U' : Set ℂ} (hsub : closure U' ⊆ (chartAt (H := ℂ) y) '' V) (hcpt : IsCompact (closure U'))
    {z : ℂ} (hz : z ∈ U') :
    (holoSectionToBddHol hV hh hsub hcpt).toFun z = h ((chartAt (H := ℂ) y).symm z)

bddHol_pullback_analyticAt

Inverse local K-bridge atom. A bounded holomorphic function on an open chart-image U' pulls back along a chart to a function that is analytic in each point's own chart, provided the chart value lands in U'. This is the local analytic input for the BddHol → OmegaD 0 direction.

theorem bddHol_pullback_analyticAt {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {y x : X}
    {U' : Set ℂ} (hU' : IsOpen U')
    (g : BddHol U') (hx : x ∈ (chartAt (H := ℂ) y).source)
    (hmem : (chartAt (H := ℂ) y) x ∈ U') :
    AnalyticAt ℂ
      ((fun z : X => g.toFun ((chartAt (H := ℂ) y) z)) ∘ (chartAt (H := ℂ) x).symm)
      ((chartAt (H := ℂ) x) x)

bddHol_pullback_mem_OmegaD_zero

Inverse K-bridge to OmegaD 0. A bounded holomorphic function on an open chart-image can be pulled back along a chart to a holomorphic section on the corresponding open domain in X. This is the inverse bridge for the BddHol ↔ OmegaD 0 comparison direction.

theorem bddHol_pullback_mem_OmegaD_zero {y : X} {V : Opens X} {U' : Set ℂ}
    (hV : (V : Set X) ⊆ (chartAt (H := ℂ) y).source) (hU' : IsOpen U')
    (himg : (chartAt (H := ℂ) y) '' (V : Set X) ⊆ U') (g : BddHol U') :
    ((fun x : X => g.toFun ((chartAt (H := ℂ) y) x)) ∘ (Subtype.val : V → X)) ∈
      OmegaD (0 : Divisor X) V

bddHol_pullback_mem_OmegaD_zero_image

Exact-image inverse K-bridge. If the BddHol domain is exactly the chart image of an open V, then pulling back along the chart gives a holomorphic OmegaD 0-section on V. This is the clean local inverse on exact chart-image domains.

theorem bddHol_pullback_mem_OmegaD_zero_image {y : X} {V : Opens X}
    (hV : (V : Set X) ⊆ (chartAt (H := ℂ) y).source)
    (g : BddHol ((chartAt (H := ℂ) y) '' (V : Set X))) :
    ((fun x : X => g.toFun ((chartAt (H := ℂ) y) x)) ∘ (Subtype.val : V → X)) ∈
      OmegaD (0 : Divisor X) V

bddHolToOmegaDGerm_zero_image

Inverse exact-image K-bridge at the germ level. Pulling a BddHol function back along the chart on the exact image of V yields an OmegaDGerm 0 section of V. This is the germ-class version of bddHolToOmegaD_zero_image, and the bridge the cochain comparison can consume.

noncomputable def bddHolToOmegaDGerm_zero_image {y : X} {V : Opens X}
    (hV : (V : Set X) ⊆ (chartAt (H := ℂ) y).source) :
    BddHol ((chartAt (H := ℂ) y) '' (V : Set X)) →ₗ[ℂ] OmegaDGerm (0 : Divisor X) V where