pushoutIsoUnopPullback_inl_hom — Mathlib

English

A pushout inl map followed by the hom of pushout-unop-pullback equals the unop of pullback.fst.

Русский

Стрела pushout.inl, затем гомоморфизм pushoutUnopPullback, равна unop от pullback.fst.

LaTeX

$$$$ \mathrm{pushout.inl}(f,g) \circ (\mathrm{pushoutUnopPullback}(f,g)).\mathrm{hom} = (\mathrm{pullback.fst}(f^{op},g^{op}))^{\mathrm{unop}}. $$$$

Lean4

@[reassoc (attr := simp)]
theorem pushoutIsoUnopPullback_inl_hom {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g] [HasPullback f.op g.op] :
    pushout.inl _ _ ≫ (pushoutIsoUnopPullback f g).hom = (pullback.fst f.op g.op).unop :=
  (IsColimit.comp_coconePointUniqueUpToIso_hom _ _ _).trans (by simp)

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