Decomposing 1 into primitive orthogonal idempotents

Decompositions of the unit of a ring A into orthogonal idempotents are the same thing as decompositions of the left regular module A into left ideals:

• a decomposition A = V₁ ⊕ ⋯ ⊕ Vₙ into left ideals produces, from the components of 1 = e₁ + ⋯ + eₙ, a complete family of orthogonal idempotents (Mathlib's DirectSum.completeOrthogonalIdempotents_idempotent), and eᵢ generates Vᵢ (DirectSum.span_singleton_idempotent);
• conversely, a complete family of orthogonal idempotents e decomposes A as the internal direct sum of the left ideals Aeᵢ (CompleteOrthogonalIdempotents.isInternal_span_singleton): the component of x in Aeᵢ is x eᵢ.

Under this dictionary a summand Aeᵢ is indecomposable exactly when eᵢ is primitive (TauCeti.isPrimitiveIdempotent_iff_isIndecomposableModule), so the Krull-Schmidt theorem for the left regular module of a left Artinian ring becomes a statement about idempotents: 1 is a sum of finitely many primitive orthogonal idempotents (TauCeti.exists_completeOrthogonalIdempotents_isPrimitiveIdempotent), and any two such decompositions have the same number of terms and are matched by a bijection under which the left ideals Aeᵢ and Afⱼ are isomorphic (CompleteOrthogonalIdempotents.exists_equiv_linearEquiv_span_singleton). The left ideals Aeᵢ are projective, being direct summands of A, and every simple module is a quotient of one of them (CompleteOrthogonalIdempotents.exists_surjective_of_isSimpleModule): this is the first half of the correspondence between the primitive idempotents of a finite-dimensional algebra and its simple modules.

Main results

• DirectSum.span_singleton_idempotent: the idempotent attached to a summand of a decomposition of A into left ideals generates that summand.
• CompleteOrthogonalIdempotents.isInternal_span_singleton: a complete family of orthogonal idempotents decomposes A as ⨁ᵢ Aeᵢ.
• TauCeti.exists_completeOrthogonalIdempotents_isPrimitiveIdempotent: in a left Artinian ring, 1 is a finite sum of primitive orthogonal idempotents.
• TauCeti.exists_surjective_span_singleton_of_sum_eq_one: if a finite family sums to 1, every simple module is a quotient of the left ideal generated by one of its terms.
• CompleteOrthogonalIdempotents.exists_equiv_linearEquiv_span_singleton: uniqueness of such a decomposition up to reindexing and isomorphism of the left ideals Aeᵢ, and CompleteOrthogonalIdempotents.card_eq_card_of_isPrimitiveIdempotent: the number of terms is an invariant of the ring.
• CompleteOrthogonalIdempotents.exists_surjective_of_isSimpleModule: every simple module is a quotient of some Aeᵢ.

References

• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.4.
• T. Y. Lam, A First Course in Noncommutative Rings, 2nd ed., §21 and §22.

theorem TauCeti.exists_surjective_span_singleton_of_sum_eq_one {A : Type u_1} {ι : Type u_2} [Ring A] [Fintype ι] {e : ι → A} (he : ∑ i : ι, e i = 1) (M : Type u_3) [AddCommGroup M] [Module A M] [IsSimpleModule A M] : ∃ (i : ι) (f : ↥(Ideal.span {e i}) →ₗ[A] M), Function.Surjective ⇑f

Every simple module is a quotient of a left ideal generated by one term of a decomposition of 1. If ∑ i, e i = 1 and m is nonzero, some e i • m is nonzero, so x ↦ x • m maps A(e i) onto the simple module. Neither idempotence nor orthogonality of e is needed.

theorem DirectSum.span_singleton_idempotent {A : Type u_1} {ι : Type u_2} [Semiring A] [DecidableEq ι] (V : ι → Ideal A) [Decomposition V] (i : ι) : Ideal.span {idempotent V i} = V i

The idempotent attached to a summand generates it. If A = ⨁ᵢ Vᵢ as left ideals and 1 = ∑ᵢ eᵢ with eᵢ ∈ Vᵢ, then Vᵢ = Aeᵢ: every x ∈ Vᵢ is its own i-th component, which is x eᵢ.

theorem IsIdempotentElem.op {M : Type u_1} [Mul M] {e : M} (he : IsIdempotentElem e) : IsIdempotentElem (MulOpposite.op e)

An idempotent stays idempotent in the opposite multiplication.

theorem IsIdempotentElem.span_singleton_eq_op_smul_top {A : Type u_1} [Semiring A] {e : A} (he : IsIdempotentElem e) : Ideal.span {e} = MulOpposite.op e • ⊤

The left ideal Ae is the piece e • A cut out by e acting on the right, that is, by MulOpposite.op e acting through the opposite ring; this is the bridge to the Peirce decomposition TauCeti.isInternal_smul_top.

theorem OrthogonalIdempotents.op {A : Type u_1} {ι : Type u_2} [Semiring A] {e : ι → A} (he : OrthogonalIdempotents e) : OrthogonalIdempotents (MulOpposite.op ∘ e)

A family of orthogonal idempotents stays orthogonal in the opposite ring.

theorem CompleteOrthogonalIdempotents.op {A : Type u_1} {ι : Type u_2} [Semiring A] [Fintype ι] {e : ι → A} (he : CompleteOrthogonalIdempotents e) : CompleteOrthogonalIdempotents (MulOpposite.op ∘ e)

A complete family of orthogonal idempotents stays complete in the opposite ring.

theorem CompleteOrthogonalIdempotents.isInternal_span_singleton {A : Type u_1} {ι : Type u_2} [Semiring A] [Fintype ι] {e : ι → A} [DecidableEq ι] (he : CompleteOrthogonalIdempotents e) : DirectSum.IsInternal fun (i : ι) => Ideal.span {e i}

A complete family of orthogonal idempotents decomposes the ring as the internal direct sum A = ⨁ᵢ Aeᵢ of the left ideals it generates, the component of x in Aeᵢ being x eᵢ. This is the converse of Mathlib's DirectSum.completeOrthogonalIdempotents_idempotent, and the Peirce decomposition TauCeti.isInternal_smul_top of A under right multiplication.

theorem CompleteOrthogonalIdempotents.exists_surjective_of_isSimpleModule {A : Type u_1} [Ring A] {ι : Type u_2} [Fintype ι] {e : ι → A} (he : CompleteOrthogonalIdempotents e) (M : Type u_3) [AddCommGroup M] [Module A M] [IsSimpleModule A M] : ∃ (i : ι) (f : ↥(Ideal.span {e i}) →ₗ[A] M), Function.Surjective ⇑f

Every simple module is a quotient of one of the left ideals Aeᵢ of a complete family of orthogonal idempotents. A nonzero m : M is ∑ᵢ eᵢ m, so some eᵢ m is nonzero, and then x ↦ x m maps Aeᵢ onto the simple module M.

theorem CompleteOrthogonalIdempotents.exists_equiv_linearEquiv_span_singleton {A : Type u_1} [Ring A] {ι : Type u_2} [Fintype ι] {e : ι → A} [IsArtinianRing A] {κ : Type u_3} [Fintype κ] {f : κ → A} (he : CompleteOrthogonalIdempotents e) (hf : CompleteOrthogonalIdempotents f) (hpe : ∀ (i : ι), TauCeti.IsPrimitiveIdempotent (e i)) (hpf : ∀ (j : κ), TauCeti.IsPrimitiveIdempotent (f j)) : ∃ (σ : ι ≃ κ), ∀ (i : ι), Nonempty (↥(Ideal.span {e i}) ≃ₗ[A] ↥(Ideal.span {f (σ i)}))

Uniqueness of a decomposition of 1 into primitive orthogonal idempotents. In a left Artinian ring, two complete families e and f of primitive orthogonal idempotents are matched by a bijection σ of their index sets under which Aeᵢ ≅ Af_{σ i}. This is the Krull-Schmidt theorem for the left regular module, read through CompleteOrthogonalIdempotents.isInternal_span_singleton.

theorem CompleteOrthogonalIdempotents.card_eq_card_of_isPrimitiveIdempotent {A : Type u_1} [Ring A] {ι : Type u_2} [Fintype ι] {e : ι → A} [IsArtinianRing A] {κ : Type u_3} [Fintype κ] {f : κ → A} (he : CompleteOrthogonalIdempotents e) (hf : CompleteOrthogonalIdempotents f) (hpe : ∀ (i : ι), TauCeti.IsPrimitiveIdempotent (e i)) (hpf : ∀ (j : κ), TauCeti.IsPrimitiveIdempotent (f j)) : Fintype.card ι = Fintype.card κ

In a left Artinian ring, the number of terms in a decomposition of 1 into primitive orthogonal idempotents does not depend on the decomposition.

theorem TauCeti.exists_completeOrthogonalIdempotents_isPrimitiveIdempotent (A : Type u_1) [Ring A] [IsArtinianRing A] : ∃ (n : ℕ) (e : Fin n → A), CompleteOrthogonalIdempotents e ∧ ∀ (i : Fin n), IsPrimitiveIdempotent (e i)

Existence of a decomposition of 1 into primitive orthogonal idempotents. In a left Artinian ring — for instance a finite-dimensional algebra over a field — 1 = e₀ + ⋯ + eₙ₋₁ for a complete family of orthogonal idempotents each of which is primitive.

The left regular module is the internal direct sum of finitely many indecomposable left ideals (TauCeti.exists_isInternal_isIndecomposableModule); the components of 1 along that decomposition are complete orthogonal idempotents generating the summands (DirectSum.span_singleton_idempotent), hence primitive.