forget₂_obj — Mathlib

English

For f: X ⟶ Y in ModuleCat, (forget₂).map f equals AddCommGrpCat.ofHom f.hom.

Русский

Для f: X ⟶ Y в ModuleCat, отображение forget₂ действует так, что (forget₂).map f = AddCommGrpCat.ofHom f.hom.

LaTeX

$$$ (\mathsf{forget}_2\;\mathrm{ModuleCat}\, R\;\mathrm AddCommGrpCat).map f = AddCommGrpCat.ofHom f.hom $$$

Lean4

@[simp]
theorem forget₂_obj (X : ModuleCat R) : (forget₂ (ModuleCat R) AddCommGrpCat).obj X = AddCommGrpCat.of X :=
  rfl

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