English
Let α be a locally finite preorder and 𝕜, 𝕝, 𝕞 be rings with actions satisfying a scalar tower. Then the three incidence algebras form a scalar tower, i.e., for all f,g,h we have (f • g) • h = f • (g • h).
Русский
Пусть α — локально конечный порядковый набор, а 𝕜, 𝕝, 𝕞 — кольца, образующие тройку скалярных действий, удовлетворяющую условию башни скаляров. Тогда три инцидентальные алгебры образуют башню скаляров: для всех f,g,h выполняется (f • g) • h = f • (g • h).
LaTeX
$$$ \forall f,g,h,\ (f \; \text{smul} \; g) \; \text{smul} \; h = f \; \text{smul} \; (g \; \text{smul} \; h). $$$$
Lean4
instance instIsScalarTower [Preorder α] [LocallyFiniteOrder α] [AddCommMonoid 𝕜] [Monoid 𝕜] [Semiring 𝕝]
[AddCommMonoid 𝕞] [SMul 𝕜 𝕝] [Module 𝕝 𝕞] [DistribMulAction 𝕜 𝕞] [IsScalarTower 𝕜 𝕝 𝕞] :
IsScalarTower (IncidenceAlgebra 𝕜 α) (IncidenceAlgebra 𝕝 α) (IncidenceAlgebra 𝕞 α) where
smul_assoc f g
h := by
ext a b
simp only [smul_apply, sum_smul, smul_sum, sum_sigma']
apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;> aesop (add unsafe le_trans)
