forget₂_map_ofHom — Mathlib

English

The forgetful functor sends the morphism of X–groups given by ofHom f to the corresponding MonCat morphism MonCat.ofHom f.hom.

Русский

Забывающий функтор переводит морфизм GrpCat вида ofHom f в соответствующий морфизм MonCat MonCat.ofHom f.hom.

LaTeX

$$$ (\\mathrm{forget}_{\\mathrm GrpCat \\to MonCat}).\\mathrm{map}(\\mathrm{ofHom} f) = \\mathrm{MonCat.ofHom}(f) $$$

Lean4

@[to_additive (attr := simp)]
theorem forget₂_map_ofHom {X Y : Type u} [Group X] [Group Y] (f : X →* Y) :
    (forget₂ GrpCat MonCat).map (ofHom f) = MonCat.ofHom f :=
  rfl

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