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.

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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

source

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

Documentation

Mathlib.CategoryTheory.Sums.Associator

Associator for binary disjoint union of categories. #