associator — Mathlib

English

The associator functor ((C × D) × E) ⥤ C × (D × E) expresses the associativity of categorical products.

Русский

Ассоциатор категорий (C × D) × E ⥤ C × (D × E) выражает ассоциативность произведений категорий.

LaTeX

$$$\text{associator}: (C\times D)\times E \to C\times D\times E$$$

Lean4

/-- The associator functor `(C × D) × E ⥤ C × (D × E)`.
-/
@[simps]
def associator : (C × D) × E ⥤ C × D × E where
  obj X := (X.1.1, (X.1.2, X.2))
  map := @fun _ _ f => (f.1.1, (f.1.2, f.2))

Похожие утверждения