Module

OpenClosed.lean

Nyll.EtaleCohomology.Constructible.OpenClosed

3 declarations indexed from sourceView source ↗

Module documentation

Constructibility across an open and its closed complement

Finite adapted stratifications on complementary pieces give one on the whole scheme when the open image is retrocompact. Affine-local base change then proves the criterion on arbitrary schemes. The condition on the open image is essential over non-noetherian bases.

Imports8

Nyll.EtaleCohomology.Constructible.FiniteGluing
Nyll.EtaleCohomology.Constructible.Locality
Nyll.EtaleCohomology.Sites.PullbackComposition
Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.Topology.Constructible

Imported by2

lemma

range_retrocompact

L31 ↗

EtaleCohomology.range_retrocompact

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 U Z : Scheme.{u}} {R : Type u} [CommRing R]

Lean source · statement

lemma range_retrocompact {Y : Scheme.{u}} (f : Y ⟶ X) [QuasiCompact f] :
    IsRetrocompact (Set.range f)

theorem

of_open_closed

L39 ↗

EtaleCohomology.HasFiniteConstructibleStratification.of_open_closed

Documentation

Finite stratifications on complementary open and closed subschemes glue, provided the open image is retrocompact.

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 U Z : Scheme.{u}} {R : Type u} [CommRing R]

Lean source · statement

theorem HasFiniteConstructibleStratification.of_open_closed
    (j : U ⟶ X) [IsOpenImmersion j] (i : Z ⟶ X) [IsClosedImmersion i]
    (hcompl : Set.range j = (Set.range i)ᶜ) (hj : IsRetrocompact (Set.range j))
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hU : HasFiniteConstructibleStratification R ((etalePullback j R).obj G))
    (hZ : HasFiniteConstructibleStratification R ((etalePullback i R).obj G)) :
    HasFiniteConstructibleStratification R G

theorem

of_open_closed

L88 ↗

EtaleCohomology.IsEtaleConstructible.of_open_closed

Documentation

Constructibility can be tested on a quasi-compact open immersion and its closed complement, without a noetherian hypothesis on the 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 U Z : Scheme.{u}} {R : Type u} [CommRing R]

Lean source · statement

theorem IsEtaleConstructible.of_open_closed
    (j : U ⟶ X) [IsOpenImmersion j] [QuasiCompact j]
    (i : Z ⟶ X) [IsClosedImmersion i]
    (hcompl : Set.range j = (Set.range i)ᶜ)
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hU : IsEtaleConstructible R ((etalePullback j R).obj G))
    (hZ : IsEtaleConstructible R ((etalePullback i R).obj G)) : IsEtaleConstructible R G

Module documentation

Constructibility across an open and its closed complement

Declarations

range_retrocompact

of_open_closed

of_open_closed