Module

PullbackUnitStalks.lean

Nyll.EtaleCohomology.Sites.PullbackUnitStalks

4 declarations indexed from sourceView source ↗

Module documentation

The actual unit on an inverse-image stalk

For a continuous functor of sites, restricting a germ at the comapped point gives a germ at the original point. Composing this concrete comparison with the adjunction unit is an isomorphism. The proof uses the stalk/skyscraper adjunctions and computes the map on representing sections; it requires no initiality of the functor between pointed neighborhoods.

Imports12

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.Limits.FinallySmall
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.Yoneda
Mathlib.CategoryTheory.Limits.Shapes.Products

Imported by2

def

restrictionComapStalkMap

L47 ↗

EtaleCohomology.Sites.restrictionComapStalkMap

Documentation

A direct-image germ at the comapped point restricts to its original germ.

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]

Lean source · statement

def restrictionComapStalkMap (G : Sheaf K A) :
    (Φ.comap F hF).sheafFiber.obj ((F.sheafPushforwardContinuous A J K).obj G) ⟶
      Φ.sheafFiber.obj G

lemma

toPresheafFiber_restrictionComapStalkMap

L55 ↗

EtaleCohomology.Sites.toPresheafFiber_restrictionComapStalkMap

Documentation

The direct-image stalk comparison sends a representing section to its germ.

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]

Lean source · statement

lemma toPresheafFiber_restrictionComapStalkMap
    (G : Sheaf K A) (U : C) (u : Φ.fiber.obj (F.obj U)) :
    (Φ.comap F hF).toPresheafFiber U u
        ((F.sheafPushforwardContinuous A J K).obj G).obj ≫
      restrictionComapStalkMap F hF Φ A G = Φ.toPresheafFiber (F.obj U) u G.obj

lemma

restrictionComapStalkMap_homEquiv

L65 ↗

EtaleCohomology.Sites.restrictionComapStalkMap_homEquiv

Documentation

Under the stalk/skyscraper adjunction, the concrete comparison is restriction.

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]
variable [HasProducts.{w} A]

Lean source · statement

lemma restrictionComapStalkMap_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
        (restrictionComapStalkMap F hF Φ A G ≫ a) =
      (F.sheafPushforwardContinuous A J K).map
        (Φ.skyscraperSheafAdjunction.homEquiv G M a)

theorem

unit_restrictionComapStalkMap_isIso

L95 ↗

EtaleCohomology.Sites.unit_restrictionComapStalkMap_isIso

Documentation

The actual unit followed by restriction of germs is the inverse-image stalk isomorphism, for any left adjoint to direct image.

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]
variable [HasProducts.{w} A]
variable (L : Sheaf J A ⥤ Sheaf K A) (adj : L ⊣ F.sheafPushforwardContinuous A J K)

Lean source · statement

theorem unit_restrictionComapStalkMap_isIso (G : Sheaf J A) :
    IsIso ((Φ.comap F hF).sheafFiber.map (adj.unit.app G) ≫
      restrictionComapStalkMap F hF Φ A (L.obj G))

Module documentation

The actual unit on an inverse-image stalk

Declarations

restrictionComapStalkMap

toPresheafFiber_restrictionComapStalkMap

restrictionComapStalkMap_homEquiv

unit_restrictionComapStalkMap_isIso