Associator for binary disjoint union of categories.

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

def CategoryTheory.sum.associator (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] : CategoryTheory.Functor ((C ⊕ D) ⊕ E) (C ⊕ D ⊕ E)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.sum.associator_obj_inl_inl (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] (X : C) : (CategoryTheory.sum.associator C D E).obj (Sum.inl (Sum.inl X)) = Sum.inl X

@[simp]

theorem CategoryTheory.sum.associator_obj_inl_inr (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] (X : D) : (CategoryTheory.sum.associator C D E).obj (Sum.inl (Sum.inr X)) = Sum.inr (Sum.inl X)

@[simp]

theorem CategoryTheory.sum.associator_obj_inr (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] (X : E) : (CategoryTheory.sum.associator C D E).obj (Sum.inr X) = Sum.inr (Sum.inr X)

@[simp]

theorem CategoryTheory.sum.associator_map_inl_inl (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] {X Y : C} (f : Sum.inl (Sum.inl X) ⟶ Sum.inl (Sum.inl Y)) : (CategoryTheory.sum.associator C D E).map f = f

@[simp]

theorem CategoryTheory.sum.associator_map_inl_inr (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] {X Y : D} (f : Sum.inl (Sum.inr X) ⟶ Sum.inl (Sum.inr Y)) : (CategoryTheory.sum.associator C D E).map f = f

@[simp]

theorem CategoryTheory.sum.associator_map_inr (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] {X Y : E} (f : Sum.inr X ⟶ Sum.inr Y) : (CategoryTheory.sum.associator C D E).map f = f

def CategoryTheory.sum.inverseAssociator (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] : CategoryTheory.Functor (C ⊕ D ⊕ E) ((C ⊕ D) ⊕ E)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.sum.inverseAssociator_obj_inl (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] (X : C) : (CategoryTheory.sum.inverseAssociator C D E).obj (Sum.inl X) = Sum.inl (Sum.inl X)

@[simp]

theorem CategoryTheory.sum.inverseAssociator_obj_inr_inl (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] (X : D) : (CategoryTheory.sum.inverseAssociator C D E).obj (Sum.inr (Sum.inl X)) = Sum.inl (Sum.inr X)

@[simp]

theorem CategoryTheory.sum.inverseAssociator_obj_inr_inr (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] (X : E) : (CategoryTheory.sum.inverseAssociator C D E).obj (Sum.inr (Sum.inr X)) = Sum.inr X

@[simp]

theorem CategoryTheory.sum.inverseAssociator_map_inl (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] {X Y : C} (f : Sum.inl X ⟶ Sum.inl Y) : (CategoryTheory.sum.inverseAssociator C D E).map f = f

@[simp]

theorem CategoryTheory.sum.inverseAssociator_map_inr_inl (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] {X Y : D} (f : Sum.inr (Sum.inl X) ⟶ Sum.inr (Sum.inl Y)) : (CategoryTheory.sum.inverseAssociator C D E).map f = f

@[simp]

theorem CategoryTheory.sum.inverseAssociator_map_inr_inr (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] {X Y : E} (f : Sum.inr (Sum.inr X) ⟶ Sum.inr (Sum.inr Y)) : (CategoryTheory.sum.inverseAssociator C D E).map f = f

def CategoryTheory.sum.associativity (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] : (C ⊕ D) ⊕ E ≌ C ⊕ D ⊕ E

The equivalence of categories expressing associativity of sums of categories.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.sum.associativity_inverse (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] : (CategoryTheory.sum.associativity C D E).inverse = CategoryTheory.sum.inverseAssociator C D E

@[simp]

theorem CategoryTheory.sum.associativity_functor (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] : (CategoryTheory.sum.associativity C D E).functor = CategoryTheory.sum.associator C D E

instance CategoryTheory.sum.associatorIsEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] : (CategoryTheory.sum.associator C D E).IsEquivalence

Equations

• ⋯ = ⋯

instance CategoryTheory.sum.inverseAssociatorIsEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u) [CategoryTheory.Category.{v, u} D] (E : Type u) [CategoryTheory.Category.{v, u} E] : (CategoryTheory.sum.inverseAssociator C D E).IsEquivalence

Equations

• ⋯ = ⋯