A complete family of orthogonal idempotents decomposes every module

Let R be a semiring and let e : ι → R be a complete orthogonal family of idempotents: eᵢ eⱼ = 0 for i ≠ j and ∑ᵢ eᵢ = 1. Then every left R-module M splits as an internal direct sum of the S-submodules eᵢ • M,

M = ⨁ᵢ eᵢ M,

the component of x in position i being eᵢ • x. This file proves that (TauCeti.isInternal_smul_top) and records the dimension count dim M = ∑ᵢ dim (eᵢ M) that follows over a division ring.

Mathlib has the family (CompleteOrthogonalIdempotents) and the converse direction — a decomposition of R itself into left ideals produces such a family (DirectSum.completeOrthogonalIdempotents_idempotent) — but not the decomposition of an arbitrary module that the family induces.

The pieces

The piece eᵢ M is Mathlib's pointwise action e i • (⊤ : Submodule S M) (scoped in Pointwise), so no new definition is introduced for it and Mathlib's pointwise API — Submodule.pointwise_smul_def, Submodule.mem_smul_pointwise_iff_exists, Submodule.smul_mem_pointwise_smul — applies to the statements below as it stands.

The two scalar rings

The pieces eᵢ • M are not R-submodules: R is noncommutative in the intended applications, and r • (eᵢ • x) need not lie in eᵢ • M. They are submodules over any second ring S whose action on M commutes with that of R, that is, under SMulCommClass R S M, which is exactly what makes multiplication by e an S-linear map (DistribSMul.toLinearMap) and is exactly the hypothesis of Mathlib's pointwise action on Submodule S M; carrying that ambient S is what makes the dimension count below available. Taking S = ℕ recovers the decomposition as additive submonoids, and an S-algebra structure on R together with IsScalarTower S R M supplies the hypothesis in the intended applications.

Main definitions

• TauCeti.smulTopMap S e f: the restriction of an R-linear map f : M →ₗ[R] N to e • M →ₗ[S] e • N.

Main results

• IsIdempotentElem.mem_smul_top_iff_smul_eq_self: for an idempotent e, membership in e • M is the fixed-point condition e • x = x. The scalar e needs only a distributive monoid action on M.
• TauCeti.isInternal_smul_top: the decomposition M = ⨁ᵢ eᵢ M, with the component of x at i being eᵢ • x (TauCeti.coe_ofBijective_coeLinearMap_symm_apply_smul_top).
• TauCeti.smul_coeLinearMap_smul_top: multiplying by eᵢ reads off the i-th component of a sum. This is what makes the sum direct.
• TauCeti.finrank_eq_sum_finrank_smul_top: for a module finite-dimensional over a division ring S, the dimensions of the pieces add up to the dimension of the module.
• IsIdempotentElem.instModuleCornerSmulTop: for a single idempotent e, the piece e • M is a module over the corner ring eAe (IsIdempotentElem.Corner), which acts by restricting the action of A, as recorded by IsIdempotentElem.Corner.coe_smul. This is the module structure the corner functor M ↦ eM of Morita theory is built on.

References

The decomposition of a module along a complete orthogonal family of idempotents is the classical Peirce decomposition; see T. Y. Lam, A First Course in Noncommutative Rings, §21, or Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Ch. I.4.

theorem IsIdempotentElem.mem_smul_top_iff_smul_eq_self {S : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring S] [Monoid R] [AddCommMonoid M] [Module S M] [DistribMulAction R M] [SMulCommClass R S M] {e : R} (he : IsIdempotentElem e) {x : M} : x ∈ e • ⊤ ↔ e • x = x

Membership in e • M for an idempotent e is a fixed-point condition. This is Mathlib's LinearMap.IsIdempotentElem.mem_range_iff for the idempotent endomorphism x ↦ e • x, whose range is the piece e • M.

theorem IsIdempotentElem.smul_eq_self_of_mem_smul_top {S : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring S] [Monoid R] [AddCommMonoid M] [Module S M] [DistribMulAction R M] [SMulCommClass R S M] {e : R} (he : IsIdempotentElem e) {x : M} (hx : x ∈ e • ⊤) : e • x = x

Multiplication by an idempotent e fixes e • M pointwise.

theorem TauCeti.smul_top_le_comap_smul_top (S : Type u_1) {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring S] [Semiring R] [AddCommMonoid M] [Module S M] [Module R M] [SMulCommClass R S M] [AddCommMonoid N] [Module S N] [Module R N] [SMulCommClass R S N] [LinearMap.CompatibleSMul M N S R] (e : R) (f : M →ₗ[R] N) : e • ⊤ ≤ Submodule.comap (↑S f) (e • ⊤)

The pieces are natural in the module: an R-linear map carries e • M into e • N.

