English
Let C, D, E be categories. There is a natural isomorphism between the functor inr_C(D ⊕ E) followed by the inverse associator and the sum of the two functors (inr_C D ∘ inl_(C ⊕ D) E) and inr_(C ⊕ D) E. Precisely, inr_C(D⊕E) ∘ inverseAssociator_{C D E} ≅ (inr_C D ∘ inl_(C ⊕ D) E) ∐' inr_(C D) E.
Русский
Пусть C, D, E — категории. Существует естественное изоморование между inr_C(D ⊕ E) ∘ inverseAssociator и суммой (inr_C D ∘ inl_(C ⊕ D) E) и inr_(C ⊕ D) E.
LaTeX
$$$$\mathrm{inr}_{C}(D\oplus E) \circ \mathrm{inverseAssociator}_{C D E} \cong (\mathrm{inr}_{C D} \circ \mathrm{inl}_{(C D) E}) \;\oplus'\; \mathrm{inr}_{(C D) E}.$$$$
Lean4
/-- Characterizing the composition of the inverse of the associator and the right inclusion. -/
@[simps!]
def inrCompInverseAssociator :
inr_ C (D ⊕ E) ⋙ inverseAssociator C D E ≅ (inr_ C D ⋙ inl_ (C ⊕ D) E).sum' <| inr_ (C ⊕ D) E :=
Functor.inrCompSum' _ _
