inl_coprodIsoPushout_inv — Mathlib

English

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

Русский

Обратный изоморфизм coprodIsoPushout, композиция с pushout.inl даёт инъекцию копродукта.

LaTeX

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

Lean4

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

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