Module

CoefficientSheaves.lean

Nyll.EtaleCohomology.Classical.CoefficientSheaves

8 declarations indexed from sourceView source ↗

Module documentation

Exactness of forgetting coefficients

Restriction along ℤ → R and the equivalence between ℤ-modules and abelian groups supply both adjoints to the coefficient-forgetting functor. This also supplies sheaf composition on sites whose object universe is larger than the coefficients.

Imports8

Nyll.EtaleCohomology.Classical.ModuleCohomology
Mathlib.Algebra.Category.Grp.ZModuleEquivalence
Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Mathlib.Algebra.Category.ModuleCat.Abelian
Mathlib.Algebra.Category.Grp.FilteredColimits
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.Sites.Adjunction
Mathlib.Algebra.Homology.ShortComplex.ShortExact

Imported by4

instance

forgetModuleRightAdjoint

L36 ↗

EtaleCohomology.Classical.forgetModuleRightAdjoint

Documentation

Forgetting module coefficients is right adjoint to extension of integer scalars.

Source context 5 commands

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

noncomputable section
universe u v w t
open CategoryTheory CategoryTheory.Limits CategoryTheory.Functor
namespace EtaleCohomology.Classical
variable (R : Type t) [CommRing R]

Lean source · statement

instance forgetModuleRightAdjoint :
    (forget₂ (ModuleCat.{max t w} R) AddCommGrpCat.{max t w}).IsRightAdjoint

instance

forgetModuleLeftAdjoint

L42 ↗

EtaleCohomology.Classical.forgetModuleLeftAdjoint

Documentation

Forgetting module coefficients is left adjoint to coextension of integer scalars.

Source context 5 commands

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

noncomputable section
universe u v w t
open CategoryTheory CategoryTheory.Limits CategoryTheory.Functor
namespace EtaleCohomology.Classical
variable (R : Type t) [CommRing R]

Lean source · statement

instance forgetModuleLeftAdjoint :
    (forget₂ (ModuleCat.{max t w} R) AddCommGrpCat.{max t w}).IsLeftAdjoint

lemma

forgetModule_preservesFilteredColimits

L49 ↗

EtaleCohomology.Classical.forgetModule_preservesFilteredColimits

Documentation

Filtered colimits are preserved even when the module universe is larger than the ring.

Source context 5 commands

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

noncomputable section
universe u v w t
open CategoryTheory CategoryTheory.Limits CategoryTheory.Functor
namespace EtaleCohomology.Classical
variable (R : Type t) [CommRing R]

Lean source · statement

lemma forgetModule_preservesFilteredColimits :
    PreservesFilteredColimitsOfSize.{max t w, max t w}
      (forget (ModuleCat.{max t w} R))

def

forgetCoefficientsSheafifyIso

L60 ↗

EtaleCohomology.Classical.forgetCoefficientsSheafifyIso

Documentation

Sheafification after forgetting coefficients agrees with forgetting a coefficient sheaf.

Source context 7 commands

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

noncomputable section
universe u v w t
open CategoryTheory CategoryTheory.Limits CategoryTheory.Functor
namespace EtaleCohomology.Classical
variable (R : Type t) [CommRing R]
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
variable [HasSheafify J (ModuleCat.{max t w} R)] [HasSheafify J AddCommGrpCat.{max t w}]

Lean source · statement

def forgetCoefficientsSheafifyIso :
    Sheaf.composeAndSheafify J (forget₂ (ModuleCat.{max t w} R) AddCommGrpCat.{max t w}) ≅
      forgetCoefficients.{u, v, max t w, t} (J := J) (R := R)

instance

forgetCoefficientsLeftAdjoint

L67 ↗

EtaleCohomology.Classical.forgetCoefficientsLeftAdjoint

Source context 7 commands

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

noncomputable section
universe u v w t
open CategoryTheory CategoryTheory.Limits CategoryTheory.Functor
namespace EtaleCohomology.Classical
variable (R : Type t) [CommRing R]
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
variable [HasSheafify J (ModuleCat.{max t w} R)] [HasSheafify J AddCommGrpCat.{max t w}]

Lean source · statement

instance forgetCoefficientsLeftAdjoint :
    (forgetCoefficients.{u, v, max t w, t} (J := J) (R := R)).IsLeftAdjoint

instance

forgetCoefficientsRightAdjoint

L71 ↗

EtaleCohomology.Classical.forgetCoefficientsRightAdjoint

Source context 7 commands

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

noncomputable section
universe u v w t
open CategoryTheory CategoryTheory.Limits CategoryTheory.Functor
namespace EtaleCohomology.Classical
variable (R : Type t) [CommRing R]
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
variable [HasSheafify J (ModuleCat.{max t w} R)] [HasSheafify J AddCommGrpCat.{max t w}]

Lean source · statement

instance forgetCoefficientsRightAdjoint :
    (forgetCoefficients.{u, v, max t w, t} (J := J) (R := R)).IsRightAdjoint

instance

forgetCoefficientsAdditive

L76 ↗

EtaleCohomology.Classical.forgetCoefficientsAdditive

Source context 7 commands

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

noncomputable section
universe u v w t
open CategoryTheory CategoryTheory.Limits CategoryTheory.Functor
namespace EtaleCohomology.Classical
variable (R : Type t) [CommRing R]
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
variable [HasSheafify J (ModuleCat.{max t w} R)] [HasSheafify J AddCommGrpCat.{max t w}]

Lean source · full declaration

instance forgetCoefficientsAdditive :
    (forgetCoefficients.{u, v, max t w, t} (J := J) (R := R)).Additive where
  map_add := by
    intro F G f g
    ext U x
    rfl

lemma

forgetCoefficients_shortExact

L84 ↗

EtaleCohomology.Classical.forgetCoefficients_shortExact

Documentation

A short exact sequence of module sheaves remains short exact after forgetting coefficients.

Source context 7 commands

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

noncomputable section
universe u v w t
open CategoryTheory CategoryTheory.Limits CategoryTheory.Functor
namespace EtaleCohomology.Classical
variable (R : Type t) [CommRing R]
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
variable [HasSheafify J (ModuleCat.{max t w} R)] [HasSheafify J AddCommGrpCat.{max t w}]

Lean source · statement

lemma forgetCoefficients_shortExact
    {S : ShortComplex (Sheaf J (ModuleCat.{max t w} R))} (hS : S.ShortExact) :
    (S.map (forgetCoefficients.{u, v, max t w, t} (J := J))).ShortExact

Module documentation

Exactness of forgetting coefficients

Declarations