ofHom_id — Mathlib

English

For any group X, the morphism in GrpCat obtained from the identity monoid hom on X, equals the identity morphism on the object of X in GrpCat.

Русский

Для группы X морфизм GrpCat, получаемый из тождественного моноидного гомоморфа на X, равен тождественному морфизму над объектом X в GrpCat.

LaTeX

$$$ \\mathrm{ofHom}(\\mathrm{MonoidHom.id}\\,X) = \\mathbf{1}_{\\mathrm{of}\\,X} $$$

Lean4

@[to_additive (attr := simp)]
theorem ofHom_id {X : Type u} [Group X] : ofHom (MonoidHom.id X) = 𝟙 (of X) :=
  rfl

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