English
There is a natural 𝕜-module structure on the incidence algebra IncidenceAlgebra 𝕝 α given by pointwise scalar action on the values in 𝕝: (c • f)(a,b) = c • f(a,b) for c ∈ 𝕜 and f ∈ IncidenceAlgebra 𝕝 α.
Русский
Существуют естественные структуры модуля над 𝕜 на инцидентальную алгебру IncidenceAlgebra 𝕝 α: скалярное действие задаётся по точкам как (c • f)(a,b) = c • f(a,b) для c ∈ 𝕜 и f ∈ IncidenceAlgebra 𝕝 α.
LaTeX
$$$ (c \; \text{smul} \; f)(a,b) = c \;\cdot\; f(a,b) \quad( c \in 𝕜,\ f \in IncidenceAlgebra 𝕝 α)$$$
Lean4
instance [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] [Semiring 𝕜] [Semiring 𝕝] [Module 𝕜 𝕝] :
Module (IncidenceAlgebra 𝕜 α) (IncidenceAlgebra 𝕝 α)
where
smul := (· • ·)
one_smul f := by ext a b hab; simp [ite_smul, hab]
mul_smul := smul_assoc
smul_add f g h := by ext; exact Eq.trans (sum_congr rfl fun x _ ↦ smul_add _ _ _) sum_add_distrib
add_smul f g h := by ext; exact Eq.trans (sum_congr rfl fun x _ ↦ add_smul _ _ _) sum_add_distrib
zero_smul f := by ext; exact sum_eq_zero fun x _ ↦ zero_smul _ _
smul_zero f := by ext; exact sum_eq_zero fun x _ ↦ smul_zero _
