NYLL
Module

Pullback.lean

Nyll.EtaleCohomology.Constructible.Pullback
10 declarations indexed from sourceView source ↗

Module documentation

Pulling back finite constructible stratifications

Open retrocompact subsets correspond to quasi-compact open immersions. Stability of quasi-compactness under base change shows that arbitrary scheme morphisms preserve constructible subsets by inverse image. Hence the actual fiber products of the strata form a finite constructible stratification.

An adapted stratification pulls back using its projection to each old stratum and the composition isomorphism for inverse image of étale sheaves. In particular constructible sheaves on an affine target pull back to constructible sheaves on arbitrary schemes, without restrictions on the morphism or the coefficient ring.

Imports12
Imported by2

Declarations

lemma

isRetrocompact_preimage_of_isOpen

L46 ↗
EtaleCohomology.isRetrocompact_preimage_of_isOpen
Documentation

Open retrocompact subsets remain retrocompact under arbitrary scheme inverse images.

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 Y : Scheme.{u}}
Lean source · statement
lemma isRetrocompact_preimage_of_isOpen (f : X ⟶ Y) {s : Set Y}
    (hs : IsOpen s) (hc : IsRetrocompact s) : IsRetrocompact (f ⁻¹' s)
lemma

isConstructible_preimage

L57 ↗
EtaleCohomology.isConstructible_preimage
Documentation

Constructible subsets pull back under arbitrary morphisms of schemes.

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 Y : Scheme.{u}}
Lean source · statement
lemma isConstructible_preimage (f : X ⟶ Y) {s : Set Y}
    (hs : Topology.IsConstructible s) : Topology.IsConstructible (f ⁻¹' s)
def

pullback

L64 ↗
EtaleCohomology.ConstructibleStratification.pullback
Documentation

Base change of the actual locally closed strata along an arbitrary scheme morphism.

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 Y : Scheme.{u}}
namespace ConstructibleStratification
Lean source · full declaration
def pullback (S : ConstructibleStratification Y) (f : X ⟶ Y) :
    ConstructibleStratification X where
  I := S.I
  finite := S.finite
  stratum i := Limits.pullback (S.map i) f
  map i := Limits.pullback.snd (S.map i) f
  isImmersion i := by
    have : IsImmersion (S.map i) := S.isImmersion i
    infer_instance
  constructible_range i := by
    rw [Scheme.Pullback.range_snd]
    exact isConstructible_preimage f (S.constructible_range i)
  disjoint := by
    intro i j hne
    rw [Scheme.Pullback.range_snd, Scheme.Pullback.range_snd]
    exact Set.disjoint_left.mpr (fun _ hx hy => Set.disjoint_left.mp (S.disjoint hne) hx hy)
  cover x := by
    obtain ⟨i, hi⟩ := S.cover (f x)
    refine ⟨i, ?_⟩
    rw [Scheme.Pullback.range_snd]
    exact hi
def

pullbackFst

L87 ↗
EtaleCohomology.ConstructibleStratification.pullbackFst
Documentation

The base-changed stratum has its actual projection to the original stratum.

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 Y : Scheme.{u}}
namespace ConstructibleStratification
Lean source · statement
def pullbackFst (S : ConstructibleStratification Y) (f : X ⟶ Y) (i : S.I) :
    (S.pullback f).stratum i ⟶ S.stratum i
lemma

pullbackFst_map

L92 ↗
EtaleCohomology.ConstructibleStratification.pullbackFst_map
Documentation

The projections commute over the original base scheme.

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 Y : Scheme.{u}}
namespace ConstructibleStratification
Lean source · statement
lemma pullbackFst_map (S : ConstructibleStratification Y) (f : X ⟶ Y) (i : S.I) :
    S.pullbackFst f i ≫ S.map i = (S.pullback f).map i ≫ f
lemma

pullback_isPullback

L97 ↗
EtaleCohomology.ConstructibleStratification.pullback_isPullback
Documentation

Each new stratum is the scheme fiber product, not just a subset with a claimed lift.

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 Y : Scheme.{u}}
namespace ConstructibleStratification
Lean source · statement
lemma pullback_isPullback (S : ConstructibleStratification Y) (f : X ⟶ Y) (i : S.I) :
    IsPullback (S.pullbackFst f i) ((S.pullback f).map i) (S.map i) f
lemma

pullback_range

L102 ↗
EtaleCohomology.ConstructibleStratification.pullback_range
Documentation

Base change gives exactly the inverse image of each stratum.

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 Y : Scheme.{u}}
namespace ConstructibleStratification
Lean source · statement
lemma pullback_range (S : ConstructibleStratification Y) (f : X ⟶ Y) (i : S.I) :
    Set.range ((S.pullback f).map i) = f ⁻¹' Set.range (S.map i)
lemma

pullback

L111 ↗
EtaleCohomology.ConstructibleStratification.IsAdaptedTo.pullback
Documentation

Pullback of finite type local constant models adapts the base-changed 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 Y : Scheme.{u}}
variable {R : Type u} [CommRing R]
Lean source · statement
lemma ConstructibleStratification.IsAdaptedTo.pullback
    {S : ConstructibleStratification Y} (f : X ⟶ Y)
    {G : Sheaf Y.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : S.IsAdaptedTo R G) :
    (S.pullback f).IsAdaptedTo R ((etalePullback f R).obj G)
lemma

pullback

L123 ↗
EtaleCohomology.HasFiniteConstructibleStratification.pullback
Documentation

A global finite adapted stratification pulls back along any scheme morphism.

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 Y : Scheme.{u}}
variable {R : Type u} [CommRing R]
Lean source · statement
lemma HasFiniteConstructibleStratification.pullback (f : X ⟶ Y)
    {G : Sheaf Y.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : HasFiniteConstructibleStratification R G) :
    HasFiniteConstructibleStratification R ((etalePullback f R).obj G)
lemma

pullback_of_isAffine

L132 ↗
EtaleCohomology.IsEtaleConstructible.pullback_of_isAffine
Documentation

On an affine target constructibility pulls back along an arbitrary morphism, even when its source is not affine or quasi-compact.

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 Y : Scheme.{u}}
variable {R : Type u} [CommRing R]
Lean source · statement
lemma IsEtaleConstructible.pullback_of_isAffine [IsAffine Y] (f : X ⟶ Y)
    {G : Sheaf Y.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : IsEtaleConstructible R G) :
    IsEtaleConstructible R ((etalePullback f 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.