English
Let C, D, E be categories. There exists a natural isomorphism between the functor obtained by composing the left inclusion into C with the sum D ⊕ E and the inverse associator, and the functor obtained by first including into C ⊕ D and then including into the sum with E. In symbols, inl_C(D ⊕ E) ∘ inverseAssociator_{C D E} ≅ inl_{C D} ∘ inl_{(C D) E}.
Русский
Пусть C, D, E — категории. Существует естественное изоморование между композициями левого включения и обратного ассоциатора и последовательной инклюзией: inl_C(D ⊕ E) ∘ inverseAssociator_{C D E} ≅ inl_{C D} ∘ inl_{(C D) E}.
LaTeX
$$$$\mathrm{inl}_{C}(D\oplus E) \circ \mathrm{inverseAssociator}_{C D E} \cong \mathrm{inl}_{C D} \circ \mathrm{inl}_{(C D) E}.$$$$
Lean4
/-- Characterizing the composition of the inverse of the associator and the left inclusion. -/
@[simps!]
def inlCompInverseAssociator : inl_ C (D ⊕ E) ⋙ inverseAssociator C D E ≅ inl_ C D ⋙ inl_ (C ⊕ D) E :=
Functor.inlCompSum' _ _
