NYLL
Module

FiniteModuleTrivialization.lean

Nyll.EtaleCohomology.Constructible.FiniteModuleTrivialization
2 declarations indexed from sourceView source ↗

Module documentation

Finite étale trivialization of module sheaves

On a connected scheme, a module sheaf with finite locally constant underlying set sheaf is trivialized by a connected finite étale surjective cover. The constant module is constructed from sections on that cover, and the actual constant-sheaf counit supplies an isomorphism respecting addition and scalars.

In particular this applies to finite type locally constant sheaves over any finite commutative coefficient ring. No base field or noetherian hypothesis is used. Finiteness of the ring is only needed for this last specialization.

Imports14
Imported by1

Declarations

theorem

exists_finite_etale_module_trivialization_of_underlying

L45 ↗
EtaleCohomology.exists_finite_etale_module_trivialization_of_underlying
Documentation

A finite locally constant underlying set sheaf has a finite étale trivialization as a module sheaf, even over an infinite coefficient ring.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology
Lean source · statement
theorem exists_finite_etale_module_trivialization_of_underlying
    {X : Scheme.{u}} [ConnectedSpace X] {R : Type u} [CommRing R]
    (G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R))
    (hG : IsEtaleFiniteLocallyConstantSet ((etaleModuleUnderlying X R).obj G)) :
    ∃ A : FiniteEtale X, ConnectedSpace A.left ∧ Surjective A.hom ∧
      ∃ M : ModuleCat.{u} R, Finite M ∧ Module.Finite R M ∧
        Nonempty ((etalePullback A.hom R).obj G ≅
          (constantSheaf A.left.smallEtaleTopology (ModuleCat.{u} R)).obj M)
theorem

exists_finite_etale_trivialization

L72 ↗
EtaleCohomology.IsEtaleFiniteTypeLocallyConstant.exists_finite_etale_trivialization
Documentation

Over a finite coefficient ring, any finite type locally constant module sheaf on a connected scheme becomes constant on a connected finite étale surjective cover.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology
Lean source · statement
theorem IsEtaleFiniteTypeLocallyConstant.exists_finite_etale_trivialization
    {X : Scheme.{u}} [ConnectedSpace X] {R : Type u} [CommRing R] [Finite R]
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : IsEtaleFiniteTypeLocallyConstant R G) :
    ∃ A : FiniteEtale X, ConnectedSpace A.left ∧ Surjective A.hom ∧
      ∃ M : ModuleCat.{u} R, Finite M ∧ Module.Finite R M ∧
        Nonempty ((etalePullback A.hom R).obj G ≅
          (constantSheaf A.left.smallEtaleTopology (ModuleCat.{u} R)).obj M)

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