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

def CategoryTheory.prod.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).

Equations

• CategoryTheory.prod.associator C D E = { obj := fun (X : (C × D) × E) => (X.1.1, X.1.2, X.2), map := fun (x x_1 : (C × D) × E) (f : x ⟶ x_1) => (f.1.1, f.1.2, f.2), map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.prod.associator_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : (C × D) × E) : (associator C D E).obj X = (X.1.1, X.1.2, X.2)

@[simp]

theorem CategoryTheory.prod.associator_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (x✝ x✝¹ : (C × D) × E) (f : x✝ ⟶ x✝¹) : (associator C D E).map f = (f.1.1, f.1.2, f.2)

def CategoryTheory.prod.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 .

Equations

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

@[simp]

theorem CategoryTheory.prod.inverseAssociator_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C × D × E) : (inverseAssociator C D E).obj X = ((X.1, X.2.1), X.2.2)

@[simp]

theorem CategoryTheory.prod.inverseAssociator_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (x✝ x✝¹ : C × D × E) (f : x✝ ⟶ x✝¹) : (inverseAssociator C D E).map f = ((f.1, f.2.1), f.2.2)

def CategoryTheory.prod.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 products of categories.

Equations

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

@[simp]

theorem CategoryTheory.prod.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

@[simp]

theorem CategoryTheory.prod.associativity_counitIso (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).counitIso = Iso.refl ((inverseAssociator C D E).comp (associator C D E))

@[simp]

theorem CategoryTheory.prod.associativity_unitIso (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).unitIso = Iso.refl (Functor.id ((C × D) × E))

@[simp]

theorem CategoryTheory.prod.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

instance CategoryTheory.prod.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.prod.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

def CategoryTheory.prod.prodFunctorToFunctorProdAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (A : Type u₄) [Category.{v₄, u₄} A] : (associativity (Functor A C) (Functor A D) (Functor A E)).functor.comp (((Functor.id (Functor A C)).prod (prodFunctorToFunctorProd A D E)).comp (prodFunctorToFunctorProd A C (D × E))) ≅ ((prodFunctorToFunctorProd A C D).prod (Functor.id (Functor A E))).comp ((prodFunctorToFunctorProd A (C × D) E).comp (associativity C D E).congrRight.functor)

The associator isomorphism is compatible with prodFunctorToFunctorProd.

Equations

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

@[simp]

theorem CategoryTheory.prod.prodFunctorToFunctorProdAssociator_hom_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (A : Type u₄) [Category.{v₄, u₄} A] (X : (Functor A C × Functor A D) × Functor A E) (X✝ : A) : ((prodFunctorToFunctorProdAssociator C D E A).hom.app X).app X✝ = (CategoryStruct.id (X.1.1.obj X✝), CategoryStruct.id (X.1.2.obj X✝), CategoryStruct.id (X.2.obj X✝))

@[simp]

theorem CategoryTheory.prod.prodFunctorToFunctorProdAssociator_inv_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (A : Type u₄) [Category.{v₄, u₄} A] (X : (Functor A C × Functor A D) × Functor A E) (X✝ : A) : ((prodFunctorToFunctorProdAssociator C D E A).inv.app X).app X✝ = (CategoryStruct.id (X.1.1.obj X✝), CategoryStruct.id (X.1.2.obj X✝), CategoryStruct.id (X.2.obj X✝))

def CategoryTheory.prod.functorProdToProdFunctorAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (A : Type u₄) [Category.{v₄, u₄} A] : (associativity C D E).congrRight.functor.comp ((functorProdToProdFunctor A C (D × E)).comp ((Functor.id (Functor A C)).prod (functorProdToProdFunctor A D E))) ≅ (functorProdToProdFunctor A (C × D) E).comp (((functorProdToProdFunctor A C D).prod (Functor.id (Functor A E))).comp (associativity (Functor A C) (Functor A D) (Functor A E)).functor)

The associator isomorphism is compatible with functorProdToProdFunctor.

Equations

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

@[simp]

theorem CategoryTheory.prod.functorProdToProdFunctorAssociator_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (A : Type u₄) [Category.{v₄, u₄} A] (X : Functor A ((C × D) × E)) : (functorProdToProdFunctorAssociator C D E A).hom.app X = (CategoryStruct.id ((X.comp (associator C D E)).comp (Prod.fst C (D × E))), CategoryStruct.id (((X.comp (associator C D E)).comp (Prod.snd C (D × E))).comp (Prod.fst D E)), CategoryStruct.id (((X.comp (associator C D E)).comp (Prod.snd C (D × E))).comp (Prod.snd D E)))

@[simp]

theorem CategoryTheory.prod.functorProdToProdFunctorAssociator_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (A : Type u₄) [Category.{v₄, u₄} A] (X : Functor A ((C × D) × E)) : (functorProdToProdFunctorAssociator C D E A).inv.app X = (CategoryStruct.id ((X.comp (associator C D E)).comp (Prod.fst C (D × E))), CategoryStruct.id (((X.comp (associator C D E)).comp (Prod.snd C (D × E))).comp (Prod.fst D E)), CategoryStruct.id (((X.comp (associator C D E)).comp (Prod.snd C (D × E))).comp (Prod.snd D E)))