English
A certain symmetry relation between left injections in a pushout diagram holds; composing the left injections with the associativity morphism yields equality with a corresponding left injection composed with a right injection, reflecting compatibility of the pushout structure with inl/inr maps.
Русский
В диаграмме пуш-аут существует симметричное соотношение между леваскими вложениями; композиция левых инъекций с морфизмом ассоциативности равна композиции соответствующей левой инъекции с правой инъекцией, отражая совместимость структуры пуш-аута с мапами inl/inr.
LaTeX
$$$ pushout.inl \\; g_1,g_2 \\; \\text{ и } pushout.inl \\; g_3,g_4$ удовлетворяют равенству, задающему совместимость инъекций с ассоциатором пуш-аута: \( pushout.inl \\_\\_ \\; \\to \\_ \\) \\,.$$
Lean4
@[reassoc (attr := simp)]
theorem inl_inl_pushoutAssoc_hom [HasPushout (g₃ ≫ (pushout.inr _ _ : X₂ ⟶ Y₁)) g₄]
[HasPushout g₁ (g₂ ≫ (pushout.inl _ _ : X₂ ⟶ Y₂))] :
pushout.inl _ _ ≫ pushout.inl _ _ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom = pushout.inl _ _ :=
by
trans f₁ ≫ l₁
· congr 1
exact (pushoutPushoutLeftIsPushout g₁ g₂ g₃ g₄).comp_coconePointUniqueUpToIso_hom _ WalkingCospan.left
· exact pushout.inl_desc _ _ _
