mathlib documentation

category_theory.adjunction.limits

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

Auxiliary definition for functoriality_is_left_adjoint.

Equations

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {J : Type v} [category_theory.small_category J] (K : J C) (c : category_theory.limits.cocone K) :
((adj.functoriality_unit K).app c).hom = adj.unit.app c.X

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {J : Type v} [category_theory.small_category J] (K : J C) (c : category_theory.limits.cocone (K F)) :

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

Equations

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {J : Type v} [category_theory.small_category J] (K : J D) (c : category_theory.limits.cone (K G)) :
((adj.functoriality_unit' K).app c).hom = adj.unit.app c.X

The unit for the adjunction forcones.functoriality K G : cone K ⥤ cone (K ⋙ G).

Auxiliary definition for functoriality_is_right_adjoint.

Equations

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {J : Type v} [category_theory.small_category J] (K : J D) (c : category_theory.limits.cone K) :

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

Equations
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 v} [category_theory.small_category J] {K : J C} (Y : D) :

auxiliary construction for cocones_iso

Equations
@[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 v} [category_theory.small_category J] {K : J C} (Y : D) (t : ((category_theory.cocones J D).obj (opposite.op (K F))).obj Y) (j : J) :
(adj.cocones_iso_component_hom Y t).app j = (adj.hom_equiv (K.obj j) Y) (t.app 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 v} [category_theory.small_category J] {K : J C} (Y : D) :

auxiliary construction for cocones_iso

Equations
@[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 v} [category_theory.small_category J] {K : J C} (Y : D) (t : (G (category_theory.cocones J C).obj (opposite.op K)).obj Y) (j : J) :
(adj.cocones_iso_component_inv Y t).app j = ((adj.hom_equiv (K.obj j) Y).symm) (t.app j)

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 v} [category_theory.small_category J] {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_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 v} [category_theory.small_category J] {K : J D} (X : Cᵒᵖ) :
(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
@[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 v} [category_theory.small_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 v} [category_theory.small_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 v} [category_theory.small_category J] {K : J D} (X : Cᵒᵖ) :
((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
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 v} [category_theory.small_category J] {K : J D} :

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