ofHom_injective — Mathlib

English

The map f ↦ ofHom f from MonoidHom X Y to CommGrpCat.Hom (of X) (of Y) is injective for commutative groups X,Y.

Русский

Отображение f ↦ ofHom f инъективно между MonoidHom X Y и CommGrpCat.Hom (of X) (of Y) для коммутативных групп X,Y.

LaTeX

$$$$ \forall X,Y\,[\mathrm{CommGroup}(X)], [\mathrm{CommGroup}(Y)],\\; \mathrm{Injective}(f \mapsto \mathrm{ofHom}(f)). $$$$

Lean4

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

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