NYLL
Module

OModulePresheaf_Leray_nonempty_E2I_equiv.lean

Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_Leray_nonempty_E2I_equiv
12 declarations indexed from sourceView source ↗

Module documentation

Identification of the first Leray spectral-sequence page with Cech cohomology of relative cohomology.

Imports2
Imported by2

Declarations

def

ker_dV_equiv

L51 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv.AlgebraicGeometry.OModulePresheaf.Leray.ker_dV_equiv
Documentation

The equivalence between vertical bicomplex cocycles and the family of relative cocycles.

Source context 21 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "D" => LerayDblCpx p πZ K K'
Lean source · full declaration
def ker_dV_equiv (a b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    LinearMap.ker ((D).dV a b) ≃ₗ[R] ∀ σ : K.Idx a, LinearMap.ker (relAltd p πZ K' (K.inter σ) b) :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  { toFun := fun x σ => ⟨biC_uncurry p πZ K K' a b x.1 σ, by
      rw [LinearMap.mem_ker, ← dV_uncurry p πZ K K' a b x.1 σ]
      have hx : (D).dV a b x.1 = 0 := LinearMap.mem_ker.mp x.2
      exact congrFun (congrArg (biC_uncurry p πZ K K' a (b + 1)) hx) σ ▸
        congrFun (map_zero (biC_uncurry p πZ K K' a (b + 1))) σ⟩
    invFun := fun y => ⟨(biC_uncurry p πZ K K' a b).symm (fun σ => (y σ).1), by
      refine LinearMap.mem_ker.mpr ((biC_uncurry p πZ K K' a (b + 1)).injective (funext fun σ =>
        ?_))
      have h := dV_uncurry p πZ K K' a b ((biC_uncurry p πZ K K' a b).symm (fun σ' => (y σ').1)) σ
      rw [(biC_uncurry p πZ K K' a b).apply_symm_apply] at h
      exact (h.trans (LinearMap.mem_ker.mp (y σ).2)).trans
        (congrFun (map_zero (biC_uncurry p πZ K K' a (b + 1))) σ).symm⟩
    map_add' := fun x y => by funext σ; rfl
    map_smul' := fun r x => by funext σ; rfl
    left_inv := fun x => Subtype.ext ((biC_uncurry p πZ K K' a b).symm_apply_apply x.1)
    right_inv := fun y => funext fun σ => Subtype.ext (congrFun ((biC_uncurry p πZ K K' a
      b).apply_symm_apply _) σ) }
theorem

ker_dV_equiv_apply_coe

L73 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv.AlgebraicGeometry.OModulePresheaf.Leray.ker_dV_equiv_apply_coe
Source context 21 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "D" => LerayDblCpx p πZ K K'
Lean source · full declaration
theorem ker_dV_equiv_apply_coe (a b : ℕ) (z : LinearMap.ker ((D).dV a b)) (σ : K.Idx a) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    (ker_dV_equiv p πZ K K' a b z σ).1 = biC_uncurry p πZ K K' a b z.1 σ := rfl
theorem

colB_eq_pi

L77 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv.AlgebraicGeometry.OModulePresheaf.Leray.colB_eq_pi
Source context 21 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "D" => LerayDblCpx p πZ K K'
Lean source · full declaration
theorem colB_eq_pi (a b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    (DoubleComplex.colB (D) a b).map (ker_dV_equiv p πZ K K' a b).toLinearMap
      = Submodule.pi Set.univ (fun σ => relAltHB p πZ K' (K.inter σ) b) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  rcases b with _ | b'
  · refine (Submodule.map_bot _).trans (Eq.symm ((Submodule.eq_bot_iff _).mpr fun y hy => ?_))
    exact funext fun σ => (Submodule.mem_bot R).mp (hy σ (Set.mem_univ σ))
  · ext y
    simp only [Submodule.mem_map, DoubleComplex.colB, Submodule.mem_comap, Submodule.coe_subtype,
      LinearMap.mem_range, Submodule.mem_pi, Set.mem_univ, true_implies, relAltHB,
        LinearEquiv.coe_toLinearMap]
    have hptw : ∀ (z : LinearMap.ker ((D).dV a (b' + 1))), ker_dV_equiv p πZ K K' a (b' + 1) z = y →
        ∀ σ, biC_uncurry p πZ K K' a (b' + 1) z.1 σ = (y σ).1 :=
      fun z hzy σ => (ker_dV_equiv_apply_coe p πZ K K' a (b' + 1) z σ).symm.trans (congrArg (fun f
        => (f σ).1) hzy)
    constructor
    · rintro ⟨z, ⟨w, hw⟩, hzy⟩ σ
      refine ⟨biC_uncurry p πZ K K' a b' w σ, ?_⟩
      have h := dV_uncurry p πZ K K' a b' w σ
      exact h.symm.trans (hw ▸ hptw z hzy σ)
    · intro hy
      refine ⟨(ker_dV_equiv p πZ K K' a (b' + 1)).symm y, ?_, (ker_dV_equiv p πZ K K' a (b' +
        1)).apply_symm_apply y⟩
      choose v hv using hy
      refine ⟨(biC_uncurry p πZ K K' a b').symm v,
        (biC_uncurry p πZ K K' a (b' + 1)).injective (funext fun σ => ?_)⟩
      have h := dV_uncurry p πZ K K' a b' ((biC_uncurry p πZ K K' a b').symm v) σ
      rw [(biC_uncurry p πZ K K' a b').apply_symm_apply] at h
      exact (h.trans (hv σ)).trans (hptw _ ((ker_dV_equiv p πZ K K' a (b' + 1)).apply_symm_apply
        y) σ).symm
def

colH_iso

L110 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv.AlgebraicGeometry.OModulePresheaf.Leray.colH_iso
Documentation

The equivalence identifying vertical cohomology with Čech cochains of relative cohomology.

Source context 21 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "D" => LerayDblCpx p πZ K K'
Lean source · statement
def colH_iso (a b : ℕ) :
    DoubleComplex.colH (D) a b ≃ₗ[R] (relHPresheaf p πZ K' b).cochain K a
theorem

colH_iso_mk

L116 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv.AlgebraicGeometry.OModulePresheaf.Leray.colH_iso_mk
Source context 21 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "D" => LerayDblCpx p πZ K K'
Lean source · full declaration
theorem colH_iso_mk (a b : ℕ) (x : LinearMap.ker ((D).dV a b)) (σ : K.Idx a) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    colH_iso p πZ K K' a b (Submodule.Quotient.mk x) σ = Submodule.Quotient.mk (ker_dV_equiv p πZ
      K K' a b x σ) :=
  rfl
theorem

colH_iso_intertwine

L122 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv.AlgebraicGeometry.OModulePresheaf.Leray.colH_iso_intertwine
Source context 21 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "D" => LerayDblCpx p πZ K K'
Lean source · statement
theorem colH_iso_intertwine (a b : ℕ) :
    (colH_iso p πZ K K' (a + 1) b).toLinearMap ∘ₗ DoubleComplex.colHdH (D) a b
      = (relHPresheaf p πZ K' b).d K a ∘ₗ (colH_iso p πZ K K' a b).toLinearMap
def

ker_colHdH_equiv

L139 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv.AlgebraicGeometry.OModulePresheaf.Leray.ker_colHdH_equiv
Documentation

The induced equivalence of horizontal cocycles after taking vertical cohomology.

Source context 21 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "D" => LerayDblCpx p πZ K K'
Lean source · statement
def ker_colHdH_equiv (a b : ℕ) :
    LinearMap.ker (DoubleComplex.colHdH (D) a b) ≃ₗ[R] LinearMap.ker ((relHPresheaf p πZ K' b).d K
      a)
theorem

ker_colHdH_equiv_apply_coe

L157 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv.AlgebraicGeometry.OModulePresheaf.Leray.ker_colHdH_equiv_apply_coe
Source context 21 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "D" => LerayDblCpx p πZ K K'
Lean source · statement
theorem ker_colHdH_equiv_apply_coe (a b : ℕ) (x : LinearMap.ker (DoubleComplex.colHdH (D) a b)) :
    (ker_colHdH_equiv p πZ K K' a b x).1 = colH_iso p πZ K K' a b x.1
def

E2I_zero_equiv

L161 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv.AlgebraicGeometry.OModulePresheaf.Leray.E2I_zero_equiv
Documentation

The degree-zero second-page equivalence with Čech cohomology of relative cohomology.

Source context 21 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "D" => LerayDblCpx p πZ K K'
Lean source · statement
def E2I_zero_equiv (b : ℕ) : DoubleComplex.E₂I (D) 0 b ≃ₗ[R] (relHPresheaf p πZ K' b).H0 K
theorem

E2IB_map_eq

L164 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv.AlgebraicGeometry.OModulePresheaf.Leray.E2IB_map_eq
Source context 21 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "D" => LerayDblCpx p πZ K K'
Lean source · statement
theorem E2IB_map_eq (a b : ℕ) :
    (DoubleComplex.E₂IB (D) (a + 1) b).map (ker_colHdH_equiv p πZ K K' (a + 1) b).toLinearMap
      = (LinearMap.range ((relHPresheaf p πZ K' b).d K a)).comap
          (LinearMap.ker ((relHPresheaf p πZ K' b).d K (a + 1))).subtype
def

E2I_succ_equiv

L193 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv.AlgebraicGeometry.OModulePresheaf.Leray.E2I_succ_equiv
Documentation

The successive-degree second-page equivalence with Čech cohomology of relative cohomology.

Source context 21 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "D" => LerayDblCpx p πZ K K'
Lean source · statement
def E2I_succ_equiv (a b : ℕ) : DoubleComplex.E₂I (D) (a + 1) b ≃ₗ[R] (relHPresheaf p πZ K'
    b).HSucc K a
theorem

nonempty_E2I_equiv

L204 ↗
AlgebraicGeometry.OModulePresheaf.Leray.nonempty_E2I_equiv
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_E2I_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.AlgebraicCurves.Cohomology.Sheaves.Proofs in
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
  OModulePresheaf_Leray_nonempty_E2I_equiv.AlgebraicGeometry.OModulePresheaf.Leray in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.Leray.nonempty_E2I_equiv
    {R : Type u} [CommRing R] {V' Z : Scheme.{u}} (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R))
    (K : Z.OrderedAffineCover) (K' : V'.OrderedAffineCover) :
    (∀ b : ℕ, Nonempty (DoubleComplex.E₂I (OModulePresheaf.Leray.LerayDblCpx p πZ K K') 0 b
        ≃ₗ[R] (OModulePresheaf.Leray.relHPresheaf p πZ K' b).H0 K)) ∧
      ∀ a b : ℕ, Nonempty (DoubleComplex.E₂I (OModulePresheaf.Leray.LerayDblCpx p πZ K K') (a + 1) b
        ≃ₗ[R] (OModulePresheaf.Leray.relHPresheaf p πZ K' b).HSucc K a)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.