The Krull-Schmidt theorem

TauCeti.exists_indecomposable_decomposition writes a module of finite length as an internal direct sum of indecomposable submodules. This file proves that the decomposition is unique: any two of them have the same number of summands, matched up to isomorphism by a bijection of the index sets.

The proof is the exchange induction. Given decompositions ⨆ i, P i = ⊤ = ⨆ j, Q j, pick an index i₀. The summand P i₀ is an indecomposable direct summand of M, so Azumaya's exchange lemma TauCeti.exists_linearEquiv_and_isCompl_biSup_ne produces a j₀ with P i₀ ≃ₗ Q j₀ and with M the direct sum of P i₀ and ⨆ j ≠ j₀, Q j. Both ⨆ i ≠ i₀, P i and ⨆ j ≠ j₀, Q j are then complements of P i₀, hence isomorphic; transporting the first decomposition along that isomorphism gives two decompositions of one module with one fewer summand, and the induction closes.

What the induction asks of the first decomposition is only that each Module.End A (P i) is local, which is all the exchange lemma consumes, so that is how the theorem is stated; finite length enters only through Fitting's lemma TauCeti.isLocalRing_end_of_isIndecomposable, in the corollaries.

Main results

• TauCeti.exists_equiv_linearEquiv_of_isLocalRing_end: the Krull-Schmidt theorem in Azumaya's generality, for a first family whose summands have local endomorphism rings and a second family of indecomposable summands.
• TauCeti.exists_equiv_linearEquiv_of_iSupIndep: the same for two families of indecomposable submodules of a module of finite length, indexed by finite types.
• TauCeti.exists_equiv_linearEquiv_of_finset: the same in the Finset and DirectSum.IsInternal packaging produced by TauCeti.exists_indecomposable_decomposition.
• TauCeti.card_eq_card_of_iSupIndep and TauCeti.card_eq_card_of_finset: in particular the two decompositions have the same number of summands.

Implementation notes

The decompositions are spelled as iSupIndep together with ⨆ i, P i = ⊤ rather than as DirectSum.IsInternal, which carries a DecidableEq hypothesis on the index type that the statement does not need; the two are interchanged inside the proofs by DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, and the Finset results are stated in the DirectSum.IsInternal form because that is what TauCeti.exists_indecomposable_decomposition produces. The finiteness of M is carried as the instance pair [IsNoetherian A M] [IsArtinian A M] on the results indexed by a type, and in the IsFiniteLength A M spelling on the Finset results.

The induction is on Nat.card of the first index type, and it changes the ambient module: the recursive call is made on ↥(⨆ j ≠ j₀, Q j). That is why it is packaged as a private auxiliary statement quantifying over the module as well, rather than run inside the theorem below. Restricting a decomposition to the submodule it spans is Mathlib's DirectSum.isInternal_biSup_submodule_of_iSupIndep; transporting one along a linear equivalence is Mathlib's LinearMap.iSupIndep_map together with the private helper below, and transporting locality of an endomorphism ring along one is TauCeti.IsLocalRing.of_ringEquiv applied to Mathlib's LinearEquiv.conjRingEquiv.

References

This implements the uniqueness bullet of Layer 2 ("the Krull-Schmidt theorem") of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md.

See I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.4.

Transporting a decomposition along a linear equivalence

The exchange induction

The Krull-Schmidt theorem

