Decomposing a module along a complete orthogonal system of idempotents

A complete orthogonal system of idempotents (eᵢ) in a commutative ring R decomposes R as a finite product of rings R ⧸ (1 - eᵢ) — that is mathlib's CompleteOrthogonalIdempotents.bijective_pi. This file supplies the module analogue: the same system decomposes every R-module M as ∏ᵢ M ⧸ (1 - eᵢ)M, compatibly with the ring decomposition.

Applying this with mathlib's QuotSMulTop.equivQuotTensor rewrites the factors as (R ⧸ (1 - eᵢ)) ⊗[R] M, which is the form in which the pieces are modules over the factor rings.

Main results

• CompleteOrthogonalIdempotents.bijective_piQuotSMulTop : the comparison map M → ∏ᵢ M ⧸ (1 - eᵢ)M is bijective.
• CompleteOrthogonalIdempotents.linearEquivPiQuotSMulTop : that map packaged as a linear equivalence.
• CompleteOrthogonalIdempotents.linearEquivPiQuotientTensor : the same, with the factors written as (R ⧸ (1 - eᵢ)) ⊗[R] M.

Implementation notes

This is a statement mathlib is missing, not a competing formulation of one it has: mathlib's CompleteOrthogonalIdempotents.bijective_pi is exactly the case M = R, and the proof here is the same two-line computation carried out with scalars acting on M. Both directions are elementary — injectivity because x = (∑ᵢ eᵢ) • x and each eᵢ • x vanishes, surjectivity by assembling ∑ᵢ eᵢ • xᵢ from lifts of the components.

The factors are QuotSMulTop (1 - eᵢ) M, mathlib's abbreviation for M ⧸ (1 - eᵢ) • ⊤, rather than the tensor products (R ⧸ (1 - eᵢ)) ⊗[R] M, because the quotient form is what the proof manipulates. linearEquivPiQuotientTensor converts.

def piQuotSMulTop {R : Type u} [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] {I : Type w} (e : I → R) : M →ₗ[R] (i : I) → QuotSMulTop (1 - e i) M

The comparison map M → ∏ᵢ M ⧸ (1 - eᵢ)M attached to a family of elements of R.

Equations

• piQuotSMulTop M e = LinearMap.pi fun (i : I) => ((1 - e i) • ⊤).mkQ

@[simp]

theorem piQuotSMulTop_apply {R : Type u} [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] {I : Type w} {e : I → R} (x : M) (i : I) : (piQuotSMulTop M e) x i = Submodule.Quotient.mk x

theorem CompleteOrthogonalIdempotents.bijective_piQuotSMulTop {R : Type u} [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] {I : Type w} [Fintype I] {e : I → R} (he : CompleteOrthogonalIdempotents e) : Function.Bijective ⇑(piQuotSMulTop M e)

A complete orthogonal system of idempotents decomposes every module. The module analogue of CompleteOrthogonalIdempotents.bijective_pi, which is the case M = R.

noncomputable def CompleteOrthogonalIdempotents.linearEquivPiQuotSMulTop {R : Type u} [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] {I : Type w} [Fintype I] (e : I → R) (he : CompleteOrthogonalIdempotents e) : M ≃ₗ[R] (i : I) → QuotSMulTop (1 - e i) M

The decomposition of M along a complete orthogonal system of idempotents, M ≃ ∏ᵢ M ⧸ (1 - eᵢ)M.

Equations

• CompleteOrthogonalIdempotents.linearEquivPiQuotSMulTop M e he = LinearEquiv.ofBijective (piQuotSMulTop M e) ⋯

@[simp]

theorem CompleteOrthogonalIdempotents.linearEquivPiQuotSMulTop_apply {R : Type u} [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] {I : Type w} [Fintype I] {e : I → R} (he : CompleteOrthogonalIdempotents e) (x : M) (i : I) : (linearEquivPiQuotSMulTop M e he) x i = Submodule.Quotient.mk x

noncomputable def CompleteOrthogonalIdempotents.linearEquivPiQuotientTensor {R : Type u} [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] {I : Type w} [Fintype I] (e : I → R) (he : CompleteOrthogonalIdempotents e) : M ≃ₗ[R] (i : I) → TensorProduct R (R ⧸ Ideal.span {1 - e i}) M

The decomposition of M with the factors written as base changes, M ≃ ∏ᵢ (R ⧸ (1 - eᵢ)) ⊗[R] M. This is the form in which each factor is a module over the corresponding factor ring of R.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompleteOrthogonalIdempotents.linearEquivPiQuotientTensor_apply {R : Type u} [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] {I : Type w} [Fintype I] {e : I → R} (he : CompleteOrthogonalIdempotents e) (x : M) (i : I) : (linearEquivPiQuotientTensor M e he) x i = 1 ⊗ₜ[R] x

The tensor-product module decomposition sends an element to its pure-tensor image in each idempotent factor.