inr_zeroCoprodIso_hom — Mathlib

English

The map coprod.inr followed by the hom part of the zero coproduct iso is the identity on X.

Русский

Сначала инъекция coprod.inr, затем компонент hom нулевого копроизведения образуют тождественный морфизм на X.

LaTeX

$$$$ \mathrm{coprod.inr} \;\circ\; (\text{zeroCoprodIso } X).\mathrm{hom} = \mathrm{id}_X. $$$$

Lean4

@[simp]
theorem inr_zeroCoprodIso_hom (X : C) : coprod.inr ≫ (zeroCoprodIso X).hom = 𝟙 X :=
  by
  dsimp [zeroCoprodIso, binaryCofanZeroLeft]
  simp

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