inverseAssociator — Mathlib

English

The inverse associator is the functor C ⊕ (D ⊕ E) → (C ⊕ D) ⊕ E giving the inverse of the associator.

Русский

Обратный ассоциатор — это функтор C ⊕ (D ⊕ E) → (C ⊕ D) ⊕ E, образующий обратный для ассоциатора.

LaTeX

$$inverseAssociator : C ⊕ (D ⊕ E) ⥤ (C ⊕ D) ⊕ E$$

Lean4

/-- The inverse associator functor `C ⊕ (D ⊕ E) ⥤ (C ⊕ D) ⊕ E` for sums of categories.
-/
def inverseAssociator : C ⊕ (D ⊕ E) ⥤ (C ⊕ D) ⊕ E :=
  inl_ C D ⋙ inl_ (C ⊕ D) E |>.sum' <| (inr_ C D ⋙ inl_ (C ⊕ D) E).sum' <| inr_ (C ⊕ D) E

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