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)]
:
The forgetful functor from Sheaf J D to sheaves of types, for a concrete category D
whose forgetful functor preserves the correct limits.
Equations
- CategoryTheory.sheafForget J = (CategoryTheory.sheafCompose J (CategoryTheory.forget D)).comp (CategoryTheory.sheafEquivSheafOfTypes J).functor
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
@[reducible, inline]
abbrev
CategoryTheory.Sheaf.composeAndSheafifyFromTypes
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(J : CategoryTheory.GrothendieckTopology C)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.HasWeakSheafify J D]
(G : CategoryTheory.Functor (Type (max v₁ u₁)) D)
:
This is the functor sending a sheaf of types X to the sheafification of X ⋙ G.
Equations
Instances For
def
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)
:
A variant of the adjunction between sheaf categories, in the case where the right adjoint is the forgetful functor to sheaves of types.
Equations
- CategoryTheory.Sheaf.adjunctionToTypes J adj = (CategoryTheory.sheafEquivSheafOfTypes J).symm.toAdjunction.comp (CategoryTheory.Sheaf.adjunction J adj)
Instances For
@[simp]
theorem
CategoryTheory.Sheaf.adjunctionToTypes_unit_app_val
{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)
(Y : CategoryTheory.SheafOfTypes J)
:
((CategoryTheory.Sheaf.adjunctionToTypes J adj).unit.app Y).val = CategoryTheory.CategoryStruct.comp
((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).unit.app ((CategoryTheory.sheafOfTypesToPresheaf J).obj Y))
(CategoryTheory.whiskerRight
(CategoryTheory.toSheafify J
(((CategoryTheory.whiskeringRight Cᵒᵖ (Type (max v₁ u₁)) D).obj G).obj
((CategoryTheory.sheafOfTypesToPresheaf J).obj Y)))
(CategoryTheory.forget D))
@[simp]
theorem
CategoryTheory.Sheaf.adjunctionToTypes_counit_app_val
{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)
(X : CategoryTheory.Sheaf J D)
:
((CategoryTheory.Sheaf.adjunctionToTypes J adj).counit.app X).val = CategoryTheory.sheafifyLift J
(CategoryTheory.CategoryStruct.comp (X.1.associator (CategoryTheory.forget D) G).hom
((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).counit.app X.1))
⋯
instance
CategoryTheory.Sheaf.instIsRightAdjointSheafOfTypesSheafForgetOfForget
{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)]
[(CategoryTheory.forget D).IsRightAdjoint]
:
(CategoryTheory.sheafForget J).IsRightAdjoint
Equations
- ⋯ = ⋯