Module

ModuleConstant.lean

Nyll.EtaleCohomology.Sites.ModuleConstant

3 declarations indexed from sourceView source ↗

Module documentation

Constant module sheaves from constant underlying set sheaves

For a functor preserving sheafification and reflecting isomorphisms, the constant-sheaf counit is an isomorphism whenever its image sheaf is constant and the target constant-sheaf functor is fully faithful. The source constant functor need not be fully faithful: the actual counit comparison already supplies the required isomorphism.

Applied to étale module sheaves, this constructs the constant module model from sections over a terminal object. The ring and the scheme are arbitrary; full faithfulness of the constant set-sheaf functor is an explicit input. The proof uses Mathlib's constantSheafAdj_counit_w and the affine étale site to supply preservation of sheafification by the module forgetful functor.

Imports14

Nyll.EtaleCohomology.Sites.ModuleSetComparison
Mathlib.Algebra.Category.ModuleCat.Adjunctions
Mathlib.Algebra.Category.ModuleCat.Colimits
Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Mathlib.Algebra.Category.ModuleCat.Limits
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.AlgebraicGeometry.Sites.Etale
Mathlib.CategoryTheory.Iso
Mathlib.CategoryTheory.Sites.ConstantSheaf
Mathlib.CategoryTheory.Sites.Equivalence
Mathlib.CategoryTheory.Sites.PreservesSheafification
Mathlib.CategoryTheory.Sites.Whiskering
Mathlib.CategoryTheory.Types.Basic
Mathlib.RingTheory.Finiteness.Basic

Imported by2

lemma

constantCounit_isIso_of_forget

L48 ↗

EtaleCohomology.Sites.constantCounit_isIso_of_forget

Documentation

The actual constant-sheaf counit is invertible if the forgotten sheaf is constant and only the target constant-sheaf functor is fully faithful.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology.Sites

Lean source · statement

lemma constantCounit_isIso_of_forget
    {C : Type*} [Category* C] (J : GrothendieckTopology C)
    {D : Type*} [Category* D] {B : Type*} [Category* B]
    [HasWeakSheafify J D] [HasWeakSheafify J B]
    (U : D ⥤ B) [J.PreservesSheafification U] [J.HasSheafCompose U]
    [U.ReflectsIsomorphisms]
    [(constantSheaf J B).Faithful] [(constantSheaf J B).Full]
    (F : Sheaf J D) [Sheaf.IsConstant J ((sheafCompose J U).obj F)]
    {T : C} (hT : IsTerminal T) :
    IsIso ((constantSheafAdj J D hT).counit.app F)

def

etaleModuleConstantIso

L72 ↗

EtaleCohomology.etaleModuleConstantIso

Documentation

A constant underlying set sheaf yields an actual constant module sheaf via the counit, with its module of global sections as the model.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

def etaleModuleConstantIso (X : Scheme.{u}) (R : Type u) [CommRing R]
    [(constantSheaf X.smallEtaleTopology (Type u)).Faithful]
    [(constantSheaf X.smallEtaleTopology (Type u)).Full]
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} R))
    [Sheaf.IsConstant X.smallEtaleTopology ((etaleModuleUnderlying X R).obj F)]
    {T : X.Etale} (hT : IsTerminal T) :
    (constantSheaf X.smallEtaleTopology (ModuleCat.{u} R)).obj (F.obj.obj (op T)) ≅ F

theorem

exists_finite_constantModule_of_underlying_iso

L93 ↗

EtaleCohomology.exists_finite_constantModule_of_underlying_iso

Documentation

A finite constant underlying set sheaf has an actual finite constant module model. The coefficient ring itself need not be finite.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

theorem exists_finite_constantModule_of_underlying_iso
    {X : Scheme.{u}} {R : Type u} [CommRing R]
    [(constantSheaf X.smallEtaleTopology (Type u)).Faithful]
    [(constantSheaf X.smallEtaleTopology (Type u)).Full]
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} R))
    (A : Type u) [Finite A]
    (e : (etaleModuleUnderlying X R).obj F ≅
      (constantSheaf X.smallEtaleTopology (Type u)).obj A)
    {T : X.Etale} (hT : IsTerminal T) :
    ∃ M : ModuleCat.{u} R, Finite M ∧ Module.Finite R M ∧
      Nonempty (F ≅ (constantSheaf X.smallEtaleTopology (ModuleCat.{u} R)).obj M)

Module documentation

Constant module sheaves from constant underlying set sheaves

Declarations

constantCounit_isIso_of_forget

etaleModuleConstantIso

exists_finite_constantModule_of_underlying_iso