homMk — Mathlib

English

The forgetful map applied to the morphism hom Mk φ hφ equals φ on the underlying AddCommGrp morphisms, i.e., the forgetful functor sees the φ part of the morphism.

Русский

Применение забывающего функтор к гом Mk φ hφ равно φ на базовом гомоморфизме.

LaTeX

$$$\mathrm{forget}_2(\mathrm{ModuleCat}.homMk\; φ\; hφ) = φ$$$

Lean4

/-- Constructor for morphisms in `ModuleCat R` which takes as inputs
a morphism between the underlying objects in `AddCommGrpCat` and the compatibility
with the scalar multiplication. -/
@[simps]
def homMk : M ⟶ N where
  hom'.toFun := φ
  hom'.map_add' _ _ := φ.hom.map_add _ _
  hom'.map_smul' r x := (congr_hom (hφ r) x).symm

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