theorem TauCeti.exists_equiv_linearEquiv_of_isLocalRing_end {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {ι : Type w} {κ : Type x} [Finite ι] [Finite κ] {P : ι → Submodule A M} {Q : κ → Submodule A M} (hP : iSupIndep P) (hPt : ⨆ (i : ι), P i = ⊤) (hPloc : ∀ (i : ι), IsLocalRing (Module.End A ↥(P i))) (hQ : iSupIndep Q) (hQt : ⨆ (j : κ), Q j = ⊤) (hQind : ∀ (j : κ), IsIndecomposableModule A ↥(Q j)) : ∃ (e : ι ≃ κ), ∀ (i : ι), Nonempty (↥(P i) ≃ₗ[A] ↥(Q (e i)))

The Krull-Schmidt theorem, in Azumaya's generality: if a module is the internal direct sum of a finite family of submodules with local endomorphism rings, and also of a finite family of indecomposable submodules, then the two families are matched by a bijection of their index sets under which corresponding summands are isomorphic.

Each summand of the first family is automatically indecomposable, by TauCeti.isIndecomposableModule_of_isLocalRing_end; for a module of finite length the converse holds too, which is TauCeti.exists_equiv_linearEquiv_of_iSupIndep below.

theorem TauCeti.exists_equiv_linearEquiv_of_iSupIndep {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] [IsNoetherian A M] [IsArtinian A M] {ι : Type w} {κ : Type x} [Finite ι] [Finite κ] {P : ι → Submodule A M} {Q : κ → Submodule A M} (hP : iSupIndep P) (hPt : ⨆ (i : ι), P i = ⊤) (hPind : ∀ (i : ι), IsIndecomposableModule A ↥(P i)) (hQ : iSupIndep Q) (hQt : ⨆ (j : κ), Q j = ⊤) (hQind : ∀ (j : κ), IsIndecomposableModule A ↥(Q j)) : ∃ (e : ι ≃ κ), ∀ (i : ι), Nonempty (↥(P i) ≃ₗ[A] ↥(Q (e i)))

The Krull-Schmidt theorem. Two decompositions of a module of finite length into indecomposable submodules are matched by a bijection of their index sets under which corresponding summands are isomorphic.

Finite length enters only through Fitting's lemma, which makes the endomorphism ring of each summand local; TauCeti.exists_equiv_linearEquiv_of_isLocalRing_end is the statement that hypothesis is really needed for. Existence of such a decomposition is TauCeti.exists_indecomposable_decomposition.

theorem TauCeti.card_eq_card_of_iSupIndep {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] [IsNoetherian A M] [IsArtinian A M] {ι : Type w} {κ : Type x} [Finite ι] [Finite κ] {P : ι → Submodule A M} {Q : κ → Submodule A M} (hP : iSupIndep P) (hPt : ⨆ (i : ι), P i = ⊤) (hPind : ∀ (i : ι), IsIndecomposableModule A ↥(P i)) (hQ : iSupIndep Q) (hQt : ⨆ (j : κ), Q j = ⊤) (hQind : ∀ (j : κ), IsIndecomposableModule A ↥(Q j)) : Nat.card ι = Nat.card κ

Two decompositions of a module of finite length into indecomposable submodules have the same number of summands.

theorem TauCeti.exists_equiv_linearEquiv_of_finset {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] (hM : IsFiniteLength A M) {s t : Finset (Submodule A M)} (hs : ∀ N ∈ s, IsIndecomposableModule A ↥N) (hsi : DirectSum.IsInternal fun (N : ↥s) => ↑N) (ht : ∀ N ∈ t, IsIndecomposableModule A ↥N) (hti : DirectSum.IsInternal fun (N : ↥t) => ↑N) : ∃ (e : ↥s ≃ ↥t), ∀ (N : ↥s), Nonempty (↥↑N ≃ₗ[A] ↥↑(e N))

The Krull-Schmidt theorem, in the Finset packaging that TauCeti.exists_indecomposable_decomposition produces: two Finsets of indecomposable submodules each presenting the module as an internal direct sum are matched by a bijection under which corresponding summands are isomorphic.

theorem TauCeti.card_eq_card_of_finset {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] (hM : IsFiniteLength A M) {s t : Finset (Submodule A M)} (hs : ∀ N ∈ s, IsIndecomposableModule A ↥N) (hsi : DirectSum.IsInternal fun (N : ↥s) => ↑N) (ht : ∀ N ∈ t, IsIndecomposableModule A ↥N) (hti : DirectSum.IsInternal fun (N : ↥t) => ↑N) : s.card = t.card

Two indecomposable decompositions of a module of finite length, in the Finset packaging TauCeti.exists_indecomposable_decomposition produces, consist of the same number of summands.