isModule — Mathlib

English

The direct sum of graded components carries a natural module structure over the base ring.

Русский

Прямая сумма градационных компонент естественным образом образует модуль над основанной кольцевой структурой.

LaTeX

$$$$ \\text{DirectSum is a module over } A. $$$$

Lean4

/-- The smul multiplication of `A` on `⨁ i, 𝓜 i` from `(⨁ i, 𝓐 i) →+ (⨁ i, 𝓜 i) →+ ⨁ i, 𝓜 i`
turns `⨁ i, 𝓜 i` into an `A`-module
-/
def isModule [DecidableEq ιA] [DecidableEq ιM] [GradedRing 𝓐] : Module A (⨁ i, 𝓜 i) :=
  { Module.compHom _ (DirectSum.decomposeRingEquiv 𝓐 : A ≃+* ⨁ i, 𝓐 i).toRingHom with
    smul := fun a b => DirectSum.decompose 𝓐 a • b }

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