Module

PullbackStalks.lean

Nyll.EtaleCohomology.Sites.PullbackStalks

9 declarations indexed from sourceView source ↗

Module documentation

Geometric stalks of inverse image

The pullback adjunction for over categories identifies geometric lifts through base change. This identifies the corresponding points of the small étale site and supplies the smallness needed for their stalks.

Taking mates under the constructed inverse-image/direct-image adjunction and the stalk/skyscraper adjunction gives the stalk formula for inverse image. Geometric stalks then detect preservation of short exact sequences.

Imports26

Nyll.EtaleCohomology.Sites.BaseChange
Nyll.EtaleCohomology.Sites.SheafFunctors
Nyll.EtaleCohomology.Sites.Stalks
Mathlib.Algebra.Category.ModuleCat.AB
Mathlib.Algebra.Category.ModuleCat.Colimits
Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Mathlib.Algebra.Category.ModuleCat.Limits
Mathlib.Algebra.Homology.ShortComplex.Basic
Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Mathlib.Algebra.Homology.ShortComplex.ShortExact
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.CategoryTheory.Comma.Over.Pullback
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.Adjunction.Mates
Mathlib.CategoryTheory.Category.Cat
Mathlib.CategoryTheory.Sites.Point.Basic
Mathlib.CategoryTheory.Sites.Point.Comap
Mathlib.CategoryTheory.Sites.Point.Category
Mathlib.CategoryTheory.Sites.Point.Skyscraper
Mathlib.CategoryTheory.Elements
Mathlib.CategoryTheory.Functor.Flat
Mathlib.CategoryTheory.Limits.Final
Mathlib.CategoryTheory.Limits.FinallySmall
Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Mathlib.CategoryTheory.Preadditive.Biproducts

Imported by15

def

geometricFiberBaseChangeIso

L59 ↗

EtaleCohomology.geometricFiberBaseChangeIso

Documentation

Geometric lifts through a base change are lifts of the composite geometric point.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X)

Lean source · statement

def geometricFiberBaseChangeIso :
    etaleBaseChange f ⋙ (Scheme.pointSmallEtale s).fiber ≅
      (Scheme.pointSmallEtale (s ≫ f)).fiber

instance

(anonymous instance)

L65 ↗

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X)

Lean source · statement

instance : InitiallySmall.{u}
    (etaleBaseChange f ⋙ (Scheme.pointSmallEtale s).fiber).Elements

instance

(anonymous instance)

L77 ↗

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X)

Lean source · statement

instance : RepresentablyFlat (etaleBaseChange f)

def

geometricPointComapIso

L80 ↗

EtaleCohomology.geometricPointComapIso

Documentation

The inverse image of the site point is the composite geometric point.

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X)
local instance : RepresentablyFlat (etaleBaseChange f) := flat_of_preservesFiniteLimits _

Lean source · full declaration

def geometricPointComapIso :
    (Scheme.pointSmallEtale s).comap (etaleBaseChange f) (etaleBaseChange_coverPreserving f) ≅
      Scheme.pointSmallEtale (s ≫ f) where
  hom := ⟨(geometricFiberBaseChangeIso f s).inv⟩
  inv := ⟨(geometricFiberBaseChangeIso f s).hom⟩
  hom_inv_id := by
    apply GrothendieckTopology.Point.Hom.ext
    exact (geometricFiberBaseChangeIso f s).hom_inv_id
  inv_hom_id := by
    apply GrothendieckTopology.Point.Hom.ext
    exact (geometricFiberBaseChangeIso f s).inv_hom_id

def

geometricComapSheafFiberIso

L95 ↗

EtaleCohomology.geometricComapSheafFiberIso

Documentation

The stalk at the comapped geometric point is the stalk at its composite point.

Source context 8 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X)
local instance : RepresentablyFlat (etaleBaseChange f) := flat_of_preservesFiniteLimits _
variable (R : Type u) [CommRing R]

Lean source · full declaration

def geometricComapSheafFiberIso :
    ((Scheme.pointSmallEtale s).comap (etaleBaseChange f)
      (etaleBaseChange_coverPreserving f)).sheafFiber (A := ModuleCat.{u} R) ≅
      (Scheme.pointSmallEtale (s ≫ f)).sheafFiber where
  hom := (geometricPointComapIso f s).inv.sheafFiber
  inv := (geometricPointComapIso f s).hom.sheafFiber
  hom_inv_id := by
    rw [← GrothendieckTopology.Point.Hom.sheafFiber_comp, Iso.hom_inv_id,
      GrothendieckTopology.Point.Hom.sheafFiber_id]
  inv_hom_id := by
    rw [← GrothendieckTopology.Point.Hom.sheafFiber_comp, Iso.inv_hom_id,
      GrothendieckTopology.Point.Hom.sheafFiber_id]

def

etalePullbackStalkIso

L109 ↗

EtaleCohomology.etalePullbackStalkIso

Documentation

The geometric stalk of inverse image is the stalk at the composite geometric point.

Source context 8 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X)
local instance : RepresentablyFlat (etaleBaseChange f) := flat_of_preservesFiniteLimits _
variable (R : Type u) [CommRing R]

Lean source · statement

def etalePullbackStalkIso :
    etalePullback f R ⋙ (Scheme.pointSmallEtale s).sheafFiber ≅
      (Scheme.pointSmallEtale (s ≫ f)).sheafFiber

lemma

etalePullback_shortExact

L122 ↗

EtaleCohomology.etalePullback_shortExact

Documentation

Inverse image on the small étale sites preserves short exact sequences.

Source context 8 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X)
local instance : RepresentablyFlat (etaleBaseChange f) := flat_of_preservesFiniteLimits _
variable (R : Type u) [CommRing R]

Lean source · statement

lemma etalePullback_shortExact
    (S : ShortComplex (Sheaf Y.smallEtaleTopology (ModuleCat.{u} R)))
    (hS : S.ShortExact) : (S.map (etalePullback f R)).ShortExact

instance

etalePullback_additive

L134 ↗

EtaleCohomology.etalePullback_additive

Source context 8 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X)
local instance : RepresentablyFlat (etaleBaseChange f) := flat_of_preservesFiniteLimits _
variable (R : Type u) [CommRing R]

Lean source · statement

instance etalePullback_additive : (etalePullback f R).Additive

instance

etalePullback_preservesFiniteLimits

L139 ↗

EtaleCohomology.etalePullback_preservesFiniteLimits

Source context 8 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X)
local instance : RepresentablyFlat (etaleBaseChange f) := flat_of_preservesFiniteLimits _
variable (R : Type u) [CommRing R]

Lean source · statement

instance etalePullback_preservesFiniteLimits : PreservesFiniteLimits (etalePullback f R)

Module documentation

Geometric stalks of inverse image

Declarations