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₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : 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₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C) : (associator C D E).obj (Sum.inl (Sum.inl X)) = Sum.inl X

@[simp]

theorem CategoryTheory.sum.associator_obj_inl_inr (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : D) : (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₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : E) : (associator C D E).obj (Sum.inr X) = Sum.inr (Sum.inr X)

@[simp]

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

@[simp]

theorem CategoryTheory.sum.associator_map_inl_inr (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {X Y : D} (f : X ⟶ Y) : (associator C D E).map ((Sum.inl_ (C ⊕ D) E).map ((Sum.inr_ C D).map f)) = (Sum.inr_ C (D ⊕ E)).map ((Sum.inl_ D E).map f)

@[simp]

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

def CategoryTheory.sum.inlCompAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : (Sum.inl_ (C ⊕ D) E).comp (associator C D E) ≅ (Sum.inl_ C (D ⊕ E)).sum' ((Sum.inl_ D E).comp (Sum.inr_ C (D ⊕ E)))

Characterizing the composition of the associator and the left inclusion.

Equations

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

@[simp]

theorem CategoryTheory.sum.inlCompAssociator_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C ⊕ D) : (inlCompAssociator C D E).inv.app X = CategoryStruct.id (((Sum.inl_ C (D ⊕ E)).sum' ((Sum.inl_ D E).comp (Sum.inr_ C (D ⊕ E)))).obj X)

@[simp]

theorem CategoryTheory.sum.inlCompAssociator_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C ⊕ D) : (inlCompAssociator C D E).hom.app X = CategoryStruct.id (((Sum.inl_ C (D ⊕ E)).sum' ((Sum.inl_ D E).comp (Sum.inr_ C (D ⊕ E)))).obj X)

def CategoryTheory.sum.inrCompAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : (Sum.inr_ (C ⊕ D) E).comp (associator C D E) ≅ (Sum.inr_ D E).comp (Sum.inr_ C (D ⊕ E))

Characterizing the composition of the associator and the right inclusion.

Equations

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

@[simp]

theorem CategoryTheory.sum.inrCompAssociator_hom_app_down_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : E) : ((inrCompAssociator C D E).hom.app X).down.down = CategoryStruct.id X

@[simp]

theorem CategoryTheory.sum.inrCompAssociator_inv_app_down_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : E) : ((inrCompAssociator C D E).inv.app X).down.down = CategoryStruct.id X

def CategoryTheory.sum.inlCompInlCompAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : (Sum.inl_ C D).comp ((Sum.inl_ (C ⊕ D) E).comp (associator C D E)) ≅ Sum.inl_ C (D ⊕ E)

Further characterizing the composition of the associator and the left inclusion.

Equations

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

@[simp]

theorem CategoryTheory.sum.inlCompInlCompAssociator_hom_app_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C) : ((inlCompInlCompAssociator C D E).hom.app X).down = CategoryStruct.comp (CategoryStruct.id (Sum.inl X)).down (CategoryStruct.id (Sum.inl X)).down

@[simp]

theorem CategoryTheory.sum.inlCompInlCompAssociator_inv_app_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C) : ((inlCompInlCompAssociator C D E).inv.app X).down = CategoryStruct.comp (CategoryStruct.id (Sum.inl X)).down (CategoryStruct.id (Sum.inl X)).down

def CategoryTheory.sum.inrCompInlCompAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : (Sum.inr_ C D).comp ((Sum.inl_ (C ⊕ D) E).comp (associator C D E)) ≅ (Sum.inl_ D E).comp (Sum.inr_ C (D ⊕ E))

Further characterizing the composition of the associator and the left inclusion.

Equations

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

@[simp]

theorem CategoryTheory.sum.inrCompInlCompAssociator_inv_app_down_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : D) : ((inrCompInlCompAssociator C D E).inv.app X).down.down = CategoryStruct.comp (CategoryStruct.id (Sum.inr (Sum.inl X))).down.down (CategoryStruct.id (Sum.inr (Sum.inl X))).down.down

@[simp]

theorem CategoryTheory.sum.inrCompInlCompAssociator_hom_app_down_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : D) : ((inrCompInlCompAssociator C D E).hom.app X).down.down = CategoryStruct.comp (CategoryStruct.id (Sum.inr (Sum.inl X))).down.down (CategoryStruct.id (Sum.inr (Sum.inl X))).down.down

def CategoryTheory.sum.inverseAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : 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₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C) : (inverseAssociator C D E).obj (Sum.inl X) = Sum.inl (Sum.inl X)

@[simp]

