Module

ModuleUnderlying.lean

Nyll.EtaleCohomology.Constructible.ModuleUnderlying

1 declaration indexed from sourceView source ↗

Module documentation

Underlying finite locally constant sheaves

Over a finite coefficient ring, the underlying set sheaf of a finite type locally constant module sheaf is finite locally constant. The original trivializing étale cover works: inverse image commutes with forgetting the module structure, and each finitely generated module over a finite ring is a finite set. The base scheme is arbitrary.

Imports4

Nyll.EtaleCohomology.Constructible.FiniteLocallyConstantSet
Nyll.EtaleCohomology.Constructible.LocallyConstant
Nyll.EtaleCohomology.Sites.ModuleSetComparison
Mathlib.RingTheory.Finiteness.Cardinality

Imported by3

lemma

isEtaleFiniteLocallyConstantSet

L32 ↗

EtaleCohomology.IsEtaleFiniteTypeLocallyConstant.isEtaleFiniteLocallyConstantSet

Documentation

Finite type local constancy over a finite ring gives finite local constancy of the underlying set sheaf, on the same étale cover.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology

Lean source · statement

lemma IsEtaleFiniteTypeLocallyConstant.isEtaleFiniteLocallyConstantSet
    {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : IsEtaleFiniteTypeLocallyConstant R G) :
    IsEtaleFiniteLocallyConstantSet ((etaleModuleUnderlying X R).obj G)

Module documentation

Underlying finite locally constant sheaves

Declarations

isEtaleFiniteLocallyConstantSet