The six-term skyscraper fragment (CC8, D7, proof plan §6.9(c)-(g))

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

• C1.retype_mem_Z1': the general (non-coboundary) retype-preserves-Z1 fact.
• h1CoverIncl_mk_retype: the D-inclusion of a retyped Z1 D 𝒰 class recovers the original Z1 D' 𝒰 class.
• memLD_of_isAdapted: on a cover adapted to diffSupp D D', every Z1 D' 𝒰-cocycle already satisfies the (smaller) D-bound — diagonal components vanish to order ⊤ (Z1.ord_diag), off-diagonal components avoid the finite set where D ≠ D' (FinCover.IsAdapted.not_mem_inf), so D = D' pointwise there.
• H1Incl_surjective: no H², no long exact sequence, no snake lemma — every class of H1 D' is already represented, on a suitably adapted cover, by a genuine Z1 D-cocycle.
• exists_tail_approx ("Lemma B"): any germ near q of order ≥ -d' is approximated, to order > -d - 1 at q, by a chart-source germ in ordGe q (-d') — a finite Laurent tail, built by iterating the one-step leading-coefficient subtraction (exists_tail_step; same correction step as WindowRank's splitting, redone on an arbitrary open W ∋ q because leadCoeff is chart-source-bound).
• windowDefect + Realizes (§6.9(c), D7): the pointwise-ord realization predicate. The design's (w q).out form is replaced by quantification over all representatives of w q (equivalent by windowDefect_bound_of_mk_eq; strictly easier to consume).
• exists_realization (§6.9(c)) and mlClass_eq_of_realizes (§6.9(d), "Lemma A" — proved without any adaptedness hypothesis: only the Realizes bounds and D = D' off diffSupp enter).
• windowConnect/windowConnect_spec (§6.9(d)): the connecting map Window D D' →ₗ H¹(D).
• exact_windowMap_windowConnect (§6.9(e)), exact_windowConnect_H1Incl (§6.9(f)): with Window.lean's exact_inclusion_windowMap/inclusion_injective and H1Incl_surjective below, this completes the six-term fragment 0 → L(D) → L(D') → Window D D' → H¹(D) → H¹(D') → 0.

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

General (non-coboundary) version of C1.retype_mem_Z1: retyping a Z1 D'-cocycle whose components all satisfy the D-bound gives a Z1 D-cocycle.

theorem RS.Cech.h1CoverIncl_mk_retype {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} {D D' : Divisor X} (h : D ≤ D') {f : C1 D' 𝒰} (hf : f ∈ Z1 D' 𝒰) (hmem : f.MemLD D) : (h1CoverIncl D 𝒰 h) ((H1Cover.mk D 𝒰) ⟨f.retype hmem, ⋯⟩) = (H1Cover.mk D' 𝒰) ⟨f, hf⟩

The D-inclusion of a retyped Z1 D 𝒰 class recovers the original Z1 D' 𝒰 class.

Small order arithmetic helpers

theorem RS.Cech.WindowAt.mk_surjective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) (d d' : ℤ) : Function.Surjective ⇑(mk p d d')

Local tail approximation ("Lemma B", §6.9(c) input)

A germ γ near q of order ≥ -d' at q is approximated to order ≥ -d by a genuine chart-source germ in ordGe q (-d') — a finite Laurent tail. Built by iterating the one-step leading-coefficient subtraction (the same correction as WindowRank.lean's splitting, redone here on an arbitrary open W ∋ q because leadCoeff is chart-source-bound).

theorem RS.Cech.tailGerm_mul_tailGerm_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] (q : X) (m : ℤ) : tailGerm q m * tailGerm q (-m) = 1

theorem RS.Cech.exists_tail_approx {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] (q : X) {W : Set X} (hW : IsOpen W) (hWs : W ⊆ (chartAt ℂ q).source) (hq : q ∈ W) {d d' : ℤ} (hdd : d ≤ d') (γ : MeroGermOn X W) (hγ : ↑(-d') ≤ γ.ord q) : ∃ (ψ : ↥(ordGe q (-d'))), ↑(-d) ≤ (γ - (MeroGermOn.restrict hWs) ↑ψ).ord q

Local tail approximation ("Lemma B"): a germ γ on an open W ∋ q inside the chart source with ord_q γ ≥ -d' is matched, to order ≥ -d at q, by a chart-source germ of ordGe q (-d') (a finite Laurent tail Σ c_m θ_{q,m}).

The window defect (D7): the pointwise-ord comparison germ

