Module

StalkAdjunction.lean

Nyll.EtaleCohomology.Sites.StalkAdjunction

4 declarations indexed from sourceView source ↗

Module documentation

Stalks of a left adjoint to restriction

Let G be a continuous functor of sites. A comparison of the fiber functors of two points induces a comparison of their skyscraper functors. If L is left adjoint to restriction along G, taking mates gives the corresponding comparison of stalks after L.

When the restricted fiber functor has no elements, the restricted skyscraper and the stalk after L are zero. The coefficient category needs products and, for stalks, colimits of the size of the points. Only the vanishing statements require zero morphisms. No scheme, field, coefficient ring, or abelian-category hypothesis is used.

The geometric comparisons and the adjunction are supplied by concrete constructions when this result is applied to extension by zero.

Imports9

Mathlib.CategoryTheory.Sites.Point.Skyscraper
Mathlib.CategoryTheory.Sites.Continuous
Mathlib.CategoryTheory.Sites.Sheaf
Mathlib.CategoryTheory.Adjunction.Mates
Mathlib.CategoryTheory.Functor.Category
Mathlib.CategoryTheory.Opposites
Mathlib.CategoryTheory.Limits.Shapes.Products
Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Mathlib.CategoryTheory.Sites.Limits

Imported by2

def

restrictionSkyscraperIso

L51 ↗

EtaleCohomology.Sites.restrictionSkyscraperIso

Documentation

A comparison of fiber functors gives a comparison of restricted skyscrapers.

Source context 5 commands

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

noncomputable section
universe w uC vC uD vD uA vA
open CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology.Sites
variable {C : Type uC} [Category.{vC} C] {D : Type uD} [Category.{vD} D]
  {J : GrothendieckTopology C} {K : GrothendieckTopology D}
  (G : C ⥤ D) [G.IsContinuous J K]
  (A : Type uA) [Category.{vA} A] [HasProducts.{w} A]
  (Φ : K.Point.{w}) (Ψ : J.Point.{w}) (e : G ⋙ Φ.fiber ≅ Ψ.fiber)

Lean source · statement

def restrictionSkyscraperIso :
    Φ.skyscraperSheafFunctor (A := A) ⋙ G.sheafPushforwardContinuous A J K ≅
      Ψ.skyscraperSheafFunctor

def

adjunctionStalkIso

L62 ↗

EtaleCohomology.Sites.adjunctionStalkIso

Documentation

A left adjoint to restriction has the stalk specified by the fiber comparison.

Source context 6 commands

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

noncomputable section
universe w uC vC uD vD uA vA
open CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology.Sites
variable {C : Type uC} [Category.{vC} C] {D : Type uD} [Category.{vD} D]
  {J : GrothendieckTopology C} {K : GrothendieckTopology D}
  (G : C ⥤ D) [G.IsContinuous J K]
  (A : Type uA) [Category.{vA} A] [HasProducts.{w} A]
  (Φ : K.Point.{w}) (Ψ : J.Point.{w}) (e : G ⋙ Φ.fiber ≅ Ψ.fiber)
variable [HasColimitsOfSize.{w, w} A]
  (L : Sheaf J A ⥤ Sheaf K A) (adj : L ⊣ G.sheafPushforwardContinuous A J K)

Lean source · statement

def adjunctionStalkIso : L ⋙ Φ.sheafFiber ≅ Ψ.sheafFiber

lemma

restrictionSkyscraper_isZero

L70 ↗

EtaleCohomology.Sites.restrictionSkyscraper_isZero

Documentation

Restricting a skyscraper gives zero when all its indexing sets are empty.

Source context 8 commands

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

noncomputable section
universe w uC vC uD vD uA vA
open CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology.Sites
variable {C : Type uC} [Category.{vC} C] {D : Type uD} [Category.{vD} D]
  {J : GrothendieckTopology C} {K : GrothendieckTopology D}
  (G : C ⥤ D) [G.IsContinuous J K]
  (A : Type uA) [Category.{vA} A] [HasProducts.{w} A]
  (Φ : K.Point.{w}) (Ψ : J.Point.{w}) (e : G ⋙ Φ.fiber ≅ Ψ.fiber)
variable [HasColimitsOfSize.{w, w} A]
  (L : Sheaf J A ⥤ Sheaf K A) (adj : L ⊣ G.sheafPushforwardContinuous A J K)
variable [HasZeroMorphisms A]
omit [HasColimitsOfSize.{w, w} A] in

Lean source · statement

lemma restrictionSkyscraper_isZero
    (h : ∀ V : C, IsEmpty (Φ.fiber.obj (G.obj V))) (M : A) :
    IsZero ((G.sheafPushforwardContinuous A J K).obj (Φ.skyscraperSheafFunctor.obj M))

lemma

adjunctionStalk_isZero

L85 ↗

EtaleCohomology.Sites.adjunctionStalk_isZero

Documentation

The stalk after a left adjoint to restriction vanishes when its fiber has no lifts.

Source context 8 commands

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

noncomputable section
universe w uC vC uD vD uA vA
open CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology.Sites
variable {C : Type uC} [Category.{vC} C] {D : Type uD} [Category.{vD} D]
  {J : GrothendieckTopology C} {K : GrothendieckTopology D}
  (G : C ⥤ D) [G.IsContinuous J K]
  (A : Type uA) [Category.{vA} A] [HasProducts.{w} A]
  (Φ : K.Point.{w}) (Ψ : J.Point.{w}) (e : G ⋙ Φ.fiber ≅ Ψ.fiber)
variable [HasColimitsOfSize.{w, w} A]
  (L : Sheaf J A ⥤ Sheaf K A) (adj : L ⊣ G.sheafPushforwardContinuous A J K)
variable [HasZeroMorphisms A]
include adj in

Lean source · statement

lemma adjunctionStalk_isZero
    (h : ∀ V : C, IsEmpty (Φ.fiber.obj (G.obj V))) (F : Sheaf J A) :
    IsZero (Φ.sheafFiber.obj (L.obj F))

Module documentation

Stalks of a left adjoint to restriction

Declarations

restrictionSkyscraperIso

adjunctionStalkIso

restrictionSkyscraper_isZero

adjunctionStalk_isZero