inl_inr_pushoutAssoc_inv — Mathlib

English

The inverse associativity morphism composes with successive right injections to reproduce a canonical right injection in the pushout diagram.

Русский

Обратный ассоциатор компонуется с правыми вложениями так, чтобы воспроизвести каноническую правую инъекцию пуш-аута.

LaTeX

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

Lean4

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

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