forget₂_map

Mathlib.Algebra.Category.ModuleCat.Basic

URI: https://scilib.ai/kg/mathlib#ModuleCat.forget₂_map

English

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

Русский

На морфизме f: X ⟶ Y в ModuleCat forget₂.map f равно AddCommGrpCat.ofHom (f.hom).

LaTeX

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

Lean4

@[simp]
theorem forget₂_map (X Y : ModuleCat R) (f : X ⟶ Y) :
    (forget₂ (ModuleCat R) AddCommGrpCat).map f = AddCommGrpCat.ofHom f.hom :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru