Module

ModuleRestriction.lean

Nyll.EtaleCohomology.Sites.ModuleRestriction

6 declarations indexed from sourceView source ↗

Module documentation

Restriction of constant module sheaves

For an étale morphism, inverse image of modules is actual restriction of presheaves. The canonical map from the constant sheaf on the source to the restriction of the constant sheaf on the target is constructed from the sheafification unit. Cocontinuity proves that this map is an isomorphism and the explicit unit formula keeps track of actual constant sections.

Imports10

Nyll.EtaleCohomology.Sites.BaseChange
Nyll.EtaleCohomology.Sites.EtaleRestriction
Nyll.EtaleCohomology.Sites.SheafFunctors
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.CategoryTheory.Sites.ConstantSheaf
Mathlib.CategoryTheory.Sites.CoverLifting
Mathlib.CategoryTheory.Sites.Localization
Mathlib.CategoryTheory.Sites.LocallyBijective
Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
Mathlib.CategoryTheory.Sites.Sheafification

Imported by3

instance

etalePostcompose_isCocontinuous

L37 ↗

EtaleCohomology.etalePostcompose_isCocontinuous

Documentation

Étale postcomposition lifts covering sieves by its base-change adjunction.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Functor
namespace EtaleCohomology
variable {U X : Scheme.{u}} (f : U ⟶ X) [Etale f] (R : Type u) [CommRing R]

Lean source · statement

instance etalePostcompose_isCocontinuous :
    (etalePostcompose f).IsCocontinuous U.smallEtaleTopology X.smallEtaleTopology

def

etalePullbackRestrictionIso

L44 ↗

EtaleCohomology.etalePullbackRestrictionIso

Documentation

Module inverse image along an étale morphism is ordinary presheaf restriction.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Functor
namespace EtaleCohomology
variable {U X : Scheme.{u}} (f : U ⟶ X) [Etale f] (R : Type u) [CommRing R]

Lean source · statement

def etalePullbackRestrictionIso :
    etalePullback f R ≅ etaleRestriction f (ModuleCat.{u} R)

def

etaleRestrictionConstantHom

L50 ↗

EtaleCohomology.etaleRestrictionConstantHom

Documentation

The canonical constant-sheaf comparison, induced by the sheafification unit.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Functor
namespace EtaleCohomology
variable {U X : Scheme.{u}} (f : U ⟶ X) [Etale f] (R : Type u) [CommRing R]

Lean source · statement

def etaleRestrictionConstantHom (M : ModuleCat.{u} R) :
    (constantSheaf U.smallEtaleTopology (ModuleCat.{u} R)).obj M ⟶
      (etaleRestriction f (ModuleCat.{u} R)).obj
        ((constantSheaf X.smallEtaleTopology (ModuleCat.{u} R)).obj M)

lemma

etaleRestrictionConstantHom_fac

L61 ↗

EtaleCohomology.etaleRestrictionConstantHom_fac

Documentation

The comparison carries the source constant section to the same target constant section.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Functor
namespace EtaleCohomology
variable {U X : Scheme.{u}} (f : U ⟶ X) [Etale f] (R : Type u) [CommRing R]

Lean source · statement

lemma etaleRestrictionConstantHom_fac (M : ModuleCat.{u} R) :
    toSheafify U.smallEtaleTopology ((Functor.const U.Etaleᵒᵖ).obj M) ≫
      (etaleRestrictionConstantHom f R M).hom =
    whiskerLeft (etalePostcompose f).op
      (toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj M))

instance

etaleRestrictionConstantHom_isIso

L68 ↗

EtaleCohomology.etaleRestrictionConstantHom_isIso

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Functor
namespace EtaleCohomology
variable {U X : Scheme.{u}} (f : U ⟶ X) [Etale f] (R : Type u) [CommRing R]

Lean source · statement

instance etaleRestrictionConstantHom_isIso (M : ModuleCat.{u} R) :
    IsIso (etaleRestrictionConstantHom f R M)

def

etaleRestrictionConstantIso

L90 ↗

EtaleCohomology.etaleRestrictionConstantIso

Documentation

Restriction of a constant module sheaf has the same constant module, with the canonical comparison on sections.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Functor
namespace EtaleCohomology
variable {U X : Scheme.{u}} (f : U ⟶ X) [Etale f] (R : Type u) [CommRing R]

Lean source · statement

def etaleRestrictionConstantIso (M : ModuleCat.{u} R) :
    (constantSheaf U.smallEtaleTopology (ModuleCat.{u} R)).obj M ≅
      (etaleRestriction f (ModuleCat.{u} R)).obj
        ((constantSheaf X.smallEtaleTopology (ModuleCat.{u} R)).obj M)

Module documentation

Restriction of constant module sheaves

Declarations

etalePostcompose_isCocontinuous

etalePullbackRestrictionIso

etaleRestrictionConstantHom

etaleRestrictionConstantHom_fac

etaleRestrictionConstantHom_isIso

etaleRestrictionConstantIso