homMk'_id — Mathlib

English

For any f : S ⟶ T.obj Y, the morphism homMk' f (𝟙 Y) is equal to the canonical identity morphism coming from the equality in the structure, i.e. eqToHom of a trivial equality.

Русский

Для любого f : S ⟶ T.obj Y морфизм homMk' f (𝟙 Y) равен каноническому тождественному морфизму, получаемому из тривиального равенства.

LaTeX

$$$homMk'\, f\ (\mathsf{1}_Y) \\ = \\ \mathrm{eqToHom}\left(\text{trivial equality} ight)$$

Lean4

theorem homMk'_id (f : StructuredArrow S T) : homMk' f (𝟙 f.right) = eqToHom (by cat_disch) := by simp [eqToHom_right]

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