hom_ofHom — Mathlib

English

Let R and S be groups and f : R →* S a group hom. The corresponding morphism in GrpCat acts on elements exactly as f does; i.e., the underlying map of the GrpCat morphism equals f.

Русский

Пусть R и S — группы и f : R →* S — гомоморфизм групп. Соответствующий морфизм в GrpCat действует на элементы так же, как и f; то есть его порождающее отображение равно f.

LaTeX

$$$ (\\mathrm{ofHom}(f)).\\mathrm{hom} = f $$$

Lean4

@[to_additive (attr := simp)]
theorem hom_ofHom {R S : Type u} [Group R] [Group S] (f : R →* S) : (ofHom f).hom = f :=
  rfl

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