forget_obj — Mathlib

English

The forgetful functor from ModuleCat(R) to AddCommGroupCat preserves objects, i.e., it sends a module to its underlying abelian group unchanged.

Русский

Забывающий функтор из ModuleCat(R) в AddCommGroupCat сохраняет объекты: модуль превращается в встроенную абелеву группу без изменения множества элементов.

LaTeX

$$$(\text{forget} \; \mathrm{ModuleCat}(R)).\mathrm{obj}(M) = M$$$

Lean4

theorem forget_obj {M : ModuleCat.{v} R} : (forget (ModuleCat.{v} R)).obj M = M :=
  rfl

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