NYLL
Module

ModuleCohomology.lean

Nyll.EtaleCohomology.Classical.ModuleCohomology
14 declarations indexed from sourceView source ↗

Module documentation

Coefficient modules on classical sheaf cohomology

The underlying additive groups are mathlib's CategoryTheory.Sheaf.H. Scalar multiplication is induced by multiplication on the coefficient sheaf. The module structures are bundled in ModuleCat, avoiding competing global module instances on the underlying Ext groups.

Imports3
  • Mathlib.Algebra.Category.ModuleCat.Basic
  • Mathlib.CategoryTheory.Sites.Whiskering
  • Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Imported by7

Declarations

abbrev

forgetCoefficients

L34 ↗
EtaleCohomology.Classical.forgetCoefficients
Documentation

Forget the coefficient action, retaining the underlying classical abelian sheaf.

Source context 7 commands

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

noncomputable section
universe u v w t h
open CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [Ring R]
variable [J.HasSheafCompose (forget₂ (ModuleCat.{w} R) AddCommGrpCat.{w})]
Lean source · statement
abbrev forgetCoefficients :
    Sheaf J (ModuleCat.{w} R) ⥤ Sheaf J AddCommGrpCat.{w}
def

coefficientAction

L39 ↗
EtaleCohomology.Classical.coefficientAction
Documentation

Multiplication by a coefficient, as an endomorphism of the underlying abelian sheaf.

Source context 7 commands

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

noncomputable section
universe u v w t h
open CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [Ring R]
variable [J.HasSheafCompose (forget₂ (ModuleCat.{w} R) AddCommGrpCat.{w})]
Lean source · statement
def coefficientAction (F : Sheaf J (ModuleCat.{w} R)) (r : R) :
    (forgetCoefficients.obj F) ⟶ (forgetCoefficients.obj F)
lemma

coefficientAction_one

L52 ↗
EtaleCohomology.Classical.coefficientAction_one
Source context 7 commands

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

noncomputable section
universe u v w t h
open CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [Ring R]
variable [J.HasSheafCompose (forget₂ (ModuleCat.{w} R) AddCommGrpCat.{w})]
Lean source · statement
lemma coefficientAction_one (F : Sheaf J (ModuleCat.{w} R)) :
    coefficientAction F 1 = 𝟙 (forgetCoefficients.obj F)
lemma

coefficientAction_zero

L59 ↗
EtaleCohomology.Classical.coefficientAction_zero
Source context 7 commands

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

noncomputable section
universe u v w t h
open CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [Ring R]
variable [J.HasSheafCompose (forget₂ (ModuleCat.{w} R) AddCommGrpCat.{w})]
Lean source · statement
lemma coefficientAction_zero (F : Sheaf J (ModuleCat.{w} R)) :
    coefficientAction F 0 = 0
lemma

coefficientAction_add

L66 ↗
EtaleCohomology.Classical.coefficientAction_add
Source context 7 commands

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

noncomputable section
universe u v w t h
open CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [Ring R]
variable [J.HasSheafCompose (forget₂ (ModuleCat.{w} R) AddCommGrpCat.{w})]
Lean source · statement
lemma coefficientAction_add (F : Sheaf J (ModuleCat.{w} R)) (r s : R) :
    coefficientAction F (r + s) = coefficientAction F r + coefficientAction F s
lemma

coefficientAction_mul

L73 ↗
EtaleCohomology.Classical.coefficientAction_mul
Source context 7 commands

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

noncomputable section
universe u v w t h
open CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [Ring R]
variable [J.HasSheafCompose (forget₂ (ModuleCat.{w} R) AddCommGrpCat.{w})]
Lean source · statement
lemma coefficientAction_mul (F : Sheaf J (ModuleCat.{w} R)) (r s : R) :
    coefficientAction F (r * s) = coefficientAction F s ≫ coefficientAction F r
lemma

coefficientAction_naturality

