The associator functor ((C × D) × E) ⥤ (C × (D × E))
and its inverse form an equivalence.
@[simp]
theorem
CategoryTheory.prod.associator_map
(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 x_1 : (C × D) × E) (f : x ⟶ x_1), (CategoryTheory.prod.associator C D E).map f = (f.fst.fst, f.fst.snd, f.snd)
@[simp]
theorem
CategoryTheory.prod.associator_obj
(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 × D) × E)
:
(CategoryTheory.prod.associator C D E).obj X = (X.fst.fst, X.fst.snd, X.snd)
def
CategoryTheory.prod.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)
.
Instances For
@[simp]
theorem
CategoryTheory.prod.inverseAssociator_map
(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 x_1 : C × D × E) (f : x ⟶ x_1),
(CategoryTheory.prod.inverseAssociator C D E).map f = ((f.fst, f.snd.fst), f.snd.snd)
@[simp]
theorem
CategoryTheory.prod.inverseAssociator_obj
(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 × D × E)
:
(CategoryTheory.prod.inverseAssociator C D E).obj X = ((X.fst, X.snd.fst), X.snd.snd)
def
CategoryTheory.prod.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
.
Instances For
def
CategoryTheory.prod.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]
:
The equivalence of categories expressing associativity of products of categories.
Instances For
instance
CategoryTheory.prod.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]
:
instance
CategoryTheory.prod.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]
: