NYLL
Module

PullbackUnitGeometricStalks.lean

Nyll.EtaleCohomology.Sites.PullbackUnitGeometricStalks
8 declarations indexed from sourceView source ↗

Module documentation

The actual inverse-image unit at a geometric lift

The concrete direct-image stalk component agrees with the restriction of germs at the comapped point. Consequently the adjunction unit followed by this component is an isomorphism. No finiteness or closed-immersion assumption is imposed on the scheme morphism.

Imports12
Imported by5

Declarations

lemma

toPresheafFiber_pointHom

L38 ↗
EtaleCohomology.toPresheafFiber_pointHom
Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
Lean source · statement
lemma toPresheafFiber_pointHom
    {C : Type (u + 1)} [Category.{u} C] {J : GrothendieckTopology C}
    {Φ Ψ : J.Point.{u}} (φ : Φ ⟶ Ψ)
    {A : Type (u + 1)} [Category.{u} A] [HasColimitsOfSize.{u, u} A]
    (P : Cᵒᵖ ⥤ A) (U : C) (a : Ψ.fiber.obj U) :
    Ψ.toPresheafFiber U a P ≫ φ.presheafFiber.app P =
      Φ.toPresheafFiber U (φ.hom.app U a) P
lemma

geometricLift_eq_baseChangeIso_inv

