smulNatTrans — Mathlib

English

Let R be a ring. For the category of R-modules, there is a canonical ring homomorphism from R into the endomorphism ring of the forgetful functor to the category of abelian groups, given on each module M by the map m ↦ r·m. This assignment is compatible with morphisms (naturality), so scalars act uniformly across all modules.

Русский

Пусть R — кольцо. Для категории R-модулей существует каноническое кольцевое гомоморфизм из R в кардинально End(F), где F есть забывающий функтор к абелевым группам, заданный на каждом модуле M через действие скаляра: m ↦ r·m. Это соответствие сохраняет структуру гомоморфизмов (натуральность).

LaTeX

$$$\exists \varphi: R \to \mathrm{End}(F) \quad\text{где } F = \mathrm{forget}_R:\mathrm{ModuleCat}(R) \to \mathrm{End}\!\big(\mathrm{forget}_R\big) \text{ и } \varphi(r)_M(m) = r \cdot m \ \forall M, m,$\nи $\varphi$ является кольцевым гомоморфизм.$$

Lean4

/-- The scalar multiplication on `ModuleCat R` considered as a morphism of rings
to the endomorphisms of the forgetful functor to `AddCommGrpCat)`. -/
@[simps]
def smulNatTrans : R →+* End (forget₂ (ModuleCat R) AddCommGrpCat)
    where
  toFun
    r :=
    { app := fun M => M.smul r
      naturality := fun _ _ _ => smul_naturality _ r }
  map_one' := NatTrans.ext (by cat_disch)
  map_zero' := NatTrans.ext (by cat_disch)
  map_mul' _ _ := NatTrans.ext (by cat_disch)
  map_add' _ _ := NatTrans.ext (by cat_disch)

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