English
The inverse of the associativity morphism interacts with the right injections in a pushout diagram, yielding an equality that expresses the compatibility of the inverse associator with pushout injections.
Русский
Обращение ассоциатора пуш-аута взаимодействует с правыми вложениями, порождая равенство, выражающее совместимость обратного ассоциатора с инъекциями пуш-аута.
LaTeX
$$$ pushout.inr \; g_3,g_4 \circ pushout.inr \; g_1,(g_2) \circ (pushoutAssoc_{g_1,g_2,g_3,g_4})^{-1} = pushout.inr \; (g_3(g_2))\, g_4$$$
Lean4
@[reassoc (attr := simp)]
theorem inr_inr_pushoutAssoc_inv [HasPushout (g₃ ≫ (pushout.inr _ _ : X₂ ⟶ Y₁)) g₄]
[HasPushout g₁ (g₂ ≫ (pushout.inl _ _ : X₂ ⟶ Y₂))] :
pushout.inr _ _ ≫ pushout.inr _ _ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv = pushout.inr _ _ :=
by
trans f₄ ≫ l₂'
· congr 1
exact
(pushoutPushoutLeftIsPushout g₁ g₂ g₃ g₄).comp_coconePointUniqueUpToIso_inv
(pushoutPushoutRightIsPushout g₁ g₂ g₃ g₄) WalkingCospan.right
· exact pushout.inr_desc _ _ _
