Module

ZariskiGeometricStalks.lean

Nyll.EtaleCohomology.Sites.ZariskiGeometricStalks

7 declarations indexed from sourceView source ↗

Module documentation

Zariski germs inside geometric étale stalks

The actual lift of a geometric point to each open neighborhood defines the map from the Zariski stalk to the geometric étale stalk. Equality in the latter occurs on an étale neighborhood. Descent to its open image proves that this map is injective for a sheaf.

Imports8

Nyll.EtaleCohomology.Sites.ZariskiSectionEquality
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.CategoryTheory.Comma.Over.Basic
Mathlib.CategoryTheory.Elements
Mathlib.CategoryTheory.Limits.HasLimits
Mathlib.CategoryTheory.Sites.Point.Basic
Mathlib.Topology.Sheaves.Stalks

Imported by2

def

zariskiGeometricLift

L38 ↗

EtaleCohomology.zariskiGeometricLift

Documentation

The actual geometric lift to an open neighborhood.

Source context 5 commands

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

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

Lean source · statement

def zariskiGeometricLift (U : X.Opens) (hU : s ξ ∈ U) :
    (Scheme.pointSmallEtale s).fiber.obj ((zariskiToEtale X).obj U)

lemma

zariskiGeometricLift_unique

L48 ↗

EtaleCohomology.zariskiGeometricLift_unique

Source context 5 commands

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

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

Lean source · statement

lemma zariskiGeometricLift_unique (U : X.Opens)
    (a b : (Scheme.pointSmallEtale s).fiber.obj ((zariskiToEtale X).obj U)) : a = b

def

zariskiGeometricNeighborhoods

L54 ↗

EtaleCohomology.zariskiGeometricNeighborhoods

Source context 5 commands

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

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

Lean source · full declaration

def zariskiGeometricNeighborhoods :
    OpenNhds (s ξ) ⥤ (Scheme.pointSmallEtale s).fiber.Elements where
  obj U := (Scheme.pointSmallEtale s).fiber.elementsMk ((zariskiToEtale X).obj U.1)
    (zariskiGeometricLift s ξ U.1 U.2)
  map {U V} g := Functor.Elements.homMk
    ((zariskiToEtale X).map ((OpenNhds.inclusion (s ξ)).map g))
    (zariskiGeometricLift_unique s V.1 _ _)
  map_id U := by
    apply Functor.Elements.hom_ext
    exact (zariskiToEtale X).map_id U.1
  map_comp g h := by
    apply Functor.Elements.hom_ext
    exact (zariskiToEtale X).map_comp _ _

def

etaleZariskiStalkToGeometricStalk

L71 ↗

EtaleCohomology.etaleZariskiStalkToGeometricStalk

Documentation

The canonical map from the actual Zariski stalk to the geometric étale stalk.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits TopologicalSpace Opposite
namespace EtaleCohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (s : Spec (CommRingCat.of Ω) ⟶ X) (ξ : Spec (CommRingCat.of Ω))
variable (F : Sheaf X.smallEtaleTopology (Type u))

Lean source · statement

def etaleZariskiStalkToGeometricStalk :
    TopCat.Presheaf.stalk ((etaleZariskiRestriction X (Type u)).obj F).obj (s ξ) ⟶
      (Scheme.pointSmallEtale s).presheafFiber.obj F.obj

lemma

germ_etaleZariskiStalkToGeometricStalk

L78 ↗

EtaleCohomology.germ_etaleZariskiStalkToGeometricStalk

Documentation

The stalk comparison sends an actual Zariski germ to its geometric germ.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits TopologicalSpace Opposite
namespace EtaleCohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (s : Spec (CommRingCat.of Ω) ⟶ X) (ξ : Spec (CommRingCat.of Ω))
variable (F : Sheaf X.smallEtaleTopology (Type u))

Lean source · statement

lemma germ_etaleZariskiStalkToGeometricStalk (U : X.Opens) (hU : s ξ ∈ U) :
    TopCat.Presheaf.germ ((etaleZariskiRestriction X (Type u)).obj F).obj U (s ξ) hU ≫
        etaleZariskiStalkToGeometricStalk s ξ F =
      (Scheme.pointSmallEtale s).toPresheafFiber ((zariskiToEtale X).obj U)
        (zariskiGeometricLift s ξ U hU) F.obj

lemma

zariski_germ_eq_of_geometric_germ_eq

L86 ↗

EtaleCohomology.zariski_germ_eq_of_geometric_germ_eq

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits TopologicalSpace Opposite
namespace EtaleCohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (s : Spec (CommRingCat.of Ω) ⟶ X) (ξ : Spec (CommRingCat.of Ω))
variable (F : Sheaf X.smallEtaleTopology (Type u))

Lean source · statement

lemma zariski_germ_eq_of_geometric_germ_eq
    (U : X.Opens) (hU : s ξ ∈ U)
    (a b : F.obj.obj (op ((zariskiToEtale X).obj U)))
    (hab : (Scheme.pointSmallEtale s).toPresheafFiber ((zariskiToEtale X).obj U)
        (zariskiGeometricLift s ξ U hU) F.obj a =
      (Scheme.pointSmallEtale s).toPresheafFiber ((zariskiToEtale X).obj U)
        (zariskiGeometricLift s ξ U hU) F.obj b) :
    TopCat.Presheaf.germ ((etaleZariskiRestriction X (Type u)).obj F).obj U (s ξ) hU a =
      TopCat.Presheaf.germ ((etaleZariskiRestriction X (Type u)).obj F).obj U (s ξ) hU b

theorem

etaleZariskiStalkToGeometricStalk_injective

L110 ↗

EtaleCohomology.etaleZariskiStalkToGeometricStalk_injective

Documentation

A Zariski germ of an étale sheaf is determined by its geometric germ.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits TopologicalSpace Opposite
namespace EtaleCohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (s : Spec (CommRingCat.of Ω) ⟶ X) (ξ : Spec (CommRingCat.of Ω))
variable (F : Sheaf X.smallEtaleTopology (Type u))

Lean source · statement

theorem etaleZariskiStalkToGeometricStalk_injective :
    Function.Injective (etaleZariskiStalkToGeometricStalk s ξ F)

Module documentation

Zariski germs inside geometric étale stalks

Declarations

zariskiGeometricLift

zariskiGeometricLift_unique

zariskiGeometricNeighborhoods

etaleZariskiStalkToGeometricStalk

germ_etaleZariskiStalkToGeometricStalk

zariski_germ_eq_of_geometric_germ_eq

etaleZariskiStalkToGeometricStalk_injective