Module

PushforwardGlobalSections.lean

Nyll.EtaleCohomology.Sites.PushforwardGlobalSections

5 declarations indexed from sourceView source ↗

Module documentation

Global sections of actual étale direct image

The base change of the identity object is canonically the identity object. Restriction through this isomorphism identifies global sections, and its geometric germs are the concrete direct-image stalk components.

Imports3

Imported by3

def

baseChangeIdentityIso

L29 ↗

EtaleCohomology.baseChangeIdentityIso

Source context 5 commands

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

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

Lean source · statement

def baseChangeIdentityIso :
    (Scheme.Etale.mk (𝟙 Y) : Y.Etale) ≅ (etaleBaseChange q).obj (Scheme.Etale.mk (𝟙 X))

def

etalePushforwardGlobalSectionsIso

L52 ↗

EtaleCohomology.etalePushforwardGlobalSectionsIso

Documentation

Global sections of actual direct image are the original global sections.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
variable (Λ : Type u) [CommRing Λ]

Lean source · statement

def etalePushforwardGlobalSectionsIso
    (F : Sheaf Y.smallEtaleTopology (ModuleCat.{u} Λ)) :
    ((etalePushforward q Λ).obj F).obj.obj (op (Scheme.Etale.mk (𝟙 X))) ≅
      F.obj.obj (op (Scheme.Etale.mk (𝟙 Y)))

lemma

etalePushforwardGlobalSectionsIso_hom

L59 ↗

EtaleCohomology.etalePushforwardGlobalSectionsIso_hom

Documentation

The forward comparison is restriction through the actual base-change lift.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
variable (Λ : Type u) [CommRing Λ]

Lean source · statement

lemma etalePushforwardGlobalSectionsIso_hom
    (F : Sheaf Y.smallEtaleTopology (ModuleCat.{u} Λ)) :
    (etalePushforwardGlobalSectionsIso q Λ F).hom =
      F.obj.map (etaleBaseChangeLift q q
        ((Category.comp_id q).trans (Category.id_comp q).symm)).op

lemma

etalePullbackGlobalSectionsMap_eq_unit

L67 ↗

EtaleCohomology.etalePullbackGlobalSectionsMap_eq_unit

Documentation

Evaluation of the unit followed by the direct-image section comparison is the original global inverse-image map.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
variable (Λ : Type u) [CommRing Λ]

Lean source · statement

lemma etalePullbackGlobalSectionsMap_eq_unit
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    ((etalePullbackPushforwardAdjunction q Λ).unit.app F).hom.app
        (op (Scheme.Etale.mk (𝟙 X))) ≫
      (etalePushforwardGlobalSectionsIso q Λ ((etalePullback q Λ).obj F)).hom =
        etalePullbackGlobalSectionsMap q Λ F

theorem

etalePushforwardGlobalSectionsIso_germ

L76 ↗

EtaleCohomology.etalePushforwardGlobalSectionsIso_germ

Documentation

A global direct-image germ restricts to the germ of the corresponding original global section at each geometric lift.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
variable (Λ : Type u) [CommRing Λ]

Lean source · statement

theorem etalePushforwardGlobalSectionsIso_germ
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (t : Spec (CommRingCat.of Ω) ⟶ X)
    (s : {s : Spec (CommRingCat.of Ω) ⟶ Y // s ≫ q = t})
    (F : Sheaf Y.smallEtaleTopology (ModuleCat.{u} Λ)) :
    etaleGlobalSectionsGerm t Λ ((etalePushforward q Λ).obj F) ≫
        etalePushforwardStalkComponent q t s F =
      (etalePushforwardGlobalSectionsIso q Λ F).hom ≫
        etaleGlobalSectionsGerm s.val Λ F

Module documentation

Global sections of actual étale direct image

Declarations

baseChangeIdentityIso

etalePushforwardGlobalSectionsIso

etalePushforwardGlobalSectionsIso_hom

etalePullbackGlobalSectionsMap_eq_unit

etalePushforwardGlobalSectionsIso_germ