English
A similar symmetry statement holds for the right and left injections in a pushout diagram, expressing compatibility of the pushout with respect to inr and inl maps and the associativity isomorphism.
Русский
Аналогичное симметричное соотношение для правых и левых вложений в пуш-ауте, выражающее совместимость пуш-аута с мапами inr и inl и ассоциативности.
LaTeX
$$$ pushout.inr \\; g_1,g_2 \\; \\text{ и } pushout.inl \\; g_3,g_4$ удовлетворяют равенству, задающему совместимость инъекций с ассоциатором пуш-аута: \( pushout.inr \\_\\_ \\; \\to \\_ \\) \\,.$$
Lean4
@[reassoc (attr := simp)]
theorem inr_inl_pushoutAssoc_hom [HasPushout (g₃ ≫ (pushout.inr _ _ : X₂ ⟶ Y₁)) g₄]
[HasPushout g₁ (g₂ ≫ (pushout.inl _ _ : X₂ ⟶ Y₂))] :
pushout.inr _ _ ≫ pushout.inl _ _ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom = pushout.inl _ _ ≫ pushout.inr _ _ :=
by
trans f₂ ≫ l₁
· congr 1
exact (pushoutPushoutLeftIsPushout g₁ g₂ g₃ g₄).comp_coconePointUniqueUpToIso_hom _ WalkingCospan.left
· exact pushout.inr_desc _ _ _
