Module

ExtensionByZeroStalks.lean

Nyll.EtaleCohomology.Sites.ExtensionByZeroStalks

8 declarations indexed from sourceView source ↗

Module documentation

Stalks and exactness of extension by zero

For an open immersion, a geometric lift through an étale scheme over the open subscheme is already a lift over that subscheme. This gives the fiber comparison used by the general site result in Sites.StalkAdjunction.

The stalk of extension by zero agrees with the original stalk inside the open subscheme and vanishes outside it. Geometric stalks then prove preservation of short exact sequences and finite limits. The schemes and commutative coefficient ring are arbitrary; no base field or finiteness hypothesis is used.

Reference: https://stacks.math.columbia.edu/tag/03S2

Imports19

Nyll.EtaleCohomology.Sites.ExtensionByZero
Nyll.EtaleCohomology.Sites.StalkAdjunction
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.Exact
Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Mathlib.Algebra.Homology.ShortComplex.ShortExact
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.Comma.Over.Basic
Mathlib.CategoryTheory.NatIso
Mathlib.CategoryTheory.Sites.Point.Skyscraper
Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Mathlib.CategoryTheory.Preadditive.Biproducts

Imported by4

def

openGeometricFiberEquiv

L54 ↗

EtaleCohomology.openGeometricFiberEquiv

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 {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ U)

Lean source · full declaration

def openGeometricFiberEquiv (V : U.Etale) :
    (Scheme.pointSmallEtale (s ≫ j)).fiber.obj ((openEtaleInclusion j).obj V) ≃
      (Scheme.pointSmallEtale s).fiber.obj V where
  toFun a := CategoryTheory.Over.homMk a.left (by
    apply (cancel_mono j).mp
    exact (Category.assoc _ _ _).trans (CategoryTheory.Over.w a))
  invFun b := CategoryTheory.Over.homMk b.left
    ((Category.assoc _ _ _).symm.trans (congrArg (fun k => k ≫ j) (CategoryTheory.Over.w b)))
  left_inv a := CategoryTheory.Over.OverMorphism.ext rfl
  right_inv b := CategoryTheory.Over.OverMorphism.ext rfl

def

openGeometricFiberIso

L66 ↗

EtaleCohomology.openGeometricFiberIso

Documentation

Restriction of the geometric fiber at an image point is the original geometric fiber.

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 {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ U)

Lean source · statement

def openGeometricFiberIso :
    openEtaleInclusion j ⋙ (Scheme.pointSmallEtale (s ≫ j)).fiber ≅
      (Scheme.pointSmallEtale s).fiber

def

etaleExtensionByZeroStalkIso

L77 ↗

EtaleCohomology.etaleExtensionByZeroStalkIso

Documentation

Inside the open subscheme, extension by zero has the original geometric stalk.

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 {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ U)
variable (R : Type u) [CommRing R]

Lean source · statement

def etaleExtensionByZeroStalkIso :
    etaleExtensionByZero j R ⋙ (Scheme.pointSmallEtale (s ≫ j)).sheafFiber ≅
      (Scheme.pointSmallEtale s).sheafFiber

lemma

etaleExtensionByZero_stalk_isZero

L87 ↗

EtaleCohomology.etaleExtensionByZero_stalk_isZero

Documentation

A geometric point with no lift to the open subscheme has zero stalk after extension.

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 {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ U)
variable (R : Type u) [CommRing R]

Lean source · statement

lemma etaleExtensionByZero_stalk_isZero (t : Spec (.of Ω) ⟶ X)
    (h : ∀ r : Spec (.of Ω) ⟶ U, r ≫ j ≠ t)
    (F : Sheaf U.smallEtaleTopology (ModuleCat.{u} R)) :
    IsZero ((Scheme.pointSmallEtale t).sheafFiber.obj ((etaleExtensionByZero j R).obj F))

lemma

etaleExtensionByZero_shortExact

L99 ↗

EtaleCohomology.etaleExtensionByZero_shortExact

Documentation

Extension by zero preserves short exact sequences of coefficient sheaves.

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 {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ U)
variable (R : Type u) [CommRing R]

Lean source · statement

lemma etaleExtensionByZero_shortExact
    (S : ShortComplex (Sheaf U.smallEtaleTopology (ModuleCat.{u} R)))
    (hS : S.ShortExact) : (S.map (etaleExtensionByZero j R)).ShortExact

lemma

etaleExtensionByZero_stalk_isZero_of_not_mem_range

L124 ↗

EtaleCohomology.etaleExtensionByZero_stalk_isZero_of_not_mem_range

Documentation

The stalk vanishes at a geometric point outside the image of the open immersion.

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 {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ U)
variable (R : Type u) [CommRing R]

Lean source · statement

lemma etaleExtensionByZero_stalk_isZero_of_not_mem_range
    (t : Spec (.of Ω) ⟶ X) (z : Spec (.of Ω)) (hz : t z ∉ Set.range j)
    (F : Sheaf U.smallEtaleTopology (ModuleCat.{u} R)) :
    IsZero ((Scheme.pointSmallEtale t).sheafFiber.obj ((etaleExtensionByZero j R).obj F))

instance

etaleExtensionByZero_additive

L134 ↗

EtaleCohomology.etaleExtensionByZero_additive

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 {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ U)
variable (R : Type u) [CommRing R]

Lean source · statement

instance etaleExtensionByZero_additive : (etaleExtensionByZero j R).Additive

instance

etaleExtensionByZero_preservesFiniteLimits

L139 ↗

EtaleCohomology.etaleExtensionByZero_preservesFiniteLimits

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 {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ U)
variable (R : Type u) [CommRing R]

Lean source · statement

instance etaleExtensionByZero_preservesFiniteLimits :
    PreservesFiniteLimits (etaleExtensionByZero j R)

Module documentation

Stalks and exactness of extension by zero

Declarations