Module

RestrictionStalks.lean

Nyll.EtaleCohomology.Sites.RestrictionStalks

1 declaration indexed from sourceView source ↗

Module documentation

Stalks of restriction under an initial neighborhood functor

If a continuous functor is initial on the categories of pointed neighborhoods, restriction of sheaves preserves the corresponding stalk. The opposite neighborhood functor is final, so the result follows from the comparison of colimits. The coefficient category only needs colimits of the size of the points; no abelian structure or scheme hypothesis is used.

Imports10

Mathlib.CategoryTheory.Sites.Point.Comap
Mathlib.CategoryTheory.Sites.Point.Basic
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

Imported by3

def

restrictionComapStalkIso

L46 ↗

EtaleCohomology.Sites.restrictionComapStalkIso

Documentation

Restriction along a continuous functor preserves the stalk when the induced functor on pointed neighborhoods is initial.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
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

def restrictionComapStalkIso :
    F.sheafPushforwardContinuous A J K ⋙ (Φ.comap F hF).sheafFiber ≅ Φ.sheafFiber

Module documentation

Stalks of restriction under an initial neighborhood functor

Declarations

restrictionComapStalkIso