ofHom_injective — Mathlib

English

The mapping f ↦ ofHom f from MonoidHoms to GrpCat morphisms is injective; i.e., if ofHom f = ofHom g then f = g.

Русский

Отображение f ↦ ofHom f из гомоморфизмов моноидов в морфизмы GrpCat инъективно; то есть если ofHom f = ofHom g, то f = g.

LaTeX

$$$ \\forall X Y,\\; f,g:X \\to^* Y,\\; \\mathrm{ofHom}(f)=\\mathrm{ofHom}(g) \\Rightarrow f=g $$$

Lean4

@[to_additive]
theorem ofHom_injective {X Y : Type u} [Group X] [Group Y] : Function.Injective (fun (f : X →* Y) ↦ ofHom f) :=
  by
  intro _ _ h
  ext
  apply ConcreteCategory.congr_hom h

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