English
Define λ on IncidenceAlgebra 𝕜 α by λ(a,b) = 1 if a ⩿ b and the interval [a,b] is nonempty with cardinality 1 or 2, and λ(a,b) = 0 otherwise; this λ is an element of the incidence algebra (the lambda function).
Русский
Задаём λ на IncidenceAlgebra 𝕜 α так, что λ(a,b) = 1, если a ⩿ b и интервал [a,b] непустой и имеет нумерацию 1 или 2, иначе λ(a,b) = 0; это элемент инцидентальной алгебры.
LaTeX
$$$ \lambda(a,b) = \begin{cases} 1, & a \mathrel{⩿} b, \\ 0, & \text{иначе} \end{cases}$$$
Lean4
instance algebraRight [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] [CommSemiring 𝕜] [CommSemiring 𝕝]
[Algebra 𝕜 𝕝] : Algebra 𝕜 (IncidenceAlgebra 𝕝 α)
where
algebraMap :=
{ toFun c := algebraMap 𝕜 𝕝 c • (1 : IncidenceAlgebra 𝕝 α)
map_one' := by ext; simp only [mul_boole, one_apply, Algebra.id.smul_eq_mul, constSMul_apply, map_one]
map_mul' c
d := by
ext a b
obtain rfl | h := eq_or_ne a b
· simp only [one_apply, Algebra.id.smul_eq_mul, mul_apply, constSMul_apply, map_mul, eq_comm, Icc_self]
simp
· simp only [one_apply, mul_one, Algebra.id.smul_eq_mul, mul_apply, zero_mul, constSMul_apply, ← ite_and,
ite_mul, mul_ite, map_mul, mul_zero, if_neg h]
refine (sum_eq_zero fun x _ ↦ ?_).symm
exact if_neg fun hx ↦ h <| hx.2.trans hx.1
map_zero' := by rw [map_zero, zero_smul]
map_add' c d := by rw [map_add, add_smul] }
commutes' c f := by classical ext a b hab; simp [if_pos hab, constSMul_apply, mul_comm]
smul_def' c f := by classical ext a b hab; simp [if_pos hab, constSMul_apply, Algebra.smul_def]