inr_coprodIsoPushout_inv — Mathlib

English

The inverse of the coprodIsoPushout composed with pushout.inr yields the coproduct injection.

Русский

Обратный изоморфизм coprodIsoPushout компонуется с pushout.inr для получения инъекции копродукта.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem inr_coprodIsoPushout_inv [HasInitial C] [HasPushouts C] (X Y : C) [HasBinaryCoproduct X Y] :
    pushout.inr _ _ ≫ (coprodIsoPushout X Y).inv = coprod.inr :=
  colimit.isoColimitCocone_ι_inv (colimitCoconeOfInitialAndPushouts (pair X Y)) ⟨.right⟩

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