theorem CategoryTheory.sum.inverseAssociator_obj_inr_inl (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : D) : (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₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : E) : (inverseAssociator C D E).obj (Sum.inr (Sum.inr X)) = Sum.inr X

@[simp]

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

@[simp]

theorem CategoryTheory.sum.inverseAssociator_map_inr_inl (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {X Y : D} (f : X ⟶ Y) : (inverseAssociator C D E).map ((Sum.inr_ C (D ⊕ E)).map ((Sum.inl_ D E).map f)) = (Sum.inl_ (C ⊕ D) E).map ((Sum.inr_ C D).map f)

@[simp]

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

def CategoryTheory.sum.inlCompInverseAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : (Sum.inl_ C (D ⊕ E)).comp (inverseAssociator C D E) ≅ (Sum.inl_ C D).comp (Sum.inl_ (C ⊕ D) E)

Characterizing the composition of the inverse of the associator and the left inclusion.

Equations

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

@[simp]

theorem CategoryTheory.sum.inlCompInverseAssociator_hom_app_down_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C) : ((inlCompInverseAssociator C D E).hom.app X).down.down = CategoryStruct.id X

@[simp]

theorem CategoryTheory.sum.inlCompInverseAssociator_inv_app_down_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C) : ((inlCompInverseAssociator C D E).inv.app X).down.down = CategoryStruct.id X

def CategoryTheory.sum.inrCompInverseAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : (Sum.inr_ C (D ⊕ E)).comp (inverseAssociator C D E) ≅ ((Sum.inr_ C D).comp (Sum.inl_ (C ⊕ D) E)).sum' (Sum.inr_ (C ⊕ D) E)

Characterizing the composition of the inverse of the associator and the right inclusion.

Equations

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

@[simp]

theorem CategoryTheory.sum.inrCompInverseAssociator_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : D ⊕ E) : (inrCompInverseAssociator C D E).hom.app X = CategoryStruct.id ((((Sum.inr_ C D).comp (Sum.inl_ (C ⊕ D) E)).sum' (Sum.inr_ (C ⊕ D) E)).obj X)

@[simp]

theorem CategoryTheory.sum.inrCompInverseAssociator_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : D ⊕ E) : (inrCompInverseAssociator C D E).inv.app X = CategoryStruct.id ((((Sum.inr_ C D).comp (Sum.inl_ (C ⊕ D) E)).sum' (Sum.inr_ (C ⊕ D) E)).obj X)

def CategoryTheory.sum.inlCompInrCompInverseAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : (Sum.inl_ D E).comp ((Sum.inr_ C (D ⊕ E)).comp (inverseAssociator C D E)) ≅ (Sum.inr_ C D).comp (Sum.inl_ (C ⊕ D) E)

Further characterizing the composition of the inverse of the associator and the right inclusion.

Equations

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

@[simp]

theorem CategoryTheory.sum.inlCompInrCompInverseAssociator_inv_app_down_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : D) : ((inlCompInrCompInverseAssociator C D E).inv.app X).down.down = CategoryStruct.comp (CategoryStruct.id (Sum.inl (Sum.inr X))).down.down (CategoryStruct.id (Sum.inl (Sum.inr X))).down.down

@[simp]

theorem CategoryTheory.sum.inlCompInrCompInverseAssociator_hom_app_down_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : D) : ((inlCompInrCompInverseAssociator C D E).hom.app X).down.down = CategoryStruct.comp (CategoryStruct.id (Sum.inl (Sum.inr X))).down.down (CategoryStruct.id (Sum.inl (Sum.inr X))).down.down

def CategoryTheory.sum.inrCompInrCompInverseAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : (Sum.inr_ D E).comp ((Sum.inr_ C (D ⊕ E)).comp (inverseAssociator C D E)) ≅ Sum.inr_ (C ⊕ D) E

Further characterizing the composition of the inverse of the associator and the right inclusion.

Equations

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

@[simp]

theorem CategoryTheory.sum.inrCompInrCompInverseAssociator_inv_app_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : E) : ((inrCompInrCompInverseAssociator C D E).inv.app X).down = CategoryStruct.comp (CategoryStruct.id (Sum.inr X)).down (CategoryStruct.id (Sum.inr X)).down

@[simp]

theorem CategoryTheory.sum.inrCompInrCompInverseAssociator_hom_app_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : E) : ((inrCompInrCompInverseAssociator C D E).hom.app X).down = CategoryStruct.comp (CategoryStruct.id (Sum.inr X)).down (CategoryStruct.id (Sum.inr X)).down

def CategoryTheory.sum.associativity (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [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₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : (associativity C D E).inverse = inverseAssociator C D E

@[simp]

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

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

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