inl_pushoutAssoc_inv — Mathlib

English

A symmetry statement about the combination of left and right injections in a pushout diagram under associativity morphisms.

Русский

Симметрия сочетания левых и правых вложений в диаграмме пуш-аута под действием морфизмов ассоциативности.

LaTeX

$$$ pushout.inr_{g_1,g_2} \circ pushout.inl_{g_3,g_4} \circ (pushoutAssoc_{g_1,g_2,g_3,g_4})^{\mathrm{inv}} = pushout.inl_{g_3,g_4} \circ pushout.inr_{g_1,g_2}$$$

Lean4

@[reassoc (attr := simp)]
theorem inl_pushoutAssoc_inv [HasPushout (g₃ ≫ (pushout.inr _ _ : X₂ ⟶ Y₁)) g₄]
    [HasPushout g₁ (g₂ ≫ (pushout.inl _ _ : X₂ ⟶ Y₂))] :
    pushout.inl _ _ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv = pushout.inl _ _ ≫ pushout.inl _ _ := by
  rw [Iso.comp_inv_eq, Category.assoc, inl_inl_pushoutAssoc_hom]

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