Module

SheafAdjunction.lean

Nyll.EtaleCohomology.Sites.SheafAdjunction

1 declaration indexed from sourceView source ↗

Module documentation

Fully faithful adjoints on sheaves

For an adjunction of continuous functors of sites with fully faithful left adjoint, the induced adjunction on sheaves has invertible counit. On each object of the source site, this counit is obtained by applying the sheaf to the opposite of the original unit, hence is an isomorphism.

The coefficient category is arbitrary. No limits, additive structure, schemes, or fields are needed.

Imports6

Mathlib.CategoryTheory.Sites.Continuous
Mathlib.CategoryTheory.Sites.Sheaf
Mathlib.CategoryTheory.Adjunction.FullyFaithful
Mathlib.CategoryTheory.Adjunction.Opposites
Mathlib.CategoryTheory.Adjunction.Whiskering
Mathlib.CategoryTheory.NatIso

Imported by2

lemma

sheafAdjunction_counit_isIso

L39 ↗

EtaleCohomology.Sites.sheafAdjunction_counit_isIso

Documentation

A fully faithful left adjoint between sites yields an invertible sheaf counit.

Source context 4 commands

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

universe uC vC uD vD uA vA
open CategoryTheory
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} {B : D ⥤ C} [G.IsContinuous J K] [B.IsContinuous K J]
  (A : Type uA) [Category.{vA} A] (adj : G ⊣ B) [G.Full] [G.Faithful]

Lean source · statement

lemma sheafAdjunction_counit_isIso :
    IsIso (adj.sheafPushforwardContinuous (E := A) J K).counit

Module documentation

Fully faithful adjoints on sheaves

Declarations

sheafAdjunction_counit_isIso