The Mittag-Leffler atom and the skyscraper fragment (CC8, D7, proof plan §6.9)

Unit: cech-cohomology (docs/design/cech-cohomology.md §4.7).

• C1.MemLD/C1.retype: a D'-cochain all of whose components satisfy the smaller D-bound, re-tagged as a D-cochain (same underlying germs).
• mlClass: the Mittag-Leffler atom — a D'-0-cochain with D-bounded coboundary yields a class in H¹(D). Both the χ connecting map (finiteness-and-chi) and laurent-tails' T[D] → H¹(D) factor through this.
• mlClass_eq_zero_iff: the vanishing criterion (the "engine" — uses H⁰ ≃ L(D') gluing and toH1's colimit description).

mlClass/mlClass_eq_zero_iff (both directions — the ⇒ half uses toH1_injective, Forster 12.4, from Injectivity.lean) are proved with zero sorries; both the χ ledger and laurent-tails' T[D] → H¹(D) map factor through mlClass. The rest of the six-term fragment — H1Incl_surjective (part (g)), windowConnect, exists_realization, Lemma A (mlClass_eq_of_realizes), exact_windowMap_windowConnect, exact_windowConnect_H1Incl — is proved in SixTerm.lean.

C1.MemLD, C1.retype

def RS.Cech.C1.MemLD {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} {D' : Divisor X} (f : C1 D' 𝒰) (D : Divisor X) : Prop

A C¹(D')-cochain all of whose components satisfy the D-bound.

Equations

• f.MemLD D = ∀ (p : Fin 𝒰.n × Fin 𝒰.n), ↑(f p) ∈ RS.LinSysOn D ↑(𝒰.U p.1 ⊓ 𝒰.U p.2)

noncomputable def RS.Cech.C1.retype {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} {D D' : Divisor X} (f : C1 D' 𝒰) (hf : f.MemLD D) : C1 D 𝒰

Re-tag a D'-cochain satisfying the D-bound as a D-cochain (same underlying germs).

Equations

• f.retype hf p = ⟨↑(f p), ⋯⟩

theorem RS.Cech.C1.retype_apply_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} {D D' : Divisor X} (f : C1 D' 𝒰) (hf : f.MemLD D) (p : Fin 𝒰.n × Fin 𝒰.n) : ↑(f.retype hf p) = ↑(f p)

theorem RS.Cech.C1.retype_mem_Z1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} {D D' : Divisor X} {g : C0 D' 𝒰} (hg : ((d0 D' 𝒰) g).MemLD D) : ((d0 D' 𝒰) g).retype hg ∈ Z1 D 𝒰

The Mittag-Leffler atom

noncomputable def RS.Cech.mlClass {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D D' : Divisor X} (𝒰 : FinCover ⊤) (g : C0 D' 𝒰) (hg : ((d0 D' 𝒰) g).MemLD D) : H1 D

The Mittag-Leffler atom (D7): a D'-0-cochain with D-bounded coboundary yields a class in H¹(D).

Equations

• RS.Cech.mlClass 𝒰 g hg = (RS.Cech.toH1 D 𝒰) ((RS.Cech.H1Cover.mk D 𝒰) ⟨((RS.Cech.d0 D' 𝒰) g).retype hg, ⋯⟩)

theorem RS.Cech.mlClass_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D D' : Divisor X} {𝒰 : FinCover ⊤} (g g' : C0 D' 𝒰) (hg : ((d0 D' 𝒰) g).MemLD D) (hg' : ((d0 D' 𝒰) g').MemLD D) (hgg' : ((d0 D' 𝒰) (g + g')).MemLD D) : mlClass 𝒰 (g + g') hgg' = mlClass 𝒰 g hg + mlClass 𝒰 g' hg'

theorem RS.Cech.mlClass_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D D' : Divisor X} {𝒰 : FinCover ⊤} (a : ℂ) (g : C0 D' 𝒰) (hg : ((d0 D' 𝒰) g).MemLD D) (hag : ((d0 D' 𝒰) (a • g)).MemLD D) : mlClass 𝒰 (a • g) hag = a • mlClass 𝒰 g hg

theorem RS.Cech.H1Incl_mlClass {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D D' : Divisor X} {𝒰 : FinCover ⊤} (h : D ≤ D') (g : C0 D' 𝒰) (hg : ((d0 D' 𝒰) g).MemLD D) : (H1Incl D h) (mlClass 𝒰 g hg) = 0

The vanishing criterion (§6.9(b), ⇐ half)

The ⇐ half below (a class realized by a global section vanishes) needs no injectivity and is what laurent-tails' truncation map α_D actually produces classes from; it is proved here with zero sorries. The ⇒ half (needing toH1_injective, Forster 12.4) is proved further down, after Injectivity.lean's import — see mlClass_eq_zero_iff below.

theorem RS.Cech.mlClass_eq_zero_of_exists {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D D' : Divisor X} {𝒰 : FinCover ⊤} (g : C0 D' 𝒰) (hg : ((d0 D' 𝒰) g).MemLD D) (φ : ↥(LinSys D')) (hφ : ∀ (i : Fin 𝒰.n), ∀ x ∈ 𝒰.U i, -↑(D x) ≤ (↑(g i) - (MeroGermOn.restrict ⋯) ↑φ).ord x) : mlClass 𝒰 g hg = 0

The vanishing criterion (§6.9(b), ⇒ half): now unlocked by toH1_injective (12.4).

theorem RS.Cech.mlClass_eq_zero_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {D D' : Divisor X} {𝒰 : FinCover ⊤} (h : D ≤ D') (g : C0 D' 𝒰) (hg : ((d0 D' 𝒰) g).MemLD D) : mlClass 𝒰 g hg = 0 ↔ ∃ (φ : ↥(LinSys D')), ∀ (i : Fin 𝒰.n), ∀ x ∈ 𝒰.U i, -↑(D x) ≤ (↑(g i) - (MeroGermOn.restrict ⋯) ↑φ).ord x

§6.9(b): the full vanishing criterion for mlClass — toH1_injective spares us any refinement: a coboundary witness for retype (d0 g) already lives on 𝒰 itself.