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)
Instances For
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]
:
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.