In this file, we show that an adjunction G ⊣ F induces an adjunction between
categories of sheaves. We also show that G preserves sheafification.
@[reducible, inline]
abbrev
CategoryTheory.sheafForget
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
{D : Type u₂}
[Category.{v₂, u₂} D]
{FD : D → D → Type u_2}
{CD : D → Type u_3}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
[J.HasSheafCompose (forget D)]
:
The forgetful functor from Sheaf J D to sheaves of types, for a concrete category D
whose forgetful functor preserves the correct limits.
Equations
Instances For
def
CategoryTheory.Sheaf.adjunction
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u_1}
[Category.{v_1, u_1} E]
{F : Functor D E}
{G : Functor E D}
[HasWeakSheafify J D]
[J.HasSheafCompose F]
(adj : G ⊣ F)
:
An adjunction adj : G ⊣ F with F : D ⥤ E and G : E ⥤ D induces an adjunction
between Sheaf J D and Sheaf J E, in contexts where one can sheafify D-valued presheaves,
and postcomposing with F preserves the property of being a sheaf.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Sheaf.adjunction_unit_app_val
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u_1}
[Category.{v_1, u_1} E]
{F : Functor D E}
{G : Functor E D}
[HasWeakSheafify J D]
[J.HasSheafCompose F]
(adj : G ⊣ F)
(X : Sheaf J E)
:
((adjunction J adj).unit.app X).val = CategoryStruct.comp ((Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.val)
(Functor.whiskerRight (toSheafify J (X.val.comp G)) F)
@[simp]
theorem
CategoryTheory.Sheaf.adjunction_counit_app_val
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u_1}
[Category.{v_1, u_1} E]
{F : Functor D E}
{G : Functor E D}
[HasWeakSheafify J D]
[J.HasSheafCompose F]
(adj : G ⊣ F)
(Y : Sheaf J D)
:
((adjunction J adj).counit.app Y).val = sheafifyLift J ((Adjunction.whiskerRight Cᵒᵖ adj).counit.app Y.val) ⋯
instance
CategoryTheory.Sheaf.instIsRightAdjointSheafComposeOfHasWeakSheafify
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u_1}
[Category.{v_1, u_1} E]
{F : Functor D E}
[HasWeakSheafify J D]
[F.IsRightAdjoint]
:
(sheafCompose J F).IsRightAdjoint
instance
CategoryTheory.Sheaf.instIsLeftAdjointComposeAndSheafify
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u_1}
[Category.{v_1, u_1} E]
{G : Functor E D}
[HasWeakSheafify J D]
[G.IsLeftAdjoint]
:
theorem
CategoryTheory.Sheaf.preservesSheafification_of_adjunction
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u_1}
[Category.{v_1, u_1} E]
{F : Functor D E}
{G : Functor E D}
(adj : G ⊣ F)
:
instance
CategoryTheory.Sheaf.instPreservesSheafificationOfIsLeftAdjoint
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u_1}
[Category.{v_1, u_1} E]
{G : Functor E D}
[G.IsLeftAdjoint]
: