H¹(D) as a directed colimit (CC8, D1)

Unit: cech-cohomology (docs/design/cech-cohomology.md §4.5, §5).

• resH1': the transition map for h : 𝒰 ≤ 𝒱, via a chosen refinement index — independent of the choice by Forster 12.3 (resH1'_eq_resH1).
• DirectedSystem instance on fun 𝒰 => H1Cover D 𝒰, from resH1_id/resH1_comp (Refinement.lean).
• H1 D: the colimit (CC8, frozen). toH1, exists_rep(_good/_refined), H1.induction_on.
• H1.lift: the universal property (target for dolbeault-comparison's comparison map).
• H1Incl: D-monotone functoriality (H1 D →ₗ H1 D' for D ≤ D'), via Module.DirectLimit.map.

toH1_injective/toH1_eq_zero_iff/subsingleton_H1_iff (needing Forster 12.4, resH1_injective) are exported from Injectivity.lean instead, which imports this file; subsingleton_H1_of_good below (the direction actually needed downstream, via good-cover cofinality) does not need 12.4 and is proved here.

The transition maps and the DirectedSystem instance

noncomputable def RS.Cech.resH1' {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {𝒰 𝒱 : FinCover ⊤} (h : 𝒰 ≤ 𝒱) : H1Cover D 𝒰 →ₗ[ℂ] H1Cover D 𝒱

The transition map for 𝒰 ≤ 𝒱, via a chosen (classical) refinement index.

Equations

• RS.Cech.resH1' D h = RS.Cech.resH1 D (RS.Cech.chosenRefIdx h) ⋯

theorem RS.Cech.resH1'_eq_resH1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {𝒰 𝒱 : FinCover ⊤} (h : 𝒰 ≤ 𝒱) (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) : resH1' D h = resH1 D τ hτ

Forster 12.3: resH1' does not depend on the chosen witness.

instance RS.Cech.directedSystemH1Cover {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) : DirectedSystem (fun (𝒰 : FinCover ⊤) => H1Cover D 𝒰) fun (x x_1 : FinCover ⊤) (h : x ≤ x_1) => ⇑(resH1' D h)

H1 D, the colimit

@[reducible, inline]

noncomputable abbrev RS.Cech.H1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) : Type u_1

CC8 (frozen by design): the first Čech cohomology of O_D on X, as a directed colimit over finite covers of X under refinement. Reducible (abbrev) so that instance search and the Module.DirectLimit API (of, lift, map, exists_of, induction_on, …) apply transparently — the same reason C0/C1/C2/H1Cover are abbrev (Cochains.lean).

Equations

• RS.Cech.H1 D = Module.DirectLimit (fun (𝒰 : RS.Cech.FinCover ⊤) => RS.Cech.H1Cover D 𝒰) fun (x x_1 : RS.Cech.FinCover ⊤) (h : x ≤ x_1) => RS.Cech.resH1' D h

noncomputable def RS.Cech.toH1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) (𝒰 : FinCover ⊤) : H1Cover D 𝒰 →ₗ[ℂ] H1 D

The canonical map from a cover-level H¹ to the colimit.

Equations

• RS.Cech.toH1 D 𝒰 = Module.DirectLimit.of ℂ (RS.Cech.FinCover ⊤) (fun (𝒰 : RS.Cech.FinCover ⊤) => RS.Cech.H1Cover D 𝒰) (fun (x x_1 : RS.Cech.FinCover ⊤) (h : x ≤ x_1) => RS.Cech.resH1' D h) 𝒰

@[simp]

theorem RS.Cech.toH1_resH1' {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {𝒰 𝒱 : FinCover ⊤} (h : 𝒰 ≤ 𝒱) (ξ : H1Cover D 𝒰) : (toH1 D 𝒱) ((resH1' D h) ξ) = (toH1 D 𝒰) ξ

theorem RS.Cech.toH1_resH1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {𝒰 𝒱 : FinCover ⊤} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) (ξ : H1Cover D 𝒰) : (toH1 D 𝒱) ((resH1 D τ hτ) ξ) = (toH1 D 𝒰) ξ

theorem RS.Cech.exists_rep {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) (ξ : H1 D) : ∃ (𝒰 : FinCover ⊤) (c : H1Cover D 𝒰), (toH1 D 𝒰) c = ξ

