H⁰(𝒰,D) ≃ L(D) (CC8, proof plan §6.1)

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

• toC0: restriction of a relative section to the cover, landing in ker d0.
• h0EquivLinSysOn: H⁰(𝒰,D) ≃ Γ(Ω, O_D) — CC8's "definitionally easy" H⁰ = L(D).
• h0Equiv: the global form H⁰(𝒰,D) ≃ L(D) for covers of X.

noncomputable def RS.Cech.toC0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : ↥(LinSysOn D ↑Ω) →ₗ[ℂ] C0 D 𝒰

Restriction of a relative section to the cover.

Equations

• RS.Cech.toC0 D 𝒰 = LinearMap.pi fun (i : Fin 𝒰.n) => RS.Cech.LinSysOn.restrictL D ⋯

theorem RS.Cech.toC0_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) (φ : ↥(LinSysOn D ↑Ω)) (i : Fin 𝒰.n) : (toC0 D 𝒰) φ i = (LinSysOn.restrictL D ⋯) φ

theorem RS.Cech.toC0_mem_ker {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) (φ : ↥(LinSysOn D ↑Ω)) : (toC0 D 𝒰) φ ∈ (d0 D 𝒰).ker

noncomputable def RS.Cech.toC0' {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : ↥(LinSysOn D ↑Ω) →ₗ[ℂ] ↥(d0 D 𝒰).ker

toC0, corestricted to land in ker d0.

Equations

• RS.Cech.toC0' D 𝒰 = LinearMap.codRestrict (RS.Cech.d0 D 𝒰).ker (RS.Cech.toC0 D 𝒰) ⋯

theorem RS.Cech.iUnion_U_eq {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : ⋃ (i : Fin 𝒰.n), ↑(𝒰.U i) = ↑Ω

The cover's members exhaust Ω (as sets).

theorem RS.Cech.toC0'_injective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : Function.Injective ⇑(toC0' D 𝒰)

theorem RS.Cech.toC0'_surjective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : Function.Surjective ⇑(toC0' D 𝒰)

theorem RS.Cech.toC0'_bijective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : Function.Bijective ⇑(toC0' D 𝒰)

noncomputable def RS.Cech.h0EquivLinSysOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : ↥(d0 D 𝒰).ker ≃ₗ[ℂ] ↥(LinSysOn D ↑Ω)

H⁰(𝒰,D) ≃ Γ(Ω,O_D) (CC8's "definitionally easy" H⁰ = L(D), relativized to Ω).

Equations

• RS.Cech.h0EquivLinSysOn D 𝒰 = (LinearEquiv.ofBijective (RS.Cech.toC0' D 𝒰) ⋯).symm

@[simp]

theorem RS.Cech.h0EquivLinSysOn_symm_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) (φ : ↥(LinSysOn D ↑Ω)) (i : Fin 𝒰.n) : ↑((h0EquivLinSysOn D 𝒰).symm φ) i = (LinSysOn.restrictL D ⋯) φ

theorem RS.Cech.h0EquivLinSysOn_symm_apply_ord {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) (φ : ↥(LinSysOn D ↑Ω)) (i : Fin 𝒰.n) {x : X} (hx : x ∈ 𝒰.U i) : (↑(↑((h0EquivLinSysOn D 𝒰).symm φ) i)).ord x = (↑φ).ord x

theorem RS.Cech.linSysOn_top_eq_linSys {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) : LinSysOn D ↑⊤ = LinSys D

The absolute LinSysOn D univ and LinSys D are the same submodule (Opens.coe_top is rfl, so only the IsOpen-gate needs unfolding).

noncomputable def RS.Cech.h0Equiv {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : Divisor X) (𝒰 : FinCover ⊤) : ↥(d0 D 𝒰).ker ≃ₗ[ℂ] ↥(LinSys D)

Global form: H⁰(𝒰,D) ≃ L(D) for covers of X.

Equations

• RS.Cech.h0Equiv D 𝒰 = RS.Cech.h0EquivLinSysOn D 𝒰 ≪≫ₗ LinearEquiv.ofEq (RS.LinSysOn D ↑⊤) (RS.LinSys D) ⋯