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₁}
[CategoryTheory.Category.{v₁, u₁} C]
(J : CategoryTheory.GrothendieckTopology C)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.ConcreteCategory D]
[J.HasSheafCompose (CategoryTheory.forget D)]
:
CategoryTheory.Functor (CategoryTheory.Sheaf J D) (CategoryTheory.Sheaf J (Type u_2))
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
(J : CategoryTheory.GrothendieckTopology C)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u_1}
[CategoryTheory.Category.{u_2, u_1} E]
{F : CategoryTheory.Functor D E}
{G : CategoryTheory.Functor E D}
[CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
(J : CategoryTheory.GrothendieckTopology C)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u_1}
[CategoryTheory.Category.{u_2, u_1} E]
{F : CategoryTheory.Functor D E}
{G : CategoryTheory.Functor E D}
[CategoryTheory.HasWeakSheafify J D]
[J.HasSheafCompose F]
(adj : G ⊣ F)
(X : CategoryTheory.Sheaf J E)
:
((CategoryTheory.Sheaf.adjunction J adj).unit.app X).val = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.val)
(CategoryTheory.whiskerRight (CategoryTheory.toSheafify J (X.val.comp G)) F)
@[simp]
theorem
CategoryTheory.Sheaf.adjunction_counit_app_val
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(J : CategoryTheory.GrothendieckTopology C)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u_1}
[CategoryTheory.Category.{u_2, u_1} E]
{F : CategoryTheory.Functor D E}
{G : CategoryTheory.Functor E D}
[CategoryTheory.HasWeakSheafify J D]
[J.HasSheafCompose F]
(adj : G ⊣ F)
(Y : CategoryTheory.Sheaf J D)
:
((CategoryTheory.Sheaf.adjunction J adj).counit.app Y).val = CategoryTheory.sheafifyLift J ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).counit.app Y.val) ⋯
instance
CategoryTheory.Sheaf.instIsRightAdjointSheafComposeOfHasWeakSheafify
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(J : CategoryTheory.GrothendieckTopology C)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u_1}
[CategoryTheory.Category.{u_2, u_1} E]
{F : CategoryTheory.Functor D E}
[CategoryTheory.HasWeakSheafify J D]
[F.IsRightAdjoint]
:
(CategoryTheory.sheafCompose J F).IsRightAdjoint
instance
CategoryTheory.Sheaf.instIsLeftAdjointComposeAndSheafify
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(J : CategoryTheory.GrothendieckTopology C)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u_1}
[CategoryTheory.Category.{u_2, u_1} E]
{G : CategoryTheory.Functor E D}
[CategoryTheory.HasWeakSheafify J D]
[G.IsLeftAdjoint]
:
(CategoryTheory.Sheaf.composeAndSheafify J G).IsLeftAdjoint
theorem
CategoryTheory.Sheaf.preservesSheafification_of_adjunction
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(J : CategoryTheory.GrothendieckTopology C)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u_1}
[CategoryTheory.Category.{u_2, u_1} E]
{F : CategoryTheory.Functor D E}
{G : CategoryTheory.Functor E D}
(adj : G ⊣ F)
:
J.PreservesSheafification G
instance
CategoryTheory.Sheaf.instPreservesSheafificationOfIsLeftAdjoint
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(J : CategoryTheory.GrothendieckTopology C)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u_1}
[CategoryTheory.Category.{u_2, u_1} E]
{G : CategoryTheory.Functor E D}
[G.IsLeftAdjoint]
:
J.PreservesSheafification G
@[deprecated CategoryTheory.Sheaf.composeAndSheafify]
def
CategoryTheory.Sheaf.composeAndSheafifyFromTypes
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u_1}
{B : Type u_2}
[CategoryTheory.Category.{u_3, u_1} A]
[CategoryTheory.Category.{u_4, u_2} B]
(F : CategoryTheory.Functor A B)
[CategoryTheory.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]
abbrev
CategoryTheory.Sheaf.adjunctionToTypes
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(J : CategoryTheory.GrothendieckTopology C)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.HasWeakSheafify J D]
[CategoryTheory.ConcreteCategory D]
[J.HasSheafCompose (CategoryTheory.forget D)]
{G : CategoryTheory.Functor (Type (max v₁ u₁)) D}
(adj : G ⊣ CategoryTheory.forget D)
:
The adjunction composeAndSheafify J G ⊣ sheafForget J.