NYLL
Module

AffineLocalRepresenter.lean

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

Module documentation

A single affine cover with a finite étale representer

A finite locally constant set sheaf on a quasi-compact scheme becomes represented by a finite étale scheme after ordinary restriction to one affine surjective étale cover. We combine a finite affine family of local representers by its disjoint union. Over an affine base, the same cover supplies a faithfully flat étale map on global section rings. Neither construction assumes a ground field, noetherianity, or quasi-separatedness.

Imports13
Imported by2

Declarations

theorem

exists_affine_localRepresenter

L44 ↗
EtaleCohomology.IsEtaleFiniteLocallyConstantSet.exists_affine_localRepresenter
Documentation

On a quasi-compact base, a finite locally constant set sheaf has a finite étale representer after restriction to one affine surjective étale cover.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {G : Sheaf X.smallEtaleTopology (Type u)}
Lean source · statement
theorem IsEtaleFiniteLocallyConstantSet.exists_affine_localRepresenter
    [CompactSpace X] (hG : IsEtaleFiniteLocallyConstantSet G) :
    ∃ (V : Scheme.{u}) (f : V ⟶ X) (hf : Etale f),
      IsAffine V ∧ Surjective f ∧ ∃ W : FiniteEtale V,
        Nonempty (((etalePostcompose (hf := hf) f).op ⋙ G.obj).RepresentableBy
          ((finiteEtaleToEtale V).obj W))
theorem

exists_affine_localRepresenter_faithfullyFlat

L74 ↗
EtaleCohomology.IsEtaleFiniteLocallyConstantSet.exists_affine_localRepresenter_faithfullyFlat
Documentation

Over an affine base, the actual affine cover carrying the representer has a faithfully flat étale map on global sections, suitable for algebra descent.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {G : Sheaf X.smallEtaleTopology (Type u)}
Lean source · statement
theorem IsEtaleFiniteLocallyConstantSet.exists_affine_localRepresenter_faithfullyFlat
    [IsAffine X] (hG : IsEtaleFiniteLocallyConstantSet G) :
    ∃ (V : Scheme.{u}) (f : V ⟶ X) (hf : Etale f),
      IsAffine V ∧ Surjective f ∧ f.appTop.hom.FaithfullyFlat ∧ f.appTop.hom.Etale ∧
        ∃ W : FiniteEtale V,
          Nonempty (((etalePostcompose (hf := hf) f).op ⋙ G.obj).RepresentableBy
            ((finiteEtaleToEtale V).obj W))

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