NYLL
Module

RestrictionAdjunction.lean

Nyll.EtaleCohomology.Sites.RestrictionAdjunction
4 declarations indexed from sourceView source ↗

Module documentation

Canonical counits and initial neighborhood functors

The colimit comparison for restriction agrees, under the stalk/skyscraper adjunctions, with restriction of maps into skyscraper sheaves. Initiality of the neighborhood functor therefore makes that restriction bijective on Hom sets. For any left adjoint to restriction, this proves that the canonical counit induces an isomorphism on the specified stalk.

The coefficient category only needs products and colimits of the size of the point. No additive, abelian, or scheme hypothesis is used.

Imports15
  • Nyll.EtaleCohomology.Sites.RestrictionStalks
  • Mathlib.CategoryTheory.Sites.Point.Comap
  • Mathlib.CategoryTheory.Sites.Point.Basic
  • Mathlib.CategoryTheory.Sites.Point.Skyscraper
  • Mathlib.CategoryTheory.Sites.Continuous
  • Mathlib.CategoryTheory.Sites.CoverPreserving
  • Mathlib.CategoryTheory.Sites.Sheaf
  • Mathlib.CategoryTheory.Elements
  • Mathlib.CategoryTheory.Functor.Flat
  • Mathlib.CategoryTheory.Functor.Category
  • Mathlib.CategoryTheory.Limits.Final
  • Mathlib.CategoryTheory.Limits.FinallySmall
  • Mathlib.CategoryTheory.Adjunction.Basic
  • Mathlib.CategoryTheory.Yoneda
  • Mathlib.CategoryTheory.Limits.Shapes.Products
Imported by2

Declarations

lemma

toPresheafFiber_restrictionComapStalkIso_hom

L53 ↗
EtaleCohomology.Sites.toPresheafFiber_restrictionComapStalkIso_hom
Documentation

The stalk comparison sends each section to its image in the original stalk.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleCohomology.Sites
universe w uC vC uD vD uA vA
variable {C : Type uC} [Category.{vC} C] {D : Type uD} [Category.{vD} D]
  {J : GrothendieckTopology C} {K : GrothendieckTopology D}
  (F : C ⥤ D) [RepresentablyFlat F] [F.IsContinuous J K]
  (hF : CoverPreserving J K F) (Φ : K.Point.{w})
  [InitiallySmall.{w} (F ⋙ Φ.fiber).Elements]
  (A : Type uA) [Category.{vA} A] [HasColimitsOfSize.{w, w} A]
  [(Functor.Elements.precomp F Φ.fiber).Initial]
Lean source · statement
lemma toPresheafFiber_restrictionComapStalkIso_hom
    (G : Sheaf K A) (X : C) (x : Φ.fiber.obj (F.obj X)) :
    (Φ.comap F hF).toPresheafFiber X x
        ((F.sheafPushforwardContinuous A J K).obj G).obj ≫
      (restrictionComapStalkIso F hF Φ A).hom.app G =
        Φ.toPresheafFiber (F.obj X) x G.obj
lemma

restrictionComapStalkIso_homEquiv

L67 ↗
EtaleCohomology.Sites.restrictionComapStalkIso_homEquiv
Documentation

Under the stalk/skyscraper adjunction, the colimit comparison is restriction of maps.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleCohomology.Sites
universe w uC vC uD vD uA vA
variable {C : Type uC} [Category.{vC} C] {D : Type uD} [Category.{vD} D]
  {J : GrothendieckTopology C} {K : GrothendieckTopology D}
  (F : C ⥤ D) [RepresentablyFlat F] [F.IsContinuous J K]
  (hF : CoverPreserving J K F) (Φ : K.Point.{w})
  [InitiallySmall.{w} (F ⋙ Φ.fiber).Elements]
  (A : Type uA) [Category.{vA} A] [HasColimitsOfSize.{w, w} A]
  [(Functor.Elements.precomp F Φ.fiber).Initial]
variable [HasProducts.{w} A]
Lean source · statement
lemma restrictionComapStalkIso_homEquiv
    (G : Sheaf K A) (M : A) (a : Φ.sheafFiber.obj G ⟶ M) :
    (Φ.comap F hF).skyscraperSheafAdjunction.homEquiv
        ((F.sheafPushforwardContinuous A J K).obj G) M
        ((restrictionComapStalkIso F hF Φ A).hom.app G ≫ a) =
      (F.sheafPushforwardContinuous A J K).map
        (Φ.skyscraperSheafAdjunction.homEquiv G M a)
lemma

restriction_skyscraperHom_bijective

L95 ↗
EtaleCohomology.Sites.restriction_skyscraperHom_bijective
Documentation

Initiality of the neighborhood functor makes restriction bijective on maps to skyscrapers.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleCohomology.Sites
universe w uC vC uD vD uA vA
variable {C : Type uC} [Category.{vC} C] {D : Type uD} [Category.{vD} D]
  {J : GrothendieckTopology C} {K : GrothendieckTopology D}
  (F : C ⥤ D) [RepresentablyFlat F] [F.IsContinuous J K]
  (hF : CoverPreserving J K F) (Φ : K.Point.{w})
  [InitiallySmall.{w} (F ⋙ Φ.fiber).Elements]
  (A : Type uA) [Category.{vA} A] [HasColimitsOfSize.{w, w} A]
  [(Functor.Elements.precomp F Φ.fiber).Initial]
variable [HasProducts.{w} A]
include hF in
Lean source · full declaration
lemma restriction_skyscraperHom_bijective (G : Sheaf K A) (M : A) :
    Function.Bijective (fun (a : G ⟶ Φ.skyscraperSheaf M) =>
      (F.sheafPushforwardContinuous A J K).map a) := by
  let e := (Φ.skyscraperSheafAdjunction.homEquiv G M).symm.trans
    ((Iso.homCongr ((restrictionComapStalkIso F hF Φ A).app G).symm (Iso.refl M)).trans
      ((Φ.comap F hF).skyscraperSheafAdjunction.homEquiv _ M))
  have he : (fun a => (F.sheafPushforwardContinuous A J K).map a) = e := by
    funext a
    dsimp [e, Iso.homCongr]
    rw [Category.comp_id, restrictionComapStalkIso_homEquiv, Equiv.apply_symm_apply]
  rw [he]
  exact e.bijective
lemma

restriction_counit_stalk_isIso

L112 ↗
EtaleCohomology.Sites.restriction_counit_stalk_isIso
Documentation

The actual adjunction counit is an isomorphism on the stalk with initial neighborhoods.

Source context 8 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleCohomology.Sites
universe w uC vC uD vD uA vA
variable {C : Type uC} [Category.{vC} C] {D : Type uD} [Category.{vD} D]
  {J : GrothendieckTopology C} {K : GrothendieckTopology D}
  (F : C ⥤ D) [RepresentablyFlat F] [F.IsContinuous J K]
  (hF : CoverPreserving J K F) (Φ : K.Point.{w})
  [InitiallySmall.{w} (F ⋙ Φ.fiber).Elements]
  (A : Type uA) [Category.{vA} A] [HasColimitsOfSize.{w, w} A]
  [(Functor.Elements.precomp F Φ.fiber).Initial]
variable [HasProducts.{w} A]
variable (L : Sheaf J A ⥤ Sheaf K A) (adj : L ⊣ F.sheafPushforwardContinuous A J K)
include hF in
Lean source · statement
lemma restriction_counit_stalk_isIso (G : Sheaf K A) :
    IsIso (Φ.sheafFiber.map (adj.counit.app G))

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