inl_comp_pushoutObjIso_hom — Mathlib

English

In a pushout setting, the composition of the pushout injection with the isomorphism pushoutObjIso equals the componentwise pushout injection at d.

Русский

В контексте pushout композиция inl с objIso совпадает с инъекцией в точке d на уровне компонентов.

LaTeX

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

Lean4

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

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