NYLL
Module

AffineRepresentability.lean

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

Module documentation

Finite étale representability on affine schemes

A finite locally constant sheaf has a finite étale local representer over a faithfully flat affine étale cover. Its universal section constructs the full algebra descent data. The invariant algebra gives a finite étale scheme with the required cartesian comparison. Descending the universal section identifies its represented sheaf with the original sheaf.

The base is any affine scheme: no ground field, noetherianity, or connectedness is required.

Imports21
Imported by2

Declarations

theorem

exists_spec_representer

L53 ↗
EtaleCohomology.IsEtaleFiniteLocallyConstantSet.exists_spec_representer
Documentation

A finite locally constant sheaf on an arbitrary ring's spectrum is represented by a finite étale scheme, constructed by effective descent.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Algebra.Descent
open scoped TensorProduct
namespace EtaleCohomology
Lean source · statement
theorem IsEtaleFiniteLocallyConstantSet.exists_spec_representer
    {R : CommRingCat.{u}} {G : Sheaf (Spec R).smallEtaleTopology (Type u)}
    (hG : IsEtaleFiniteLocallyConstantSet G) :
    ∃ Z : FiniteEtale (Spec R),
      Nonempty (G.obj.RepresentableBy ((finiteEtaleToEtale (Spec R)).obj Z))
theorem

exists_affine_representer

L107 ↗
EtaleCohomology.IsEtaleFiniteLocallyConstantSet.exists_affine_representer
Documentation

Every finite locally constant sheaf on an affine scheme is represented by a finite étale scheme. The affine chart is removed using its actual isomorphism.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Algebra.Descent
open scoped TensorProduct
namespace EtaleCohomology
Lean source · statement
theorem IsEtaleFiniteLocallyConstantSet.exists_affine_representer
    {X : Scheme.{u}} [IsAffine X] {G : Sheaf X.smallEtaleTopology (Type u)}
    (hG : IsEtaleFiniteLocallyConstantSet G) :
    ∃ Z : FiniteEtale X, Nonempty (G.obj.RepresentableBy ((finiteEtaleToEtale X).obj Z))

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