Documentation

LeanPool.JacobianDiffgeo.Cech.Injectivity

Forster 12.4: refinement maps are injective on H¹ (CC8, D8, proof plan §6.7) #

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

source
theorem RS.Cech.iUnion_inf_eq {X : Type u_1} [TopologicalSpace X] {Ω : TopologicalSpace.Opens X} {𝒱 : FinCover Ω} (A : TopologicalSpace.Opens X) (hA : A ≤ Ω) :
⋃ (k : Fin 𝒱.n), ↑(A ⊓ 𝒱.U k) = ↑A

Any member A ≤ Ω is exhausted by its intersections with the members of a cover 𝒱 of Ω (§6.7's covering fact, used both to glue injPatch over 𝒰.U i and to compare cochains over 𝒰.U i ⊓ 𝒰.U j).

source
noncomputable def RS.Cech.injPatch {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) (f : C1 D 𝒰) (g : C0 D 𝒱) (i : Fin 𝒰.n) (k : Fin 𝒱.n) :
↥(LinSysOn D ↑(𝒰.U i ⊓ 𝒱.U k))

The local candidate for the glued section on 𝒰.U i, restricted to 𝒰.U i ⊓ 𝒱.U k (Forster p. 99 / §6.7).

Equations
Instances For
    source
    theorem RS.Cech.injPatch_compat {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 𝒰) {g : C0 D 𝒱} (hgeq : (resC1 D τ hτ) f = (d0 D 𝒱) g) (i : Fin 𝒰.n) (k l : Fin 𝒱.n) :
    (MeroGermOn.restrict ⋯) ↑(injPatch D τ hτ f g i k) = (MeroGermOn.restrict ⋯) ↑(injPatch D τ hτ f g i l)
    source
    theorem RS.Cech.exists_injGlue {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) {f : C1 D 𝒰} (hf : f ∈ Z1 D 𝒰) {g : C0 D 𝒱} (hgeq : (resC1 D τ hτ) f = (d0 D 𝒱) g) (i : Fin 𝒰.n) :
    ∃ (ψ : ↥(LinSysOn D ↑(𝒰.U i))), ∀ (k : Fin 𝒱.n), (LinSysOn.restrictL D ⋯) ψ = injPatch D τ hτ f g i k

    Glue the local candidates injPatch D τ hτ f g i · (compatible by injPatch_compat) into a genuine section on the whole member 𝒰.U i (Forster p. 99 / §6.7, sheaf axioms only).

    source
    theorem RS.Cech.d0_injGlue_eq_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) {f : C1 D 𝒰} (hf : f ∈ Z1 D 𝒰) {g : C0 D 𝒱} (_hgeq : (resC1 D τ hτ) f = (d0 D 𝒱) g) (ψ : (i : Fin 𝒰.n) → ↥(LinSysOn D ↑(𝒰.U i))) (hψ : ∀ (i : Fin 𝒰.n) (k : Fin 𝒱.n), (LinSysOn.restrictL D ⋯) (ψ i) = injPatch D τ hτ f g i k) :
    (d0 D 𝒰) ψ = -f

    The glued cochain ψ is a coboundary witness for -f (a sign artifact of injPatch's convention, harmless — f = d0 D 𝒰 (-ψ)).

    source
    theorem RS.Cech.resH1_injective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : Divisor X) {Ω : TopologicalSpace.Opens X} {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) :
    Function.Injective ⇑(resH1 D τ hτ)

    Forster 12.4 / Miranda IX.3.11: refinement maps are injective on H¹ — a pure sheaf-axiom argument (MeroGermOn.exists_glue/glue_unique), no analysis.

    source
    theorem RS.Cech.toH1_injective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : Divisor X) (𝒰 : FinCover ⊤) :
    Function.Injective ⇑(toH1 D 𝒰)

    12.4 + exists_eq_of_of_eq: every cover-level H¹ embeds in the colimit H1 D.

    source
    @[simp]
    theorem RS.Cech.toH1_eq_zero_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : Divisor X) {𝒰 : FinCover ⊤} (c : H1Cover D 𝒰) :
    (toH1 D 𝒰) c = 0 ↔ c = 0
    source
    theorem RS.Cech.subsingleton_H1_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : Divisor X) :
    Subsingleton (H1 D) ↔ ∀ (𝒰 : FinCover ⊤), Subsingleton (H1Cover D 𝒰)

    The colimit H1 D vanishes iff every cover-level H¹(𝒰,D) vanishes.