inr_pushoutAssoc_hom — Mathlib

English

Naturality of pushout morphisms: a commuting diagram expresses that postcomposing by a pushout morphism after whiskering equals whiskering followed by a pushout morphism.

Русский

Естественность морфизмов пушаута: диаграмма суммирования сходится, т.е. посткомпозицируя пуш-аут морфизм после вайскорения, получаем эквивалентную диаграмму.

LaTeX

$$$ F.map (f.snd) \\circ y.iso.inv = x.iso.inv \\circ G.map (f.fst) $$$

Lean4

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

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