forget₂_obj_moduleCat_of — Mathlib

English

For a Type X with additive group and R-module structure, forget₂.obj (ModuleCat.of R X) = AddCommGrpCat.of X.

Русский

Для типа X с аддитивной структурой и структурой модуля над R, forgetting₂ отображает ModuleCat.of R X в AddCommGrpCat.of X.

LaTeX

$$$ (\mathsf{forget}_2\;\mathrm{ModuleCat}\, R) .\mathrm{obj} (\mathrm{ModuleCat}.of\; R\; X) = \mathrm{AddCommGrpCat}.of X $$$

Lean4

theorem forget₂_obj_moduleCat_of (X : Type v) [AddCommGroup X] [Module R X] :
    (forget₂ (ModuleCat R) AddCommGrpCat).obj (of R X) = AddCommGrpCat.of X :=
  rfl

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