Leray's theorem and the cocycle-trade lemma (Jacobian/DolbeaultComparison/Leray.lean)

Unit: dolbeault-comparison (docs/design/dolbeault-comparison.md §5). This is the FIRST file of the unit and the gate for finiteness-and-chi (§0.1 of the design): everything here uses only cech's cover/cochain/colimit machinery, mero's gluing sheaf axioms, and dbar's disk acyclicity (subsingleton_h1Cover_of_isChartDisk, general-D, added to Jacobian/Dbar/DiskAcyclic.lean under this unit's authorization) as black boxes — no Form01, no PoU, no dbar-solving.

• FinCover.induced 𝒱 V : FinCover V: the induced cover of a member V of ⊤'s cover 𝒱.
• exists_goodCover: good covers exist (3-line corollary of cech's exists_good_refinement).
• exists_trade (Forster 14.6(a), qualitative): cocycles on any refinement of a good cover are, up to coboundary, restrictions of cocycles on the good cover — the Schwartz surjectivity input for finiteness-and-chi.
• resH1_surjective_of_isGood / toH1_surjective_of_isGood (Leray 12.8 surjectivity; injectivity is cech's toH1_injective, ALREADY on disk) / h1CoverEquiv.

A reusable lattice fact

theorem RS.Cech.inf_inf_inf_le {X : Type u_1} [TopologicalSpace X] (a b c : TopologicalSpace.Opens X) : a ⊓ b ⊓ (a ⊓ c) ≤ b ⊓ c

The induced cover of a member

def RS.Cech.FinCover.induced {X : Type u_1} [TopologicalSpace X] (𝒱 : FinCover ⊤) (V : TopologicalSpace.Opens X) : FinCover V

The induced cover of a member: (V ⊓ 𝒱.U α)_α : FinCover V for V ≤ ⊤.

Equations

• 𝒱.induced V = { n := 𝒱.n, U := fun (α : Fin 𝒱.n) => V ⊓ 𝒱.U α, le_base := ⋯, covers := ⋯ }

@[simp]

theorem RS.Cech.FinCover.induced_n {X : Type u_1} [TopologicalSpace X] (𝒱 : FinCover ⊤) (V : TopologicalSpace.Opens X) : (𝒱.induced V).n = 𝒱.n

@[simp]

theorem RS.Cech.FinCover.induced_U {X : Type u_1} [TopologicalSpace X] (𝒱 : FinCover ⊤) (V : TopologicalSpace.Opens X) (α : Fin 𝒱.n) : (𝒱.induced V).U α = V ⊓ 𝒱.U α

theorem RS.Cech.exists_goodCover {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [CompactSpace X] : ∃ (𝒰 : FinCover ⊤), 𝒰.IsGood

Good covers exist (§6.3 of cech-cohomology, applied to the trivial cover).

§5 step 1: the induced cocycle

noncomputable def RS.Cech.indCocycle {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) (i : Fin 𝒰.n) (f : C1 D 𝒱) : C1 D (𝒱.induced (𝒰.U i))

The induced cocycle on 𝒱.induced (𝒰.U i) (§5 step 1): componentwise restriction of f along the "drop the 𝒰.U i factor" lattice map.

Equations

• RS.Cech.indCocycle D i f p = (RS.Cech.LinSysOn.restrictL D ⋯) (f p)

theorem RS.Cech.indCocycle_mem_Z1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) (i : Fin 𝒰.n) {f : C1 D 𝒱} (hf : f ∈ Z1 D 𝒱) : indCocycle D i f ∈ Z1 D (𝒱.induced (𝒰.U i))

§5 step 2: member splitting via disk acyclicity

theorem RS.Cech.exists_splitting {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) [T2Space X] [CompactSpace X] (h𝒰 : 𝒰.IsGood) {f : C1 D 𝒱} (hf : f ∈ Z1 D 𝒱) : ∃ (gFam : (i : Fin 𝒰.n) → C0 D (𝒱.induced (𝒰.U i))), ∀ (i : Fin 𝒰.n), (d0 D (𝒱.induced (𝒰.U i))) (gFam i) = indCocycle D i f

Step 2: each induced cocycle splits, since 𝒰.U i is a chart disk (disk acyclicity).

theorem RS.Cech.splitting_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) {f : C1 D 𝒱} {gFam : (i : Fin 𝒰.n) → C0 D (𝒱.induced (𝒰.U i))} (hgFam : ∀ (i : Fin 𝒰.n), (d0 D (𝒱.induced (𝒰.U i))) (gFam i) = indCocycle D i f) (i : Fin 𝒰.n) (α β : Fin 𝒱.n) : (LinSysOn.restrictL D ⋯) (gFam i β) - (LinSysOn.restrictL D ⋯) (gFam i α) = indCocycle D i f (α, β)

The pointwise splitting identity extracted from exists_splitting, at LinSysOn (submodule) level (used both for the cross-glue compatibility and for the final comparison, §5 steps 3/5).

theorem RS.Cech.splitting_eq' {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) {f : C1 D 𝒱} {gFam : (i : Fin 𝒰.n) → C0 D (𝒱.induced (𝒰.U i))} (hgFam : ∀ (i : Fin 𝒰.n), (d0 D (𝒱.induced (𝒰.U i))) (gFam i) = indCocycle D i f) (i : Fin 𝒰.n) (α β : Fin 𝒱.n) : (MeroGermOn.restrict ⋯) ↑(gFam i β) - (MeroGermOn.restrict ⋯) ↑(gFam i α) = (MeroGermOn.restrict ⋯) ↑(f (α, β))

Raw MeroGermOn-level form of splitting_eq.

theorem RS.Cech.splitting_eq_restrict {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) {f : C1 D 𝒱} {gFam : (i : Fin 𝒰.n) → C0 D (𝒱.induced (𝒰.U i))} (hgFam : ∀ (i : Fin 𝒰.n), (d0 D (𝒱.induced (𝒰.U i))) (gFam i) = indCocycle D i f) (i : Fin 𝒰.n) (α β : Fin 𝒱.n) {W : TopologicalSpace.Opens X} (hWα : W ≤ (𝒱.induced (𝒰.U i)).U α) (hWβ : W ≤ (𝒱.induced (𝒰.U i)).U β) (hWαβ : W ≤ 𝒱.U α ⊓ 𝒱.U β) : (MeroGermOn.restrict hWβ) ↑(gFam i β) - (MeroGermOn.restrict hWα) ↑(gFam i α) = (MeroGermOn.restrict hWαβ) ↑(f (α, β))

splitting_eq', restricted down to an arbitrary smaller open W (§5 step 3's workhorse: lets us compare the splittings at TWO different good-cover members i, j on their common overlap with a member of 𝒱).

