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]
:
The associator functor (C × D) × E ⥤ C × (D × E)
.
Equations
Instances For
@[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)
:
@[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✝¹)
:
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]
:
The inverse associator functor C × (D × E) ⥤ (C × D) × E
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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)
:
@[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✝¹)
:
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]
:
The equivalence of categories expressing associativity of products of categories.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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]
:
@[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]
:
@[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]
:
@[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]
:
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