NYLL
Module

AbelianPullbackMate.lean

Nyll.EtaleFundamentalGroups.Cohomology.AbelianPullbackMate
13 declarations indexed from sourceView source ↗

Module documentation

Canonical inverse-image comparison for underlying abelian sheaves

This comparison is the mate of the identity between the actual direct-image functors. Its invertibility is detected on geometric stalks. The mate formula retains the adjunction compatibility needed to transport constant sections.

Imports4
Imported by3

Declarations

def

abelianUnderlying

L30 ↗
EtaleFundamentalGroups.Cohomology.abelianUnderlying
Documentation

Forget the abelian group structure of an étale sheaf.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
Lean source · statement
def abelianUnderlying :
    Sheaf X.smallEtaleTopology (AddCommGrpCat.{u}) ⥤ Sheaf X.smallEtaleTopology (Type u)
def

abelianPushforwardUnderlyingIso

L36 ↗
EtaleFundamentalGroups.Cohomology.abelianPushforwardUnderlyingIso
Documentation

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

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
variable {X} {Y : Scheme.{u}} (f : X ⟶ Y)
Lean source · statement
def abelianPushforwardUnderlyingIso :
    etaleAbelianPushforward f ⋙ abelianUnderlying Y ≅
      abelianUnderlying X ⋙ etaleSetPushforward f
def

abelianPullbackUnderlyingComparison

L41 ↗
EtaleFundamentalGroups.Cohomology.abelianPullbackUnderlyingComparison
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 CategoryTheory.Limits Opposite EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
variable {X} {Y : Scheme.{u}} (f : X ⟶ Y)
Lean source · statement
def abelianPullbackUnderlyingComparison :
    abelianUnderlying Y ⋙ etaleSetPullback f ⟶
      etaleAbelianPullback f ⋙ abelianUnderlying X
theorem

abelianPullbackUnderlyingComparison_homEquiv

L50 ↗
EtaleFundamentalGroups.Cohomology.abelianPullbackUnderlyingComparison_homEquiv
Documentation

The underlying-set comparison respects the actual inverse-image adjunctions.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
variable {X} {Y : Scheme.{u}} (f : X ⟶ Y)
Lean source · statement
theorem abelianPullbackUnderlyingComparison_homEquiv
    (F : Sheaf Y.smallEtaleTopology AddCommGrpCat.{u})
    (G : Sheaf X.smallEtaleTopology AddCommGrpCat.{u})
    (k : (etaleAbelianPullback f).obj F ⟶ G) :
    (etaleSetPullbackPushforwardAdjunction f).homEquiv _ _
        ((abelianPullbackUnderlyingComparison f).app F ≫
          (abelianUnderlying X).map k) =
      (abelianUnderlying Y).map
        ((etaleAbelianPullbackPushforwardAdjunction f).homEquiv _ _ k)
def

stalkAbelianUnderlyingSquare

L80 ↗
EtaleFundamentalGroups.Cohomology.Sites.stalkAbelianUnderlyingSquare
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology.Sites
variable {C : Type (u + 1)} [Category.{u} C] {J : GrothendieckTopology C}
  (Φ : GrothendieckTopology.Point.{u} J)
Lean source · statement
def stalkAbelianUnderlyingSquare :
    TwoSquare (sheafCompose J (forget (AddCommGrpCat.{u})))
      (Φ.sheafFiber (A := AddCommGrpCat.{u}))
      (Φ.sheafFiber (A := Type u)) (forget (AddCommGrpCat.{u}))
def

skyscraperAbelianUnderlyingSquare

L86 ↗
EtaleFundamentalGroups.Cohomology.Sites.skyscraperAbelianUnderlyingSquare
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology.Sites
variable {C : Type (u + 1)} [Category.{u} C] {J : GrothendieckTopology C}
  (Φ : GrothendieckTopology.Point.{u} J)
Lean source · statement
def skyscraperAbelianUnderlyingSquare :
    TwoSquare (Φ.skyscraperSheafFunctor (A := AddCommGrpCat.{u}))
      (forget (AddCommGrpCat.{u})) (sheafCompose J (forget (AddCommGrpCat.{u})))
      (Φ.skyscraperSheafFunctor (A := Type u))
lemma

skyscraperAbelianUnderlyingSquare_app

