# mathlibdocumentation

category_theory.sums.associator

# Associator for binary disjoint union of categories. #

The associator functor ((C ⊕ D) ⊕ E) ⥤ (C ⊕ (D ⊕ E)) and its inverse form an equivalence.

def category_theory.sum.associator (C : Type u) (D : Type u) (E : Type u)  :
(C D) E C D E

The associator functor (C ⊕ D) ⊕ E ⥤ C ⊕ (D ⊕ E) for sums of categories.

Equations
Instances for category_theory.sum.associator
@[simp]
theorem category_theory.sum.associator_obj_inl_inl (C : Type u) (D : Type u) (E : Type u) (X : C) :
@[simp]
theorem category_theory.sum.associator_obj_inl_inr (C : Type u) (D : Type u) (E : Type u) (X : D) :
@[simp]
theorem category_theory.sum.associator_obj_inr (C : Type u) (D : Type u) (E : Type u) (X : E) :
@[simp]
theorem category_theory.sum.associator_map_inl_inl (C : Type u) (D : Type u) (E : Type u) {X Y : C} (f : sum.inl (sum.inl X) sum.inl (sum.inl Y)) :
.map f = f
@[simp]
theorem category_theory.sum.associator_map_inl_inr (C : Type u) (D : Type u) (E : Type u) {X Y : D} (f : sum.inl (sum.inr X) sum.inl (sum.inr Y)) :
.map f = f
@[simp]
theorem category_theory.sum.associator_map_inr (C : Type u) (D : Type u) (E : Type u) {X Y : E} (f : ) :
.map f = f
def category_theory.sum.inverse_associator (C : Type u) (D : Type u) (E : Type u)  :
C D E (C D) E

The inverse associator functor C ⊕ (D ⊕ E) ⥤ (C ⊕ D) ⊕ E for sums of categories.

Equations
Instances for category_theory.sum.inverse_associator
@[simp]
theorem category_theory.sum.inverse_associator_obj_inl (C : Type u) (D : Type u) (E : Type u) (X : C) :
@[simp]
theorem category_theory.sum.inverse_associator_obj_inr_inl (C : Type u) (D : Type u) (E : Type u) (X : D) :
@[simp]
theorem category_theory.sum.inverse_associator_obj_inr_inr (C : Type u) (D : Type u) (E : Type u) (X : E) :
(sum.inr (sum.inr X)) =
@[simp]
theorem category_theory.sum.inverse_associator_map_inl (C : Type u) (D : Type u) (E : Type u) {X Y : C} (f : ) :
= f
@[simp]
theorem category_theory.sum.inverse_associator_map_inr_inl (C : Type u) (D : Type u) (E : Type u) {X Y : D} (f : sum.inr (sum.inl X) sum.inr (sum.inl Y)) :
= f
@[simp]
theorem category_theory.sum.inverse_associator_map_inr_inr (C : Type u) (D : Type u) (E : Type u) {X Y : E} (f : sum.inr (sum.inr X) sum.inr (sum.inr Y)) :
= f
def category_theory.sum.associativity (C : Type u) (D : Type u) (E : Type u)  :
(C D) E C D E

The equivalence of categories expressing associativity of sums of categories.

Equations
@[protected, instance]
def category_theory.sum.associator_is_equivalence (C : Type u) (D : Type u) (E : Type u)  :
Equations
@[protected, instance]
def category_theory.sum.inverse_associator_is_equivalence (C : Type u) (D : Type u) (E : Type u)  :
Equations