NYLL
Module

Representability.lean

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

Module documentation

Finite étale representability of finite locally constant sheaves

Every finite locally constant sheaf of sets on the small étale site of an arbitrary scheme is represented by a finite étale scheme. Restricting to the directed affine open cover supplies affine representers by effective descent. Their canonical gluing represents the original sheaf.

No connectedness, quasi-compactness, quasi-separatedness, or ground field hypothesis is imposed on the base. The result also gives an actual isomorphism with the sheaf associated to the finite étale representer.

Imports13
Imported by4

Declarations

theorem

exists_representer

L44 ↗
EtaleCohomology.IsEtaleFiniteLocallyConstantSet.exists_representer
Documentation

Every finite locally constant sheaf on an arbitrary scheme has a finite étale representer, obtained by gluing its affine representers.

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 IsEtaleFiniteLocallyConstantSet.exists_representer
    {X : Scheme.{u}} {G : Sheaf X.smallEtaleTopology (Type u)}
    (hG : IsEtaleFiniteLocallyConstantSet G) :
    ∃ Z : FiniteEtale X,
      Nonempty (G.obj.RepresentableBy ((finiteEtaleToEtale X).obj Z))
theorem

exists_finiteEtaleSheaf_iso

L70 ↗
EtaleCohomology.IsEtaleFiniteLocallyConstantSet.exists_finiteEtaleSheaf_iso
Documentation

A finite locally constant sheaf is isomorphic to the actual sheaf of sections of a finite étale scheme over its base.

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 IsEtaleFiniteLocallyConstantSet.exists_finiteEtaleSheaf_iso
    {X : Scheme.{u}} {G : Sheaf X.smallEtaleTopology (Type u)}
    (hG : IsEtaleFiniteLocallyConstantSet G) :
    ∃ Z : FiniteEtale X, Nonempty ((finiteEtaleSheaf X).obj Z ≅ G)

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