NYLL
Module

FreeAbelianYoneda.lean

Nyll.EtaleCohomology.Classical.FreeAbelianYoneda
10 declarations indexed from sourceView source ↗

Module documentation

Free abelian representables and actual sheaf sections

The free abelian sheaves used in mathlib's Sheaf.cohomologyPresheaf corepresent evaluation. We record this equivalence and its two naturalities so that local lifting of sections can be applied to the actual Ext groups.

Imports3
  • Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
  • Mathlib.CategoryTheory.Adjunction.Whiskering
  • Mathlib.Algebra.Category.Grp.ForgetCorepresentable
Imported by4

Declarations

abbrev

freeAbelianSheafYoneda

L29 ↗
EtaleCohomology.freeAbelianSheafYoneda
Documentation

The same free abelian representable functor used by actual sheaf cohomology.

Source context 5 commands

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

noncomputable section
universe v u
open CategoryTheory Opposite
namespace EtaleCohomology
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{v}]
Lean source · statement
abbrev freeAbelianSheafYoneda : C ⥤ Sheaf J AddCommGrpCat.{v}
def

freeAbelianSheafYonedaHomEquiv

L34 ↗
EtaleCohomology.freeAbelianSheafYonedaHomEquiv
Documentation

Sheafification, the free abelian adjunction, and Yoneda identify morphisms from a free abelian representable with actual sections.

Source context 5 commands

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

noncomputable section
universe v u
open CategoryTheory Opposite
namespace EtaleCohomology
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{v}]
Lean source · statement
def freeAbelianSheafYonedaHomEquiv (V : C) (F : Sheaf J AddCommGrpCat.{v}) :
    ((freeAbelianSheafYoneda J).obj V ⟶ F) ≃ F.obj.obj (op V)
theorem

freeAbelianSheafYonedaHomEquiv_apply

L41 ↗
EtaleCohomology.freeAbelianSheafYonedaHomEquiv_apply
Documentation

The equivalence evaluates the sheafified morphism on the identity generator.

Source context 5 commands

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

noncomputable section
universe v u
open CategoryTheory Opposite
namespace EtaleCohomology
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{v}]
Lean source · statement
theorem freeAbelianSheafYonedaHomEquiv_apply (V : C)
    (F : Sheaf J AddCommGrpCat.{v}) (a : (freeAbelianSheafYoneda J).obj V ⟶ F) :
    freeAbelianSheafYonedaHomEquiv J V F a =
      (((sheafificationAdjunction J AddCommGrpCat.{v}).homEquiv
        (yoneda.obj V ⋙ AddCommGrpCat.free) F a).app (op V))
          (FreeAbelianGroup.of (𝟙 V))
theorem

freeAbelianSheafYonedaHomEquiv_postcomp

L49 ↗
EtaleCohomology.freeAbelianSheafYonedaHomEquiv_postcomp
Documentation

Evaluation is natural in the coefficient sheaf.

Source context 5 commands

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

noncomputable section
universe v u
open CategoryTheory Opposite
namespace EtaleCohomology
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{v}]
Lean source · statement
theorem freeAbelianSheafYonedaHomEquiv_postcomp (V : C)
    {F G : Sheaf J AddCommGrpCat.{v}}
    (a : (freeAbelianSheafYoneda J).obj V ⟶ F) (η : F ⟶ G) :
    freeAbelianSheafYonedaHomEquiv J V G (a ≫ η) =
      η.hom.app (op V) (freeAbelianSheafYonedaHomEquiv J V F a)
theorem

freeAbelianSheafYonedaHomEquiv_precomp

L58 ↗
EtaleCohomology.freeAbelianSheafYonedaHomEquiv_precomp
Documentation

Evaluation is natural in the object of the site.

Source context 5 commands

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

noncomputable section
universe v u
open CategoryTheory Opposite
namespace EtaleCohomology
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{v}]
Lean source · statement
theorem freeAbelianSheafYonedaHomEquiv_precomp {V W : C} (f : V ⟶ W)
    (F : Sheaf J AddCommGrpCat.{v}) (a : (freeAbelianSheafYoneda J).obj W ⟶ F) :
    freeAbelianSheafYonedaHomEquiv J V F ((freeAbelianSheafYoneda J).map f ≫ a) =
      F.obj.map f.op (freeAbelianSheafYonedaHomEquiv J W F a)
