moduleRight — Mathlib

English

Under appropriate finiteness and decidability hypotheses, IncidenceAlgebra 𝕜 α carries a natural 𝕜-algebra structure extending the scalar action, with the algebra map sending c ∈ 𝕜 to c • 1 in IncidenceAlgebra 𝕝 α.

Русский

При соответствующих ограничениях на конечность и разрешимость, IncidenceAlgebra 𝕝 α обладает естественной структурой 𝕜-алгебры, продолжающей скалярное действие, где алгебраическая карта отправляет c ∈ 𝕜 в c • 1 в IncidenceAlgebra 𝕝 α.

LaTeX

$$$ \text{AlgebraMap}_{𝕜\to 𝕝}(c) = c \cdot 1_{IncidenceAlgebra 𝕝 α}$$$

Lean4

instance moduleRight [Preorder α] [Semiring 𝕜] [AddCommMonoid 𝕝] [Module 𝕜 𝕝] : Module 𝕜 (IncidenceAlgebra 𝕝 α) :=
  DFunLike.coe_injective.module _ ⟨⟨((⇑) : IncidenceAlgebra 𝕝 α → α → α → 𝕝), coe_zero⟩, coe_add⟩ coe_constSMul

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