L52 ↗
EtaleCohomology.geometricLift_eq_baseChangeIso_inv
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)
  {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (s : Spec (CommRingCat.of Ω) ⟶ Y)
Lean source · statement
lemma geometricLift_eq_baseChangeIso_inv
    (U : X.Etale) (a : (Scheme.pointSmallEtale (s ≫ q)).fiber.obj U) :
    (geometricFiberBaseChangeIso q s).inv.app U a =
      etalePushforwardGeometricLift q (s ≫ q) ⟨s, rfl⟩ U a
instance

representablyFlat_etaleBaseChange_unitStalks

L62 ↗
EtaleCohomology.representablyFlat_etaleBaseChange_unitStalks
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)
  {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (s : Spec (CommRingCat.of Ω) ⟶ Y)
variable (Λ : Type u) [CommRing Λ]
Lean source · statement
instance representablyFlat_etaleBaseChange_unitStalks :
    RepresentablyFlat (etaleBaseChange q)
theorem

etalePushforwardStalkComponent_eq_comap

L67 ↗
EtaleCohomology.etalePushforwardStalkComponent_eq_comap
Documentation

The concrete component at a geometric lift is the comapped-point restriction map, transported through the existing point comparison.

Source context 7 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)
  {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (s : Spec (CommRingCat.of Ω) ⟶ Y)
variable (Λ : Type u) [CommRing Λ]
local instance representablyFlat_etaleBaseChange_unitStalks :
    RepresentablyFlat (etaleBaseChange q) := flat_of_preservesFiniteLimits _
Lean source · statement
theorem etalePushforwardStalkComponent_eq_comap
    (G : Sheaf Y.smallEtaleTopology (ModuleCat.{u} Λ)) :
    (geometricComapSheafFiberIso q s Λ).inv.app ((etalePushforward q Λ).obj G) ≫
        Sites.restrictionComapStalkMap (etaleBaseChange q)
          (etaleBaseChange_coverPreserving q) (Scheme.pointSmallEtale s) (ModuleCat.{u} Λ) G =
      etalePushforwardStalkComponent q (s ≫ q) ⟨s, rfl⟩ G
theorem

etalePullbackUnit_stalkComponent_isIso

L104 ↗
EtaleCohomology.etalePullbackUnit_stalkComponent_isIso
Documentation

The actual inverse-image unit followed by the actual direct-image component is an isomorphism at every geometric lift.

Source context 7 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)
  {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (s : Spec (CommRingCat.of Ω) ⟶ Y)
variable (Λ : Type u) [CommRing Λ]
local instance representablyFlat_etaleBaseChange_unitStalks :
    RepresentablyFlat (etaleBaseChange q) := flat_of_preservesFiniteLimits _
Lean source · statement
theorem etalePullbackUnit_stalkComponent_isIso
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    IsIso ((Scheme.pointSmallEtale (s ≫ q)).sheafFiber.map
        ((etalePullbackPushforwardAdjunction q Λ).unit.app F) ≫
      etalePushforwardStalkComponent q (s ≫ q) ⟨s, rfl⟩ ((etalePullback q Λ).obj F))
theorem

etalePullbackSectionMap_toPresheafFiber

L134 ↗
EtaleCohomology.etalePullbackSectionMap_toPresheafFiber
Documentation

A section pulled through a commuting square has the germ obtained from its original germ by the actual inverse-image unit and lift component.

Source context 7 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)
  {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (s : Spec (CommRingCat.of Ω) ⟶ Y)
variable (Λ : Type u) [CommRing Λ]
local instance representablyFlat_etaleBaseChange_unitStalks :
    RepresentablyFlat (etaleBaseChange q) := flat_of_preservesFiniteLimits _
Lean source · full declaration
theorem etalePullbackSectionMap_toPresheafFiber
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ))
    {U : Y.Etale} {V : X.Etale}
    (l : U.left ⟶ V.left) (hl : l ≫ V.hom = U.hom ≫ q)
    (a : (Scheme.pointSmallEtale s).fiber.obj U) :
    etalePullbackSectionMap q Λ F l hl ≫
        (Scheme.pointSmallEtale s).toPresheafFiber U a ((etalePullback q Λ).obj F).obj =
      (Scheme.pointSmallEtale (s ≫ q)).toPresheafFiber V
          (Over.homMk (a.left ≫ l) (by
            change (Over.mk s ⟶ Over.mk U.hom) at a
            change (a.left ≫ l) ≫ V.hom = s ≫ q
            rw [Category.assoc, hl, ← Category.assoc]
            exact congrArg (fun k : Spec (CommRingCat.of Ω) ⟶ Y => k ≫ q) a.w)) F.obj ≫
        (Scheme.pointSmallEtale (s ≫ q)).sheafFiber.map
          ((etalePullbackPushforwardAdjunction q Λ).unit.app F) ≫
        etalePushforwardStalkComponent q (s ≫ q) ⟨s, rfl⟩
          ((etalePullback q Λ).obj F) := by
  let G : Sheaf Y.smallEtaleTopology (ModuleCat.{u} Λ) := (etalePullback q Λ).obj F
  let H : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ) := (etalePushforward q Λ).obj G
  let η : F ⟶ H := (etalePullbackPushforwardAdjunction q Λ).unit.app F
  let b : (Scheme.pointSmallEtale (s ≫ q)).fiber.obj V :=
    Over.homMk (a.left ≫ l) (by
      change (Over.mk s ⟶ Over.mk U.hom) at a
      change (a.left ≫ l) ≫ V.hom = s ≫ q
      rw [Category.assoc, hl, ← Category.assoc]
      exact congrArg (fun k : Spec (CommRingCat.of Ω) ⟶ Y => k ≫ q) a.w)
  let j : U ⟶ (etaleBaseChange q).obj V := etaleBaseChangeLift q l hl
  have hj : (Scheme.pointSmallEtale s).fiber.map j a =
      etalePushforwardGeometricLift q (s ≫ q) ⟨s, rfl⟩ V b := by
    let a₀ : Spec (CommRingCat.of Ω) ⟶ U.left := a.left
    let j₀ : U.left ⟶ pullback V.hom q := j.left
    let c : Spec (CommRingCat.of Ω) ⟶ pullback V.hom q :=
      (etalePushforwardGeometricLift q (s ≫ q) ⟨s, rfl⟩ V b).left
    have hj₁ : j₀ ≫ pullback.fst V.hom q = l := pullback.lift_fst _ _ _
    have hj₂ : j₀ ≫ pullback.snd V.hom q = U.hom := pullback.lift_snd _ _ _
    have hc₁ : c ≫ pullback.fst V.hom q = a₀ ≫ l := pullback.lift_fst _ _ _
    have hc₂ : c ≫ pullback.snd V.hom q = s := pullback.lift_snd _ _ _
    apply Over.OverMorphism.ext
    change a₀ ≫ j₀ = c
    apply pullback.hom_ext
    · rw [Category.assoc, hj₁, hc₁]
    · rw [Category.assoc, hj₂, hc₂]
      exact a.w
  let ηV : F.obj.obj (op V) ⟶ G.obj.obj (op ((etaleBaseChange q).obj V)) :=
    η.hom.app (op V)
  let γ : G.obj.obj (op ((etaleBaseChange q).obj V)) ⟶
      (Scheme.pointSmallEtale (s ≫ q)).presheafFiber.obj H.obj :=
    (Scheme.pointSmallEtale (s ≫ q)).toPresheafFiber V b H.obj
  let c : (Scheme.pointSmallEtale (s ≫ q)).presheafFiber.obj H.obj ⟶
      (Scheme.pointSmallEtale s).presheafFiber.obj G.obj :=
    etalePushforwardStalkComponent q (s ≫ q) ⟨s, rfl⟩ G
  have hn : (Scheme.pointSmallEtale (s ≫ q)).toPresheafFiber V b F.obj ≫
      (Scheme.pointSmallEtale (s ≫ q)).presheafFiber.map η.hom = ηV ≫ γ :=
    (Scheme.pointSmallEtale (s ≫ q)).toPresheafFiber_naturality η.hom V b
  have hc : γ ≫ c = (Scheme.pointSmallEtale s).toPresheafFiber
      ((etaleBaseChange q).obj V) (etalePushforwardGeometricLift q (s ≫ q) ⟨s, rfl⟩ V b)
        G.obj := toPresheafFiber_etalePushforwardStalkComponent q (s ≫ q) ⟨s, rfl⟩ G V b
  change (ηV ≫ G.obj.map j.op) ≫
      (Scheme.pointSmallEtale s).toPresheafFiber U a G.obj =
    (Scheme.pointSmallEtale (s ≫ q)).toPresheafFiber V b F.obj ≫
      (Scheme.pointSmallEtale (s ≫ q)).presheafFiber.map η.hom ≫ c
  rw [Category.assoc, (Scheme.pointSmallEtale s).toPresheafFiber_w, hj,
    ← Category.assoc, hn, Category.assoc, hc]
