ModuleFiniteLocallyConstantEquivalence.lean
Nyll.EtaleCohomology.Constructible.FiniteLocallyConstantEquivalence
3 declarations indexed from sourceView source ↗ Module documentation
Finite étale schemes and finite locally constant sheaves
The represented-sheaf functor gives an equivalence from finite étale schemes over an arbitrary scheme to the full subcategory of finite locally constant sheaves on its small étale site. Full faithfulness is the existing Yoneda comparison. Essential surjectivity uses the actual finite étale representer constructed by affine effective descent and Zariski gluing.
No finiteness, connectedness, separation, or field hypothesis is imposed on the base. The inverse functor and its unit and counit come from the proved full faithfulness and essential surjectivity, without new global instances.
Declarations
EtaleCohomology.EtaleFiniteLocallyConstantSetSheaf
DocumentationThe full subcategory of finite locally constant set sheaves on the small étale site.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology
EtaleCohomology.finiteEtaleToFiniteLocallyConstantSetSheaf
DocumentationThe sheaf of sections of a finite étale scheme, with its proved finite local constancy.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology
EtaleCohomology.finiteEtaleEquivFiniteLocallyConstantSetSheaf
DocumentationFinite étale schemes are equivalent to finite locally constant étale set sheaves.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology