NYLL
Module

ModuleSetComparison.lean

Nyll.EtaleCohomology.Sites.ModuleSetComparison
13 declarations indexed from sourceView source ↗

Module documentation

Underlying set sheaves of étale module sheaves

Forgetting the module structure commutes with constant sheaves, direct image, and inverse image. The inverse-image comparison is the mate of the identity between the two direct-image composites. Its invertibility is proved on geometric stalks using the filtered-colimit comparison for the forgetful functor and the stalk/skyscraper adjunctions. No field or finiteness assumption is imposed on the base schemes or the coefficient ring.

Imports21
Imported by11

Declarations

def

etaleModuleUnderlying

L47 ↗
EtaleCohomology.etaleModuleUnderlying
Documentation

Forget the module structure of an é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 : Scheme.{u}) (R : Type u) [CommRing R]
Lean source · statement
def etaleModuleUnderlying :
    Sheaf X.smallEtaleTopology (ModuleCat.{u} R) ⥤ Sheaf X.smallEtaleTopology (Type u)
def

etaleConstantModuleUnderlyingIso

L52 ↗
EtaleCohomology.etaleConstantModuleUnderlyingIso
Documentation

The underlying set sheaf of a constant module sheaf is the constant set 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 : Scheme.{u}) (R : Type u) [CommRing R]
Lean source · statement
def etaleConstantModuleUnderlyingIso :
    constantSheaf X.smallEtaleTopology (ModuleCat.{u} R) ⋙ etaleModuleUnderlying X R ≅
      forget (ModuleCat.{u} R) ⋙ constantSheaf X.smallEtaleTopology (Type u)
def

etalePushforwardModuleUnderlyingIso

L63 ↗
EtaleCohomology.etalePushforwardModuleUnderlyingIso
Documentation

Direct image commutes with forgetting module structure, by restriction of presheaves.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
variable (X : Scheme.{u}) (R : Type u) [CommRing R]
variable {X} {Y : Scheme.{u}} (f : X ⟶ Y)
Lean source · statement
def etalePushforwardModuleUnderlyingIso :
    etalePushforward f R ⋙ etaleModuleUnderlying Y R ≅
      etaleModuleUnderlying X R ⋙ etaleSetPushforward f
def

etalePullbackModuleUnderlyingComparison

L68 ↗
EtaleCohomology.etalePullbackModuleUnderlyingComparison
Documentation

The canonical inverse-image comparison, obtained as the mate of the direct-image identity.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
variable (X : Scheme.{u}) (R : Type u) [CommRing R]
variable {X} {Y : Scheme.{u}} (f : X ⟶ Y)
Lean source · statement
def etalePullbackModuleUnderlyingComparison :
    etaleModuleUnderlying Y R ⋙ etaleSetPullback f ⟶
      etalePullback f R ⋙ etaleModuleUnderlying X R
def

stalkModuleUnderlyingSquare

L81 ↗
EtaleCohomology.Sites.stalkModuleUnderlyingSquare
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.Sites
variable {C : Type (u + 1)} [Category.{u} C] {J : GrothendieckTopology C}
  (Φ : GrothendieckTopology.Point.{u} J) (R : Type u) [CommRing R]
Lean source · statement
def stalkModuleUnderlyingSquare :
    TwoSquare (sheafCompose J (forget (ModuleCat.{u} R)))
      (Φ.sheafFiber (A := ModuleCat.{u} R))
      (Φ.sheafFiber (A := Type u)) (forget (ModuleCat.{u} R))
def

skyscraperModuleUnderlyingSquare

L87 ↗
EtaleCohomology.Sites.skyscraperModuleUnderlyingSquare
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.Sites
variable {C : Type (u + 1)} [Category.{u} C] {J : GrothendieckTopology C}
  (Φ : GrothendieckTopology.Point.{u} J) (R : Type u) [CommRing R]
Lean source · statement
def skyscraperModuleUnderlyingSquare :
    TwoSquare (Φ.skyscraperSheafFunctor (A := ModuleCat.{u} R))
      (forget (ModuleCat.{u} R)) (sheafCompose J (forget (ModuleCat.{u} R)))
      (Φ.skyscraperSheafFunctor (A := Type u))
lemma

skyscraperModuleUnderlyingSquare_app

L94 ↗
EtaleCohomology.Sites.skyscraperModuleUnderlyingSquare_app
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.Sites
variable {C : Type (u + 1)} [Category.{u} C] {J : GrothendieckTopology C}
  (Φ : GrothendieckTopology.Point.{u} J) (R : Type u) [CommRing R]
Lean source · statement
lemma skyscraperModuleUnderlyingSquare_app (M : ModuleCat.{u} R) :
    (skyscraperModuleUnderlyingSquare Φ R).natTrans.app M =
      Φ.skyscraperSheafAdjunction.homEquiv _ _
        ((stalkModuleUnderlyingSquare Φ R).natTrans.app (Φ.skyscraperSheaf M) ≫
          (forget (ModuleCat.{u} R)).map (Φ.skyscraperSheafAdjunction.counit.app M))
lemma

skyscraperModuleUnderlyingSquare_app_π