L93 ↗
EtaleFundamentalGroups.Cohomology.Sites.skyscraperAbelianUnderlyingSquare_app
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology.Sites
variable {C : Type (u + 1)} [Category.{u} C] {J : GrothendieckTopology C}
  (Φ : GrothendieckTopology.Point.{u} J)
Lean source · statement
lemma skyscraperAbelianUnderlyingSquare_app (M : AddCommGrpCat.{u}) :
    (skyscraperAbelianUnderlyingSquare Φ).natTrans.app M =
      Φ.skyscraperSheafAdjunction.homEquiv _ _
        ((stalkAbelianUnderlyingSquare Φ).natTrans.app (Φ.skyscraperSheaf M) ≫
          (forget (AddCommGrpCat.{u})).map (Φ.skyscraperSheafAdjunction.counit.app M))
lemma

skyscraperAbelianUnderlyingSquare_app_π

L104 ↗
EtaleFundamentalGroups.Cohomology.Sites.skyscraperAbelianUnderlyingSquare_app_π
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology.Sites
variable {C : Type (u + 1)} [Category.{u} C] {J : GrothendieckTopology C}
  (Φ : GrothendieckTopology.Point.{u} J)
Lean source · full declaration
lemma skyscraperAbelianUnderlyingSquare_app_π
    (M : AddCommGrpCat.{u}) (V : C) (v : Φ.fiber.obj V) :
    ((skyscraperAbelianUnderlyingSquare Φ).natTrans.app M).hom.app (op V) ≫
        Pi.π (fun _ : Φ.fiber.obj V => (forget (AddCommGrpCat.{u})).obj M) v =
      (forget (AddCommGrpCat.{u})).map (Pi.π (fun _ : Φ.fiber.obj V => M) v) := by
  rw [skyscraperAbelianUnderlyingSquare_app]
  erw [Φ.skyscraperSheafAdjunction_homEquiv_apply_hom]
  change (Φ.skyscraperPresheafHomEquiv
    ((Φ.presheafFiberCompIso (forget (AddCommGrpCat.{u}))).hom.app
      (Φ.skyscraperPresheaf M) ≫
        (forget (AddCommGrpCat.{u})).map (Φ.skyscraperSheafAdjunction.counit.app M))).app
      (op V) ≫ Pi.π _ v = _
  erw [Φ.skyscraperPresheafHomEquiv_app_π]
  change Φ.toPresheafFiber V v ((Φ.skyscraperSheaf M).obj ⋙ forget (AddCommGrpCat.{u})) ≫
      ((Φ.presheafFiberCompIso (forget (AddCommGrpCat.{u}))).hom.app
        (Φ.skyscraperSheaf M).obj ≫
          (forget (AddCommGrpCat.{u})).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)

L135 ↗
Source context 6 commands

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

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

skyscraperAbelianUnderlyingSquare_comap

L137 ↗
EtaleFundamentalGroups.Cohomology.skyscraperAbelianUnderlyingSquare_comap
Source context 7 commands

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

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

abelianPullbackUnderlyingComparison_stalk_isIso

L162 ↗
EtaleFundamentalGroups.Cohomology.abelianPullbackUnderlyingComparison_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 CategoryTheory.Limits Opposite EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology
open scoped TwoSquare
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X)
local instance : RepresentablyFlat (etaleBaseChange f) := flat_of_preservesFiniteLimits _
Lean source · statement
lemma abelianPullbackUnderlyingComparison_stalk_isIso
    (F : Sheaf Y.smallEtaleTopology (AddCommGrpCat.{u})) :
    IsIso ((Scheme.pointSmallEtale s).sheafFiber.map
      ((abelianPullbackUnderlyingComparison f).app F))
lemma

abelianPullbackUnderlyingComparison_isIso

L216 ↗
EtaleFundamentalGroups.Cohomology.abelianPullbackUnderlyingComparison_isIso
Documentation

Geometric points detect that inverse image commutes with forgetting abelian group structure.

Source context 7 commands

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

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

abelianPullbackUnderlyingMateIso

L230 ↗
EtaleFundamentalGroups.Cohomology.abelianPullbackUnderlyingMateIso
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 CategoryTheory.Limits Opposite EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology
open scoped TwoSquare
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X)
local instance : RepresentablyFlat (etaleBaseChange f) := flat_of_preservesFiniteLimits _
Lean source · statement
def abelianPullbackUnderlyingMateIso :
    etaleAbelianPullback f ⋙ abelianUnderlying X ≅
      abelianUnderlying Y ⋙ etaleSetPullback f

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