NYLL
Module

Locality.lean

Nyll.EtaleCohomology.Constructible.Locality
4 declarations indexed from sourceView source ↗

Module documentation

Zariski locality and arbitrary pullback of constructible étale sheaves

On a qcqs scheme, affine-local constructibility is equivalent to a finite adapted stratification. On any scheme it is Zariski local. Pullback along any scheme morphism preserves constructibility: affine neighborhoods of source points map into affine opens of the target, and their finite stratifications glue by the preceding geometric refinement theorem.

Imports11
Imported by2

Declarations

theorem

hasFiniteConstructibleStratification

L38 ↗
EtaleCohomology.IsEtaleConstructible.hasFiniteConstructibleStratification
Documentation

A constructible sheaf on a qcqs scheme admits one finite adapted stratification.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology
variable {X Y : Scheme.{u}} {R : Type u} [CommRing R]
Lean source · statement
theorem IsEtaleConstructible.hasFiniteConstructibleStratification
    [CompactSpace X] [QuasiSeparatedSpace X]
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)} (hG : IsEtaleConstructible R G) :
    HasFiniteConstructibleStratification R G
theorem

pullback

L49 ↗
EtaleCohomology.IsEtaleConstructible.pullback
Documentation

Constructibility pulls back along every scheme morphism, with no quasi-compactness, separation, or noetherianity condition on the morphism.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology
variable {X Y : Scheme.{u}} {R : Type u} [CommRing R]
Lean source · statement
theorem IsEtaleConstructible.pullback (f : X ⟶ Y)
    {G : Sheaf Y.smallEtaleTopology (ModuleCat.{u} R)} (hG : IsEtaleConstructible R G) :
    IsEtaleConstructible R ((etalePullback f R).obj G)
theorem

of_open_neighborhoods

L77 ↗
EtaleCohomology.IsEtaleConstructible.of_open_neighborhoods
Documentation

Constructibility can be verified on an open neighborhood of each point.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology
variable {X Y : Scheme.{u}} {R : Type u} [CommRing R]
Lean source · statement
theorem IsEtaleConstructible.of_open_neighborhoods
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : ∀ x : X, ∃ U : X.Opens, x ∈ U ∧
      IsEtaleConstructible R ((etalePullback U.ι R).obj G)) :
    IsEtaleConstructible R G
theorem

isEtaleConstructible_iff_open_cover

L102 ↗
EtaleCohomology.isEtaleConstructible_iff_open_cover
Documentation

Constructibility is local for an arbitrary family of open subsets covering the base.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology
variable {X Y : Scheme.{u}} {R : Type u} [CommRing R]
Lean source · statement
theorem isEtaleConstructible_iff_open_cover {ι : Type u} (U : ι → X.Opens)
    (hcover : ∀ x : X, ∃ i : ι, x ∈ U i)
    (G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)) :
    IsEtaleConstructible R G ↔
      ∀ i : ι, IsEtaleConstructible R ((etalePullback (U i).ι R).obj G)

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