§5 step 3: cross-glue

noncomputable def RS.Cech.patch {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) (gFam : (i : Fin 𝒰.n) → C0 D (𝒱.induced (𝒰.U i))) (i j : Fin 𝒰.n) (α : Fin 𝒱.n) : ↥(LinSysOn D (↑(𝒰.U i) ⊓ ↑(𝒰.U j) ⊓ ↑(𝒱.U α)))

The local candidate for the glued section on 𝒰.U i ⊓ 𝒰.U j (§5 step 3).

Equations

• RS.Cech.patch D gFam i j α = (RS.Cech.LinSysOn.restrictL D ⋯) (gFam j α) - (RS.Cech.LinSysOn.restrictL D ⋯) (gFam i α)

theorem RS.Cech.patch_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) (gFam : (i : Fin 𝒰.n) → C0 D (𝒱.induced (𝒰.U i))) (i j : Fin 𝒰.n) (α : Fin 𝒱.n) : ↑(patch D gFam i j α) = (MeroGermOn.restrict ⋯) ↑(gFam j α) - (MeroGermOn.restrict ⋯) ↑(gFam i α)

theorem RS.Cech.patch_compat {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) {f : C1 D 𝒱} {gFam : (i : Fin 𝒰.n) → C0 D (𝒱.induced (𝒰.U i))} (hgFam : ∀ (i : Fin 𝒰.n), (d0 D (𝒱.induced (𝒰.U i))) (gFam i) = indCocycle D i f) (i j : Fin 𝒰.n) (α β : Fin 𝒱.n) : (MeroGermOn.restrict ⋯) ↑(patch D gFam i j α) = (MeroGermOn.restrict ⋯) ↑(patch D gFam i j β)

