Adjunctions and limits #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A left adjoint preserves colimits (category_theory.adjunction.left_adjoint_preserves_colimits),
and a right adjoint preserves limits (category_theory.adjunction.right_adjoint_preserves_limits).
Equivalences create and reflect (co)limits.
(category_theory.adjunction.is_equivalence_creates_limits,
category_theory.adjunction.is_equivalence_creates_colimits,
category_theory.adjunction.is_equivalence_reflects_limits,
category_theory.adjunction.is_equivalence_reflects_colimits,)
In category_theory.adjunction.cocones_iso we show that
when F ⊣ G,
the functor associating to each Y the cocones over K ⋙ F with cone point Y
is naturally isomorphic to
the functor associating to each Y the cocones over K with cone point G.obj Y.
def
category_theory.adjunction.functoriality_right_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
(K : J ⥤ C) :
The right adjoint of cocones.functoriality K F : cocone K ⥤ cocone (K ⋙ F).
Auxiliary definition for functoriality_is_left_adjoint.
Equations
- adj.functoriality_right_adjoint K = category_theory.limits.cocones.functoriality (K ⋙ F) G ⋙ category_theory.limits.cocones.precompose (K.right_unitor.inv ≫ category_theory.whisker_left K adj.unit ≫ (K.associator F G).inv)
def
category_theory.adjunction.functoriality_unit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
(K : J ⥤ C) :
The unit for the adjunction for cocones.functoriality K F : cocone K ⥤ cocone (K ⋙ F).
Auxiliary definition for functoriality_is_left_adjoint.
Equations
- adj.functoriality_unit K = {app := λ (c : category_theory.limits.cocone K), {hom := adj.unit.app c.X, w' := _}, naturality' := _}
@[simp]
theorem
category_theory.adjunction.functoriality_unit_app_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
(K : J ⥤ C)
(c : category_theory.limits.cocone K) :
def
category_theory.adjunction.functoriality_counit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
(K : J ⥤ C) :
The counit for the adjunction for cocones.functoriality K F : cocone K ⥤ cocone (K ⋙ F).
Auxiliary definition for functoriality_is_left_adjoint.
Equations
- adj.functoriality_counit K = {app := λ (c : category_theory.limits.cocone (K ⋙ F)), {hom := adj.counit.app c.X, w' := _}, naturality' := _}
@[simp]
theorem
category_theory.adjunction.functoriality_counit_app_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
(K : J ⥤ C)
(c : category_theory.limits.cocone (K ⋙ F)) :
def
category_theory.adjunction.functoriality_is_left_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
(K : J ⥤ C) :
The functor cocones.functoriality K F : cocone K ⥤ cocone (K ⋙ F) is a left adjoint.
Equations
- adj.functoriality_is_left_adjoint K = {right := adj.functoriality_right_adjoint K, adj := category_theory.adjunction.mk_of_unit_counit {unit := adj.functoriality_unit K, counit := adj.functoriality_counit K, left_triangle' := _, right_triangle' := _}}
def
category_theory.adjunction.left_adjoint_preserves_colimits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G) :
A left adjoint preserves colimits.
See https://stacks.math.columbia.edu/tag/0038.
Equations
- adj.left_adjoint_preserves_colimits = {preserves_colimits_of_shape := λ (J : Type u) (𝒥 : category_theory.category J), {preserves_colimit := λ (F_1 : J ⥤ C), {preserves := λ (c : category_theory.limits.cocone F_1) (hc : category_theory.limits.is_colimit c), category_theory.limits.is_colimit.iso_unique_cocone_morphism.inv (λ (s : category_theory.limits.cocone (F_1 ⋙ F)), (category_theory.is_left_adjoint.adj.hom_equiv c s).unique)}}}
@[protected, instance]
def
category_theory.adjunction.is_equivalence_preserves_colimits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(E : C ⥤ D)
[category_theory.is_equivalence E] :
@[protected, instance]
def
category_theory.adjunction.is_equivalence_reflects_colimits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(E : D ⥤ C)
[category_theory.is_equivalence E] :
Equations
- category_theory.adjunction.is_equivalence_reflects_colimits E = {reflects_colimits_of_shape := λ (J : Type u) (𝒥 : category_theory.category J), {reflects_colimit := λ (K : J ⥤ D), {reflects := λ (c : category_theory.limits.cocone K) (t : category_theory.limits.is_colimit (E.map_cocone c)), (⇑((category_theory.limits.is_colimit.precompose_inv_equiv K.right_unitor ((𝟭 D).map_cocone c)).symm) (category_theory.limits.is_colimit.map_cocone_equiv E.as_equivalence.unit_iso.symm (category_theory.limits.is_colimit_of_preserves E.inv t))).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.adjunction.is_equivalence_reflects_colimits._aux_1 J 𝒥 K c) _)}}}
@[protected, instance]
def
category_theory.adjunction.is_equivalence_creates_colimits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(H : D ⥤ C)
[category_theory.is_equivalence H] :
Equations
- category_theory.adjunction.is_equivalence_creates_colimits H = {creates_colimits_of_shape := λ (J : Type u) (𝒥 : category_theory.category J), {creates_colimit := λ (F : J ⥤ D), {to_reflects_colimit := category_theory.limits.reflects_colimit_of_reflects_colimits_of_shape F H (category_theory.limits.reflects_colimits_of_shape_of_reflects_colimits J H), lifts := λ (c : category_theory.limits.cocone (F ⋙ H)) (t : category_theory.limits.is_colimit c), {lifted_cocone := H.map_cocone_inv c, valid_lift := H.map_cocone_map_cocone_inv c}}}}
theorem
category_theory.adjunction.has_colimit_comp_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type u}
[category_theory.category J]
(K : J ⥤ C)
(E : C ⥤ D)
[category_theory.is_equivalence E]
[category_theory.limits.has_colimit K] :
theorem
category_theory.adjunction.has_colimit_of_comp_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type u}
[category_theory.category J]
(K : J ⥤ C)
(E : C ⥤ D)
[category_theory.is_equivalence E]
[category_theory.limits.has_colimit (K ⋙ E)] :
theorem
category_theory.adjunction.has_colimits_of_shape_of_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type u}
[category_theory.category J]
(E : C ⥤ D)
[category_theory.is_equivalence E]
[category_theory.limits.has_colimits_of_shape J D] :
Transport a has_colimits_of_shape instance across an equivalence.
theorem
category_theory.adjunction.has_colimits_of_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(E : C ⥤ D)
[category_theory.is_equivalence E]
[category_theory.limits.has_colimits_of_size D] :
Transport a has_colimits instance across an equivalence.
def
category_theory.adjunction.functoriality_left_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
(K : J ⥤ D) :
The left adjoint of cones.functoriality K G : cone K ⥤ cone (K ⋙ G).
Auxiliary definition for functoriality_is_right_adjoint.
Equations
- adj.functoriality_left_adjoint K = category_theory.limits.cones.functoriality (K ⋙ G) F ⋙ category_theory.limits.cones.postcompose ((K.associator G F).hom ≫ category_theory.whisker_left K adj.counit ≫ K.right_unitor.hom)
@[simp]
theorem
category_theory.adjunction.functoriality_unit'_app_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
(K : J ⥤ D)
(c : category_theory.limits.cone (K ⋙ G)) :
def
category_theory.adjunction.functoriality_unit'
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
(K : J ⥤ D) :
The unit for the adjunction forcones.functoriality K G : cone K ⥤ cone (K ⋙ G).
Auxiliary definition for functoriality_is_right_adjoint.
Equations
- adj.functoriality_unit' K = {app := λ (c : category_theory.limits.cone (K ⋙ G)), {hom := adj.unit.app c.X, w' := _}, naturality' := _}
def
category_theory.adjunction.functoriality_counit'
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
(K : J ⥤ D) :
The counit for the adjunction forcones.functoriality K G : cone K ⥤ cone (K ⋙ G).
Auxiliary definition for functoriality_is_right_adjoint.
Equations
- adj.functoriality_counit' K = {app := λ (c : category_theory.limits.cone K), {hom := adj.counit.app c.X, w' := _}, naturality' := _}
@[simp]
theorem
category_theory.adjunction.functoriality_counit'_app_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
(K : J ⥤ D)
(c : category_theory.limits.cone K) :
def
category_theory.adjunction.functoriality_is_right_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
(K : J ⥤ D) :
The functor cones.functoriality K G : cone K ⥤ cone (K ⋙ G) is a right adjoint.
Equations
- adj.functoriality_is_right_adjoint K = {left := adj.functoriality_left_adjoint K, adj := category_theory.adjunction.mk_of_unit_counit {unit := adj.functoriality_unit' K, counit := adj.functoriality_counit' K, left_triangle' := _, right_triangle' := _}}
def
category_theory.adjunction.right_adjoint_preserves_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G) :
A right adjoint preserves limits.
See https://stacks.math.columbia.edu/tag/0038.
Equations
- adj.right_adjoint_preserves_limits = {preserves_limits_of_shape := λ (J : Type u) (𝒥 : category_theory.category J), {preserves_limit := λ (K : J ⥤ D), {preserves := λ (c : category_theory.limits.cone K) (hc : category_theory.limits.is_limit c), category_theory.limits.is_limit.iso_unique_cone_morphism.inv (λ (s : category_theory.limits.cone (K ⋙ G)), (category_theory.is_right_adjoint.adj.hom_equiv s c).symm.unique)}}}
@[protected, instance]
def
category_theory.adjunction.is_equivalence_preserves_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(E : D ⥤ C)
[category_theory.is_equivalence E] :
@[protected, instance]
def
category_theory.adjunction.is_equivalence_reflects_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(E : D ⥤ C)
[category_theory.is_equivalence E] :
Equations
- category_theory.adjunction.is_equivalence_reflects_limits E = {reflects_limits_of_shape := λ (J : Type u) (𝒥 : category_theory.category J), {reflects_limit := λ (K : J ⥤ D), {reflects := λ (c : category_theory.limits.cone K) (t : category_theory.limits.is_limit (E.map_cone c)), (⇑((category_theory.limits.is_limit.postcompose_hom_equiv K.left_unitor ((𝟭 D).map_cone c)).symm) (category_theory.limits.is_limit.map_cone_equiv E.as_equivalence.unit_iso.symm (category_theory.limits.is_limit_of_preserves E.inv t))).of_iso_limit (category_theory.limits.cones.ext (category_theory.adjunction.is_equivalence_reflects_limits._aux_1 J 𝒥 K c) _)}}}
@[protected, instance]
def
category_theory.adjunction.is_equivalence_creates_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(H : D ⥤ C)
[category_theory.is_equivalence H] :
Equations
- category_theory.adjunction.is_equivalence_creates_limits H = {creates_limits_of_shape := λ (J : Type u) (𝒥 : category_theory.category J), {creates_limit := λ (F : J ⥤ D), {to_reflects_limit := category_theory.limits.reflects_limit_of_reflects_limits_of_shape F H (category_theory.limits.reflects_limits_of_shape_of_reflects_limits J H), lifts := λ (c : category_theory.limits.cone (F ⋙ H)) (t : category_theory.limits.is_limit c), {lifted_cone := H.map_cone_inv c, valid_lift := H.map_cone_map_cone_inv c}}}}
theorem
category_theory.adjunction.has_limit_comp_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type u}
[category_theory.category J]
(K : J ⥤ D)
(E : D ⥤ C)
[category_theory.is_equivalence E]
[category_theory.limits.has_limit K] :
theorem
category_theory.adjunction.has_limit_of_comp_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type u}
[category_theory.category J]
(K : J ⥤ D)
(E : D ⥤ C)
[category_theory.is_equivalence E]
[category_theory.limits.has_limit (K ⋙ E)] :
theorem
category_theory.adjunction.has_limits_of_shape_of_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type u}
[category_theory.category J]
(E : D ⥤ C)
[category_theory.is_equivalence E]
[category_theory.limits.has_limits_of_shape J C] :
Transport a has_limits_of_shape instance across an equivalence.
theorem
category_theory.adjunction.has_limits_of_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(E : D ⥤ C)
[category_theory.is_equivalence E]
[category_theory.limits.has_limits_of_size C] :
Transport a has_limits instance across an equivalence.
def
category_theory.adjunction.cocones_iso_component_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
{K : J ⥤ C}
(Y : D)
(t : ((category_theory.cocones J D).obj (opposite.op (K ⋙ F))).obj Y) :
(G ⋙ (category_theory.cocones J C).obj (opposite.op K)).obj Y
auxiliary construction for cocones_iso
Equations
- adj.cocones_iso_component_hom Y t = {app := λ (j : J), ⇑(adj.hom_equiv (K.obj j) Y) (t.app j), naturality' := _}
@[simp]
theorem
category_theory.adjunction.cocones_iso_component_hom_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
{K : J ⥤ C}
(Y : D)
(t : ((category_theory.cocones J D).obj (opposite.op (K ⋙ F))).obj Y)
(j : J) :
def
category_theory.adjunction.cocones_iso_component_inv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
{K : J ⥤ C}
(Y : D)
(t : (G ⋙ (category_theory.cocones J C).obj (opposite.op K)).obj Y) :
((category_theory.cocones J D).obj (opposite.op (K ⋙ F))).obj Y
auxiliary construction for cocones_iso
Equations
- adj.cocones_iso_component_inv Y t = {app := λ (j : J), ⇑((adj.hom_equiv (K.obj j) Y).symm) (t.app j), naturality' := _}
@[simp]
theorem
category_theory.adjunction.cocones_iso_component_inv_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
{K : J ⥤ C}
(Y : D)
(t : (G ⋙ (category_theory.cocones J C).obj (opposite.op K)).obj Y)
(j : J) :
def
category_theory.adjunction.cones_iso_component_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
{K : J ⥤ D}
(X : Cᵒᵖ)
(t : (F.op ⋙ (category_theory.cones J D).obj K).obj X) :
((category_theory.cones J C).obj (K ⋙ G)).obj X
auxiliary construction for cones_iso
Equations
- adj.cones_iso_component_hom X t = {app := λ (j : J), ⇑(adj.hom_equiv (opposite.unop X) (K.obj j)) (t.app j), naturality' := _}
@[simp]
theorem
category_theory.adjunction.cones_iso_component_hom_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
{K : J ⥤ D}
(X : Cᵒᵖ)
(t : (F.op ⋙ (category_theory.cones J D).obj K).obj X)
(j : J) :
(adj.cones_iso_component_hom X t).app j = ⇑(adj.hom_equiv (opposite.unop X) (K.obj j)) (t.app j)
@[simp]
theorem
category_theory.adjunction.cones_iso_component_inv_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
{K : J ⥤ D}
(X : Cᵒᵖ)
(t : ((category_theory.cones J C).obj (K ⋙ G)).obj X)
(j : J) :
(adj.cones_iso_component_inv X t).app j = ⇑((adj.hom_equiv (opposite.unop X) (K.obj j)).symm) (t.app j)
def
category_theory.adjunction.cones_iso_component_inv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
{K : J ⥤ D}
(X : Cᵒᵖ)
(t : ((category_theory.cones J C).obj (K ⋙ G)).obj X) :
(F.op ⋙ (category_theory.cones J D).obj K).obj X
auxiliary construction for cones_iso
Equations
- adj.cones_iso_component_inv X t = {app := λ (j : J), ⇑((adj.hom_equiv (opposite.unop X) (K.obj j)).symm) (t.app j), naturality' := _}
def
category_theory.adjunction.cocones_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
{K : J ⥤ C} :
(category_theory.cocones J D).obj (opposite.op (K ⋙ F)) ≅ G ⋙ (category_theory.cocones J C).obj (opposite.op K)
When F ⊣ G,
the functor associating to each Y the cocones over K ⋙ F with cone point Y
is naturally isomorphic to
the functor associating to each Y the cocones over K with cone point G.obj Y.
Equations
- adj.cocones_iso = category_theory.nat_iso.of_components (λ (Y : D), {hom := adj.cocones_iso_component_hom Y, inv := adj.cocones_iso_component_inv Y, hom_inv_id' := _, inv_hom_id' := _}) _
def
category_theory.adjunction.cones_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type u}
[category_theory.category J]
{K : J ⥤ D} :
F.op ⋙ (category_theory.cones J D).obj K ≅ (category_theory.cones J C).obj (K ⋙ G)
When F ⊣ G,
the functor associating to each X the cones over K with cone point F.op.obj X
is naturally isomorphic to
the functor associating to each X the cones over K ⋙ G with cone point X.
Equations
- adj.cones_iso = category_theory.nat_iso.of_components (λ (X : Cᵒᵖ), {hom := adj.cones_iso_component_hom X, inv := adj.cones_iso_component_inv X, hom_inv_id' := _, inv_hom_id' := _}) _