English
If R is the direct sum of left ideals V_i over a finite index set I, then e_i := idempotent V i form a complete orthogonal set: e_i e_j = 0 for i ≠ j, e_i^2 = e_i, and ∑ e_i = 1.
Русский
Если R распадается на конечную сумму левых идеалов V_i, то e_i образуют полную ортогональную систему идемпотентов.
LaTeX
$$Complete Orthogonal Idempotents: e_i^2 = e_i, e_i e_j = 0 (i≠j), ∑_{i∈I} e_i = 1$$
Lean4
/-- If a semiring can be decomposed into direct sum of finite left ideals `Vᵢ`
where `1 = e₁ + ... + eₙ` and `eᵢ ∈ Vᵢ`, then `eᵢ` is a family of complete
orthogonal idempotents. -/
theorem completeOrthogonalIdempotents_idempotent [Fintype I] : CompleteOrthogonalIdempotents (idempotent V)
where
idem := isIdempotentElem_idempotent V
ortho i j
hij := by
simp only
rw [← decompose_eq_mul_idempotent, idempotent, decompose_coe, of_eq_of_ne (h := hij.symm), Submodule.coe_zero]
complete := by
apply (decompose V).injective
refine DFunLike.ext _ _ fun i ↦ ?_
rw [decompose_sum, DFinsupp.finset_sum_apply]
simp [idempotent, of_apply]
