mathlib documentation

category_theory.​adjunction.​limits

category_theory.​adjunction.​limits

@[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

@[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)) :

@[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

@[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) :

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)

@[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_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
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)

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
@[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 {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} :

Equations