Module

LocallyConstant.lean

Nyll.EtaleCohomology.Constructible.LocallyConstant

10 declarations indexed from sourceView source ↗

Module documentation

Locally constant étale sheaves of modules

Local constancy means that an actual étale cover trivializes the sheaf as a sheafification of a constant presheaf. A predicate on the constant models allows the same base-change and cover-refinement proofs to treat arbitrary modules and finitely generated modules. No hypothesis on a base field, noetherianity, or finiteness of the coefficient ring is imposed here.

See the definitions and inverse-image property in https://stacks.math.columbia.edu/tag/09Y8 .

Imports8

Nyll.EtaleCohomology.Sites.ConstantPullback
Nyll.EtaleCohomology.Sites.PullbackComposition
Nyll.EtaleCohomology.Sites.SheafFunctors
Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.CategoryTheory.Sites.ConstantSheaf
Mathlib.CategoryTheory.Sites.Hypercover.Zero
Mathlib.RingTheory.Finiteness.Basic

Imported by11

def

IsEtaleLocallyConstantWith

L41 ↗

EtaleCohomology.IsEtaleLocallyConstantWith

Documentation

Étale locally, the sheaf is constant with a model satisfying P. The model may vary among the members of the 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}} (R : Type u) [CommRing R]

Lean source · statement

def IsEtaleLocallyConstantWith (P : ModuleCat.{u} R → Prop)
    (G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)) : Prop

def

IsEtaleLocallyConstant

L49 ↗

EtaleCohomology.IsEtaleLocallyConstant

Documentation

A sheaf of modules is locally constant if it is constant on an é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 Y : Scheme.{u}} (R : Type u) [CommRing R]

Lean source · statement

def IsEtaleLocallyConstant (G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)) : Prop

def

IsEtaleFiniteTypeLocallyConstant

L54 ↗

EtaleCohomology.IsEtaleFiniteTypeLocallyConstant

Documentation

A finite type locally constant sheaf has finitely generated constant module models on an é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 Y : Scheme.{u}} (R : Type u) [CommRing R]

Lean source · statement

def IsEtaleFiniteTypeLocallyConstant (G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)) : Prop

lemma

of_iso

L60 ↗

EtaleCohomology.IsEtaleLocallyConstantWith.of_iso

Documentation

Isomorphic sheaves have the same possible local constant models.

Source context 6 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}} (R : Type u) [CommRing R]
variable {R} {P : ModuleCat.{u} R → Prop}

Lean source · statement

lemma IsEtaleLocallyConstantWith.of_iso
    {G H : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : IsEtaleLocallyConstantWith R P G) (e : G ≅ H) :
    IsEtaleLocallyConstantWith R P H

lemma

constant

L70 ↗

EtaleCohomology.IsEtaleLocallyConstantWith.constant

Documentation

A constant sheaf is trivialized by the identity cover.

Source context 6 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}} (R : Type u) [CommRing R]
variable {R} {P : ModuleCat.{u} R → Prop}

Lean source · statement

lemma IsEtaleLocallyConstantWith.constant (M : ModuleCat.{u} R) (hM : P M) :
    IsEtaleLocallyConstantWith R P
      ((constantSheaf X.smallEtaleTopology (ModuleCat.{u} R)).obj M)

lemma

pullback

L78 ↗

EtaleCohomology.IsEtaleLocallyConstantWith.pullback

Documentation

Pulling back the trivializing cover preserves its constant models.

Source context 6 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}} (R : Type u) [CommRing R]
variable {R} {P : ModuleCat.{u} R → Prop}

Lean source · statement

lemma IsEtaleLocallyConstantWith.pullback (f : X ⟶ Y)
    {G : Sheaf Y.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : IsEtaleLocallyConstantWith R P G) :
    IsEtaleLocallyConstantWith R P ((etalePullback f R).obj G)

lemma

of_cover

L96 ↗

EtaleCohomology.IsEtaleLocallyConstantWith.of_cover

Documentation

Local constant models on every member of an étale cover give local constant models on the original scheme, by composing the covers.

Source context 6 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}} (R : Type u) [CommRing R]
variable {R} {P : ModuleCat.{u} R → Prop}

Lean source · full declaration

lemma IsEtaleLocallyConstantWith.of_cover
    (𝒰 : X.Cover.{u} (Scheme.precoverage (show MorphismProperty Scheme.{u} from @Etale)))
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : ∀ a : 𝒰.I₀,
      IsEtaleLocallyConstantWith R P ((etalePullback (𝒰.f a) R).obj G)) :
    IsEtaleLocallyConstantWith R P G := by
  choose 𝒱 h𝒱 using hG
  refine ⟨𝒰.bind 𝒱, ?_⟩
  rintro ⟨a, b⟩
  obtain ⟨M, hM, ⟨eM⟩⟩ := h𝒱 a b
  exact ⟨M, hM, ⟨(etalePullbackCompIso ((𝒱 a).f b) (𝒰.f a) R).app G ≪≫ eM⟩⟩

lemma

isEtaleLocallyConstant_iff

L110 ↗

EtaleCohomology.isEtaleLocallyConstant_iff

Documentation

The definition agrees with being constant in mathlib's sense on an étale cover.

Source context 6 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}} (R : Type u) [CommRing R]
variable {R} {P : ModuleCat.{u} R → Prop}

Lean source · full declaration

lemma isEtaleLocallyConstant_iff
    (G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)) :
    IsEtaleLocallyConstant R G ↔
      ∃ 𝒰 : X.Cover.{u} (Scheme.precoverage (show MorphismProperty Scheme.{u} from @Etale)),
        ∀ a : 𝒰.I₀,
          Sheaf.IsConstant (𝒰.X a).smallEtaleTopology ((etalePullback (𝒰.f a) R).obj G) := by
  constructor
  · rintro ⟨𝒰, h𝒰⟩
    refine ⟨𝒰, fun a => ?_⟩
    obtain ⟨M, _, ⟨eM⟩⟩ := h𝒰 a
    exact Sheaf.isConstant_of_iso (𝒰.X a).smallEtaleTopology eM
  · rintro ⟨𝒰, h𝒰⟩
    refine ⟨𝒰, fun a => ?_⟩
    have := h𝒰 a
    obtain ⟨M, ⟨eM⟩⟩ := ((etalePullback (𝒰.f a) R).obj G).mem_essImage_of_isConstant
    exact ⟨M, trivial, ⟨eM.symm⟩⟩

lemma

isEtaleLocallyConstant

L128 ↗

EtaleCohomology.IsEtaleFiniteTypeLocallyConstant.isEtaleLocallyConstant

Documentation

Forgetting finite generation gives ordinary local constancy.

Source context 6 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}} (R : Type u) [CommRing R]
variable {R} {P : ModuleCat.{u} R → Prop}

Lean source · statement

lemma IsEtaleFiniteTypeLocallyConstant.isEtaleLocallyConstant
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : IsEtaleFiniteTypeLocallyConstant R G) : IsEtaleLocallyConstant R G

lemma

isEtaleLocallyConstant_of_isConstant

L137 ↗

EtaleCohomology.isEtaleLocallyConstant_of_isConstant

Documentation

A constant sheaf in mathlib's sense is étale locally constant.

Source context 6 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}} (R : Type u) [CommRing R]
variable {R} {P : ModuleCat.{u} R → Prop}

Lean source · statement

lemma isEtaleLocallyConstant_of_isConstant
    (G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R))
    [Sheaf.IsConstant X.smallEtaleTopology G] : IsEtaleLocallyConstant R G

Module documentation

Locally constant étale sheaves of modules

Declarations