Refinement maps, 12.3 independence (CC8)

Unit: cech-cohomology (docs/design/cech-cohomology.md §4.4, proof plans §6.4–§6.7).

• resC0/resC1: restriction of cochains along a chosen refinement index τ.
• Z1.rel_res: the cocycle-relation workhorse (§6.5) — any cocycle triple relation, restricted down to any smaller open.
• resZ1/resH1: the induced maps on cocycles / cover-level H¹.
• resH1_indep (Forster 12.3): the induced H¹-map does not depend on the chosen refinement index — the DirectedSystem key for Colimit.lean.

Forster 12.4 (resH1_injective/toH1_injective) has landed — see Injectivity.lean (sheaf-axiom gluing argument via injPatch/exists_injGlue, no analysis).

Restriction along a refinement index

noncomputable def RS.Cech.resC0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) : C0 D 𝒰 →ₗ[ℂ] C0 D 𝒱

Restriction of 0-cochains along a refinement index τ.

Equations

• RS.Cech.resC0 D τ hτ = LinearMap.pi fun (k : Fin 𝒱.n) => RS.Cech.LinSysOn.restrictL D ⋯ ∘ₗ LinearMap.proj (τ k)

theorem RS.Cech.resC0_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) (f : C0 D 𝒰) (k : Fin 𝒱.n) : (resC0 D τ hτ) f k = (LinSysOn.restrictL D ⋯) (f (τ k))

noncomputable def RS.Cech.resC1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) : C1 D 𝒰 →ₗ[ℂ] C1 D 𝒱

Restriction of 1-cochains along a refinement index τ.

Equations

• RS.Cech.resC1 D τ hτ = LinearMap.pi fun (p : Fin 𝒱.n × Fin 𝒱.n) => RS.Cech.LinSysOn.restrictL D ⋯ ∘ₗ LinearMap.proj (τ p.1, τ p.2)

theorem RS.Cech.resC1_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) (f : C1 D 𝒰) (p : Fin 𝒱.n × Fin 𝒱.n) : (resC1 D τ hτ) f p = (LinSysOn.restrictL D ⋯) (f (τ p.1, τ p.2))

theorem RS.Cech.resC1_comp_d0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) : resC1 D τ hτ ∘ₗ d0 D 𝒰 = d0 D 𝒱 ∘ₗ resC0 D τ hτ

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

The cocycle-relation workhorse (§6.5)

theorem RS.Cech.Z1.rel_res {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} {f : C1 D 𝒰} (hf : f ∈ Z1 D 𝒰) (a b c : Fin 𝒰.n) {W : TopologicalSpace.Opens X} (h : W ≤ 𝒰.U a ⊓ 𝒰.U b ⊓ 𝒰.U c) (hbc : W ≤ 𝒰.U b ⊓ 𝒰.U c) (hac : W ≤ 𝒰.U a ⊓ 𝒰.U c) (hab : W ≤ 𝒰.U a ⊓ 𝒰.U b) : (LinSysOn.restrictL D hbc) (f (b, c)) - (LinSysOn.restrictL D hac) (f (a, c)) + (LinSysOn.restrictL D hab) (f (a, b)) = 0

Forster p. 97 / the workhorse: any cocycle-relation triple, restricted to any smaller open W (via arbitrary — by proof irrelevance, any — witnessing inequalities).

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

resZ1, resH1

noncomputable def RS.Cech.resZ1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) : ↥(Z1 D 𝒰) →ₗ[ℂ] ↥(Z1 D 𝒱)

The induced map on 1-cocycles.

Equations

• RS.Cech.resZ1 D τ hτ = (RS.Cech.resC1 D τ hτ).restrict ⋯

theorem RS.Cech.resZ1_apply_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) (f : ↥(Z1 D 𝒰)) : ↑((resZ1 D τ hτ) f) = (resC1 D τ hτ) ↑f

noncomputable def RS.Cech.resH1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) : H1Cover D 𝒰 →ₗ[ℂ] H1Cover D 𝒱

The induced map on cover-level H¹.

Equations

• RS.Cech.resH1 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.resZ1 D τ hτ) ⋯

@[simp]

theorem RS.Cech.resH1_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) (f : ↥(Z1 D 𝒰)) : (resH1 D τ hτ) ((H1Cover.mk D 𝒰) f) = (H1Cover.mk D 𝒱) ((resZ1 D τ hτ) f)

Refinement independence (Forster 12.3)

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

Functor laws: identity and composition

theorem RS.Cech.resC0_id {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} (h : IsRefIdx 𝒰 𝒰 id) : resC0 D id h = LinearMap.id

theorem RS.Cech.resC1_id {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} (h : IsRefIdx 𝒰 𝒰 id) : resC1 D id h = LinearMap.id

theorem RS.Cech.resZ1_id {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} (h : IsRefIdx 𝒰 𝒰 id) : resZ1 D id h = LinearMap.id

theorem RS.Cech.resH1_id {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 : FinCover Ω} (h : IsRefIdx 𝒰 𝒰 id) : resH1 D id h = LinearMap.id

theorem RS.Cech.resC0_comp {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) {𝒲 : FinCover Ω} (σ : Fin 𝒲.n → Fin 𝒱.n) (hσ : IsRefIdx 𝒱 𝒲 σ) : resC0 D σ hσ ∘ₗ resC0 D τ hτ = resC0 D (τ ∘ σ) ⋯

theorem RS.Cech.resC1_comp {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) {𝒲 : FinCover Ω} (σ : Fin 𝒲.n → Fin 𝒱.n) (hσ : IsRefIdx 𝒱 𝒲 σ) : resC1 D σ hσ ∘ₗ resC1 D τ hτ = resC1 D (τ ∘ σ) ⋯

theorem RS.Cech.resZ1_comp {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) {𝒲 : FinCover Ω} (σ : Fin 𝒲.n → Fin 𝒱.n) (hσ : IsRefIdx 𝒱 𝒲 σ) (f : ↥(Z1 D 𝒰)) : (resZ1 D σ hσ) ((resZ1 D τ hτ) f) = (resZ1 D (τ ∘ σ) ⋯) f

theorem RS.Cech.resH1_comp {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) {𝒲 : FinCover Ω} (σ : Fin 𝒲.n → Fin 𝒱.n) (hσ : IsRefIdx 𝒱 𝒲 σ) : resH1 D σ hσ ∘ₗ resH1 D τ hτ = resH1 D (τ ∘ σ) ⋯