inrCompInrCompInverseAssociator — Mathlib

English

There is a natural isomorphism between inr_D_E ∘ inr_C(D ⊕ E) ∘ inverseAssociator_C D E and inr_(C ⊕ D) E, established by whiskering with inr and then applying sum with inr.

Русский

Существует естественное изоморождение между inr_D_E ∘ inr_C(D ⊕ E) ∘ inverseAssociator_{C D E} и inr_(C ⊕ D) E, получаемое при помощи whiskering и суммирования по inr.

LaTeX

$$$$\mathrm{inr}_{D E} \circ \mathrm{inr}_{C}(D\oplus E) \circ \mathrm{inverseAssociator}_{C D E} \cong \mathrm{inr}_{(C \oplus D)} E.$$$$

Lean4

/-- Further characterizing the composition of the inverse of the associator and the right
inclusion. -/
@[simps!]
def inrCompInrCompInverseAssociator : inr_ D E ⋙ inr_ C (D ⊕ E) ⋙ inverseAssociator C D E ≅ inr_ (C ⊕ D) E :=
  isoWhiskerLeft (inr_ _ _) (inrCompInverseAssociator C D E) ≪≫ Functor.inrCompSum' _ _

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