instHasForget₂GrpCat — Mathlib

English

There exists a forgetful functor from the category of profinite groups to the category of groups (GrpCat). On objects it assigns to a profinite group its underlying group, and on morphisms it assigns the underlying group homomorphism.

Русский

Существуют функтор забывания между категорией профинированных групп и категорией групп. На объектах он отправляет профинитную группу на соответствующую ей обычную группу, а на гомоморфизмах – на соответствующий гомоморфизм групп.

LaTeX

$$$\mathrm{Forget2}\;\mathrm{ProfiniteGrp}\;\mathrm{GrpCat}$$$

Lean4

@[to_additive]
instance : HasForget₂ ProfiniteGrp GrpCat where
  forget₂.obj P := GrpCat.of P
  forget₂.map f := GrpCat.ofHom f.hom.toMonoidHom

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