L105 ↗
EtaleCohomology.Sites.skyscraperModuleUnderlyingSquare_app_π
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.Sites
variable {C : Type (u + 1)} [Category.{u} C] {J : GrothendieckTopology C}
  (Φ : GrothendieckTopology.Point.{u} J) (R : Type u) [CommRing R]
Lean source · full declaration
lemma skyscraperModuleUnderlyingSquare_app_π
    (M : ModuleCat.{u} R) (V : C) (v : Φ.fiber.obj V) :
    ((skyscraperModuleUnderlyingSquare Φ R).natTrans.app M).hom.app (op V) ≫
        Pi.π (fun _ : Φ.fiber.obj V => (forget (ModuleCat.{u} R)).obj M) v =
      (forget (ModuleCat.{u} R)).map (Pi.π (fun _ : Φ.fiber.obj V => M) v) := by
  rw [skyscraperModuleUnderlyingSquare_app]
  erw [Φ.skyscraperSheafAdjunction_homEquiv_apply_hom]
  change (Φ.skyscraperPresheafHomEquiv
    ((Φ.presheafFiberCompIso (forget (ModuleCat.{u} R))).hom.app
      (Φ.skyscraperPresheaf M) ≫
        (forget (ModuleCat.{u} R)).map (Φ.skyscraperSheafAdjunction.counit.app M))).app
      (op V) ≫ Pi.π _ v = _
  erw [Φ.skyscraperPresheafHomEquiv_app_π]
  change Φ.toPresheafFiber V v ((Φ.skyscraperSheaf M).obj ⋙ forget (ModuleCat.{u} R)) ≫
      ((Φ.presheafFiberCompIso (forget (ModuleCat.{u} R))).hom.app
        (Φ.skyscraperSheaf M).obj ≫
          (forget (ModuleCat.{u} R)).map (Φ.skyscraperSheafAdjunction.counit.app M)) = _
  rw [← Category.assoc, Φ.toPresheafFiber_presheafFiberCompIso_hom_app]
  erw [← Functor.map_comp]
  congr 1
  rw [← Adjunction.homEquiv_symm_id Φ.skyscraperSheafAdjunction M]
  erw [Φ.skyscraperSheafAdjunction_homEquiv_symm_apply]
  exact Φ.toPresheafFiber_skyscraperPresheafHomEquiv_symm (𝟙 _) V v
instance

(anonymous instance)

L136 ↗
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
open scoped TwoSquare
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (R : Type u) [CommRing R]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X)
Lean source · statement
instance : RepresentablyFlat (etaleBaseChange f)
lemma

skyscraperModuleUnderlyingSquare_comap

L138 ↗
EtaleCohomology.skyscraperModuleUnderlyingSquare_comap
Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
open scoped TwoSquare
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (R : Type u) [CommRing R]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X)
local instance : RepresentablyFlat (etaleBaseChange f) := flat_of_preservesFiniteLimits _
Lean source · statement
lemma skyscraperModuleUnderlyingSquare_comap :
    Sites.skyscraperModuleUnderlyingSquare
        ((Scheme.pointSmallEtale s).comap (etaleBaseChange f)
          (etaleBaseChange_coverPreserving f)) R =
      (Sites.skyscraperModuleUnderlyingSquare (Scheme.pointSmallEtale s) R) ≫ₕ
        (etalePushforwardModuleUnderlyingIso R f).hom
lemma

etalePullbackModuleUnderlyingComparison_stalk_isIso

L163 ↗
EtaleCohomology.etalePullbackModuleUnderlyingComparison_stalk_isIso
Documentation

The inverse-image comparison is an isomorphism at every geometric point.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
open scoped TwoSquare
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (R : Type u) [CommRing R]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X)
local instance : RepresentablyFlat (etaleBaseChange f) := flat_of_preservesFiniteLimits _
Lean source · statement
lemma etalePullbackModuleUnderlyingComparison_stalk_isIso
    (F : Sheaf Y.smallEtaleTopology (ModuleCat.{u} R)) :
    IsIso ((Scheme.pointSmallEtale s).sheafFiber.map
      ((etalePullbackModuleUnderlyingComparison R f).app F))
lemma

etalePullbackModuleUnderlyingComparison_isIso

L217 ↗
EtaleCohomology.etalePullbackModuleUnderlyingComparison_isIso
Documentation

Geometric points detect that inverse image commutes with forgetting module structure.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
open scoped TwoSquare
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (R : Type u) [CommRing R]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X)
local instance : RepresentablyFlat (etaleBaseChange f) := flat_of_preservesFiniteLimits _
Lean source · statement
lemma etalePullbackModuleUnderlyingComparison_isIso :
    IsIso (etalePullbackModuleUnderlyingComparison R f)
def

etalePullbackModuleUnderlyingIso

L231 ↗
EtaleCohomology.etalePullbackModuleUnderlyingIso
Documentation

Underlying set sheaves commute with inverse image for every morphism of schemes.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
open scoped TwoSquare
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (R : Type u) [CommRing R]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X)
local instance : RepresentablyFlat (etaleBaseChange f) := flat_of_preservesFiniteLimits _
Lean source · statement
def etalePullbackModuleUnderlyingIso :
    etalePullback f R ⋙ etaleModuleUnderlying X R ≅
      etaleModuleUnderlying Y R ⋙ etaleSetPullback f

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.