noncomputable def RS.Cech.windowDefect {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {V : TopologicalSpace.Opens X} {q : X} (γ : MeroGermOn X ↑V) (ψ : MeroGermOn X (chartAt ℂ q).source) : MeroGermOn X (↑V ∩ (chartAt ℂ q).source)

The comparison germ of a local section γ (on a member V) against a chart-source germ ψ at q, on the common open V ∩ (chartAt ℂ q).source (D7: all realization bookkeeping is a pointwise ord bound on this germ).

Equations

• RS.Cech.windowDefect γ ψ = (RS.MeroGermOn.restrict ⋯) γ - (RS.MeroGermOn.restrict ⋯) ψ

theorem RS.Cech.windowDefect_ord_congr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {V : TopologicalSpace.Opens X} {q : X} {T : Set X} (hT : IsOpen T) (hTV : T ⊆ ↑V) (hTs : T ⊆ (chartAt ℂ q).source) (hqT : q ∈ T) (γ : MeroGermOn X ↑V) (ψ : MeroGermOn X (chartAt ℂ q).source) : (windowDefect γ ψ).ord q = ((MeroGermOn.restrict hTV) γ - (MeroGermOn.restrict hTs) ψ).ord q

The ord of the defect at q can be computed after restricting both germs to any open T ∋ q inside both domains (the normalization workhorse for all defect bookkeeping).

theorem RS.Cech.windowDefect_ord_restrict {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {V V' : TopologicalSpace.Opens X} {q : X} (hVV' : V' ≤ V) (hq : q ∈ V') (γ : MeroGermOn X ↑V) (ψ : MeroGermOn X (chartAt ℂ q).source) : (windowDefect ((MeroGermOn.restrict hVV') γ) ψ).ord q = (windowDefect γ ψ).ord q

Restricting the local section to a smaller member does not change the defect's ord.

theorem RS.Cech.windowDefect_bound_of_mk_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {V : TopologicalSpace.Opens X} {q : X} (hq : q ∈ V) {dq d'q : ℤ} {γ : MeroGermOn X ↑V} {ψ₀ ψ : ↥(ordGe q (-d'q))} (hmk : (WindowAt.mk q dq d'q) ψ₀ = (WindowAt.mk q dq d'q) ψ) (hb : ↑(-dq) ≤ (windowDefect γ ↑ψ₀).ord q) : ↑(-dq) ≤ (windowDefect γ ↑ψ).ord q

Rep-change: the defect bound only depends on the WindowAt-class of the chart-source germ (two representatives differ by ordGe q (-dq), which is absorbed by ord_add). This is why Realizes may quantify over all representatives.

C1.MemLD closure properties

theorem RS.Cech.C1.MemLD.res {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} {D D' : Divisor X} {𝒱 : FinCover Ω} {f : C1 D' 𝒰} (hf : f.MemLD D) (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) : ((resC1 D' τ hτ) f).MemLD D

theorem RS.Cech.memLD_d0_res {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} {D D' : Divisor X} {𝒱 : FinCover Ω} {g : C0 D' 𝒰} (hg : ((d0 D' 𝒰) g).MemLD D) (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) : ((d0 D' 𝒱) ((resC0 D' τ hτ) g)).MemLD D

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

theorem RS.Cech.C1.MemLD.smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} {D D' : Divisor X} (a : ℂ) {f : C1 D' 𝒰} (hf : f.MemLD D) : (a • f).MemLD D

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

theorem RS.Cech.memLD_d0_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} {D D' : Divisor X} (a : ℂ) {g : C0 D' 𝒰} (hg : ((d0 D' 𝒰) g).MemLD D) : ((d0 D' 𝒰) (a • g)).MemLD D

mlClass is refinement-stable (§6.9(a), mlClass_res)

theorem RS.Cech.mlClass_res {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D D' : Divisor X} {𝒰 𝒱 : FinCover ⊤} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) (g : C0 D' 𝒰) (hg : ((d0 D' 𝒰) g).MemLD D) (hgr : ((d0 D' 𝒱) ((resC0 D' τ hτ) g)).MemLD D) : mlClass 𝒱 ((resC0 D' τ hτ) g) hgr = mlClass 𝒰 g hg

theorem RS.Cech.memLD_of_isAdapted {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D D' : Divisor X} [T2Space X] [CompactSpace X] {𝒲 : FinCover ⊤} (hadapt : 𝒲.IsAdapted (diffSupp D D')) {f : C1 D' 𝒲} (hf : f ∈ Z1 D' 𝒲) : f.MemLD D

On a cover adapted to diffSupp D D', every Z1 D'-cocycle already satisfies the D-bound componentwise: diagonal components vanish to order ⊤, off-diagonal components avoid the finite set where D ≠ D' (adaptedness), hence D = D' there and the D'-bound is the D-bound.

theorem RS.Cech.H1Incl_surjective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D D' : Divisor X} [T2Space X] [CompactSpace X] (h : D ≤ D') : Function.Surjective ⇑(H1Incl D h)

Realizes (§6.9(c), D7): the pointwise-ord realization predicate

def RS.Cech.Realizes {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D D' : Divisor X} [T2Space X] [CompactSpace X] (𝒰 : FinCover ⊤) (g : C0 D' 𝒰) (w : Window D D') : Prop

g realizes the window vector w (pointwise-ord form, D7): at every q of diffSupp D D' and every member containing q, the defect of g's component against any representative of w q has order ≥ -(D q) at q. (Deviation from the design's (w q).out formulation: quantifying over all representatives is equivalent by windowDefect_bound_of_mk_eq, and strictly easier to consume.)

Equations

• One or more equations did not get rendered due to their size.

theorem RS.Cech.Realizes.res {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D D' : Divisor X} [T2Space X] [CompactSpace X] {𝒰 𝒱 : FinCover ⊤} {g : C0 D' 𝒰} {w : Window D D'} (hr : Realizes 𝒰 g w) (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) : Realizes 𝒱 ((resC0 D' τ hτ) g) w

theorem RS.Cech.Realizes.add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D D' : Divisor X} [T2Space X] [CompactSpace X] {𝒰 : FinCover ⊤} {g g' : C0 D' 𝒰} {w w' : Window D D'} (hr : Realizes 𝒰 g w) (hr' : Realizes 𝒰 g' w') : Realizes 𝒰 (g + g') (w + w')

theorem RS.Cech.Realizes.smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D D' : Divisor X} [T2Space X] [CompactSpace X] {𝒰 : FinCover ⊤} (a : ℂ) {g : C0 D' 𝒰} {w : Window D D'} (hr : Realizes 𝒰 g w) : Realizes 𝒰 (a • g) (a • w)

Lemma A (§6.9(d)): independence of the realization

theorem RS.Cech.mlClass_eq_of_realizes {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D D' : Divisor X} [T2Space X] [CompactSpace X] {𝒰 𝒰' : FinCover ⊤} {g : C0 D' 𝒰} {g' : C0 D' 𝒰'} (hg : ((d0 D' 𝒰) g).MemLD D) (hg' : ((d0 D' 𝒰') g').MemLD D) {w : Window D D'} (hr : Realizes 𝒰 g w) (hr' : Realizes 𝒰' g' w) : mlClass 𝒰 g hg = mlClass 𝒰' g' hg'

Lemma A (§6.9(d)): any two Mittag-Leffler realizations of the same window vector give the same H¹(D)-class. No adaptedness is needed: at diffSupp-points the two Realizes bounds control the difference, everywhere else D = D' and the D'-bounds do.

exists_realization (§6.9(c))

theorem RS.Cech.exists_realization {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {D D' : Divisor X} [T2Space X] [CompactSpace X] (_h : D ≤ D') (w : Window D D') : ∃ (𝒰 : FinCover ⊤) (g : C0 D' 𝒰) (_ : ((d0 D' 𝒰) g).MemLD D), Realizes 𝒰 g w ∧ 𝒰.IsAdapted (diffSupp D D')

Adapted-cover realization (§6.9(c)): every window vector is realized by a Mittag-Leffler 0-cochain on a cover adapted to diffSupp D D' — on the (unique) member through q, the restriction of a chart-source representative of w q, shrunk into a pole-free zone avoiding all other points of diffSupp D D' ∪ supp D ∪ supp D'; 0 elsewhere.

The connecting map windowConnect (§6.9(d))

noncomputable def RS.Cech.windowConnect {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {D D' : Divisor X} [T2Space X] [CompactSpace X] (h : D ≤ D') : Window D D' →ₗ[ℂ] H1 D

The connecting map δ of the six-term skyscraper fragment (§6.9(d)): realize the window vector on an adapted cover (exists_realization), take the Mittag-Leffler class (mlClass); well-defined by Lemma A (mlClass_eq_of_realizes), which also gives linearity.

Equations

• RS.Cech.windowConnect h = { toFun := RS.Cech.windowConnectRaw✝ h, map_add' := ⋯, map_smul' := ⋯ }

theorem RS.Cech.windowConnect_spec {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {D D' : Divisor X} [T2Space X] [CompactSpace X] (h : D ≤ D') (w : Window D D') {𝒰 : FinCover ⊤} {g : C0 D' 𝒰} (hg : ((d0 D' 𝒰) g).MemLD D) (hr : Realizes 𝒰 g w) : (windowConnect h) w = mlClass 𝒰 g hg

windowConnect agrees with the Mittag-Leffler class of any realization (the working form of the connecting map — this is what consumers should use).

theorem RS.Cech.H1Incl_windowConnect {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {D D' : Divisor X} [T2Space X] [CompactSpace X] (h : D ≤ D') (w : Window D D') : (H1Incl D h) ((windowConnect h) w) = 0

Exactness (§6.9(e)/(f))

theorem RS.Cech.exact_windowMap_windowConnect {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {D D' : Divisor X} [T2Space X] [CompactSpace X] (h : D ≤ D') : Function.Exact ⇑(windowMap h) ⇑(windowConnect h)

Exactness at Window D D' (§6.9(e)): windowConnect h w = 0 iff w is the window vector of a global section of L(D').

theorem RS.Cech.exact_windowConnect_H1Incl {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {D D' : Divisor X} [T2Space X] [CompactSpace X] (h : D ≤ D') : Function.Exact ⇑(windowConnect h) ⇑(H1Incl D h)

Exactness at H¹(D) (§6.9(f)): the kernel of H1Incl is exactly the image of the connecting map — toH1_injective (Forster 12.4) turns the vanishing into a D'-coboundary witness on the representing cover itself, and exists_tail_approx reads off its window vector.