L80 ↗
EtaleCohomology.Classical.coefficientAction_naturality
Source context 7 commands

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

noncomputable section
universe u v w t h
open CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [Ring R]
variable [J.HasSheafCompose (forget₂ (ModuleCat.{w} R) AddCommGrpCat.{w})]
Lean source · statement
lemma coefficientAction_naturality {F G : Sheaf J (ModuleCat.{w} R)}
    (f : F ⟶ G) (r : R) :
    coefficientAction F r ≫ forgetCoefficients.map f =
      forgetCoefficients.map f ≫ coefficientAction G r
abbrev

cohomologyModule

L91 ↗
EtaleCohomology.Classical.cohomologyModule
Documentation

The coefficient action on the existing Ext definition of classical cohomology.

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 Opposite
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [Ring R]
variable [J.HasSheafCompose (forget₂ (ModuleCat.{w} R) AddCommGrpCat.{w})]
variable [HasSheafify J AddCommGrpCat.{w}]
variable [HasExt.{h} (Sheaf J AddCommGrpCat.{w})]
Lean source · full declaration
abbrev cohomologyModule (F : Sheaf J (ModuleCat.{w} R)) (n : ℕ) :
    Module R ((forgetCoefficients.obj F).H n) where
  smul r x := Sheaf.H.map (coefficientAction F r) n x
  one_smul x := by
    change Sheaf.H.map (coefficientAction F 1) n x = x
    rw [coefficientAction_one, Sheaf.H.map_id_apply]
  mul_smul r s x := by
    change Sheaf.H.map (coefficientAction F (r * s)) n x =
      Sheaf.H.map (coefficientAction F r) n (Sheaf.H.map (coefficientAction F s) n x)
    rw [coefficientAction_mul, Sheaf.H.map_comp_apply]
  smul_zero r := (Sheaf.H.map (coefficientAction F r) n).map_zero
  smul_add r x y := (Sheaf.H.map (coefficientAction F r) n).map_add x y
  add_smul r s x := by
    change Sheaf.H.map (coefficientAction F (r + s)) n x =
      Sheaf.H.map (coefficientAction F r) n x + Sheaf.H.map (coefficientAction F s) n x
    rw [coefficientAction_add, Sheaf.H.map_add_apply]
  zero_smul x := by
    change Sheaf.H.map (coefficientAction F 0) n x = 0
    rw [coefficientAction_zero]
    change (Sheaf.functorH J n).map 0 x = 0
    rw [Functor.map_zero]
    rfl
def

cohomology

L115 ↗
EtaleCohomology.Classical.cohomology
Documentation

Classical sheaf cohomology with its canonical coefficient module structure.

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 Opposite
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [Ring R]
variable [J.HasSheafCompose (forget₂ (ModuleCat.{w} R) AddCommGrpCat.{w})]
variable [HasSheafify J AddCommGrpCat.{w}]
variable [HasExt.{h} (Sheaf J AddCommGrpCat.{w})]
Lean source · statement
def cohomology (F : Sheaf J (ModuleCat.{w} R)) (n : ℕ) : ModuleCat.{h} R
lemma

cohomology_smul

L120 ↗
EtaleCohomology.Classical.cohomology_smul
Documentation

Scalar multiplication is the cohomology map of the scalar endomorphism of the sheaf.

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 Opposite
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [Ring R]
variable [J.HasSheafCompose (forget₂ (ModuleCat.{w} R) AddCommGrpCat.{w})]
variable [HasSheafify J AddCommGrpCat.{w}]
variable [HasExt.{h} (Sheaf J AddCommGrpCat.{w})]
Lean source · statement
lemma cohomology_smul (F : Sheaf J (ModuleCat.{w} R)) (n : ℕ) (r : R)
    (x : cohomology F n) :
    r • x = Sheaf.H.map (coefficientAction F r) n x
def

cohomologyMap

L125 ↗
EtaleCohomology.Classical.cohomologyMap
Documentation

