English
Let α be a locally finite preorder. For any scalar rings 𝕜, 𝕝 and functions f ∈ IncidenceAlgebra 𝕜 α, g ∈ IncidenceAlgebra 𝕝 α, the product is given by a convolution formula: (f • g)(a,b) = sum over x in Icc(a,b) of f(a,x) • g(x,b), where the operation • denotes the natural scalar action of 𝕜 on 𝕝.
Русский
Пусть α — локально сконечный частично упорядоченный множество. Для скаляров 𝕜, 𝕝 и функций f ∈ IncidenceAlgebra 𝕜 α, g ∈ IncidenceAlgebra 𝕝 α произведение задаётся свёрткой: (f • g)(a,b) = ∑_{x ∈ Icc(a,b)} f(a,x) • g(x,b), где • обозначает скалярное действие 𝕜 на 𝕝.
LaTeX
$$$ (f \; \bullet \; g)(a,b) = \sum _{x \in Icc(a,b)} f(a,x) \;\cdot\; g(x,b) $$$
Lean4
@[simp]
theorem smul_apply (f : IncidenceAlgebra 𝕜 α) (g : IncidenceAlgebra 𝕝 α) (a b : α) :
(f • g) a b = ∑ x ∈ Icc a b, f a x • g x b :=
rfl
