NYLL
Module

ExactSequence.lean

Nyll.EtaleCohomology.Classical.ExactSequence
7 declarations indexed from sourceView source ↗

Module documentation

Coefficient-linear long exact sequences

The connecting morphism is mathlib's Ext connecting homomorphism. Its linearity follows from naturality under scalar multiplication on the short exact sequence. Exactness is inherited from the existing classical cohomology long exact sequence, using the proved exactness of the coefficient-forgetting functor.

Imports4
Imported by2

Declarations

def

coefficientActionShortComplex

L36 ↗
EtaleCohomology.Classical.coefficientActionShortComplex
Documentation

Scalar multiplication acts on the entire underlying short complex.

Source context 8 commands

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

noncomputable section
universe u v w t h
open CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [CommRing R]
variable [HasSheafify J (ModuleCat.{max t w} R)] [HasSheafify J AddCommGrpCat.{max t w}]
variable [HasExt.{h} (Sheaf J AddCommGrpCat.{max t w})]
Lean source · full declaration
def coefficientActionShortComplex (S : ShortComplex (Sheaf J (ModuleCat.{max t w} R)))
    (r : R) :
    S.map (forgetCoefficients.{u, v, max t w, t} (J := J)) ⟶
      S.map (forgetCoefficients.{u, v, max t w, t} (J := J)) where
  τ₁ := coefficientAction S.X₁ r
  τ₂ := coefficientAction S.X₂ r
  τ₃ := coefficientAction S.X₃ r
  comm₁₂ := coefficientAction_naturality S.f r
  comm₂₃ := coefficientAction_naturality S.g r
def

connecting

L49 ↗
EtaleCohomology.Classical.connecting
Documentation

The connecting homomorphism, with its canonical coefficient linearity.

Source context 9 commands

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

noncomputable section
universe u v w t h
open CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [CommRing R]
variable [HasSheafify J (ModuleCat.{max t w} R)] [HasSheafify J AddCommGrpCat.{max t w}]
variable [HasExt.{h} (Sheaf J AddCommGrpCat.{max t w})]
variable {S : ShortComplex (Sheaf J (ModuleCat.{max t w} R))} (hS : S.ShortExact)
Lean source · full declaration
def connecting (n : ℕ) :
    cohomology.{u, v, max t w, t, h} S.X₃ n →ₗ[R]
      cohomology.{u, v, max t w, t, h} S.X₁ (n + 1) where
  toFun := Sheaf.H.δ.{h, max t w, v, u}
    (forgetCoefficients_shortExact R J hS) n (n + 1) rfl
  map_add' := (Sheaf.H.δ.{h, max t w, v, u}
    (forgetCoefficients_shortExact R J hS) n (n + 1) rfl).map_add
  map_smul' r x := by
    change ((forgetCoefficients.{u, v, max t w, t} (J := J)).obj S.X₃).H n at x
    exact Sheaf.H.δ_naturality.{h, max t w, v, u} n (n + 1) rfl
      (forgetCoefficients_shortExact R J hS) (forgetCoefficients_shortExact R J hS)
      (coefficientActionShortComplex S r) x
lemma

connecting_apply

L63 ↗
EtaleCohomology.Classical.connecting_apply
Documentation

The underlying function of the connecting map is mathlib's classical boundary map.

Source context 9 commands

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

noncomputable section
universe u v w t h
open CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [CommRing R]
variable [HasSheafify J (ModuleCat.{max t w} R)] [HasSheafify J AddCommGrpCat.{max t w}]
variable [HasExt.{h} (Sheaf J AddCommGrpCat.{max t w})]
variable {S : ShortComplex (Sheaf J (ModuleCat.{max t w} R))} (hS : S.ShortExact)
Lean source · statement
lemma connecting_apply (n : ℕ)
    (x : cohomology.{u, v, max t w, t, h} S.X₃ n) :
    connecting.{u, v, w, t, h} hS n x =
      Sheaf.H.δ.{h, max t w, v, u}
        (forgetCoefficients_shortExact R J hS) n (n + 1) rfl x
lemma

connecting_naturality

L70 ↗
EtaleCohomology.Classical.connecting_naturality
Documentation

Naturality of the coefficient-linear connecting map.

Source context 9 commands

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

noncomputable section
universe u v w t h
open CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [CommRing R]
variable [HasSheafify J (ModuleCat.{max t w} R)] [HasSheafify J AddCommGrpCat.{max t w}]
variable [HasExt.{h} (Sheaf J AddCommGrpCat.{max t w})]
variable {S : ShortComplex (Sheaf J (ModuleCat.{max t w} R))} (hS : S.ShortExact)
Lean source · statement
lemma connecting_naturality
    {S₁ S₂ : ShortComplex (Sheaf J (ModuleCat.{max t w} R))}
    (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂) (n : ℕ)
    (x : cohomology.{u, v, max t w, t, h} S₁.X₃ n) :
    connecting.{u, v, w, t, h} h₂ n
        (cohomologyMap.{u, v, max t w, t, h} f.τ₃ n x) =
      cohomologyMap.{u, v, max t w, t, h} f.τ₁ (n + 1)
        (connecting.{u, v, w, t, h} h₁ n x)
lemma

cohomology_exact

L103 ↗
EtaleCohomology.Classical.cohomology_exact
Documentation

Exactness at the middle coefficient sheaf in every degree.

Source context 10 commands

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

noncomputable section
universe u v w t h
open CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [CommRing R]
variable [HasSheafify J (ModuleCat.{max t w} R)] [HasSheafify J AddCommGrpCat.{max t w}]
variable [HasExt.{h} (Sheaf J AddCommGrpCat.{max t w})]
variable {S : ShortComplex (Sheaf J (ModuleCat.{max t w} R))} (hS : S.ShortExact)
include hS in
Lean source · statement
lemma cohomology_exact (n : ℕ) :
    Function.Exact (cohomologyMap.{u, v, max t w, t, h} S.f n)
      (cohomologyMap.{u, v, max t w, t, h} S.g n)
lemma

cohomology_exact_connecting

L111 ↗
EtaleCohomology.Classical.cohomology_exact_connecting
Documentation

Exactness at the source of the connecting map.

Source context 9 commands

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

noncomputable section
universe u v w t h
open CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [CommRing R]
variable [HasSheafify J (ModuleCat.{max t w} R)] [HasSheafify J AddCommGrpCat.{max t w}]
variable [HasExt.{h} (Sheaf J AddCommGrpCat.{max t w})]
variable {S : ShortComplex (Sheaf J (ModuleCat.{max t w} R))} (hS : S.ShortExact)
Lean source · statement
lemma cohomology_exact_connecting (n : ℕ) :
    Function.Exact (cohomologyMap.{u, v, max t w, t, h} S.g n)
      (connecting.{u, v, w, t, h} hS n)
lemma

connecting_exact_cohomology

L119 ↗
EtaleCohomology.Classical.connecting_exact_cohomology
Documentation

Exactness at the target of the connecting map.

Source context 9 commands

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

noncomputable section
universe u v w t h
open CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [CommRing R]
variable [HasSheafify J (ModuleCat.{max t w} R)] [HasSheafify J AddCommGrpCat.{max t w}]
variable [HasExt.{h} (Sheaf J AddCommGrpCat.{max t w})]
variable {S : ShortComplex (Sheaf J (ModuleCat.{max t w} R))} (hS : S.ShortExact)
Lean source · statement
lemma connecting_exact_cohomology (n : ℕ) :
    Function.Exact (connecting.{u, v, w, t, h} hS n)
      (cohomologyMap.{u, v, max t w, t, h} S.f (n + 1))

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