Module

SheafFunctors.lean

Nyll.EtaleCohomology.Sites.SheafFunctors

11 declarations indexed from sourceView source ↗

Module documentation

Direct and inverse image of étale coefficient sheaves

Direct image is precomposition with base change on the small étale site. Inverse image is constructed by restriction to the affine étale site, left Kan extension, and sheafification. Essential smallness of the affine site supplies the colimits defining the Kan extension, without enlarging the coefficient universe.

The affine-site comparison transports the Kan-extension adjunction to the ordinary small étale sites. Exactness of inverse image and the comparison of geometric stalks are subsequent steps.

Imports12

Nyll.EtaleCohomology.Sites.BaseChange
Mathlib.Algebra.Category.ModuleCat.Adjunctions
Mathlib.Algebra.Category.ModuleCat.Colimits
Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Mathlib.Algebra.Category.ModuleCat.Limits
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.Sites.Continuous
Mathlib.CategoryTheory.Sites.Pullback
Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Mathlib.CategoryTheory.Limits.EssentiallySmall
Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Imported by38

def

etalePushforward

L45 ↗

EtaleCohomology.etalePushforward

Documentation

Direct image of module-valued étale sheaves.

Source context 5 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) (R : Type u) [CommRing R]

Lean source · statement

def etalePushforward :
    Sheaf X.smallEtaleTopology (ModuleCat.{u} R) ⥤
      Sheaf Y.smallEtaleTopology (ModuleCat.{u} R)

def

affineEtaleBaseChange

L52 ↗

EtaleCohomology.affineEtaleBaseChange

Documentation

Base change restricted to affine étale objects of the source site.

Source context 5 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) (R : Type u) [CommRing R]

Lean source · statement

def affineEtaleBaseChange : Y.AffineEtale ⥤ X.Etale

instance

(anonymous instance)

L55 ↗

Source context 5 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) (R : Type u) [CommRing R]

Lean source · statement

instance : (affineEtaleBaseChange f).IsContinuous (Scheme.AffineEtale.topology Y)
    X.smallEtaleTopology

instance

(anonymous instance)

L60 ↗

Source context 5 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) (R : Type u) [CommRing R]

Lean source · statement

instance (F : Y.AffineEtaleᵒᵖ ⥤ ModuleCat.{u} R) :
    (affineEtaleBaseChange f).op.HasPointwiseLeftKanExtension F

def

etalePullback

L70 ↗

EtaleCohomology.etalePullback

Documentation

Inverse image, constructed from the affine-site comparison, left Kan extension, and sheafification.

Source context 5 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) (R : Type u) [CommRing R]

Lean source · statement

def etalePullback :
    Sheaf Y.smallEtaleTopology (ModuleCat.{u} R) ⥤
      Sheaf X.smallEtaleTopology (ModuleCat.{u} R)

def

affineEtalePushforwardIso

L78 ↗

EtaleCohomology.affineEtalePushforwardIso

Source context 5 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) (R : Type u) [CommRing R]

Lean source · statement

def affineEtalePushforwardIso :
    (affineEtaleBaseChange f).sheafPushforwardContinuous (ModuleCat.{u} R)
        (Scheme.AffineEtale.topology Y) X.smallEtaleTopology ≅
      etalePushforward f R ⋙ (Scheme.AffineEtale.sheafEquiv Y (ModuleCat.{u} R)).inverse

def

affineEtalePushforwardComposeIso

L86 ↗

EtaleCohomology.affineEtalePushforwardComposeIso

Source context 5 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) (R : Type u) [CommRing R]

Lean source · statement

def affineEtalePushforwardComposeIso :
    (affineEtaleBaseChange f).sheafPushforwardContinuous (ModuleCat.{u} R)
        (Scheme.AffineEtale.topology Y) X.smallEtaleTopology ⋙
        (Scheme.AffineEtale.sheafEquiv Y (ModuleCat.{u} R)).functor ≅
      etalePushforward f R

def

etalePullbackPushforwardAdjunction

L99 ↗

EtaleCohomology.etalePullbackPushforwardAdjunction

Documentation

The usual inverse-image/direct-image adjunction on the small étale sites.

Source context 5 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) (R : Type u) [CommRing R]

Lean source · statement

def etalePullbackPushforwardAdjunction : etalePullback f R ⊣ etalePushforward f R

instance

(anonymous instance)

L106 ↗

Source context 5 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) (R : Type u) [CommRing R]

Lean source · statement

instance : (etalePullback f R).IsLeftAdjoint

instance

(anonymous instance)

L109 ↗

Source context 5 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) (R : Type u) [CommRing R]

Lean source · statement

instance : (etalePushforward f R).IsRightAdjoint

lemma

etalePushforward_sections

L113 ↗

EtaleCohomology.etalePushforward_sections

Documentation

Sections of direct image are sections on the base-changed étale object.

Source context 5 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) (R : Type u) [CommRing R]

Lean source · statement

lemma etalePushforward_sections
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)) (U : Y.Etale) :
    ((etalePushforward f R).obj F).obj.obj (op U) =
      F.obj.obj (op ((etaleBaseChange f).obj U))

Module documentation

Direct and inverse image of étale coefficient sheaves

Declarations