Module

Basic.lean

Nyll.EtaleCohomology.Constructible.Basic

17 declarations indexed from sourceView source ↗

Module documentation

Constructible étale sheaves of modules

A finite constructible stratification is adapted to a module sheaf when its inverse image on each actual locally closed stratum is finite type locally constant. Constructibility requires such a stratification on every affine open subscheme. Thus the definition does not assume that the whole scheme has a finite stratification, nor that the scheme or coefficient ring is noetherian.

Finite type locally constant sheaves satisfy this definition. Adapted finite stratifications can be refined simultaneously using actual fiber products.

Imports11

Nyll.EtaleCohomology.Constructible.LocallyConstant
Nyll.EtaleCohomology.Constructible.LocallyConstantProducts
Nyll.EtaleCohomology.Constructible.Stratification
Nyll.EtaleCohomology.Sites.PullbackComposition
Nyll.EtaleCohomology.Sites.PullbackStalks
Nyll.EtaleCohomology.Sites.SheafFunctors
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Sites.Etale
Mathlib.CategoryTheory.Sites.Sheaf
Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts

Imported by8

def

IsAdaptedTo

L45 ↗

EtaleCohomology.ConstructibleStratification.IsAdaptedTo

Documentation

A stratification is adapted to a sheaf if its restrictions to all strata are finite type locally constant.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]

Lean source · statement

def ConstructibleStratification.IsAdaptedTo (S : ConstructibleStratification X)
    (G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)) : Prop

def

HasFiniteConstructibleStratification

L50 ↗

EtaleCohomology.HasFiniteConstructibleStratification

Documentation

The sheaf admits one finite constructible stratification on the whole base.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]

Lean source · statement

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

def

IsEtaleConstructible

L55 ↗

EtaleCohomology.IsEtaleConstructible

Documentation

Constructibility is finite stratifiability on every affine open subscheme.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]

Lean source · statement

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

lemma

of_iso

L62 ↗

EtaleCohomology.ConstructibleStratification.IsAdaptedTo.of_iso

Documentation

Transport an adapted stratification along a genuine sheaf isomorphism.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]
variable {R}

Lean source · statement

lemma ConstructibleStratification.IsAdaptedTo.of_iso
    {S : ConstructibleStratification X}
    {G H : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : S.IsAdaptedTo R G) (e : G ≅ H) : S.IsAdaptedTo R H

lemma

commonRefinementLeft

L70 ↗

EtaleCohomology.ConstructibleStratification.IsAdaptedTo.commonRefinementLeft

Documentation

The fiber-product refinement remains adapted to the first sheaf.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]
variable {R}

Lean source · statement

lemma ConstructibleStratification.IsAdaptedTo.commonRefinementLeft
    {S : ConstructibleStratification X} (T : ConstructibleStratification X)
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : S.IsAdaptedTo R G) : (S.commonRefinement T).IsAdaptedTo R G

lemma

commonRefinementRight

L79 ↗

EtaleCohomology.ConstructibleStratification.IsAdaptedTo.commonRefinementRight

Documentation

The fiber-product refinement remains adapted to the second sheaf.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]
variable {R}

Lean source · statement

lemma ConstructibleStratification.IsAdaptedTo.commonRefinementRight
    (S : ConstructibleStratification X) {T : ConstructibleStratification X}
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : T.IsAdaptedTo R G) : (S.commonRefinement T).IsAdaptedTo R G

lemma

prod

L90 ↗

EtaleCohomology.ConstructibleStratification.IsAdaptedTo.prod

Documentation

A common adapted stratification is also adapted to the binary product.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]
variable {R}

Lean source · statement

lemma ConstructibleStratification.IsAdaptedTo.prod
    {S : ConstructibleStratification X}
    {G H : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : S.IsAdaptedTo R G) (hH : S.IsAdaptedTo R H) :
    S.IsAdaptedTo R (G ⨯ H)

lemma

restrict

L100 ↗

EtaleCohomology.ConstructibleStratification.IsAdaptedTo.restrict

Documentation

Restricting actual strata to an open subscheme preserves adaptedness.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]
variable {R}

Lean source · statement

lemma ConstructibleStratification.IsAdaptedTo.restrict
    {S : ConstructibleStratification X} (U : X.Opens)
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : S.IsAdaptedTo R G) :
    (S.restrict U).IsAdaptedTo R ((etalePullback U.ι R).obj G)

lemma

hasFiniteConstructibleStratification

L112 ↗

EtaleCohomology.IsEtaleFiniteTypeLocallyConstant.hasFiniteConstructibleStratification

Documentation

Finite type local constancy supplies the one-stratum finite stratification.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]
variable {R}

Lean source · statement

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

lemma

of_iso

L120 ↗

EtaleCohomology.HasFiniteConstructibleStratification.of_iso

Documentation

The same finite stratification works for isomorphic sheaves.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]
variable {R}

Lean source · statement

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

theorem

exists_common

L128 ↗

EtaleCohomology.HasFiniteConstructibleStratification.exists_common

Documentation

Two finitely stratifiable sheaves admit one common adapted stratification.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]
variable {R}

Lean source · statement

theorem HasFiniteConstructibleStratification.exists_common
    {G H : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : HasFiniteConstructibleStratification R G)
    (hH : HasFiniteConstructibleStratification R H) :
    ∃ S : ConstructibleStratification X, S.IsAdaptedTo R G ∧ S.IsAdaptedTo R H

lemma

prod

L138 ↗

EtaleCohomology.HasFiniteConstructibleStratification.prod

Documentation

Common refinement supplies finite stratifiability of a binary product.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]
variable {R}

Lean source · statement

lemma HasFiniteConstructibleStratification.prod
    {G H : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : HasFiniteConstructibleStratification R G)
    (hH : HasFiniteConstructibleStratification R H) :
    HasFiniteConstructibleStratification R (G ⨯ H)

lemma

restrict

L147 ↗

EtaleCohomology.HasFiniteConstructibleStratification.restrict

Documentation

A finite adapted stratification restricts to every open subscheme.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]
variable {R}

Lean source · statement

lemma HasFiniteConstructibleStratification.restrict
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : HasFiniteConstructibleStratification R G) (U : X.Opens) :
    HasFiniteConstructibleStratification R ((etalePullback U.ι R).obj G)

lemma

isEtaleConstructible

L155 ↗

EtaleCohomology.HasFiniteConstructibleStratification.isEtaleConstructible

Documentation

One global finite adapted stratification supplies the affine-local definition.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]
variable {R}

Lean source · statement

lemma HasFiniteConstructibleStratification.isEtaleConstructible
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : HasFiniteConstructibleStratification R G) : IsEtaleConstructible R G

lemma

isEtaleConstructible

L161 ↗

EtaleCohomology.IsEtaleFiniteTypeLocallyConstant.isEtaleConstructible

Documentation

Finite type locally constant sheaves are constructible on arbitrary schemes.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]
variable {R}

Lean source · statement

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

lemma

of_iso

L169 ↗

EtaleCohomology.IsEtaleConstructible.of_iso

Documentation

Constructibility is invariant under isomorphism.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]
variable {R}

Lean source · statement

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

lemma

prod

L176 ↗

EtaleCohomology.IsEtaleConstructible.prod

Documentation

Binary products of constructible module sheaves are constructible.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} (R : Type u) [CommRing R]
variable {R}

Lean source · statement

lemma IsEtaleConstructible.prod
    {G H : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : IsEtaleConstructible R G) (hH : IsEtaleConstructible R H) :
    IsEtaleConstructible R (G ⨯ H)

Module documentation

Constructible étale sheaves of modules

Declarations