mathlib documentation

category_theory.products.associator

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

def category_theory.prod.associator (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (E : Type u₃) [category_theory.category E] :
(C × D) × E C × D × E

The associator functor (C × D) × E ⥤ C × (D × E).

Equations
Instances for category_theory.prod.associator
@[simp]
theorem category_theory.prod.associator_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (E : Type u₃) [category_theory.category E] (X : (C × D) × E) :
@[simp]
theorem category_theory.prod.associator_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (E : Type u₃) [category_theory.category E] (_x _x_1 : (C × D) × E) (f : _x _x_1) :
@[simp]
theorem category_theory.prod.inverse_associator_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (E : Type u₃) [category_theory.category E] (_x _x_1 : C × D × E) (f : _x _x_1) :
def category_theory.prod.inverse_associator (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (E : Type u₃) [category_theory.category E] :
C × D × E (C × D) × E

The inverse associator functor C × (D × E) ⥤ (C × D) × E.

Equations
Instances for category_theory.prod.inverse_associator
@[simp]
theorem category_theory.prod.inverse_associator_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (E : Type u₃) [category_theory.category E] (X : C × D × E) :
def category_theory.prod.associativity (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (E : Type u₃) [category_theory.category E] :
(C × D) × E C × D × E

The equivalence of categories expressing associativity of products of categories.

Equations