Module

SetSheafFunctors.lean

Nyll.EtaleCohomology.Sites.SetSheafFunctors

10 declarations indexed from sourceView source ↗

Module documentation

Inverse image of set-valued étale sheaves

The affine étale site supplies the small colimits for inverse image in the same universe as the values. The resulting functor is left adjoint to restriction along base change. Constant sheaves are preserved, and inverse image of the sheaf represented by an étale scheme is represented by its scheme-theoretic base change.

These constructions apply to arbitrary scheme morphisms and are used to transfer local splittings of finite étale covers to sheaves of finite sets.

Imports15

Nyll.EtaleCohomology.Sites.BaseChange
Nyll.EtaleCohomology.Sites.SheafFunctors
Nyll.EtaleCohomology.Sites.ConstantPullback
Nyll.EtaleCohomology.Sites.Subcanonical
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Mathlib.CategoryTheory.Limits.EssentiallySmall
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Mathlib.CategoryTheory.Sites.ConstantSheaf
Mathlib.CategoryTheory.Sites.Continuous
Mathlib.CategoryTheory.Sites.Pullback
Mathlib.CategoryTheory.Sites.Subcanonical
Mathlib.CategoryTheory.Yoneda

Imported by12

def

etaleSetPushforward

L47 ↗

EtaleCohomology.etaleSetPushforward

Documentation

Direct image of sheaves of sets on the small étale sites.

Source context 5 commands

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

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

Lean source · statement

def etaleSetPushforward :
    Sheaf X.smallEtaleTopology (Type u) ⥤ Sheaf Y.smallEtaleTopology (Type u)

instance

(anonymous instance)

L52 ↗

Source context 5 commands

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

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

Lean source · statement

instance (F : Y.AffineEtaleᵒᵖ ⥤ Type u) :
    (affineEtaleBaseChange f).op.HasPointwiseLeftKanExtension F

def

etaleSetPullback

L60 ↗

EtaleCohomology.etaleSetPullback

Documentation

Inverse image of sheaves of sets, using left Kan extension and sheafification.

Source context 5 commands

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

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

Lean source · statement

def etaleSetPullback :
    Sheaf Y.smallEtaleTopology (Type u) ⥤ Sheaf X.smallEtaleTopology (Type u)

def

affineEtaleSetPushforwardComposeIso

L67 ↗

EtaleCohomology.affineEtaleSetPushforwardComposeIso

Source context 5 commands

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

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

Lean source · statement

def affineEtaleSetPushforwardComposeIso :
    (affineEtaleBaseChange f).sheafPushforwardContinuous (Type u)
        (Scheme.AffineEtale.topology Y) X.smallEtaleTopology ⋙
        (Scheme.AffineEtale.sheafEquiv Y (Type u)).functor ≅
      etaleSetPushforward f

def

etaleSetPullbackPushforwardAdjunction

L83 ↗

EtaleCohomology.etaleSetPullbackPushforwardAdjunction

Documentation

The inverse-image/direct-image adjunction for set-valued étale sheaves.

Source context 5 commands

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

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

Lean source · statement

def etaleSetPullbackPushforwardAdjunction : etaleSetPullback f ⊣ etaleSetPushforward f

instance

(anonymous instance)

L90 ↗

Source context 5 commands

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

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

Lean source · statement

instance : (etaleSetPullback f).IsLeftAdjoint

instance

(anonymous instance)

L93 ↗

Source context 5 commands

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

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

Lean source · statement

instance : (etaleSetPushforward f).IsRightAdjoint

def

etaleSetPullbackConstantIso

L97 ↗

EtaleCohomology.etaleSetPullbackConstantIso

Documentation

Pullback preserves the constant value of a set-valued étale sheaf.

Source context 5 commands

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

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

Lean source · statement

def etaleSetPullbackConstantIso :
    constantSheaf Y.smallEtaleTopology (Type u) ⋙ etaleSetPullback f ≅
      constantSheaf X.smallEtaleTopology (Type u)

def

etaleSetPullbackYonedaHomEquiv

L104 ↗

EtaleCohomology.etaleSetPullbackYonedaHomEquiv

Source context 5 commands

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

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

Lean source · statement

def etaleSetPullbackYonedaHomEquiv (U : Y.Etale)
    (G : Sheaf X.smallEtaleTopology (Type u)) :
    ((etaleSetPullback f).obj (Y.smallEtaleTopology.yoneda.obj U) ⟶ G) ≃
      (X.smallEtaleTopology.yoneda.obj ((etaleBaseChange f).obj U) ⟶ G)

def

etaleSetPullbackYonedaObjIso

L112 ↗

EtaleCohomology.etaleSetPullbackYonedaObjIso

Documentation

Inverse image of a represented étale sheaf is represented by the pullback scheme.

Source context 5 commands

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

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

Lean source · statement

def etaleSetPullbackYonedaObjIso (U : Y.Etale) :
    (etaleSetPullback f).obj (Y.smallEtaleTopology.yoneda.obj U) ≅
      X.smallEtaleTopology.yoneda.obj ((etaleBaseChange f).obj U)

Module documentation

Inverse image of set-valued étale sheaves

Declarations