def TauCeti.smulTopMap (S : Type u_1) {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring S] [Semiring R] [AddCommMonoid M] [Module S M] [Module R M] [SMulCommClass R S M] [AddCommMonoid N] [Module S N] [Module R N] [SMulCommClass R S N] [LinearMap.CompatibleSMul M N S R] (e : R) (f : M →ₗ[R] N) : ↥(e • ⊤) →ₗ[S] ↥(e • ⊤)

The restriction of an R-linear map M → N to the pieces cut out by e, an S-linear map e • M → e • N. This is TauCeti.smul_top_le_comap_smul_top promoted to the map it describes.

Equations

• TauCeti.smulTopMap S e f = (↑S f).restrict ⋯

@[simp]

theorem TauCeti.coe_smulTopMap_apply {S : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring S] [Semiring R] [AddCommMonoid M] [Module S M] [Module R M] [SMulCommClass R S M] [AddCommMonoid N] [Module S N] [Module R N] [SMulCommClass R S N] [LinearMap.CompatibleSMul M N S R] (e : R) (f : M →ₗ[R] N) (x : ↥(e • ⊤)) : ↑((smulTopMap S e f) x) = f ↑x

@[simp]

theorem TauCeti.smulTopMap_id {S : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring S] [Semiring R] [AddCommMonoid M] [Module S M] [Module R M] [SMulCommClass R S M] [LinearMap.CompatibleSMul M M S R] (e : R) : smulTopMap S e LinearMap.id = LinearMap.id

The restriction to the pieces is functorial: the identity restricts to the identity.

@[simp]