Compatibility of the patches on overlaps (§5 step 3).

theorem RS.Cech.exists_crossGlue {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) {f : C1 D 𝒱} (_hf : f ∈ Z1 D 𝒱) {gFam : (i : Fin 𝒰.n) → C0 D (𝒱.induced (𝒰.U i))} (hgFam : ∀ (i : Fin 𝒰.n), (d0 D (𝒱.induced (𝒰.U i))) (gFam i) = indCocycle D i f) (i j : Fin 𝒰.n) : ∃ (Φ : MeroGermOn X (↑(𝒰.U i) ⊓ ↑(𝒰.U j))), ∀ (α : Fin 𝒱.n), (MeroGermOn.restrict ⋯) Φ = ↑(patch D gFam i j α)

The glued section F_{ij} on 𝒰.U i ⊓ 𝒰.U j, restricting back to patch on each Uᵢ⊓Uⱼ⊓Vα (§5 step 3).

theorem RS.Cech.exists_crossGlueLinSysOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) {f : C1 D 𝒱} (hf : f ∈ Z1 D 𝒱) {gFam : (i : Fin 𝒰.n) → C0 D (𝒱.induced (𝒰.U i))} (hgFam : ∀ (i : Fin 𝒰.n), (d0 D (𝒱.induced (𝒰.U i))) (gFam i) = indCocycle D i f) (i j : Fin 𝒰.n) : ∃ (Φ : ↥(LinSysOn D (↑(𝒰.U i) ⊓ ↑(𝒰.U j)))), ∀ (α : Fin 𝒱.n), (LinSysOn.restrictL D ⋯) Φ = patch D gFam i j α

The glued section, packaged as a LinSysOn element (§5 step 3, LinSysOn-level): the crossGlue witness restricts back to patch on each Uᵢ⊓Uⱼ⊓Vα.

theorem RS.Cech.patch_restrict {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) (gFam : (i : Fin 𝒰.n) → C0 D (𝒱.induced (𝒰.U i))) (i j : Fin 𝒰.n) (α : Fin 𝒱.n) {W : TopologicalSpace.Opens X} (hWj : W ≤ (𝒱.induced (𝒰.U j)).U α) (hWi : W ≤ (𝒱.induced (𝒰.U i)).U α) (hWij : W ≤ 𝒰.U i ⊓ 𝒰.U j ⊓ 𝒱.U α) : (MeroGermOn.restrict hWij) ↑(patch D gFam i j α) = (MeroGermOn.restrict hWj) ↑(gFam j α) - (MeroGermOn.restrict hWi) ↑(gFam i α)

patch, restricted further down to an arbitrary open W (LinSysOn-level unfolding of patch_coe, reused for both step 4's triple relation and step 5's final comparison).

theorem RS.Cech.exists_crossGlueFam {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) {f : C1 D 𝒱} (hf : f ∈ Z1 D 𝒱) {gFam : (i : Fin 𝒰.n) → C0 D (𝒱.induced (𝒰.U i))} (hgFam : ∀ (i : Fin 𝒰.n), (d0 D (𝒱.induced (𝒰.U i))) (gFam i) = indCocycle D i f) : ∃ (F : C1 D 𝒰), ∀ (i j : Fin 𝒰.n) (α : Fin 𝒱.n), (LinSysOn.restrictL D ⋯) (F (i, j)) = patch D gFam i j α

The glued sections F_{ij}, packaged as a full 1-cochain on 𝒰 (§5 step 3, LinSysOn level): a choice of crossGlue-witness for every pair.

§5 step 4: F ∈ Z1 D 𝒰