def

freeAbelianSheafYonedaTerminalIso

L82 ↗
EtaleCohomology.freeAbelianSheafYonedaTerminalIso
Documentation

At a terminal object, the free abelian representable is the actual constant integer sheaf. Both objects corepresent the same evaluation functor.

Source context 5 commands

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

noncomputable section
universe v u
open CategoryTheory Opposite
namespace EtaleCohomology
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{v}]
Lean source · statement
def freeAbelianSheafYonedaTerminalIso {T : C} (hT : Limits.IsTerminal T) :
    (freeAbelianSheafYoneda J).obj T ≅
      (constantSheaf J AddCommGrpCat.{v}).obj (AddCommGrpCat.of (ULift.{v} ℤ))
def

sheafCohomologyTerminalEquiv

L106 ↗
EtaleCohomology.sheafCohomologyTerminalEquiv
Documentation

The actual cohomology presheaf at a terminal object agrees with actual classical sheaf cohomology in every degree.

Source context 5 commands

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

noncomputable section
universe v u
open CategoryTheory Opposite
namespace EtaleCohomology
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{v}]
Lean source · statement
def sheafCohomologyTerminalEquiv
    [CategoryTheory.HasExt.{v} (Sheaf J AddCommGrpCat.{v})]
    {T : C} (hT : Limits.IsTerminal T) (F : Sheaf J AddCommGrpCat.{v}) (n : ℕ) :
    Sheaf.H.{v} F n ≃+ Sheaf.H'.{v} F n T
abbrev

freeAbelianSheafYonedaCoverCofork

L117 ↗
EtaleCohomology.freeAbelianSheafYonedaCoverCofork
Documentation

A singleton cover gives the first coequalizer of the actual free abelian Cech resolution. The relation maps are the two actual pullback projections, not a supplied descent comparison.

Source context 5 commands

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

noncomputable section
universe v u
open CategoryTheory Opposite
namespace EtaleCohomology
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{v}]
Lean source · statement
abbrev freeAbelianSheafYonedaCoverCofork {V W : C} (f : V ⟶ W)
    [Limits.HasPullback f f] :
    Limits.Cofork
      ((freeAbelianSheafYoneda J).map (Limits.pullback.fst f f))
      ((freeAbelianSheafYoneda J).map (Limits.pullback.snd f f))
def

freeAbelianSheafYonedaCoverIsColimit

L128 ↗
EtaleCohomology.freeAbelianSheafYonedaCoverIsColimit
Documentation

Sheaf descent proves the coequalizer universal property for a covering morphism. This is the degree-zero exactness input for the actual Cech resolution used in field/Galois cohomology comparison.

Source context 5 commands

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

noncomputable section
universe v u
open CategoryTheory Opposite
namespace EtaleCohomology
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{v}]
Lean source · statement
def freeAbelianSheafYonedaCoverIsColimit {V W : C} (f : V ⟶ W)
    [Limits.HasPullback f f] (hf : Sieve.generate (Presieve.singleton f) ∈ J W) :
    Limits.IsColimit (freeAbelianSheafYonedaCoverCofork J f)
theorem

freeAbelianSheafYoneda_map_epi_of_cover

L183 ↗
EtaleCohomology.freeAbelianSheafYoneda_map_epi_of_cover
Documentation

The augmentation of the free abelian Cech resolution of a singleton cover is an epimorphism of actual abelian sheaves.

Source context 5 commands

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

noncomputable section
universe v u
open CategoryTheory Opposite
namespace EtaleCohomology
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{v}]
Lean source · statement
theorem freeAbelianSheafYoneda_map_epi_of_cover {V W : C} (f : V ⟶ W)
    [Limits.HasPullback f f] (hf : Sieve.generate (Presieve.singleton f) ∈ J W) :
    Epi ((freeAbelianSheafYoneda J).map f)

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