mathlibdocumentation

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₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} (K : J C) :

The right adjoint of cocones.functoriality K F : cocone K ⥤ cocone (K ⋙ F).

Auxiliary definition for functoriality_is_left_adjoint.

Equations
def category_theory.adjunction.functoriality_unit {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} (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
@[simp]
theorem category_theory.adjunction.functoriality_unit_app_hom {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} (K : J C)  :
def category_theory.adjunction.functoriality_counit {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} (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
@[simp]
theorem category_theory.adjunction.functoriality_counit_app_hom {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} (K : J C) (c : category_theory.limits.cocone (K F)) :
def category_theory.adjunction.functoriality_is_left_adjoint {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} (K : J C) :

The functor cocones.functoriality K F : cocone K ⥤ cocone (K ⋙ F) is a left adjoint.

Equations
def category_theory.adjunction.left_adjoint_preserves_colimits {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) :

Equations
@[protected, instance]
def category_theory.adjunction.is_equivalence_preserves_colimits {C : Type u₁} {D : Type u₂} (E : C D)  :
Equations
@[protected, instance]
def category_theory.adjunction.is_equivalence_reflects_colimits {C : Type u₁} {D : Type u₂} (E : D C)  :
Equations
@[protected, instance]
def category_theory.adjunction.is_equivalence_creates_colimits {C : Type u₁} {D : Type u₂} (H : D C)  :
Equations
theorem category_theory.adjunction.has_colimit_comp_equivalence {C : Type u₁} {D : Type u₂} {J : Type u} (K : J C) (E : C D)  :
theorem category_theory.adjunction.has_colimit_of_comp_equivalence {C : Type u₁} {D : Type u₂} {J : Type u} (K : J C) (E : C D)  :
theorem category_theory.adjunction.has_colimits_of_shape_of_equivalence {C : Type u₁} {D : Type u₂} {J : Type u} (E : C D)  :

Transport a has_colimits_of_shape instance across an equivalence.

theorem category_theory.adjunction.has_colimits_of_equivalence {C : Type u₁} {D : Type u₂} (E : C D)  :

Transport a has_colimits instance across an equivalence.

def category_theory.adjunction.functoriality_left_adjoint {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} (K : J D) :

The left adjoint of cones.functoriality K G : cone K ⥤ cone (K ⋙ G).

Auxiliary definition for functoriality_is_right_adjoint.

Equations
@[simp]
theorem category_theory.adjunction.functoriality_unit'_app_hom {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} (K : J D) (c : category_theory.limits.cone (K G)) :
def category_theory.adjunction.functoriality_unit' {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} (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
def category_theory.adjunction.functoriality_counit' {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} (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
@[simp]
theorem category_theory.adjunction.functoriality_counit'_app_hom {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} (K : J D)  :
def category_theory.adjunction.functoriality_is_right_adjoint {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} (K : J D) :

The functor cones.functoriality K G : cone K ⥤ cone (K ⋙ G) is a right adjoint.

Equations
def category_theory.adjunction.right_adjoint_preserves_limits {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) :

Equations
@[protected, instance]
def category_theory.adjunction.is_equivalence_preserves_limits {C : Type u₁} {D : Type u₂} (E : D C)  :
Equations
@[protected, instance]
def category_theory.adjunction.is_equivalence_reflects_limits {C : Type u₁} {D : Type u₂} (E : D C)  :
Equations
@[protected, instance]
def category_theory.adjunction.is_equivalence_creates_limits {C : Type u₁} {D : Type u₂} (H : D C)  :
Equations
theorem category_theory.adjunction.has_limit_comp_equivalence {C : Type u₁} {D : Type u₂} {J : Type u} (K : J D) (E : D C)  :
theorem category_theory.adjunction.has_limit_of_comp_equivalence {C : Type u₁} {D : Type u₂} {J : Type u} (K : J D) (E : D C)  :
theorem category_theory.adjunction.has_limits_of_shape_of_equivalence {C : Type u₁} {D : Type u₂} {J : Type u} (E : D C)  :

Transport a has_limits_of_shape instance across an equivalence.

theorem category_theory.adjunction.has_limits_of_equivalence {C : Type u₁} {D : Type u₂} (E : D C)  :

Transport a has_limits instance across an equivalence.

def category_theory.adjunction.cocones_iso_component_hom {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} {K : J C} (Y : D) (t : D).obj (opposite.op (K F))).obj Y) :
(G .obj (opposite.op K)).obj Y

auxiliary construction for cocones_iso

Equations
@[simp]
theorem category_theory.adjunction.cocones_iso_component_hom_app {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} {K : J C} (Y : D) (t : D).obj (opposite.op (K F))).obj Y) (j : J) :
t).app j = (adj.hom_equiv (K.obj j) Y) (t.app j)
def category_theory.adjunction.cocones_iso_component_inv {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} {K : J C} (Y : D) (t : (G .obj (opposite.op K)).obj Y) :
D).obj (opposite.op (K F))).obj Y

auxiliary construction for cocones_iso

Equations
@[simp]
theorem category_theory.adjunction.cocones_iso_component_inv_app {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} {K : J C} (Y : D) (t : (G .obj (opposite.op K)).obj Y) (j : J) :
t).app j = ((adj.hom_equiv (K.obj j) Y).symm) (t.app j)
def category_theory.adjunction.cones_iso_component_hom {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} {K : J D} (X : Cᵒᵖ) (t : (F.op .obj K).obj X) :
C).obj (K G)).obj X

auxiliary construction for cones_iso

Equations
@[simp]
theorem category_theory.adjunction.cones_iso_component_hom_app {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} {K : J D} (X : Cᵒᵖ) (t : (F.op .obj K).obj X) (j : J) :
@[simp]
theorem category_theory.adjunction.cones_iso_component_inv_app {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} {K : J D} (X : Cᵒᵖ) (t : C).obj (K G)).obj X) (j : J) :
def category_theory.adjunction.cones_iso_component_inv {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} {K : J D} (X : Cᵒᵖ) (t : C).obj (K G)).obj X) :
(F.op .obj K).obj X

auxiliary construction for cones_iso

Equations
def category_theory.adjunction.cocones_iso {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} {K : J C} :

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
def category_theory.adjunction.cones_iso {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {J : Type u} {K : J D} :
F.op .obj K .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