A morphism of coefficient sheaves induces a linear map on classical cohomology.

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 Opposite
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [Ring R]
variable [J.HasSheafCompose (forget₂ (ModuleCat.{w} R) AddCommGrpCat.{w})]
variable [HasSheafify J AddCommGrpCat.{w}]
variable [HasExt.{h} (Sheaf J AddCommGrpCat.{w})]
Lean source · full declaration
def cohomologyMap {F G : Sheaf J (ModuleCat.{w} R)} (f : F ⟶ G) (n : ℕ) :
    cohomology F n →ₗ[R] cohomology G n where
  toFun := Sheaf.H.map (forgetCoefficients.map f) n
  map_add' := (Sheaf.H.map (forgetCoefficients.map f) n).map_add
  map_smul' r x := by
    change (forgetCoefficients.obj F).H n at x
    change Sheaf.H.map (forgetCoefficients.map f) n
        (Sheaf.H.map (coefficientAction F r) n x) =
      Sheaf.H.map (coefficientAction G r) n
        (Sheaf.H.map (forgetCoefficients.map f) n x)
    rw [← Sheaf.H.map_comp_apply, coefficientAction_naturality,
      Sheaf.H.map_comp_apply]
lemma

cohomologyMap_apply

L139 ↗
EtaleCohomology.Classical.cohomologyMap_apply
Documentation

The underlying function of the coefficient-linear map is the classical cohomology 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 Opposite
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [Ring R]
variable [J.HasSheafCompose (forget₂ (ModuleCat.{w} R) AddCommGrpCat.{w})]
variable [HasSheafify J AddCommGrpCat.{w}]
variable [HasExt.{h} (Sheaf J AddCommGrpCat.{w})]
Lean source · statement
lemma cohomologyMap_apply {F G : Sheaf J (ModuleCat.{w} R)} (f : F ⟶ G) (n : ℕ)
    (x : cohomology F n) :
    cohomologyMap f n x = Sheaf.H.map (forgetCoefficients.map f) n x
def

cohomologyZeroEquiv

L144 ↗
EtaleCohomology.Classical.cohomologyZeroEquiv
Documentation

The usual degree-zero comparison is linear over the coefficient ring.

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 Opposite
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [Ring R]
variable [J.HasSheafCompose (forget₂ (ModuleCat.{w} R) AddCommGrpCat.{w})]
variable [HasSheafify J AddCommGrpCat.{w}]
variable [HasExt.{h} (Sheaf J AddCommGrpCat.{w})]
Lean source · full declaration
def cohomologyZeroEquiv (F : Sheaf J (ModuleCat.{w} R))
    {T : C} (hT : IsTerminal T) :
    cohomology F 0 ≃ₗ[R] F.obj.obj (op T) where
  toAddEquiv := Sheaf.H.equiv₀ (forgetCoefficients.obj F) hT
  map_smul' r x :=
    (Sheaf.H.equiv₀_naturality hT (coefficientAction F r) x).symm
lemma

cohomologyZeroEquiv_naturality

L152 ↗
EtaleCohomology.Classical.cohomologyZeroEquiv_naturality
Documentation

Naturality of the coefficient-linear degree-zero comparison.

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 Opposite
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
variable {R : Type t} [Ring R]
variable [J.HasSheafCompose (forget₂ (ModuleCat.{w} R) AddCommGrpCat.{w})]
variable [HasSheafify J AddCommGrpCat.{w}]
variable [HasExt.{h} (Sheaf J AddCommGrpCat.{w})]
Lean source · statement
lemma cohomologyZeroEquiv_naturality {F G : Sheaf J (ModuleCat.{w} R)}
    (f : F ⟶ G) {T : C} (hT : IsTerminal T) (x : cohomology F 0) :
    cohomologyZeroEquiv G hT (cohomologyMap f 0 x) =
      f.hom.app (op T) (cohomologyZeroEquiv F hT x)

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