theorem TauCeti.smulTopMap_comp {S : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {R : Type u_5} [Semiring S] [Semiring R] [AddCommMonoid M] [Module S M] [Module R M] [SMulCommClass R S M] [AddCommMonoid N] [Module S N] [Module R N] [SMulCommClass R S N] [AddCommMonoid P] [Module S P] [Module R P] [SMulCommClass R S P] [LinearMap.CompatibleSMul M N S R] [LinearMap.CompatibleSMul N P S R] [LinearMap.CompatibleSMul M P S R] (e : R) (g : N →ₗ[R] P) (f : M →ₗ[R] N) : smulTopMap S e (g ∘ₗ f) = smulTopMap S e g ∘ₗ smulTopMap S e f

The restriction to the pieces is functorial: a composite restricts to the composite of the restrictions.

theorem TauCeti.smul_eq_zero_of_ne_of_mem_smul_top {S : Type u_1} {M : Type u_2} {R : Type u_3} {ι : Type u_4} [Semiring S] [Semiring R] [AddCommMonoid M] [Module S M] [Module R M] [SMulCommClass R S M] {e : ι → R} (he : OrthogonalIdempotents e) {i j : ι} (hij : i ≠ j) {x : M} (hx : x ∈ e j • ⊤) : e i • x = 0

An orthogonal idempotent annihilates the piece cut out by any of the others.

theorem TauCeti.iSupIndep_smul_top {S : Type u_1} {M : Type u_2} {R : Type u_3} {ι : Type u_4} [Semiring S] [Semiring R] [AddCommMonoid M] [Module S M] [Module R M] [SMulCommClass R S M] {e : ι → R} (he : OrthogonalIdempotents e) : iSupIndep fun (i : ι) => e i • ⊤

The pieces cut out by an orthogonal family are independent: the piece at i meets the supremum of the others only in 0, because eᵢ fixes the former and kills the latter.

theorem TauCeti.sum_smul_eq_self_of_sum_eq_one {M : Type u_2} {R : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {e : ι → R} [Fintype ι] (he : ∑ i : ι, e i = 1) (x : M) : ∑ i : ι, e i • x = x

A decomposition of the unit decomposes every element: if ∑ᵢ eᵢ = 1 then x = ∑ᵢ eᵢ • x. Neither idempotency nor orthogonality is needed.

theorem TauCeti.iSup_smul_top_eq_top_of_sum_eq_one {S : Type u_1} {M : Type u_2} {R : Type u_3} {ι : Type u_4} [Semiring S] [Semiring R] [AddCommMonoid M] [Module S M] [Module R M] [SMulCommClass R S M] {e : ι → R} [Fintype ι] (he : ∑ i : ι, e i = 1) : ⨆ (i : ι), e i • ⊤ = ⊤

The pieces cut out by a decomposition of the unit span the module.

theorem TauCeti.smul_coeLinearMap_smul_top {S : Type u_1} {M : Type u_2} {R : Type u_3} {ι : Type u_4} [Semiring S] [Semiring R] [AddCommMonoid M] [Module S M] [Module R M] [SMulCommClass R S M] {e : ι → R} [DecidableEq ι] (he : OrthogonalIdempotents e) (z : DirectSum ι fun (i : ι) => ↥(e i • ⊤)) (j : ι) : e j • (DirectSum.coeLinearMap fun (i : ι) => e i • ⊤) z = ↑(z j)

Multiplying by eⱼ reads off the j-th component of a sum: in ∑ᵢ zᵢ with zᵢ ∈ eᵢ M, the idempotent eⱼ fixes the term at j and annihilates all the others. This is what makes the sum direct.

theorem TauCeti.isInternal_smul_top {S : Type u_1} {M : Type u_2} {R : Type u_3} {ι : Type u_4} [Semiring S] [Semiring R] [AddCommMonoid M] [Module S M] [Module R M] [SMulCommClass R S M] {e : ι → R} [DecidableEq ι] [Fintype ι] (he : CompleteOrthogonalIdempotents e) : DirectSum.IsInternal fun (i : ι) => e i • ⊤

A complete orthogonal family of idempotents decomposes every module: M = ⨁ᵢ eᵢ M.

The S-submodule at i is eᵢ • M, and the component of x there is eᵢ • x.

@[simp]

theorem TauCeti.coe_ofBijective_coeLinearMap_symm_apply_smul_top {S : Type u_1} {M : Type u_2} {R : Type u_3} {ι : Type u_4} [Semiring S] [Semiring R] [AddCommMonoid M] [Module S M] [Module R M] [SMulCommClass R S M] {e : ι → R} [DecidableEq ι] [Fintype ι] (he : CompleteOrthogonalIdempotents e) (x : M) (i : ι) : ↑(((LinearEquiv.ofBijective (DirectSum.coeLinearMap fun (i : ι) => e i • ⊤) ⋯).symm x) i) = e i • x

The component of x at i is eᵢ • x: this is the inverse of the decomposition, read off one index at a time. The isomorphism ⨁ᵢ eᵢ M ≃ₗ[S] M is the canonical LinearEquiv.ofBijective (DirectSum.coeLinearMap _) of an internal direct sum, so Mathlib's DirectSum.IsInternal.ofBijective_coeLinearMap_same and friends apply to it as well.

theorem TauCeti.finrank_eq_sum_finrank_smul_top {S : Type u_1} {M : Type u_2} {R : Type u_3} {ι : Type u_4} [DivisionRing S] [Semiring R] [AddCommGroup M] [Module S M] [Module R M] [SMulCommClass R S M] {e : ι → R} [Fintype ι] [Module.Finite S M] (he : CompleteOrthogonalIdempotents e) : Module.finrank S M = ∑ i : ι, Module.finrank S ↥(e i • ⊤)

The dimension count: for a module finite-dimensional over a division ring S, the dimensions of the pieces add up to the dimension of the module.

The pieces as modules over the corner ring

@[instance_reducible]

instance IsIdempotentElem.instSMulCornerSmulTop {S : Type u_1} {M : Type u_2} {A : Type u_3} [Semiring S] [Semiring A] [AddCommMonoid M] [Module S M] [Module A M] [SMulCommClass A S M] {e : A} (he : IsIdempotentElem e) : SMul he.Corner ↥(e • ⊤)

The corner ring eAe acts on the piece e • M by restricting the action of A.

Equations

• he.instSMulCornerSmulTop = { smul := fun (b : he.Corner) (x : ↥(e • ⊤)) => ⟨↑b • ↑x, ⋯⟩ }

@[simp]

theorem IsIdempotentElem.Corner.coe_smul {S : Type u_1} {M : Type u_2} {A : Type u_3} [Semiring S] [Semiring A] [AddCommMonoid M] [Module S M] [Module A M] [SMulCommClass A S M] {e : A} (he : IsIdempotentElem e) (b : he.Corner) (x : ↥(e • ⊤)) : ↑(b • x) = ↑b • ↑x

@[instance_reducible]

instance IsIdempotentElem.instModuleCornerSmulTop {S : Type u_1} {M : Type u_2} {A : Type u_3} [Semiring S] [Semiring A] [AddCommMonoid M] [Module S M] [Module A M] [SMulCommClass A S M] {e : A} (he : IsIdempotentElem e) : Module he.Corner ↥(e • ⊤)

The piece e • M of an A-module is a module over the corner ring eAe. Its unit e acts trivially because e fixes e • M pointwise.

Equations

• he.instModuleCornerSmulTop = { toSMul := he.instSMulCornerSmulTop, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

theorem IsIdempotentElem.coe_algebraMap_corner_smul {S : Type u_1} {M : Type u_2} {A : Type u_3} [Semiring S] [Semiring A] [AddCommMonoid M] [Module S M] [Module A M] [SMulCommClass A S M] {e : A} (he : IsIdempotentElem e) {R : Type u_4} [CommSemiring R] [Algebra R A] (r : R) (x : ↥(e • ⊤)) : ↑((algebraMap R he.Corner) r • x) = (algebraMap R A) r • ↑x

On the piece e • M, the scalar r • e of the corner ring acts as r does on M.