inr_comp_pushoutObjIso_hom — Mathlib

English

Similarly for the right injection, the app at d composed with the isomorphism hom yields the componentwise right injection at d.

Русский

Аналогично для правой инъекции: отображение вправо через изоморфизм дает компонентную инъекцию справа.

LaTeX

$$$ (pushout.inr\\, f\\, g).app\\, d \\;\\circ\\; (pushoutObjIso\\, f\\, g\\, d).hom = pushout.inr\$ f.{\\rm app}\\, d\$\$ g.{\\rm app}\\, d\$ $$$

Lean4

@[reassoc (attr := simp)]
theorem inr_comp_pushoutObjIso_hom (f : F ⟶ G) (g : F ⟶ H) (d : D) :
    (pushout.inr f g).app d ≫ (pushoutObjIso f g d).hom = pushout.inr (f.app d) (g.app d) := by simp [pushoutObjIso]

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