NYLL
Module

FiniteGluing.lean

Nyll.EtaleCohomology.Constructible.FiniteGluing
3 declarations indexed from sourceView source ↗

Module documentation

Finite adapted stratifications from local pieces

A finite covering by constructible immersed pieces with finite type locally constant restrictions admits a disjoint adapted stratification. We first partition the images and then take actual fiber products with the original pieces. Thus containment of images is never used as an unproved scheme lift.

This gives finite stratifications from finite retrocompact open covers, and from affine neighborhoods on quasi-compact quasi-separated schemes.

Imports13
Imported by3

Declarations

theorem

of_finite_immersion_cover

L43 ↗
EtaleCohomology.HasFiniteConstructibleStratification.of_finite_immersion_cover
Documentation

A finite immersed constructible covering with locally constant models can be refined to an actual disjoint adapted stratification.

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
theorem HasFiniteConstructibleStratification.of_finite_immersion_cover
    {ι : Type u} [Finite ι] (Z : ι → Scheme.{u}) (f : ∀ i : ι, Z i ⟶ X)
    (hf : ∀ i : ι, IsImmersion (f i))
    (hc : ∀ i : ι, Topology.IsConstructible (Set.range (f i)))
    (hcover : ∀ x : X, ∃ i : ι, x ∈ Set.range (f i))
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : ∀ i : ι, IsEtaleFiniteTypeLocallyConstant R ((etalePullback (f i) R).obj G)) :
    HasFiniteConstructibleStratification R G
theorem

of_finite_open_cover

L92 ↗
EtaleCohomology.HasFiniteConstructibleStratification.of_finite_open_cover
Documentation

Finite adapted stratifications glue across a finite retrocompact open cover.

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
theorem HasFiniteConstructibleStratification.of_finite_open_cover
    {ι : Type u} [Finite ι] (U : ι → X.Opens)
    (hc : ∀ i : ι, IsRetrocompact (U i : Set X))
    (hcover : ∀ x : X, ∃ i : ι, x ∈ U i)
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : ∀ i : ι, HasFiniteConstructibleStratification R ((etalePullback (U i).ι R).obj G)) :
    HasFiniteConstructibleStratification R G
theorem

of_affine_neighborhoods

L124 ↗
EtaleCohomology.HasFiniteConstructibleStratification.of_affine_neighborhoods
Documentation

On a qcqs scheme, affine neighborhoods with finite stratifications give one finite stratification of the whole scheme.

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
theorem HasFiniteConstructibleStratification.of_affine_neighborhoods
    [CompactSpace X] [QuasiSeparatedSpace X]
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : ∀ x : X, ∃ U : X.affineOpens, x ∈ U.1 ∧
      HasFiniteConstructibleStratification R ((etalePullback U.1.ι R).obj G)) :
    HasFiniteConstructibleStratification R G

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