NYLL
Module

ZariskiModuleBaseChange.lean

Nyll.EtaleCohomology.Sites.ZariskiModuleBaseChange
5 declarations indexed from sourceView source ↗

Module documentation

Underlying Zariski sets of module-valued étale inverse image

Forgetting modules and restricting to opens gives an actual sheaf of sets. Direct image commutes with these operations. Taking mates compares its topological inverse image with the underlying Zariski sheaf of module-valued étale inverse image, including the actual chosen adjunction units.

Imports7
Imported by5

Declarations

instance

moduleForget_hasSheafCompose

L33 ↗
EtaleCohomology.moduleForget_hasSheafCompose
Source context 4 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace EtaleCohomology
Lean source · statement
instance moduleForget_hasSheafCompose {C : Type v} [Category.{w} C]
    (J : GrothendieckTopology C) (Λ : Type u) [CommRing Λ] :
    J.HasSheafCompose (forget (ModuleCat.{u} Λ))
def

etaleModuleZariskiRestriction

L42 ↗
EtaleCohomology.etaleModuleZariskiRestriction
Documentation

The underlying sheaf of sets on the actual Zariski opens of the scheme.

Source context 5 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace EtaleCohomology
local instance moduleForget_hasSheafCompose {C : Type v} [Category.{w} C]
    (J : GrothendieckTopology C) (Λ : Type u) [CommRing Λ] :
    J.HasSheafCompose (forget (ModuleCat.{u} Λ)) := by
  let : Limits.PreservesLimitsOfSize.{w, max v w} (forget (ModuleCat.{u} Λ)) :=
    (ModuleCat.adj Λ).rightAdjoint_preservesLimits
  exact hasSheafCompose_of_preservesLimitsOfSize
    (F := forget (ModuleCat.{u} Λ)) J
Lean source · statement
def etaleModuleZariskiRestriction (X : Scheme.{u}) (Λ : Type u) [CommRing Λ] :
    Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ) ⥤
      Sheaf (Opens.grothendieckTopology X) (Type u)
def

etaleModuleZariskiPushforwardIso

L52 ↗
EtaleCohomology.etaleModuleZariskiPushforwardIso
Documentation

The underlying Zariski sheaf of module direct image is its actual topological direct image.

Source context 6 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace EtaleCohomology
local instance moduleForget_hasSheafCompose {C : Type v} [Category.{w} C]
    (J : GrothendieckTopology C) (Λ : Type u) [CommRing Λ] :
    J.HasSheafCompose (forget (ModuleCat.{u} Λ)) := by
  let : Limits.PreservesLimitsOfSize.{w, max v w} (forget (ModuleCat.{u} Λ)) :=
    (ModuleCat.adj Λ).rightAdjoint_preservesLimits
  exact hasSheafCompose_of_preservesLimitsOfSize
    (F := forget (ModuleCat.{u} Λ)) J
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (Λ : Type u) [CommRing Λ]
Lean source · statement
def etaleModuleZariskiPushforwardIso :
    etalePushforward f Λ ⋙ etaleModuleZariskiRestriction Y Λ ≅
      etaleModuleZariskiRestriction X Λ ⋙ TopCat.Sheaf.pushforward (Type u) f.base
def

etaleModuleZariskiPullbackComparison

L60 ↗
EtaleCohomology.etaleModuleZariskiPullbackComparison
Documentation

The canonical mixed comparison from topological set inverse image to the underlying Zariski sheaf of module-valued étale inverse image.

Source context 6 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace EtaleCohomology
local instance moduleForget_hasSheafCompose {C : Type v} [Category.{w} C]
    (J : GrothendieckTopology C) (Λ : Type u) [CommRing Λ] :
    J.HasSheafCompose (forget (ModuleCat.{u} Λ)) := by
  let : Limits.PreservesLimitsOfSize.{w, max v w} (forget (ModuleCat.{u} Λ)) :=
    (ModuleCat.adj Λ).rightAdjoint_preservesLimits
  exact hasSheafCompose_of_preservesLimitsOfSize
    (F := forget (ModuleCat.{u} Λ)) J
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (Λ : Type u) [CommRing Λ]
Lean source · statement
def etaleModuleZariskiPullbackComparison :
    etaleModuleZariskiRestriction Y Λ ⋙ TopCat.Sheaf.pullback (Type u) f.base ⟶
      etalePullback f Λ ⋙ etaleModuleZariskiRestriction X Λ
lemma

etaleModuleZariskiPullbackComparison_unit

L69 ↗
EtaleCohomology.etaleModuleZariskiPullbackComparison_unit
Documentation

The mixed comparison carries the actual topological unit to the underlying actual module-valued étale unit.

Source context 6 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory TopologicalSpace
namespace EtaleCohomology
local instance moduleForget_hasSheafCompose {C : Type v} [Category.{w} C]
    (J : GrothendieckTopology C) (Λ : Type u) [CommRing Λ] :
    J.HasSheafCompose (forget (ModuleCat.{u} Λ)) := by
  let : Limits.PreservesLimitsOfSize.{w, max v w} (forget (ModuleCat.{u} Λ)) :=
    (ModuleCat.adj Λ).rightAdjoint_preservesLimits
  exact hasSheafCompose_of_preservesLimitsOfSize
    (F := forget (ModuleCat.{u} Λ)) J
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (Λ : Type u) [CommRing Λ]
Lean source · statement
lemma etaleModuleZariskiPullbackComparison_unit
    (F : Sheaf Y.smallEtaleTopology (ModuleCat.{u} Λ)) :
    (etaleModuleZariskiRestriction Y Λ).map
        ((etalePullbackPushforwardAdjunction f Λ).unit.app F) ≫
      (etaleModuleZariskiPushforwardIso f Λ).hom.app ((etalePullback f Λ).obj F) =
    (TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) f.base).unit.app
        ((etaleModuleZariskiRestriction Y Λ).obj F) ≫
      (TopCat.Sheaf.pushforward (Type u) f.base).map
        ((etaleModuleZariskiPullbackComparison f Λ).app F)

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