isoOfHom_id_inv — Mathlib

English

For any X and any hf ∈ W(𝟙 X), the inv of isoOfHom on identity morphism is the identity morphism.

Русский

Для любого X и hf ∈ W(𝟙 X) обратный к isoOfHom на тождественном морфизме равен тождеству.

LaTeX

$$$(\\text{isoOfHom } L W (\\mathrm{Id}_X) hf).inv = \\mathrm{Id}_{L.obj X}$$$

Lean4

@[simp]
theorem isoOfHom_id_inv (X : C) (hX : W (𝟙 X)) : (isoOfHom L W (𝟙 X) hX).inv = 𝟙 _ := by
  rw [← cancel_mono (isoOfHom L W (𝟙 X) hX).hom, Iso.inv_hom_id, id_comp, isoOfHom_hom, Functor.map_id]

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