Module

ConstantPullback.lean

Nyll.EtaleCohomology.Sites.ConstantPullback

3 declarations indexed from sourceView source ↗

Module documentation

Inverse image of constant sheaves

For a continuous functor preserving a terminal object, composition of its left adjoint with the constant-sheaf functor is left adjoint to global sections on the target site. Uniqueness of left adjoints gives the constant sheaf comparison. Applying this to étale base change shows that inverse image along any scheme morphism preserves constant coefficient sheaves.

Imports9

Nyll.EtaleCohomology.Sites.BaseChange
Nyll.EtaleCohomology.Sites.SheafFunctors
Mathlib.Algebra.Category.ModuleCat.Colimits
Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.CategoryTheory.Sites.ConstantSheaf
Mathlib.CategoryTheory.Sites.Continuous
Mathlib.CategoryTheory.Adjunction.Unique
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Imported by7

def

constantSheafCompLeftAdjointIso

L44 ↗

EtaleCohomology.Sites.constantSheafCompLeftAdjointIso

Documentation

The left adjoint to restriction preserves constant sheaves when the site functor carries the chosen terminal object to a terminal object.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe uC vC uD vD uA vA u
namespace EtaleCohomology.Sites
variable {C : Type uC} [Category.{vC} C] {D : Type uD} [Category.{vD} D]
  {J : GrothendieckTopology C} {K : GrothendieckTopology D}
  (F : C ⥤ D) [F.IsContinuous J K]
  (A : Type uA) [Category.{vA} A] [HasWeakSheafify J A] [HasWeakSheafify K A]
  {T : C} (hT : IsTerminal T) (hFT : IsTerminal (F.obj T))
  (L : Sheaf J A ⥤ Sheaf K A) (adj : L ⊣ F.sheafPushforwardContinuous A J K)

Lean source · statement

def constantSheafCompLeftAdjointIso :
    constantSheaf J A ⋙ L ≅ constantSheaf K A

def

etalePullbackConstantIso

L55 ↗

EtaleCohomology.etalePullbackConstantIso

Documentation

Inverse image of a constant étale coefficient sheaf has the same constant value.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe uC vC uD vD uA vA u
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (R : Type u) [CommRing R]

Lean source · statement

def etalePullbackConstantIso :
    constantSheaf Y.smallEtaleTopology (ModuleCat.{u} R) ⋙ etalePullback f R ≅
      constantSheaf X.smallEtaleTopology (ModuleCat.{u} R)

lemma

etalePullback_isConstant

L63 ↗

EtaleCohomology.etalePullback_isConstant

Documentation

Inverse image preserves the existing constant-sheaf predicate.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe uC vC uD vD uA vA u
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (R : Type u) [CommRing R]

Lean source · statement

lemma etalePullback_isConstant (G : Sheaf Y.smallEtaleTopology (ModuleCat.{u} R))
    [Sheaf.IsConstant Y.smallEtaleTopology G] :
    Sheaf.IsConstant X.smallEtaleTopology ((etalePullback f R).obj G)

Module documentation

Inverse image of constant sheaves

Declarations

constantSheafCompLeftAdjointIso

etalePullbackConstantIso

etalePullback_isConstant