Čech cochains, coboundary maps, Z¹/B¹/H¹(𝒰,D) (CC8, D5/D6)

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

• LinSysOn.restrictL: restriction of relative linear systems as a ℂ-linear map (wrapper on mero's restrict AlgHom), with the presheaf laws restrictL_restrictL/restrictL_id and ord-rigidity ord_restrictL.
• MeroGermOn.congrSet [Compat, D6]: transport along a propositional set equality.
• C0/C1/C2 (full-product cochains, D5), d0/d1 (coboundary), d1_comp_d0.
• Z1/B1/H1Cover — the cover-level Čech H¹(𝒰,D).

LinSysOn.restrictL

noncomputable def RS.Cech.LinSysOn.restrictL {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {V U : TopologicalSpace.Opens X} (D : Divisor X) (h : V ≤ U) : ↥(LinSysOn D ↑U) →ₗ[ℂ] ↥(LinSysOn D ↑V)

Restriction as a ℂ-linear map of relative linear systems (wrapper on mero's restrict).

Equations

• RS.Cech.LinSysOn.restrictL D h = (RS.MeroGermOn.restrict h).toLinearMap.restrict ⋯

@[simp]

theorem RS.Cech.restrictL_apply_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {V U : TopologicalSpace.Opens X} (D : Divisor X) (h : V ≤ U) (φ : ↥(LinSysOn D ↑U)) : ↑((LinSysOn.restrictL D h) φ) = (MeroGermOn.restrict h) ↑φ

theorem RS.Cech.restrictL_restrictL {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {W V U : TopologicalSpace.Opens X} (D : Divisor X) (h1 : V ≤ U) (h2 : W ≤ V) (h3 : W ≤ U) (φ : ↥(LinSysOn D ↑U)) : (LinSysOn.restrictL D h2) ((LinSysOn.restrictL D h1) φ) = (LinSysOn.restrictL D h3) φ

@[simp]

theorem RS.Cech.restrictL_id {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : TopologicalSpace.Opens X} (D : Divisor X) (φ : ↥(LinSysOn D ↑U)) : (LinSysOn.restrictL D ⋯) φ = φ

theorem RS.Cech.ord_restrictL {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {V U : TopologicalSpace.Opens X} (D : Divisor X) (h : V ≤ U) {x : X} (hx : x ∈ V) (φ : ↥(LinSysOn D ↑U)) : (↑((LinSysOn.restrictL D h) φ)).ord x = (↑φ).ord x

MeroGermOn.congrSet (Compat, D6)

noncomputable def RS.Cech.MeroGermOn.congrSet {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U V : Set X} (h : U = V) : MeroGermOn X U ≃ₗ[ℂ] MeroGermOn X V

Transport along a propositional set equality (D6): built from restrict both ways using the presheaf laws. Used to move gluing targets ⋃ i, ↑(U i) against ↑Ω.

Equations

• RS.Cech.MeroGermOn.congrSet h = LinearEquiv.ofLinearMap (RS.MeroGermOn.restrict ⋯).toLinearMap (RS.MeroGermOn.restrict ⋯).toLinearMap ⋯ ⋯

Cochains C0/C1/C2 (D5: full-product convention)

@[reducible, inline]

abbrev RS.Cech.C0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : Type u_1

0-cochains. Reducible (abbrev): lets instance search and ext/funext see straight through to the underlying Pi type, which is what actually carries the AddCommGroup/Module structure — avoids diamond/opacity friction in d0_apply/d1_apply/Z1/H1Cover.

Equations

• RS.Cech.C0 D 𝒰 = ((i : Fin 𝒰.n) → ↥(RS.LinSysOn D ↑(𝒰.U i)))

@[reducible, inline]

abbrev RS.Cech.C1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : Type u_1

1-cochains (full product over ordered pairs, D5 — no i < j convention).

Equations

• RS.Cech.C1 D 𝒰 = ((p : Fin 𝒰.n × Fin 𝒰.n) → ↥(RS.LinSysOn D ↑(𝒰.U p.1 ⊓ 𝒰.U p.2)))

@[reducible, inline]

abbrev RS.Cech.C2 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : Type u_1

2-cochains (kept internal; only used to define Z1 via ker d1).

Equations

• RS.Cech.C2 D 𝒰 = ((t : Fin 𝒰.n × Fin 𝒰.n × Fin 𝒰.n) → ↥(RS.LinSysOn D ↑(𝒰.U t.1 ⊓ 𝒰.U t.2.1 ⊓ 𝒰.U t.2.2)))

The coboundary maps

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

(δ⁰f)_{ij} = f_j − f_i (after restriction to U i ⊓ U j).

Equations

• RS.Cech.d0 D 𝒰 = LinearMap.pi fun (p : Fin 𝒰.n × Fin 𝒰.n) => RS.Cech.LinSysOn.restrictL D ⋯ ∘ₗ LinearMap.proj p.2 - RS.Cech.LinSysOn.restrictL D ⋯ ∘ₗ LinearMap.proj p.1

@[simp]

theorem RS.Cech.d0_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) (f : C0 D 𝒰) (p : Fin 𝒰.n × Fin 𝒰.n) : (d0 D 𝒰) f p = (LinSysOn.restrictL D ⋯) (f p.2) - (LinSysOn.restrictL D ⋯) (f p.1)

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

(δ¹f)_{ijk} = f_{jk} − f_{ik} + f_{ij} (after restriction to U i ⊓ U j ⊓ U k).

Equations

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

@[simp]

theorem RS.Cech.d1_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) (f : C1 D 𝒰) (t : Fin 𝒰.n × Fin 𝒰.n × Fin 𝒰.n) : (d1 D 𝒰) f t = (LinSysOn.restrictL D ⋯) (f (t.2.1, t.2.2)) - (LinSysOn.restrictL D ⋯) (f (t.1, t.2.2)) + (LinSysOn.restrictL D ⋯) (f (t.1, t.2.1))

theorem RS.Cech.d1_comp_d0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : d1 D 𝒰 ∘ₗ d0 D 𝒰 = 0

Z1, B1, H1Cover

noncomputable def RS.Cech.Z1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : Submodule ℂ (C1 D 𝒰)

1-cocycles.

Equations

• RS.Cech.Z1 D 𝒰 = (RS.Cech.d1 D 𝒰).ker

noncomputable def RS.Cech.B1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : Submodule ℂ (C1 D 𝒰)

1-coboundaries.

Equations

• RS.Cech.B1 D 𝒰 = (RS.Cech.d0 D 𝒰).range

@[instance_reducible]

noncomputable instance RS.Cech.instAddCommGroupZ1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : AddCommGroup ↥(Z1 D 𝒰)

Registered explicitly (rather than left to ad-hoc re-derivation at H1Cover's ⧸): the newer toolchain's synthInstance no longer reliably re-discharges the dependent Pi-instance goal ∀ i, AddCommGroup ↥(RS.LinSysOn D _) that Submodule.addCommGroup/Submodule.instModule would otherwise have to solve afresh (as a precondition on the ambient C1 D 𝒰) at every downstream use of Z1 D 𝒰 ⧸ _. Supplying the resolved instance for ↥(Z1 D 𝒰) once, directly, lets every later lookup match it verbatim instead of re-deriving it.

Equations

• RS.Cech.instAddCommGroupZ1 D 𝒰 = (RS.Cech.Z1 D 𝒰).addCommGroup

@[instance_reducible]

noncomputable instance RS.Cech.instModuleZ1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : Module ℂ ↥(Z1 D 𝒰)

Equations

• RS.Cech.instModuleZ1 D 𝒰 = (RS.Cech.Z1 D 𝒰).module

theorem RS.Cech.B1_le_Z1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : B1 D 𝒰 ≤ Z1 D 𝒰

theorem RS.Cech.mem_Z1_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) (f : C1 D 𝒰) : f ∈ Z1 D 𝒰 ↔ ∀ (t : Fin 𝒰.n × Fin 𝒰.n × Fin 𝒰.n), (d1 D 𝒰) f t = 0

@[reducible, inline]

noncomputable abbrev RS.Cech.H1Cover {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : Type u_1

The Čech H¹(𝒰,D) at cover level. Reducible (abbrev) for the same reason as C0/C1/C2.

Equations

• RS.Cech.H1Cover D 𝒰 = (↥(RS.Cech.Z1 D 𝒰) ⧸ Submodule.comap (RS.Cech.Z1 D 𝒰).subtype (RS.Cech.B1 D 𝒰))

noncomputable def RS.Cech.H1Cover.mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : ↥(Z1 D 𝒰) →ₗ[ℂ] H1Cover D 𝒰

The quotient map onto H¹(𝒰,D).

Equations

• RS.Cech.H1Cover.mk D 𝒰 = (Submodule.comap (RS.Cech.Z1 D 𝒰).subtype (RS.Cech.B1 D 𝒰)).mkQ

theorem RS.Cech.H1Cover.mk_surjective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : Function.Surjective ⇑(mk D 𝒰)

theorem RS.Cech.H1Cover.mk_eq_zero_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) (f : ↥(Z1 D 𝒰)) : (mk D 𝒰) f = 0 ↔ ↑f ∈ B1 D 𝒰

theorem RS.Cech.subsingleton_h1Cover_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) : Subsingleton (H1Cover D 𝒰) ↔ Z1 D 𝒰 ≤ B1 D 𝒰

Diagonal vanishing (used by the skyscraper fragment §6.9(g))

theorem RS.Cech.Z1.ord_diag {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} (𝒰 : FinCover Ω) {f : C1 D 𝒰} (hf : f ∈ Z1 D 𝒰) (i : Fin 𝒰.n) {x : X} (hx : x ∈ 𝒰.U i ⊓ 𝒰.U i) : (↑(f (i, i))).ord x = ⊤