English
The incidence algebra IncidenceAlgebra 𝕜 α over a locally finite preorder α is a semiring, with convolution as multiplication and 1, 0 as the unit and zero.
Русский
Инцидентная алгебра над 𝕜 для локально конечного предorder α образует полукольцо: умножение — свёртка, единица — 1, ноль — 0.
LaTeX
$$$$ \\text{If } [Preorder\\ α], [LocallyFiniteOrder α], [DecidableEq α], [Semiring 𝕜], \\text{ then } \\operatorname{IncidenceAlgebra} 𝕜 α \\text{ is a semiring with } (f * g)(a,b) = \\sum_{a \\le x \\le b} f(a,x)\\,g(x,b). $$$$
Lean4
instance instSemiring [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] [Semiring 𝕜] : Semiring (IncidenceAlgebra 𝕜 α)
where
__ := instNonAssocSemiring
mul := (· * ·)
mul_assoc f g
h := by
ext a b
simp only [mul_apply, sum_mul, mul_sum, sum_sigma']
apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;> aesop (add simp mul_assoc) (add unsafe le_trans)
one := 1
zero := 0
