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]
[HasForget D]
[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.{u_2, 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.{u_2, 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) (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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, u_1} E]
{G : Functor E D}
[G.IsLeftAdjoint]
:
@[deprecated CategoryTheory.Sheaf.composeAndSheafify (since := "2024-11-26")]
def
CategoryTheory.Sheaf.composeAndSheafifyFromTypes
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u_1}
{B : Type u_2}
[Category.{u_3, u_1} A]
[Category.{u_4, u_2} B]
(F : Functor A B)
[HasWeakSheafify J B]
:
Alias of CategoryTheory.Sheaf.composeAndSheafify.
This is the functor sending a sheaf X : Sheaf J A to the sheafification
of X.val ⋙ F.
Equations
Instances For
@[reducible, inline, deprecated CategoryTheory.Sheaf.adjunction (since := "2024-11-26")]
abbrev
CategoryTheory.Sheaf.adjunctionToTypes
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasWeakSheafify J D]
[HasForget D]
[J.HasSheafCompose (forget D)]
{G : Functor (Type (max v₁ u₁)) D}
(adj : G ⊣ forget D)
:
The adjunction composeAndSheafify J G ⊣ sheafForget J.