theorem RS.Cech.exists_rep_good {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) [CompactSpace X] (ξ : H1 D) : ∃ (𝒰 : FinCover ⊤), 𝒰.IsGood ∧ ∃ (c : H1Cover D 𝒰), (toH1 D 𝒰) c = ξ

Refine the produced cover to a good one, pushing the class along (§5.3).

theorem RS.Cech.exists_rep_refined {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) (𝒰₀ : FinCover ⊤) (ξ : H1 D) : ∃ (𝒰 : FinCover ⊤) (_ : 𝒰₀ ≤ 𝒰) (c : H1Cover D 𝒰), (toH1 D 𝒰) c = ξ

theorem RS.Cech.H1.induction_on {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {C : H1 D → Prop} (ξ : H1 D) (ih : ∀ (𝒰 : FinCover ⊤) (c : H1Cover D 𝒰), C ((toH1 D 𝒰) c)) : C ξ

Subsingleton criteria not requiring 12.4

theorem RS.Cech.subsingleton_H1_of_all_subsingleton {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) (h : ∀ (𝒰 : FinCover ⊤), Subsingleton (H1Cover D 𝒰)) : Subsingleton (H1 D)

If every cover-level H¹ vanishes, so does the colimit (no injectivity needed: every class already has a cover-level representative, and the hypothesis kills every representative).

theorem RS.Cech.subsingleton_H1_of_good {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) [CompactSpace X] (h : ∀ (𝒰 : FinCover ⊤), 𝒰.IsGood → Subsingleton (H1Cover D 𝒰)) : Subsingleton (H1 D)

If every good cover-level H¹ vanishes, so does the colimit (good covers are cofinal).

The universal property

noncomputable def RS.Cech.H1.lift {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {P : Type u_2} [AddCommGroup P] [Module ℂ P] (g : (𝒰 : FinCover ⊤) → H1Cover D 𝒰 →ₗ[ℂ] P) (hg : ∀ (𝒰 𝒱 : FinCover ⊤) (h : 𝒰 ≤ 𝒱) (ξ : H1Cover D 𝒰), (g 𝒱) ((resH1' D h) ξ) = (g 𝒰) ξ) : H1 D →ₗ[ℂ] P

The universal property of H¹(D) (target for dolbeault-comparison's comparison map).

Equations

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

@[simp]

theorem RS.Cech.H1.lift_toH1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {P : Type u_2} [AddCommGroup P] [Module ℂ P] (g : (𝒰 : FinCover ⊤) → H1Cover D 𝒰 →ₗ[ℂ] P) (hg : ∀ (𝒰 𝒱 : FinCover ⊤) (h : 𝒰 ≤ 𝒱) (ξ : H1Cover D 𝒰), (g 𝒱) ((resH1' D h) ξ) = (g 𝒰) ξ) (𝒰 : FinCover ⊤) (ξ : H1Cover D 𝒰) : (lift D g hg) ((toH1 D 𝒰) ξ) = (g 𝒰) ξ

D-functoriality

theorem RS.Cech.linSysOn_mono {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {D D' : Divisor X} (h : D ≤ D') : LinSysOn D U ≤ LinSysOn D' U

Compat: requested from meromorphic-and-divisors (docs/requests/meromorphic-and-divisors.md item 1), not yet upstreamed — proved locally (one-line carrier implication).

theorem RS.Cech.inclusion_restrictL_comm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {D' : Divisor X} {V U : TopologicalSpace.Opens X} (h' : V ≤ U) (hD : D ≤ D') (φ : ↥(LinSysOn D ↑U)) : (Submodule.inclusion ⋯) ((LinSysOn.restrictL D h') φ) = (LinSysOn.restrictL D' h') ((Submodule.inclusion ⋯) φ)

noncomputable def RS.Cech.inclC1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {D' : Divisor X} {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) (h : D ≤ D') : C1 D 𝒰 →ₗ[ℂ] C1 D' 𝒰

D-inclusion of 1-cochains (Submodule.inclusion, componentwise).

Equations

• RS.Cech.inclC1 D 𝒰 h = LinearMap.pi fun (p : Fin 𝒰.n × Fin 𝒰.n) => Submodule.inclusion ⋯ ∘ₗ LinearMap.proj p

theorem RS.Cech.inclC1_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {D' : Divisor X} {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} (h : D ≤ D') (f : C1 D 𝒰) (p : Fin 𝒰.n × Fin 𝒰.n) : (inclC1 D 𝒰 h) f p = (Submodule.inclusion ⋯) (f p)

noncomputable def RS.Cech.inclC0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {D' : Divisor X} {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) (h : D ≤ D') : C0 D 𝒰 →ₗ[ℂ] C0 D' 𝒰

D-inclusion of 0-cochains.

Equations

• RS.Cech.inclC0 D 𝒰 h = LinearMap.pi fun (i : Fin 𝒰.n) => Submodule.inclusion ⋯ ∘ₗ LinearMap.proj i

theorem RS.Cech.inclC0_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {D' : Divisor X} {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} (h : D ≤ D') (f : C0 D 𝒰) (i : Fin 𝒰.n) : (inclC0 D 𝒰 h) f i = (Submodule.inclusion ⋯) (f i)

theorem RS.Cech.inclC1_mem_Z1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {D' : Divisor X} {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} (h : D ≤ D') {f : C1 D 𝒰} (hf : f ∈ Z1 D 𝒰) : (inclC1 D 𝒰 h) f ∈ Z1 D' 𝒰

noncomputable def RS.Cech.h1CoverIncl {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {D' : Divisor X} {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) (h : D ≤ D') : H1Cover D 𝒰 →ₗ[ℂ] H1Cover D' 𝒰

D-inclusion on cover-level H¹.

Equations

• RS.Cech.h1CoverIncl D 𝒰 h = (Submodule.comap (RS.Cech.Z1 D 𝒰).subtype (RS.Cech.B1 D 𝒰)).mapQ (Submodule.comap (RS.Cech.Z1 D' 𝒰).subtype (RS.Cech.B1 D' 𝒰)) ((RS.Cech.inclC1 D 𝒰 h).restrict ⋯) ⋯

theorem RS.Cech.h1CoverIncl_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {D' : Divisor X} {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} (h : D ≤ D') (f : ↥(Z1 D 𝒰)) : (h1CoverIncl D 𝒰 h) ((H1Cover.mk D 𝒰) f) = (H1Cover.mk D' 𝒰) (((inclC1 D 𝒰 h).restrict ⋯) f)

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

theorem RS.Cech.h1CoverIncl_resH1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {D' : Divisor X} {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (h : D ≤ D') (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) (ξ : H1Cover D 𝒰) : (h1CoverIncl D 𝒱 h) ((resH1 D τ hτ) ξ) = (resH1 D' τ hτ) ((h1CoverIncl D 𝒰 h) ξ)

noncomputable def RS.Cech.H1Incl {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {D' : Divisor X} (h : D ≤ D') : H1 D →ₗ[ℂ] H1 D'

D-monotone functoriality of H¹: H1Incl h : H1 D →ₗ H1 D' for D ≤ D'.

Equations

• RS.Cech.H1Incl D h = Module.DirectLimit.map (fun (𝒰 : RS.Cech.FinCover ⊤) => RS.Cech.h1CoverIncl D 𝒰 h) ⋯

@[simp]

theorem RS.Cech.H1Incl_toH1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {D' : Divisor X} (h : D ≤ D') (𝒰 : FinCover ⊤) (c : H1Cover D 𝒰) : (H1Incl D h) ((toH1 D 𝒰) c) = (toH1 D' 𝒰) ((h1CoverIncl D 𝒰 h) c)

theorem RS.Cech.H1Incl_id {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) : H1Incl D ⋯ = LinearMap.id

theorem RS.Cech.H1Incl_comp {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {D' D'' : Divisor X} (h : D ≤ D') (h' : D' ≤ D'') : H1Incl D' h' ∘ₗ H1Incl D h = H1Incl D ⋯

Leray interface (recorded; proof owned by dolbeault-comparison / dbar-solvability)

toH1_surjective_of_isGood [CompactSpace X] {𝒰 : FinCover (⊤ : Opens X)} (h𝒰 : 𝒰.IsGood) : Function.Surjective (toH1 D 𝒰)

together with toH1_injective (Injectivity.lean) this is Forster 12.8. Its input, disk acyclicity ∀ (V : Opens X), IsChartDisk V → ∀ 𝒱 : FinCover V, Subsingleton (H1Cover D 𝒱), is owned by dbar-solvability; the surjectivity statement itself is owned by dolbeault-comparison. Neither is proved in this unit (§7).