NYLL
Module

PushforwardStalkComparison.lean

Nyll.EtaleCohomology.Sites.PushforwardStalkComparison
7 declarations indexed from sourceView source ↗

Module documentation

The actual stalk comparison for étale direct image

An ambient pointed étale neighborhood pulls back to a pointed neighborhood at every lift of the geometric point. Passing to the defining stalk colimits constructs the canonical direct-image stalk map to the product of the lifted stalks. The construction applies to every scheme morphism and is natural in the sheaf. Finiteness and algebraic closedness enter only in the later proof that this comparison is an isomorphism for finite morphisms.

Imports7
  • Nyll.EtaleCohomology.Sites.BaseChange
  • Mathlib.AlgebraicGeometry.Sites.EtalePoint
  • Mathlib.CategoryTheory.Limits.Shapes.Products
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  • Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
  • Mathlib.CategoryTheory.Sites.Point.Basic
  • Mathlib.CategoryTheory.Sites.Continuous
Imported by6

Declarations

def

etalePushforwardGeometricLift

L41 ↗
EtaleCohomology.etalePushforwardGeometricLift
Documentation

The actual lift into the scheme-theoretic base change of a pointed étale neighborhood.

Source context 5 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
  {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (t : Spec (CommRingCat.of Ω) ⟶ X)
  (s : {s : Spec (CommRingCat.of Ω) ⟶ Y // s ≫ q = t})
Lean source · statement
def etalePushforwardGeometricLift (U : X.Etale)
    (a : (Scheme.pointSmallEtale t).fiber.obj U) :
    (Scheme.pointSmallEtale s.val).fiber.obj ((etaleBaseChange q).obj U)
lemma

etalePushforwardGeometricLift_naturality

L51 ↗
EtaleCohomology.etalePushforwardGeometricLift_naturality
Documentation

The geometric lifts commute with a morphism of ambient neighborhoods.

Source context 5 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
  {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (t : Spec (CommRingCat.of Ω) ⟶ X)
  (s : {s : Spec (CommRingCat.of Ω) ⟶ Y // s ≫ q = t})
Lean source · statement
lemma etalePushforwardGeometricLift_naturality {U V : X.Etale} (g : U ⟶ V)
    (a : (Scheme.pointSmallEtale t).fiber.obj U) :
    (Scheme.pointSmallEtale s.val).fiber.map ((etaleBaseChange q).map g)
        (etalePushforwardGeometricLift q t s U a) =
      etalePushforwardGeometricLift q t s V ((Scheme.pointSmallEtale t).fiber.map g a)
def

etalePushforwardStalkComponent

L84 ↗
EtaleCohomology.etalePushforwardStalkComponent
Documentation

Restricting a direct-image germ to a chosen geometric lift.

Source context 6 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
  {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (t : Spec (CommRingCat.of Ω) ⟶ X)
  (s : {s : Spec (CommRingCat.of Ω) ⟶ Y // s ≫ q = t})
variable {A : Type v} [Category.{w} A] [HasColimitsOfSize.{u, u} A]
  (F : Sheaf Y.smallEtaleTopology A)
Lean source · statement
def etalePushforwardStalkComponent :
    (Scheme.pointSmallEtale t).sheafFiber.obj
        (((etaleBaseChange q).sheafPushforwardContinuous A
          X.smallEtaleTopology Y.smallEtaleTopology).obj F) ⟶
      (Scheme.pointSmallEtale s.val).sheafFiber.obj F
lemma

toPresheafFiber_etalePushforwardStalkComponent

L102 ↗
EtaleCohomology.toPresheafFiber_etalePushforwardStalkComponent
Documentation

The component comparison sends a representing section to its actual germ in the pullback neighborhood.

Source context 6 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
  {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (t : Spec (CommRingCat.of Ω) ⟶ X)
  (s : {s : Spec (CommRingCat.of Ω) ⟶ Y // s ≫ q = t})
variable {A : Type v} [Category.{w} A] [HasColimitsOfSize.{u, u} A]
  (F : Sheaf Y.smallEtaleTopology A)
Lean source · statement
lemma toPresheafFiber_etalePushforwardStalkComponent (U : X.Etale)
    (a : (Scheme.pointSmallEtale t).fiber.obj U) :
    (Scheme.pointSmallEtale t).toPresheafFiber U a
        (((etaleBaseChange q).sheafPushforwardContinuous A
          X.smallEtaleTopology Y.smallEtaleTopology).obj F).obj ≫
        etalePushforwardStalkComponent q t s F =
      (Scheme.pointSmallEtale s.val).toPresheafFiber
        ((etaleBaseChange q).obj U) (etalePushforwardGeometricLift q t s U a) F.obj
lemma

etalePushforwardStalkComponent_naturality

L115 ↗
EtaleCohomology.etalePushforwardStalkComponent_naturality
Documentation

The component comparison is natural in the actual sheaf.

Source context 7 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
  {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (t : Spec (CommRingCat.of Ω) ⟶ X)
  (s : {s : Spec (CommRingCat.of Ω) ⟶ Y // s ≫ q = t})
variable {A : Type v} [Category.{w} A] [HasColimitsOfSize.{u, u} A]
  (F : Sheaf Y.smallEtaleTopology A)
variable {F} {G : Sheaf Y.smallEtaleTopology A}
Lean source · statement
lemma etalePushforwardStalkComponent_naturality (η : F ⟶ G) :
    (Scheme.pointSmallEtale t).sheafFiber.map
        (((etaleBaseChange q).sheafPushforwardContinuous A
          X.smallEtaleTopology Y.smallEtaleTopology).map η) ≫
        etalePushforwardStalkComponent q t s G =
      etalePushforwardStalkComponent q t s F ≫
        (Scheme.pointSmallEtale s.val).sheafFiber.map η
def

etalePushforwardStalkComparison

L158 ↗
EtaleCohomology.etalePushforwardStalkComparison
Documentation

The canonical map from a direct-image geometric stalk to the product of the stalks at all geometric lifts with the same field.

Source context 8 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
  {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (t : Spec (CommRingCat.of Ω) ⟶ X)
  (s : {s : Spec (CommRingCat.of Ω) ⟶ Y // s ≫ q = t})
variable {A : Type v} [Category.{w} A] [HasColimitsOfSize.{u, u} A]
  (F : Sheaf Y.smallEtaleTopology A)
variable {F} {G : Sheaf Y.smallEtaleTopology A}
variable [HasProducts.{u} A] (F)
Lean source · full declaration
def etalePushforwardStalkComparison :
    (Scheme.pointSmallEtale t).sheafFiber.obj
        (((etaleBaseChange q).sheafPushforwardContinuous A
          X.smallEtaleTopology Y.smallEtaleTopology).obj F) ⟶
      ∏ᶜ fun s : {s : Spec (CommRingCat.of Ω) ⟶ Y // s ≫ q = t} =>
        (Scheme.pointSmallEtale s.val).sheafFiber.obj F :=
  Pi.lift (fun s => etalePushforwardStalkComponent q t s F)
lemma

etalePushforwardStalkComparison_π

L167 ↗
EtaleCohomology.etalePushforwardStalkComparison_π
Documentation

Every product projection is the corresponding actual germ comparison.

Source context 8 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
  {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (t : Spec (CommRingCat.of Ω) ⟶ X)
  (s : {s : Spec (CommRingCat.of Ω) ⟶ Y // s ≫ q = t})
variable {A : Type v} [Category.{w} A] [HasColimitsOfSize.{u, u} A]
  (F : Sheaf Y.smallEtaleTopology A)
variable {F} {G : Sheaf Y.smallEtaleTopology A}
variable [HasProducts.{u} A] (F)
Lean source · full declaration
lemma etalePushforwardStalkComparison_π :
    etalePushforwardStalkComparison q t F ≫
        Pi.π (fun s : {s : Spec (CommRingCat.of Ω) ⟶ Y // s ≫ q = t} =>
          (Scheme.pointSmallEtale s.val).sheafFiber.obj F) s =
      etalePushforwardStalkComponent q t s F :=
  Pi.lift_comp_π _ _

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