Module

AbelianSheafFunctors.lean

Nyll.EtaleCohomology.Classical.AbelianSheafFunctors

12 declarations indexed from sourceView source ↗

Module documentation

Abelian direct and inverse image on the small étale site

Transport the constructed exact inverse image of integer module sheaves through the equivalence with abelian sheaves. Direct image is the actual restriction along étale base change. This connects these functors to mathlib's Sheaf.H.

Imports15

Nyll.EtaleCohomology.Classical.CoefficientSheaves
Nyll.EtaleCohomology.Sites.ClosedImmersionExact
Nyll.EtaleCohomology.Sites.PullbackStalks
Nyll.EtaleCohomology.Sites.ConstantPullback
Mathlib.Algebra.Category.Grp.ZModuleEquivalence
Mathlib.Algebra.Category.Grp.AB
Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Mathlib.Algebra.Ring.ULift
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.CategoryTheory.Adjunction.Limits
Mathlib.CategoryTheory.Adjunction.Unique
Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Mathlib.CategoryTheory.Preadditive.Biproducts
Mathlib.CategoryTheory.Sites.Continuous
Mathlib.CategoryTheory.Sites.Whiskering

Imported by8

def

integerSheafEquivalence

L43 ↗

EtaleCohomology.Classical.integerSheafEquivalence

Documentation

Integer module sheaves and abelian sheaves have the same objects and maps, up to the coefficient-category equivalence.

Source context 5 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology.Classical
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)

Lean source · statement

def integerSheafEquivalence :
    Sheaf J (ModuleCat.{w} (ULift.{w} ℤ)) ≌ Sheaf J AddCommGrpCat.{w}

def

etaleAbelianPushforward

L73 ↗

EtaleCohomology.etaleAbelianPushforward

Documentation

Direct image of abelian étale sheaves, by restriction along base change.

Source context 5 commands

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

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

Lean source · statement

def etaleAbelianPushforward :
    Sheaf X.smallEtaleTopology AddCommGrpCat.{u} ⥤
      Sheaf Y.smallEtaleTopology AddCommGrpCat.{u}

def

etaleAbelianPullback

L81 ↗

EtaleCohomology.etaleAbelianPullback

Documentation

Inverse image of abelian sheaves, using the actual inverse image of integer module sheaves.

Source context 5 commands

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

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

Lean source · statement

def etaleAbelianPullback :
    Sheaf Y.smallEtaleTopology AddCommGrpCat.{u} ⥤
      Sheaf X.smallEtaleTopology AddCommGrpCat.{u}

def

etaleAbelianPushforwardTransportIso

L88 ↗

EtaleCohomology.etaleAbelianPushforwardTransportIso

Source context 5 commands

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

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

Lean source · statement

def etaleAbelianPushforwardTransportIso :
    (Classical.integerSheafEquivalence X.smallEtaleTopology).inverse ⋙
        etalePushforward f (ULift.{u} ℤ) ⋙
          (Classical.integerSheafEquivalence Y.smallEtaleTopology).functor ≅
      etaleAbelianPushforward f

def

etaleAbelianPullbackPushforwardAdjunction

L106 ↗

EtaleCohomology.etaleAbelianPullbackPushforwardAdjunction

Documentation

The inverse-image/direct-image adjunction for the abelian sheaves used in classical cohomology.

Source context 5 commands

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

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

Lean source · statement

def etaleAbelianPullbackPushforwardAdjunction :
    etaleAbelianPullback f ⊣ etaleAbelianPushforward f

instance

(anonymous instance)

L113 ↗

Source context 5 commands

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

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

Lean source · statement

instance : (etaleAbelianPullback f).IsLeftAdjoint

instance

(anonymous instance)

L116 ↗

Source context 5 commands

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

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

Lean source · statement

instance : (etaleAbelianPushforward f).IsRightAdjoint

instance

etaleAbelianPullback_preservesFiniteLimits

L119 ↗

EtaleCohomology.etaleAbelianPullback_preservesFiniteLimits

Source context 5 commands

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

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

Lean source · statement

instance etaleAbelianPullback_preservesFiniteLimits :
    PreservesFiniteLimits (etaleAbelianPullback f)

instance

etaleAbelianPullback_additive

L124 ↗

EtaleCohomology.etaleAbelianPullback_additive

Source context 5 commands

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

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

Lean source · statement

instance etaleAbelianPullback_additive : (etaleAbelianPullback f).Additive

instance

etaleAbelianPushforward_additive

L129 ↗

EtaleCohomology.etaleAbelianPushforward_additive

Source context 5 commands

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

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

Lean source · statement

instance etaleAbelianPushforward_additive : (etaleAbelianPushforward f).Additive

instance

etaleAbelianPushforwardClosed_preservesFiniteColimits

L134 ↗

EtaleCohomology.etaleAbelianPushforwardClosed_preservesFiniteColimits

Source context 5 commands

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

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

Lean source · statement

instance etaleAbelianPushforwardClosed_preservesFiniteColimits [IsClosedImmersion f] :
    PreservesFiniteColimits (etaleAbelianPushforward f)

def

etaleAbelianPullbackConstantIso

L139 ↗

EtaleCohomology.etaleAbelianPullbackConstantIso

Documentation

Inverse image preserves the constant abelian sheaves defining Sheaf.H.

Source context 5 commands

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

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

Lean source · statement

def etaleAbelianPullbackConstantIso :
    constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u} ⋙ etaleAbelianPullback f ≅
      constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}

Module documentation

Abelian direct and inverse image on the small étale site

Declarations