THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file, we show that an adjunction F ⊣ G induces an adjunction between
categories of sheaves, under certain hypotheses on F and G.
@[reducible]
def
category_theory.Sheaf_forget
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.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.
@[reducible]
noncomputable
def
category_theory.Sheaf.compose_and_sheafify
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(G : E ⥤ D) :
This is the functor sending a sheaf X : Sheaf J E to the sheafification
of X ⋙ G.
@[simp]
theorem
category_theory.Sheaf.compose_equiv_symm_apply_val
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
{F : D ⥤ E}
{G : E ⥤ D}
[Π (X : C) (S : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (S.index P).multicospan F]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(adj : G ⊣ F)
(X : category_theory.Sheaf J E)
(Y : category_theory.Sheaf J D)
(γ : X ⟶ (category_theory.Sheaf_compose J F).obj Y) :
(⇑((category_theory.Sheaf.compose_equiv J adj X Y).symm) γ).val = J.sheafify_lift (⇑(((category_theory.adjunction.whisker_right Cᵒᵖ adj).hom_equiv ((category_theory.Sheaf_to_presheaf J E).obj X) Y.val).symm) ((category_theory.Sheaf_to_presheaf J E).map γ)) _
noncomputable
def
category_theory.Sheaf.compose_equiv
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
{F : D ⥤ E}
{G : E ⥤ D}
[Π (X : C) (S : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (S.index P).multicospan F]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(adj : G ⊣ F)
(X : category_theory.Sheaf J E)
(Y : category_theory.Sheaf J D) :
((category_theory.Sheaf.compose_and_sheafify J G).obj X ⟶ Y) ≃ (X ⟶ (category_theory.Sheaf_compose J F).obj Y)
An auxiliary definition to be used in defining category_theory.Sheaf.adjunction below.
Equations
- category_theory.Sheaf.compose_equiv J adj X Y = let A : (category_theory.whiskering_right Cᵒᵖ E D).obj G ⊣ (category_theory.whiskering_right Cᵒᵖ D E).obj F := category_theory.adjunction.whisker_right Cᵒᵖ adj in {to_fun := λ (η : (category_theory.Sheaf.compose_and_sheafify J G).obj X ⟶ Y), {val := ⇑(A.hom_equiv ((category_theory.Sheaf_to_presheaf J E).obj X) Y.val) (J.to_sheafify (((category_theory.whiskering_right Cᵒᵖ E D).obj G).obj ((category_theory.Sheaf_to_presheaf J E).obj X)) ≫ η.val)}, inv_fun := λ (γ : X ⟶ (category_theory.Sheaf_compose J F).obj Y), {val := J.sheafify_lift (⇑((A.hom_equiv ((category_theory.Sheaf_to_presheaf J E).obj X) Y.val).symm) ((category_theory.Sheaf_to_presheaf J E).map γ)) _}, left_inv := _, right_inv := _}
@[simp]
theorem
category_theory.Sheaf.compose_equiv_apply_val
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
{F : D ⥤ E}
{G : E ⥤ D}
[Π (X : C) (S : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (S.index P).multicospan F]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(adj : G ⊣ F)
(X : category_theory.Sheaf J E)
(Y : category_theory.Sheaf J D)
(η : (category_theory.Sheaf.compose_and_sheafify J G).obj X ⟶ Y) :
(⇑(category_theory.Sheaf.compose_equiv J adj X Y) η).val = ⇑((category_theory.adjunction.whisker_right Cᵒᵖ adj).hom_equiv ((category_theory.Sheaf_to_presheaf J E).obj X) Y.val) (J.to_sheafify (((category_theory.whiskering_right Cᵒᵖ E D).obj G).obj ((category_theory.Sheaf_to_presheaf J E).obj X)) ≫ η.val)
@[simp]
theorem
category_theory.Sheaf.adjunction_counit_app_val
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
{F : D ⥤ E}
{G : E ⥤ D}
[Π (X : C) (S : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (S.index P).multicospan F]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(adj : G ⊣ F)
(Y : category_theory.Sheaf J D) :
noncomputable
def
category_theory.Sheaf.adjunction
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
{F : D ⥤ E}
{G : E ⥤ D}
[Π (X : C) (S : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (S.index P).multicospan F]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(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 F preserves the correct limits.
@[simp]
theorem
category_theory.Sheaf.adjunction_unit_app_val
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
{F : D ⥤ E}
{G : E ⥤ D}
[Π (X : C) (S : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (S.index P).multicospan F]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(adj : G ⊣ F)
(X : category_theory.Sheaf J E) :
((category_theory.Sheaf.adjunction J adj).unit.app X).val = (category_theory.adjunction.whisker_right Cᵒᵖ adj).unit.app X.val ≫ category_theory.whisker_right (J.to_sheafify (X.val ⋙ G)) F
@[protected, instance]
noncomputable
def
category_theory.Sheaf.category_theory.Sheaf_compose.category_theory.is_right_adjoint
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
{F : D ⥤ E}
[Π (X : C) (S : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (S.index P).multicospan F]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
[category_theory.is_right_adjoint F] :
@[reducible]
noncomputable
def
category_theory.Sheaf.compose_and_sheafify_from_types
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(G : Type (max v u) ⥤ D) :
This is the functor sending a sheaf of types X to the sheafification of X ⋙ G.
noncomputable
def
category_theory.Sheaf.adjunction_to_types
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
{G : Type (max v u) ⥤ D}
(adj : G ⊣ category_theory.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
@[simp]
theorem
category_theory.Sheaf.adjunction_to_types_unit_app_val
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
{G : Type (max v u) ⥤ D}
(adj : G ⊣ category_theory.forget D)
(Y : category_theory.SheafOfTypes J) :
((category_theory.Sheaf.adjunction_to_types J adj).unit.app Y).val = (category_theory.adjunction.whisker_right Cᵒᵖ adj).unit.app ((category_theory.SheafOfTypes_to_presheaf J).obj Y) ≫ category_theory.whisker_right (J.to_sheafify (((category_theory.whiskering_right Cᵒᵖ (Type (max v u)) D).obj G).obj ((𝟭 (category_theory.SheafOfTypes J)).obj Y).val)) (category_theory.forget D)
@[simp]
theorem
category_theory.Sheaf.adjunction_to_types_counit_app_val
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
{G : Type (max v u) ⥤ D}
(adj : G ⊣ category_theory.forget D)
(X : category_theory.Sheaf J D) :
((category_theory.Sheaf.adjunction_to_types J adj).counit.app X).val = J.sheafify_lift ((X.val.associator (category_theory.forget D) G).hom ≫ (category_theory.adjunction.whisker_right Cᵒᵖ adj).counit.app X.val) _
@[protected, instance]
noncomputable
def
category_theory.Sheaf.category_theory.Sheaf_forget.category_theory.is_right_adjoint
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
[category_theory.is_right_adjoint (category_theory.forget D)] :
Equations
- category_theory.Sheaf.category_theory.Sheaf_forget.category_theory.is_right_adjoint J = {left := category_theory.Sheaf.compose_and_sheafify_from_types J (category_theory.left_adjoint (category_theory.forget D)), adj := category_theory.Sheaf.adjunction_to_types J (category_theory.adjunction.of_right_adjoint (category_theory.forget D))}