hasForgetToAddCommGroup — Mathlib

English

There is a forgetful functor from ModuleCat R to AddCommGrpCat sending a module to its underlying additive abelian group.

Русский

Существует функтор забывания из ModuleCat R к AddCommGrpCat, отправляющий модуль в его базовую абелеву группу.

LaTeX

$$$ \text{Forget}_2: \mathrm{ModuleCat}(R) \to \mathrm{AddCommGrpCat} $$$

Lean4

instance hasForgetToAddCommGroup : HasForget₂ (ModuleCat R) AddCommGrpCat where
  forget₂ :=
    { obj := fun M => AddCommGrpCat.of M
      map := fun f => AddCommGrpCat.ofHom f.hom.toAddMonoidHom }

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