def

etaleGlobalSectionsGerm

L199 ↗
EtaleCohomology.etaleGlobalSectionsGerm
Documentation

The germ of a global section at a geometric point.

Source context 7 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)
  {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (s : Spec (CommRingCat.of Ω) ⟶ Y)
variable (Λ : Type u) [CommRing Λ]
local instance representablyFlat_etaleBaseChange_unitStalks :
    RepresentablyFlat (etaleBaseChange q) := flat_of_preservesFiniteLimits _
Lean source · statement
def etaleGlobalSectionsGerm
    (F : Sheaf Y.smallEtaleTopology (ModuleCat.{u} Λ)) :
    F.obj.obj (op (Scheme.Etale.mk (𝟙 Y))) ⟶
      (Scheme.pointSmallEtale s).sheafFiber.obj F
theorem

etalePullbackGlobalSectionsMap_germ

L207 ↗
EtaleCohomology.etalePullbackGlobalSectionsMap_germ
Documentation

Global pullback commutes with the actual maps on geometric stalks.

Source context 7 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)
  {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (s : Spec (CommRingCat.of Ω) ⟶ Y)
variable (Λ : Type u) [CommRing Λ]
local instance representablyFlat_etaleBaseChange_unitStalks :
    RepresentablyFlat (etaleBaseChange q) := flat_of_preservesFiniteLimits _
Lean source · statement
theorem etalePullbackGlobalSectionsMap_germ
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    etalePullbackGlobalSectionsMap q Λ F ≫
        etaleGlobalSectionsGerm s Λ ((etalePullback q Λ).obj F) =
      etaleGlobalSectionsGerm (s ≫ q) Λ F ≫
        (Scheme.pointSmallEtale (s ≫ q)).sheafFiber.map
          ((etalePullbackPushforwardAdjunction q Λ).unit.app F) ≫
        etalePushforwardStalkComponent q (s ≫ q) ⟨s, rfl⟩
          ((etalePullback q Λ).obj F)

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