Module

ZariskiBaseChange.lean

Nyll.EtaleCohomology.Sites.ZariskiBaseChange

5 declarations indexed from sourceView source ↗

Module documentation

Zariski restriction and actual étale base change

The cartesian square of an open subscheme and its inverse image compares the existing small-site base change with the inverse-image functor on opens. It induces the direct-image comparison on sheaves. Its adjunction mate is the actual map from topological inverse image to restricted étale inverse image, with the corresponding equality of the chosen adjunction units.

Imports8

Nyll.EtaleCohomology.Sites.ZariskiRestriction
Nyll.EtaleCohomology.Sites.BaseChange
Nyll.EtaleCohomology.Sites.SetSheafFunctors
Mathlib.AlgebraicGeometry.Restrict
Mathlib.CategoryTheory.Adjunction.Mates
Mathlib.CategoryTheory.MorphismProperty.Comma
Mathlib.CategoryTheory.Sites.Continuous
Mathlib.Topology.Sheaves.Functors

Imported by2

def

zariskiBaseChangeObjIso

L37 ↗

EtaleCohomology.zariskiBaseChangeObjIso

Source context 5 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)

Lean source · statement

def zariskiBaseChangeObjIso (U : Y.Opens) :
    (etaleBaseChange f).obj ((zariskiToEtale Y).obj U) ≅
      (zariskiToEtale X).obj ((Opens.map f.base).obj U)

def

zariskiToEtaleBaseChangeIso

L47 ↗

EtaleCohomology.zariskiToEtaleBaseChangeIso

Documentation

The actual pullback of an open subscheme is its inverse-image open.

Source context 5 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)

Lean source · statement

def zariskiToEtaleBaseChangeIso :
    zariskiToEtale Y ⋙ etaleBaseChange f ≅
      Opens.map f.base ⋙ zariskiToEtale X

def

etaleZariskiPushforwardIso

L61 ↗

EtaleCohomology.etaleZariskiPushforwardIso

Documentation

Restricting étale direct image to opens agrees with topological direct image of the restricted sheaf.

Source context 6 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable (A : Type v) [Category.{w} A]

Lean source · statement

def etaleZariskiPushforwardIso :
    (etaleBaseChange f).sheafPushforwardContinuous A
        Y.smallEtaleTopology X.smallEtaleTopology ⋙ etaleZariskiRestriction Y A ≅
      etaleZariskiRestriction X A ⋙ TopCat.Sheaf.pushforward A f.base

def

etaleZariskiSetPullbackComparison

L77 ↗

EtaleCohomology.etaleZariskiSetPullbackComparison

Documentation

The canonical map from topological inverse image to the Zariski restriction of actual set-valued étale inverse image.

Source context 6 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable (A : Type v) [Category.{w} A]

Lean source · statement

def etaleZariskiSetPullbackComparison :
    etaleZariskiRestriction Y (Type u) ⋙ TopCat.Sheaf.pullback (Type u) f.base ⟶
      etaleSetPullback f ⋙ etaleZariskiRestriction X (Type u)

lemma

etaleZariskiSetPullbackComparison_unit

L86 ↗

EtaleCohomology.etaleZariskiSetPullbackComparison_unit

Documentation

The comparison identifies the actual étale adjunction unit with the topological adjunction unit followed by the constructed comparison.

Source context 6 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable (A : Type v) [Category.{w} A]

Lean source · statement

lemma etaleZariskiSetPullbackComparison_unit
    (F : Sheaf Y.smallEtaleTopology (Type u)) :
    (etaleZariskiRestriction Y (Type u)).map
        ((etaleSetPullbackPushforwardAdjunction f).unit.app F) ≫
      (etaleZariskiPushforwardIso f (Type u)).hom.app ((etaleSetPullback f).obj F) =
    (TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) f.base).unit.app
        ((etaleZariskiRestriction Y (Type u)).obj F) ≫
      (TopCat.Sheaf.pushforward (Type u) f.base).map
        ((etaleZariskiSetPullbackComparison f).app F)

Module documentation

Zariski restriction and actual étale base change

Declarations

zariskiBaseChangeObjIso

zariskiToEtaleBaseChangeIso

etaleZariskiPushforwardIso

etaleZariskiSetPullbackComparison

etaleZariskiSetPullbackComparison_unit