NYLL
Module

OModulePresheaf_Leray_nonempty_HTot_equiv.lean

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

Module documentation

Identification of Leray total cohomology with cohomology on the preimage cover.

Imports4
Imported by2

Declarations

theorem

dTot_single_apply_succ

L57 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv.AlgebraicGeometry.OModulePresheaf.Leray.Stair.dTot_single_apply_succ
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace Stair
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section Generic
variable {R : Type u} [CommRing R] {D : DoubleComplex.Bounded R}
Lean source · full declaration
theorem dTot_single_apply_succ {n pp q : ℕ} (h : pp + 1 + q = n + 1)
    (j : DoubleComplex.Diag n) (x : D.C j.1.1 j.1.2) (hne : pp + 1 ≠ j.1.1) :
    DoubleComplex.dTot D n
        (Pi.single (M := fun i : DoubleComplex.Diag n => D.C i.1.1 i.1.2) j x)
        ⟨(pp + 1, q), h⟩
      = D.dH pp q (Pi.single (M := fun i : DoubleComplex.Diag n => D.C i.1.1 i.1.2)
          j x ⟨(pp, q), by omega⟩) := by
  match q, h with
  | 0, h => exact DoubleComplex.dTot_apply_succ_zero h _
  | q' + 1, h =>
    rw [DoubleComplex.dTot_apply_succ_succ]
    refine add_eq_left.mpr ?_
    rw [Pi.single_eq_of_ne (fun heq => hne (congrArg (fun i => i.1.1) heq)), map_zero, smul_zero]
def

eK'

L85 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv.AlgebraicGeometry.OModulePresheaf.Leray.Stair.eK'
Documentation

Embed the cochains on K' into the horizontal-degree-zero column of the Leray total complex through biAug.

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace Stair
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section Edge
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 "DL" => LerayDblCpx p πZ K K'
Lean source · statement
def eK' (n : ℕ) :
    (OModulePresheaf.unit (p ≫ πZ)).cochain K' n →ₗ[R] DoubleComplex.Tot (DL) n
theorem

eK'_apply_zero

L90 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv.AlgebraicGeometry.OModulePresheaf.Leray.Stair.eK'_apply_zero
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace Stair
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section Edge
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 "DL" => LerayDblCpx p πZ K K'
Lean source · statement
theorem eK'_apply_zero {n : ℕ} (h : 0 + n = n) (y : (OModulePresheaf.unit (p ≫ πZ)).cochain K' n) :
    eK' p πZ K K' n y ⟨(0, n), h⟩ = biAug p πZ K K' n y
theorem

eK'_apply_pos

