English
There is a natural K-algebra structure on the space of simple functions α →ₛ β, provided K is a commutative semiring, β is a semiring, and β is an algebra over K; the algebra map is given by sending k ∈ K to the constant function α →ₛ β with value algebraMap K β k.
Русский
Существует естественная структура K-алгебры на множестве простых функций α →ₛ β, если K — коммутативный полугруппа, β — полугруппа, и β — алгебра над K; алгебраическая карта отправляет элемент k ∈ K в константную функцию α →ₛ β, принимающую значение algebraMap K β k.
LaTeX
$$$\\text{Algebra}_K(\\alpha \\to_{\\mathcal{S}} \\beta)\\;\\text{ with }\\; \\text{algebraMap}(k) = \\text{const}_{\\alpha}(\\text{algebraMap}_{K}^{\\beta}(k)).$$$
Lean4
instance [CommSemiring K] [Semiring β] [Algebra K β] : Algebra K (α →ₛ β)
where
algebraMap :=
{ toFun r := const α <| algebraMap K β r
map_one' := ext fun _ ↦ algebraMap K β |>.map_one ▸ rfl
map_mul' _ _ := ext fun _ ↦ algebraMap K β |>.map_mul ..
map_zero' := ext fun _ ↦ algebraMap K β |>.map_zero ▸ rfl
map_add' _ _ := ext fun _ ↦ algebraMap K β |>.map_add .. }
commutes' _ _ := ext fun _ ↦ Algebra.commutes ..
smul_def' _ _ := ext fun _ ↦ Algebra.smul_def ..
