19.20. Finiteness.CechRefinementLeray🔗

Jacobians.Finiteness.CechRefinementLeray — source

RefinementDescend

The Leray DESCEND condition (injectivity input). A 𝔘-cocycle whose refinement is a 𝔙-coboundary was already a 𝔘-coboundary (ker (refineH1 hr) = 0). This is Forster 12.8 (injectivity of the coarse→fine map on H¹); for 𝒪 with germ-class sections it is the H⁰ gluing of the splitting η, again an overlap-acyclicity consequence.

def RefinementDescend (hr : IsRefinement 𝔙 𝔘 r) (D : Divisor X) : Prop

refineH1_mk_eq_iff

refineH1 hr [g] = [t] (in H¹) ⟺ refineC1 g − t is a 𝔙-coboundary. The bridge between the quotient H¹-class equality and the cocycle-level "mod coboundary" statement (Submodule.Quotient.eq; membership in (coboundaries1).submoduleOf (cocycles1) is defeq to ↑· ∈ coboundaries1).

theorem refineH1_mk_eq_iff (hr : IsRefinement 𝔙 𝔘 r) (g : ↥(𝔘.cocycles1 D))
    (t : ↥(𝔙.cocycles1 D)) :
    hr.refineH1 D (Submodule.Quotient.mk g) = Submodule.Quotient.mk t ↔
      hr.refineC1 (g : 𝔘.Cochain1) - (t : 𝔙.Cochain1) ∈ 𝔙.coboundaries1 D

refineH1_injective_iff_descend

Injectivity of refineH1 ⟺ the Leray DESCEND condition.

theorem refineH1_injective_iff_descend (hr : IsRefinement 𝔙 𝔘 r) :
    Function.Injective (hr.refineH1 D) ↔ RefinementDescend hr D