Decomposition of the identity of a semiring into orthogonal idempotents

In this file we show that if a semiring R can be decomposed into a direct sum of (left) ideals R = V₁ ⊕ V₂ ⊕ ⋯ ⊕ Vₙ then in the corresponding decomposition 1 = e₁ + e₂ + ⋯ + eₙ with eᵢ ∈ Vᵢ, each eᵢ is an idempotent and the eᵢ's form a family of complete orthogonal idempotents.

def DirectSum.idempotent {R : Type u_1} {I : Type u_2} [Semiring R] [DecidableEq I] (V : I → Ideal R) [Decomposition V] (i : I) : R

The decomposition of (1 : R) where 1 = e₁ + e₂ + ⋯ + eₙ which is induced by the decomposition of the semiring R = V1 ⊕ V2 ⊕ ⋯ ⊕ Vn.

Equations

• DirectSum.idempotent V i = ↑(((DirectSum.decompose V) 1) i)

theorem DirectSum.decompose_eq_mul_idempotent {R : Type u_1} {I : Type u_2} [Semiring R] [DecidableEq I] (V : I → Ideal R) [Decomposition V] (x : R) (i : I) : ↑(((decompose V) x) i) = x * idempotent V i

theorem DirectSum.isIdempotentElem_idempotent {R : Type u_1} {I : Type u_2} [Semiring R] [DecidableEq I] (V : I → Ideal R) [Decomposition V] (i : I) : IsIdempotentElem (idempotent V i)

theorem DirectSum.completeOrthogonalIdempotents_idempotent {R : Type u_1} {I : Type u_2} [Semiring R] [DecidableEq I] (V : I → Ideal R) [Decomposition V] [Fintype I] : CompleteOrthogonalIdempotents (idempotent V)

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.