inverseAssociator — Mathlib

English

The inverse associator is the inverse functor to the associator, providing the isomorphism ((C × D) × E) ≅ (C × D) × E.

Русский

Обратный ассоциатор является обратным к ассоциатору и задаёт изоморфизм ((C × D) × E) ≅ (C × D) × E.

LaTeX

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

Lean4

/-- The inverse associator functor `C × (D × E) ⥤ (C × D) × E `.
-/
@[simps]
def inverseAssociator : C × D × E ⥤ (C × D) × E
    where
  obj X := ((X.1, X.2.1), X.2.2)
  map := @fun _ _ f => ((f.1, f.2.1), f.2.2)

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