inl_coprodIsoPushout_hom — Mathlib

English

The inl leg interacts with the pushout isomorphism as expected: inl maps to the pushout left inclusion.

Русский

Левая составляющая inl взаимодействует с изоморфизмом пушоута через left-включение копродукта.

LaTeX

$$$coprod.inl \\;\\gg\\; (coprodIsoPushout X Y).hom = pushout.inl _ _$$$

Lean4

@[reassoc (attr := simp)]
theorem inl_coprodIsoPushout_hom [HasInitial C] [HasPushouts C] (X Y : C) [HasBinaryCoproduct X Y] :
    coprod.inl ≫ (coprodIsoPushout X Y).hom = pushout.inl _ _ :=
  colimit.isoColimitCocone_ι_hom (colimitCoconeOfInitialAndPushouts _) _

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