inr_coprodIsoPushout_hom — Mathlib

English

The inr leg interacts with the pushout isomorphism as expected: inr maps to the pushout right inclusion.

Русский

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

LaTeX

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

Lean4

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

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