theorem RS.Cech.crossGlueFam_mem_Z1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) {F : C1 D 𝒰} {gFam : (i : Fin 𝒰.n) → C0 D (𝒱.induced (𝒰.U i))} (hF : ∀ (i j : Fin 𝒰.n) (α : Fin 𝒱.n), (LinSysOn.restrictL D ⋯) (F (i, j)) = patch D gFam i j α) : F ∈ Z1 D 𝒰

Step 4: the glued family is a genuine cocycle on 𝒰 (the triple relation telescopes term-by-term from the patch definition — pure algebra, no further analytic input).

§5 step 5: the comparison on 𝒱

noncomputable def RS.Cech.tradeH0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) (gFam : (i : Fin 𝒰.n) → C0 D (𝒱.induced (𝒰.U i))) : C0 D 𝒱

The 0-cochain h of §5 step 5: h_α := restrict g^{τα}_α.

Equations

• RS.Cech.tradeH0 D τ hτ gFam α = (RS.Cech.LinSysOn.restrictL D ⋯) (gFam (τ α) α)

theorem RS.Cech.resC1_crossGlueFam_add_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) {f : C1 D 𝒱} (_hf : f ∈ Z1 D 𝒱) {gFam : (i : Fin 𝒰.n) → C0 D (𝒱.induced (𝒰.U i))} (hgFam : ∀ (i : Fin 𝒰.n), (d0 D (𝒱.induced (𝒰.U i))) (gFam i) = indCocycle D i f) {F : C1 D 𝒰} (hF : ∀ (i j : Fin 𝒰.n) (α : Fin 𝒱.n), (LinSysOn.restrictL D ⋯) (F (i, j)) = patch D gFam i j α) : (resC1 D τ hτ) F + f = (d0 D 𝒱) (tradeH0 D τ hτ gFam)

Step 5's frozen conclusion: resC1 F + f = d0 h.

§5 steps 6-7: exists_trade, Leray's theorem, h1CoverEquiv

theorem RS.Cech.exists_trade {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) [T2Space X] [CompactSpace X] (h𝒰 : 𝒰.IsGood) (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) (f : ↥(Z1 D 𝒱)) : ∃ (F : ↥(Z1 D 𝒰)) (g : C0 D 𝒱), ↑((resZ1 D τ hτ) F) = ↑f + (d0 D 𝒱) g

Forster 14.6(a), qualitative (all D): cocycles on any refinement of a good cover are, up to coboundary, restrictions of cocycles on the good cover. THE Schwartz surjectivity input for finiteness-and-chi.

theorem RS.Cech.resH1_surjective_of_isGood {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 𝒱 : FinCover ⊤} (D : Divisor X) [T2Space X] [CompactSpace X] (h𝒰 : 𝒰.IsGood) (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) : Function.Surjective ⇑(resH1 D τ hτ)

Forster 14.6(a) at H1Cover-level: the qualitative trade.

theorem RS.Cech.toH1_surjective_of_isGood {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 : FinCover ⊤} (D : Divisor X) [T2Space X] [CompactSpace X] (h𝒰 : 𝒰.IsGood) : Function.Surjective ⇑(toH1 D 𝒰)

LERAY (Forster 12.8 surjectivity half; injectivity is cech's toH1_injective, already on disk). Discharges the interface recorded in cech's Colimit.lean.

noncomputable def RS.Cech.h1CoverEquiv {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 : FinCover ⊤} (D : Divisor X) [T2Space X] [CompactSpace X] (h𝒰 : 𝒰.IsGood) : H1Cover D 𝒰 ≃ₗ[ℂ] H1 D

Cover-level H¹ computes the colimit on good covers — finiteness transfers dimensions through this.

Equations

• RS.Cech.h1CoverEquiv D h𝒰 = LinearEquiv.ofBijective (RS.Cech.toH1 D 𝒰) ⋯

@[simp]

theorem RS.Cech.h1CoverEquiv_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 : FinCover ⊤} (D : Divisor X) [T2Space X] [CompactSpace X] (h𝒰 : 𝒰.IsGood) (c : H1Cover D 𝒰) : (h1CoverEquiv D h𝒰) c = (toH1 D 𝒰) c