L94 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv.AlgebraicGeometry.OModulePresheaf.Leray.Stair.eK'_apply_pos
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace Stair
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section Edge
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 "DL" => LerayDblCpx p πZ K K'
Lean source · statement
theorem eK'_apply_pos {n p' q : ℕ} (h : p' + 1 + q = n)
    (y : (OModulePresheaf.unit (p ≫ πZ)).cochain K' n) :
    eK' p πZ K K' n y ⟨(p' + 1, q), h⟩ = 0
theorem

dH_biAug

L112 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv.AlgebraicGeometry.OModulePresheaf.Leray.Stair.dH_biAug
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace Stair
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section Main
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ] [IsSeparated (p ≫ πZ)]
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "DL" => LerayDblCpx p πZ K K'
Lean source · statement
theorem dH_biAug (b : ℕ) (y : (OModulePresheaf.unit (p ≫ πZ)).cochain K' b) :
    (DL).dH 0 b (biAug p πZ K K' b y) = 0
theorem

eK'_chain

L116 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv.AlgebraicGeometry.OModulePresheaf.Leray.Stair.eK'_chain
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace Stair
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section Main
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ] [IsSeparated (p ≫ πZ)]
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "DL" => LerayDblCpx p πZ K K'
Lean source · statement
theorem eK'_chain (n : ℕ) :
    DoubleComplex.dTot (DL) n ∘ₗ eK' p πZ K K' n
      = eK' p πZ K K' (n + 1) ∘ₗ (OModulePresheaf.unit (p ≫ πZ)).d K' n
theorem

stair_surj

L143 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv.AlgebraicGeometry.OModulePresheaf.Leray.Stair.stair_surj
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace Stair
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section Main
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ] [IsSeparated (p ≫ πZ)]
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "DL" => LerayDblCpx p πZ K K'
Lean source · statement
theorem stair_surj (n : ℕ)
    (c : DoubleComplex.Tot (DL) (n + 1)) (hc : DoubleComplex.dTot (DL) (n + 1) c = 0) :
    ∃ (y : (OModulePresheaf.unit (p ≫ πZ)).cochain K' (n + 1)) (bb : DoubleComplex.Tot (DL) n),
      (OModulePresheaf.unit (p ≫ πZ)).d K' (n + 1) y = 0 ∧
      c = eK' p πZ K K' (n + 1) y + DoubleComplex.dTot (DL) n bb
theorem

stair_inj

L226 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv.AlgebraicGeometry.OModulePresheaf.Leray.Stair.stair_inj
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace Stair
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section Main
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ] [IsSeparated (p ≫ πZ)]
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "DL" => LerayDblCpx p πZ K K'
Lean source · statement
theorem stair_inj (n : ℕ) (y : (OModulePresheaf.unit (p ≫ πZ)).cochain K' (n + 1))
    (bb : DoubleComplex.Tot (DL) n)
    (hb : eK' p πZ K K' (n + 1) y = DoubleComplex.dTot (DL) n bb) :
    ∃ y', y = (OModulePresheaf.unit (p ≫ πZ)).d K' n y'
def

HeK'

L300 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv.AlgebraicGeometry.OModulePresheaf.Leray.Stair.HeK'
Documentation

The map from positive-degree cohomology on K' to Leray total cohomology induced by eK'.

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace Stair
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section Main
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ] [IsSeparated (p ≫ πZ)]
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "DL" => LerayDblCpx p πZ K K'
Lean source · statement
def HeK' (n : ℕ) :
    (OModulePresheaf.unit (p ≫ πZ)).HSucc K' n →ₗ[R] DoubleComplex.HTot (DL) (n + 1)
def

HTotSuccEquiv

L319 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv.AlgebraicGeometry.OModulePresheaf.Leray.Stair.HTotSuccEquiv
Documentation

Identify positive-degree Leray total cohomology with cohomology on K' by the bijectivity of HeK'.

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace Stair
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section Main
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ] [IsSeparated (p ≫ πZ)]
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "DL" => LerayDblCpx p πZ K K'
Lean source · statement
def HTotSuccEquiv (n : ℕ) :
    DoubleComplex.HTot (DL) (n + 1) ≃ₗ[R] (OModulePresheaf.unit (p ≫ πZ)).HSucc K' n
def

HTotZeroEquiv

L340 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv.AlgebraicGeometry.OModulePresheaf.Leray.Stair.HTotZeroEquiv
Documentation

Identify degree-zero Leray total cohomology with the cocycles on K' using eK'.

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_HTot_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace Stair
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section Main
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ] [IsSeparated (p ≫ πZ)]
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
local notation "DL" => LerayDblCpx p πZ K K'
Lean source · statement
def HTotZeroEquiv :
    DoubleComplex.HTot (DL) 0 ≃ₗ[R] (OModulePresheaf.unit (p ≫ πZ)).H0 K'
theorem

nonempty_HTot_equiv

L383 ↗
AlgebraicGeometry.OModulePresheaf.Leray.nonempty_HTot_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_HTot_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_HTot_equiv.AlgebraicGeometry.OModulePresheaf.Leray in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.Leray.nonempty_HTot_equiv
    {R : Type u} [CommRing R] {V' Z : Scheme.{u}} (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R))
    [IsSeparated πZ] [IsSeparated (p ≫ πZ)] (K : Z.OrderedAffineCover) (K' :
      V'.OrderedAffineCover) :
    Nonempty (DoubleComplex.HTot (OModulePresheaf.Leray.LerayDblCpx p πZ K K') 0
        ≃ₗ[R] (OModulePresheaf.unit (p ≫ πZ)).H0 K') ∧
      ∀ n : ℕ, Nonempty (DoubleComplex.HTot (OModulePresheaf.Leray.LerayDblCpx p πZ K K') (n + 1)
        ≃ₗ[R] (OModulePresheaf.unit (p ≫ πZ)).HSucc K' n)

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