A machine-checked solution to the Jacobians challenge

19.14. Finiteness.CechModelDifferential🔗

Jacobians.Finiteness.CechModelDifferential — source

coverTransition

The cover chart transition τ_{ab} = φ_b ∘ φ_a⁻¹ (chart-a coordinates → chart-b coordinates), for the cover charts indexed a, b : Fin #chartCover. Used to transport the b-side 0-cochain component into chart-a coordinates for the Čech δ⁰.

noncomputable def coverTransition (a b : Fin ((chartCover : Finset X).card)) : ℂ → ℂ

continuousOn_coverTransition_Kov

The transition τ_{ab} is continuous on the compact overlap-shrinking Kov (a,b) (chart-a image of innerShrunk a ∩ innerShrunk b): at each point it is analytic (transition_analyticAt_of_mem, both centres' sources containing the inner-shrunk overlap point), hence continuous.

theorem continuousOn_coverTransition_Kov (a b : Fin ((chartCover : Finset X).card)) :
    ContinuousOn (coverTransition (X := X) a b) ((chartCoverOverlapData (X := X)).Kov (a, b))

mapsTo_coverTransition_Kov

The transition τ_{ab} maps the shrinking Kov (a,b) (chart-a coordinates) into coverSetImage b (chart-b image of chartOpen b), where the b-component of a 0-cochain is bounded-holomorphic. A point φ_a x with x ∈ innerShrunk a ∩ innerShrunk b maps to φ_b x ∈ φ_b '' (innerShrunk b) ⊆ φ_b '' (chartOpen b) = coverSetImage b.

theorem mapsTo_coverTransition_Kov {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X]
    (a b : Fin ((chartCover : Finset X).card)) :
    Set.MapsTo (coverTransition (X := X) a b) ((chartCoverOverlapData (X := X)).Kov (a, b))
      (coverSetImage (X := X) b)

transportComp

The off-diagonal transport CLM. The b-component f b : BddHol (coverSetImage b), transported to chart-a coordinates through τ_{ab} and read on the compact shrinking Kov (a,b), as a bounded-continuous function there. This is the + half of (δ⁰f)_{ab} (the cross-chart piece), built from BddHol.precompCLM with the two transition witnesses.

noncomputable def transportComp (a b : Fin ((chartCover : Finset X).card)) :
    BddHol (coverSetImage (X := X) b) →L[ℂ] ((chartCoverOverlapData (X := X)).Kov (a, b) →ᵇ ℂ)

Kov_subset_coverSetImage_fst

The shrinking Kov (a,b) lies in coverSetImage a (chart-a image of innerShrunk a ∩ innerShrunk b ⊆ chartOpen a), so the a-component restricts directly.

theorem Kov_subset_coverSetImage_fst {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X]
    (a b : Fin ((chartCover : Finset X).card)) :
    (chartCoverOverlapData (X := X)).Kov (a, b) ⊆ coverSetImage (X := X) a

restrictComp

The diagonal restriction CLM. The a-component f a : BddHol (coverSetImage a), restricted to the shrinking Kov (a,b) ⊆ coverSetImage a, as a bounded-continuous function there. This is the − half of (δ⁰f)_{ab} (the same-chart piece), built from BddHol.restrictCLM.

noncomputable def restrictComp (a b : Fin ((chartCover : Finset X).card)) :
    BddHol (coverSetImage (X := X) a) →L[ℂ] ((chartCoverOverlapData (X := X)).Kov (a, b) →ᵇ ℂ)

delta0Model

The cross-chart Čech δ⁰ of the chart-cover sup-norm model: Cochain0Model →L[ℂ] Cshr (chartCoverOverlapData's shrinking 1-cochains). Componentwise on overlap (a,b), (δ⁰f)_{ab} = (transport of f b to chart-a) − (restriction of f a) on Kov (a,b), the genuine Čech coboundary with the b-side transported through the holomorphic transition τ_{ab}. Assembled by ContinuousLinearMap.pi over the off-diagonal transport transportComp and diagonal restriction restrictComp.

noncomputable def delta0Model :
    Cochain0Model (X := X) →L[ℂ] (chartCoverOverlapData (X := X)).Cshr

delta0Model_apply

The component identity for δ⁰ at overlap p = (a,b): the off-diagonal transport of f b minus the diagonal restriction of f a.

theorem delta0Model_apply (f : Cochain0Model (X := X)) (p : (chartCoverOverlapData (X := X)).J) :
    delta0Model f p = transportComp p.1 p.2 (f p.2) - restrictComp p.1 p.2 (f p.1)

delta0Model_apply_apply

The Čech coboundary pointwise formula. On the shrinking Kov (a,b), the δ⁰ value at a point z is f b evaluated at the transported point τ_{ab} z minus f a at z — the explicit cross-chart Čech δ⁰ formula (δ⁰f)_{ab}(z) = f_b(τ_{ab} z) − f_a(z).

theorem delta0Model_apply_apply (f : Cochain0Model (X := X))
    (p : (chartCoverOverlapData (X := X)).J) (z : (chartCoverOverlapData (X := X)).Kov p) :
    delta0Model f p z = (f p.2).toFun (coverTransition p.1 p.2 z.1) - (f p.1).toFun z.1

analyticOn_coverTransition_triple

The cover transition τ_{ab} is analytic on the OPEN triple chart-image coverTripleImage (a,b,c): at each point it is analytic (transition\_analyticAt\_of\_mem, both centres' sources containing the triple outer-overlap point), hence analytic on the set.

theorem analyticOn_coverTransition_triple (a b c : Fin ((chartCover : Finset X).card)) :
    AnalyticOn ℂ (coverTransition (X := X) a b) (coverTripleImage (X := X) (a, b, c))

mapsTo_coverTransition_triple

The cover transition τ_{ab} maps the OPEN triple chart-image coverTripleImage (a,b,c) (chart-a coordinates) into Uov (b,c) (chart-b image of chartOpen b ∩ chartOpen c). A point φ_a x with x ∈ chartOpen a ∩ chartOpen b ∩ chartOpen c maps to φ_b x with x ∈ chartOpen b ∩ chartOpen c.

theorem mapsTo_coverTransition_triple {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X]
    (a b c : Fin ((chartCover : Finset X).card)) :
    Set.MapsTo (coverTransition (X := X) a b) (coverTripleImage (X := X) (a, b, c))
      ((chartCoverOverlapData (X := X)).Uov (b, c))

coverTripleImage_subset_Uov_fst_snd

The open triple chart-image coverTripleImage (a,b,c) lies in Uov (a,b) (chart-a image of chartOpen a ∩ chartOpen b ⊇ chartOpen a ∩ chartOpen b ∩ chartOpen c), so f_{ab} restricts.

theorem coverTripleImage_subset_Uov_fst_snd {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X]
    (a b c : Fin ((chartCover : Finset X).card)) :
    coverTripleImage (X := X) (a, b, c) ⊆ (chartCoverOverlapData (X := X)).Uov (a, b)

coverTripleImage_subset_Uov_fst_trd

The open triple chart-image coverTripleImage (a,b,c) lies in Uov (a,c) (chart-a image of chartOpen a ∩ chartOpen c ⊇ chartOpen a ∩ chartOpen b ∩ chartOpen c), so f_{ac} restricts.

theorem coverTripleImage_subset_Uov_fst_trd {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X]
    (a b c : Fin ((chartCover : Finset X).card)) :
    coverTripleImage (X := X) (a, b, c) ⊆ (chartCoverOverlapData (X := X)).Uov (a, c)

transportCovTriple

The cover-side transport CLM. The (b,c)-component f_{bc} : BddHol (Uov (b,c)), transported to chart-a coordinates through the analytic transition τ_{ab} and landing on the open triple-image, as a BddHol (coverTripleImage (a,b,c)). The cross-chart + piece of (δ¹f)_{abc}, via BddHol.precompHolCLM.

noncomputable def transportCovTriple (a b c : Fin ((chartCover : Finset X).card)) :
    BddHol ((chartCoverOverlapData (X := X)).Uov (b, c)) →L[ℂ]
      BddHol (coverTripleImage (X := X) (a, b, c))

delta1CovModel

The cross-chart Čech δ¹ on the COVER side Cochain2CovModel. Componentwise on the triple (a,b,c), (δ¹f)_{abc} = (transport of f_{bc} to chart-a) − (restriction of f_{ac}) + (restriction of f_{ab}) on the open triple-image coverTripleImage (a,b,c) — the genuine Čech coboundary with the cross-chart (b,c)-component transported through the holomorphic transition τ_{ab}. Assembled by ContinuousLinearMap.pi over the cover-side transport transportCovTriple and the two diagonal open-restrictions BddHol.restrictOpenCLM.

noncomputable def delta1CovModel :
    DiskOverlapData.Ccov (chartCoverOverlapData (X := X)) →L[ℂ] Cochain2CovModel (X := X)

delta1CovModel_apply

The component identity for the cover-side δ¹ at the triple t = (a,b,c).

theorem delta1CovModel_apply (f : DiskOverlapData.Ccov (chartCoverOverlapData (X := X)))
    (t : Fin ((chartCover : Finset X).card) × Fin ((chartCover : Finset X).card) ×
      Fin ((chartCover : Finset X).card)) :
    delta1CovModel f t = transportCovTriple t.1 t.2.1 t.2.2 (f (t.2.1, t.2.2))
      - BddHol.restrictOpenCLM (coverTripleImage_subset_Uov_fst_trd t.1 t.2.1 t.2.2)
        (f (t.1, t.2.2))
      + BddHol.restrictOpenCLM (coverTripleImage_subset_Uov_fst_snd t.1 t.2.1 t.2.2)
          (f (t.1, t.2.1))

delta1CovModel_toFun_of_mem

The cover-side Čech coboundary pointwise formula. On the open triple-image, the δ¹ value at z is f_{bc} at the transported point τ_{ab} z minus f_{ac} at z plus f_{ab} at z — the explicit cross-chart Čech δ¹ formula (δ¹f)_{abc}(z) = f_{bc}(τ_{ab} z) − f_{ac}(z) + f_{ab}(z).

theorem delta1CovModel_toFun_of_mem (f : DiskOverlapData.Ccov (chartCoverOverlapData (X := X)))
    (t : Fin ((chartCover : Finset X).card) × Fin ((chartCover : Finset X).card) ×
      Fin ((chartCover : Finset X).card)) {z : ℂ} (hz : z ∈ coverTripleImage (X := X) t) :
    (delta1CovModel f t).toFun z
      = (f (t.2.1, t.2.2)).toFun (coverTransition t.1 t.2.1 z)
        - (f (t.1, t.2.2)).toFun z + (f (t.1, t.2.1)).toFun z

subtypeCM

Build a C(↥S, ↥T) from a ContinuousOn f S mapping S into T. The continuous reindexing the shrinking-side δ¹ precomposes with.

noncomputable def subtypeCM {S T : Set ℂ} {f : ℂ → ℂ} (hf : ContinuousOn f S)
    (hmaps : Set.MapsTo f S T) : C(↥S, ↥T)

subtypeCM_apply

@[simp] theorem subtypeCM_apply {S T : Set ℂ} {f : ℂ → ℂ} (hf : ContinuousOn f S)
    (hmaps : Set.MapsTo f S T) (z : ↥S) : (subtypeCM hf hmaps z : ℂ) = f z.1

continuousOn_coverTransition_triple

The transition τ_{ab} is continuous on the compact triple shrinking coverTripleShrink (a,b,c) (at each point analytic, hence continuous).

theorem continuousOn_coverTransition_triple (a b c : Fin ((chartCover : Finset X).card)) :
    ContinuousOn (coverTransition (X := X) a b) (coverTripleShrink (X := X) (a, b, c))

mapsTo_coverTransition_triple_shrink

The transition τ_{ab} maps the compact triple shrinking coverTripleShrink (a,b,c) (chart-a coordinates) into Kov (b,c) (chart-b image of innerShrunk b ∩ innerShrunk c).

theorem mapsTo_coverTransition_triple_shrink {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X]
    (a b c : Fin ((chartCover : Finset X).card)) :
    Set.MapsTo (coverTransition (X := X) a b) (coverTripleShrink (X := X) (a, b, c))
      ((chartCoverOverlapData (X := X)).Kov (b, c))

coverTripleShrink_subset_Kov_fst_snd

The compact triple shrinking coverTripleShrink (a,b,c) lies in Kov (a,b) (chart-a image of innerShrunk a ∩ innerShrunk b ⊇ innerShrunk a ∩ innerShrunk b ∩ innerShrunk c).

theorem coverTripleShrink_subset_Kov_fst_snd {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X]
    (a b c : Fin ((chartCover : Finset X).card)) :
    coverTripleShrink (X := X) (a, b, c) ⊆ (chartCoverOverlapData (X := X)).Kov (a, b)

coverTripleShrink_subset_Kov_fst_trd

The compact triple shrinking coverTripleShrink (a,b,c) lies in Kov (a,c).

theorem coverTripleShrink_subset_Kov_fst_trd {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X]
    (a b c : Fin ((chartCover : Finset X).card)) :
    coverTripleShrink (X := X) (a, b, c) ⊆ (chartCoverOverlapData (X := X)).Kov (a, c)

coverTransitionTripleCM

The transition reindexing C(↥coverTripleShrink (a,b,c), ↥Kov (b,c)) for the cross-chart s_{bc} transport.

noncomputable def coverTransitionTripleCM (a b c : Fin ((chartCover : Finset X).card)) :
    C(↥(coverTripleShrink (X := X) (a, b, c)), ↥((chartCoverOverlapData (X := X)).Kov (b, c)))

inclTripleFstSndCM

The inclusion reindexing C(↥coverTripleShrink (a,b,c), ↥Kov (a,b)) for the diagonal s_{ab}.

noncomputable def inclTripleFstSndCM (a b c : Fin ((chartCover : Finset X).card)) :
    C(↥(coverTripleShrink (X := X) (a, b, c)), ↥((chartCoverOverlapData (X := X)).Kov (a, b)))

inclTripleFstTrdCM

The inclusion reindexing C(↥coverTripleShrink (a,b,c), ↥Kov (a,c)) for the diagonal s_{ac}.

noncomputable def inclTripleFstTrdCM (a b c : Fin ((chartCover : Finset X).card)) :
    C(↥(coverTripleShrink (X := X) (a, b, c)), ↥((chartCoverOverlapData (X := X)).Kov (a, c)))

delta1Model

The cross-chart Čech δ¹ on the SHRINKING side Cshr →L[ℂ] Cochain2Model. Componentwise on the triple (a,b,c), (δ¹s)_{abc} = (s_{bc} ∘ τ_{ab}) − (s_{ac}|·) + (s_{ab}|·) on coverTripleShrink (a,b,c), the genuine Čech coboundary with the (b,c)-component transported chart-b→chart-a through the holomorphic transition τ_{ab}. Assembled by ContinuousLinearMap.pi over the bounded-continuous precompositions bcfCompContinuousCLM with the transition reindexing and the two inclusions.

noncomputable def delta1Model :
    (chartCoverOverlapData (X := X)).Cshr →L[ℂ] Cochain2Model (X := X)

delta1Model_apply

The component identity for the shrinking-side δ¹ at the triple t = (a,b,c).

theorem delta1Model_apply (s : (chartCoverOverlapData (X := X)).Cshr)
    (t : Fin ((chartCover : Finset X).card) × Fin ((chartCover : Finset X).card) ×
      Fin ((chartCover : Finset X).card)) :
    delta1Model s t = (s (t.2.1, t.2.2)).compContinuous (coverTransitionTripleCM t.1 t.2.1 t.2.2)
      - (s (t.1, t.2.2)).compContinuous (inclTripleFstTrdCM t.1 t.2.1 t.2.2)
      + (s (t.1, t.2.1)).compContinuous (inclTripleFstSndCM t.1 t.2.1 t.2.2)

delta1Model_apply_apply

The shrinking-side Čech coboundary pointwise formula. On the compact triple shrinking, the δ¹ value at z is s_{bc} at the transported point τ_{ab} z minus s_{ac} at z plus s_{ab} at z — the explicit cross-chart Čech δ¹ formula (δ¹s)_{abc}(z) = s_{bc}(τ_{ab} z) − s_{ac}(z) + s_{ab}(z) (s_{ac}, s_{ab} at the *same point* z, via the inclusion of compacts).

theorem delta1Model_apply_apply (s : (chartCoverOverlapData (X := X)).Cshr)
    (t : Fin ((chartCover : Finset X).card) × Fin ((chartCover : Finset X).card) ×
      Fin ((chartCover : Finset X).card)) (z : ↥(coverTripleShrink (X := X) t)) :
    delta1Model s t z
      = s (t.2.1, t.2.2)
        ⟨coverTransition t.1 t.2.1 z.1, mapsTo_coverTransition_triple_shrink _ _ _ z.2⟩
        - s (t.1, t.2.2) ⟨z.1, coverTripleShrink_subset_Kov_fst_trd _ _ _ z.2⟩
        + s (t.1, t.2.1) ⟨z.1, coverTripleShrink_subset_Kov_fst_snd _ _ _ z.2⟩

coverTransition_cocycle

The chart-transition cocycle identity on the triple shrinking: τ_{bc}(τ_{ab} z) = τ_{ac} z for z ∈ coverTripleShrink (a,b,c). Geometrically φ_c ∘ φ_b⁻¹ ∘ φ_b ∘ φ_a⁻¹ = φ_c ∘ φ_a⁻¹ where the inner cancellations φ_b⁻¹∘φ_b, φ_a⁻¹∘φ_a hold because the triple-overlap point x lies in all three chart sources. This is the algebraic heart of δ¹∘δ⁰ = 0 (the f_c-terms land at the SAME point).

theorem coverTransition_cocycle {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X]
    (a b c : Fin ((chartCover : Finset X).card)) {z : ℂ}
    (hz : z ∈ coverTripleShrink (X := X) (a, b, c)) :
    coverTransition b c (coverTransition a b z) = coverTransition a c z

delta1_comp_delta0_eq_zero

δ¹ ∘ δ⁰ = 0 (the Čech hδδ). The composite of the cross-chart δ⁰ and the shrinking-side δ¹ vanishes — the defining Čech-complex identity δ² = 0. Pointwise on the triple shrinking the six terms of (δ¹(δ⁰f))_{abc}(z) collapse to f_c(τ_{bc}(τ_{ab} z)) − f_c(τ_{ac} z), which is 0 by the cocycle identity coverTransition_cocycle (the two f_c-arguments coincide). This makes the sup-norm cochains a genuine Čech δ-complex (B¹ ⊆ Z¹), the Coboundaries.hδδ field for the chart-cover model.

theorem delta1_comp_delta0_eq_zero :
    (delta1Model (X := X)).comp delta0Model = 0

coverTripleShrink_subset_coverTripleImage

The compact triple shrinking lies in the open triple-image (chart-a image of innerShrunk a ∩ innerShrunk b ∩ innerShrunk c ⊆ chartOpen a ∩ chartOpen b ∩ chartOpen c). So a 2-cochain holomorphic on the open triple-image restricts to a bounded-continuous function on the compact triple shrinking.

theorem coverTripleShrink_subset_coverTripleImage {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X]
    (t : Fin ((chartCover : Finset X).card) ×
    Fin ((chartCover : Finset X).card) × Fin ((chartCover : Finset X).card)) :
    coverTripleShrink (X := X) t ⊆ coverTripleImage (X := X) t

rho2Model

The 2-cochain restriction ρ² : Cochain2CovModel →L Cochain2Model (cover → shrinking), componentwise BddHol.restrictCLM from the open triple-image to the compact triple shrinking. Carries the cover-side δ¹ to the shrinking-side δ¹ (the commuting square rho2_comp_delta1Cov).

noncomputable def rho2Model : Cochain2CovModel (X := X) →L[ℂ] Cochain2Model (X := X)

rho2Model_apply

@[simp] theorem rho2Model_apply {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X]
    (g : Cochain2CovModel (X := X))
    (t : Fin ((chartCover : Finset X).card) × Fin ((chartCover : Finset X).card) ×
      Fin ((chartCover : Finset X).card)) :
    rho2Model g t = BddHol.restrictCLM (coverTripleShrink_subset_coverTripleImage t) (g t)

delta1_comp_rhoRaw_eq_rho2_comp_delta1Cov

The commuting square δ¹_shr ∘ ρ = ρ² ∘ δ¹_cov. Restricting a cover 1-cochain to the shrinking and applying the shrinking δ¹ is the same as applying the cover δ¹ and restricting the resulting 2-cochain — the Čech naturality of δ¹ under cover-refinement. Pointwise both sides equal x_{bc}(τ_{ab} z) − x_{ac}(z) + x_{ab}(z) on the triple shrinking. This is the bridge that gives the Coboundaries.hcomm field (restriction carries cocycles to cocycles).

theorem delta1_comp_rhoRaw_eq_rho2_comp_delta1Cov :
    (delta1Model (X := X)).comp (chartCoverOverlapData (X := X)).rhoRaw
      = rho2Model.comp delta1CovModel

delta1_rhoRaw_eq_zero_of_delta1Cov_eq_zero

hcomm for the chart cover (restriction carries cover-cocycles to shrinking-cocycles). If a cover 1-cochain x is a cocycle (δ¹_cov x = 0), then its restriction ρ x is a shrinking cocycle (δ¹_shr (ρ x) = 0). Immediate from the commuting square δ¹_shr∘ρ = ρ²∘δ¹_cov: δ¹_shr(ρ x) = ρ²(δ¹_cov x) = ρ²(0) = 0. This is the Coboundaries.hcomm field for the chart-cover model.

theorem delta1_rhoRaw_eq_zero_of_delta1Cov_eq_zero
    (x : DiskOverlapData.Ccov (chartCoverOverlapData (X := X)))
    (hx : delta1CovModel x = 0) :
    delta1Model ((chartCoverOverlapData (X := X)).rhoRaw x) = 0

delta1Model_diagonal_eq_zero

The diagonal of a shrinking 1-cocycle vanishes (a structural necessary condition for the ChartCoverContinuousLeray hypothesis). For any cocycle s (delta1Model s = 0) and any cover index a, the diagonal component s (a,a) is 0 on Kov (a,a): the triple (a,a,a) gives (δ¹s)_{aaa}(z) = s_{aa}(τ_{aa} z) − s_{aa}(z) + s_{aa}(z), and τ_{aa} = id on Kov (a,a), so this collapses to s_{aa}(z) = 0. This pins the cocycle structure used by the (corrected) disk-acyclicity splitting; it is the chart-cover analogue of the antisymmetry/diagonal Čech relations.

theorem delta1Model_diagonal_eq_zero (s : (chartCoverOverlapData (X := X)).Cshr)
    (hs : delta1Model (X := X) s = 0) (a : Fin ((chartCover : Finset X).card))
    (z : ↥(coverTripleShrink (X := X) (a, a, a))) :
    s (a, a) ⟨z.1, coverTripleShrink_subset_Kov_fst_snd a a a z.2⟩ = 0

ChartCoverDifferentialData

The standard chart-cover Čech differential bundle, packaging δ⁰, δ¹, δ¹cov, δ¹∘δ⁰ = 0, and commuting-square data. This is the structural half of the model construction; the leray field is handled separately downstream.

structure ChartCoverDifferentialData where

chartCoverDifferentialData

The standard chart-cover Čech differential data, packaged as a single record.

noncomputable def chartCoverDifferentialData : ChartCoverDifferentialData (X := X) where