NYLL
Module

FiniteLocallyConstantSet.lean

Nyll.EtaleCohomology.Constructible.FiniteLocallyConstantSet
9 declarations indexed from sourceView source ↗

Module documentation

Finite locally constant étale sheaves of sets

A sheaf is finite locally constant if it is a constant sheaf of a finite set on an actual étale cover. The model may depend on the member of the cover. This property is local for the étale topology and is preserved by arbitrary inverse image.

The sheaf represented by any finite étale morphism has this property: its scheme-theoretic local splitting identifies its inverse image with the sheaf represented by a finite disjoint union of copies of the base, which is the corresponding finite constant sheaf. No assumption on a ground field, connectedness, or noetherianity is needed.

Finite constant sheaves are explicitly represented by finite étale schemes. The full converse for locally constant sheaves requires effective descent.

Imports12
Imported by14

Declarations

lemma

finite_copies_projection

L48 ↗
EtaleCohomology.finite_copies_projection
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 Y : Scheme.{u}}
Lean source · full declaration
lemma finite_copies_projection (X : Scheme.{u}) (ι : Type u) [Finite ι] :
    IsFinite (Sigma.desc (fun _ : ι => 𝟙 X)) := by
  let T : FiniteEtale X := MorphismProperty.Over.mk ⊤ (𝟙 X)
    (show IsFiniteEtale (𝟙 X) from ⟨⟩)
  let F := FiniteEtale.forget X ⋙ CategoryTheory.Over.forget X
  let W : FiniteEtale X := ∐ fun _ : ι => T
  let S : Over X := (FiniteEtale.forget X).obj W
  have : PreservesFiniteCoproducts F :=
    inferInstanceAs (PreservesFiniteCoproducts (FiniteEtale.forget X ⋙ Over.forget X))
  have : IsIso (sigmaComparison F (fun _ : ι => T)) := inferInstance
  have : IsFinite S.hom := W.prop.toIsFinite
  have he : sigmaComparison F (fun _ : ι => T) ≫ S.hom =
      Sigma.desc (fun _ : ι => ((FiniteEtale.forget X).obj T).hom) := by
    apply Sigma.hom_ext
    intro i
    rw [Sigma.ι_comp_desc, ← Category.assoc, ι_comp_sigmaComparison]
    exact Over.w ((FiniteEtale.forget X).map (Sigma.ι (fun _ : ι => T) i))
  have hfin : IsFinite (sigmaComparison F (fun _ : ι => T) ≫ S.hom) := inferInstance
  rw [he] at hfin
  exact hfin
def

finiteEtaleCopies

L71 ↗
EtaleCohomology.finiteEtaleCopies
Documentation

A finite disjoint union of copies of the base as a finite étale scheme. Finiteness follows from the existing finite-coproduct preservation theorem.

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 Y : Scheme.{u}}
Lean source · statement
def finiteEtaleCopies (X : Scheme.{u}) (ι : Type u) [Finite ι] : FiniteEtale X
def

finiteEtaleCopiesSheafIso

L77 ↗
EtaleCohomology.finiteEtaleCopiesSheafIso
Documentation

The finite constant sheaf is represented by the corresponding finite étale scheme.

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 Y : Scheme.{u}}
Lean source · statement
def finiteEtaleCopiesSheafIso (X : Scheme.{u}) (ι : Type u) [Finite ι] :
    (finiteEtaleSheaf X).obj (finiteEtaleCopies X ι) ≅
      (constantSheaf X.smallEtaleTopology (Type u)).obj ι
def

IsEtaleFiniteLocallyConstantSet

L83 ↗
EtaleCohomology.IsEtaleFiniteLocallyConstantSet
Documentation

An actual étale cover trivializes the sheaf with finite set models.

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 Y : Scheme.{u}}
Lean source · statement
def IsEtaleFiniteLocallyConstantSet (G : Sheaf X.smallEtaleTopology (Type u)) : Prop
lemma

of_iso

L90 ↗
EtaleCohomology.IsEtaleFiniteLocallyConstantSet.of_iso
Documentation

Finite local constancy is invariant under isomorphisms of sheaves.

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 Y : Scheme.{u}}
Lean source · statement
lemma IsEtaleFiniteLocallyConstantSet.of_iso
    {G H : Sheaf X.smallEtaleTopology (Type u)}
    (hG : IsEtaleFiniteLocallyConstantSet G) (e : G ≅ H) :
    IsEtaleFiniteLocallyConstantSet H
lemma

constant

L100 ↗
EtaleCohomology.IsEtaleFiniteLocallyConstantSet.constant
Documentation

A finite constant sheaf is trivialized by the identity 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 Y : Scheme.{u}}
Lean source · statement
lemma IsEtaleFiniteLocallyConstantSet.constant (A : Type u) [Finite A] :
    IsEtaleFiniteLocallyConstantSet ((constantSheaf X.smallEtaleTopology (Type u)).obj A)
lemma

pullback

L107 ↗
EtaleCohomology.IsEtaleFiniteLocallyConstantSet.pullback
Documentation

Pulling back a trivializing cover preserves its finite constant models.

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 Y : Scheme.{u}}
Lean source · statement
lemma IsEtaleFiniteLocallyConstantSet.pullback (f : X ⟶ Y)
    {G : Sheaf Y.smallEtaleTopology (Type u)} (hG : IsEtaleFiniteLocallyConstantSet G) :
    IsEtaleFiniteLocallyConstantSet ((etaleSetPullback f).obj G)
lemma

of_cover

L122 ↗
EtaleCohomology.IsEtaleFiniteLocallyConstantSet.of_cover
Documentation

Finite local constancy descends through an étale cover by composing covers.

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 Y : Scheme.{u}}
Lean source · full declaration
lemma IsEtaleFiniteLocallyConstantSet.of_cover
    (𝒰 : X.Cover.{u} (Scheme.precoverage (show MorphismProperty Scheme.{u} from @Etale)))
    {G : Sheaf X.smallEtaleTopology (Type u)}
    (hG : ∀ a : 𝒰.I₀, IsEtaleFiniteLocallyConstantSet ((etaleSetPullback (𝒰.f a)).obj G)) :
    IsEtaleFiniteLocallyConstantSet G := by
  choose 𝒱 h𝒱 using hG
  refine ⟨𝒰.bind 𝒱, ?_⟩
  rintro ⟨a, b⟩
  obtain ⟨A, hA, ⟨eA⟩⟩ := h𝒱 a b
  exact ⟨A, hA, ⟨(etaleSetPullbackCompIso ((𝒱 a).f b) (𝒰.f a)).app G ≪≫ eA⟩⟩
theorem

finiteEtaleSheaf_isEtaleFiniteLocallyConstantSet

L134 ↗
EtaleCohomology.finiteEtaleSheaf_isEtaleFiniteLocallyConstantSet
Documentation

The sheaf represented by a finite étale cover is finite locally constant.

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 Y : Scheme.{u}}
Lean source · statement
theorem finiteEtaleSheaf_isEtaleFiniteLocallyConstantSet (W : FiniteEtale X) :
    IsEtaleFiniteLocallyConstantSet ((finiteEtaleSheaf X).obj W)

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