The Krull-Schmidt theorem for external direct sums

TauCeti.exists_indecomposable_decomposition and TauCeti.exists_equiv_linearEquiv_of_iSupIndep state the two halves of the Krull-Schmidt theorem for families of submodules of one fixed module. A client that starts from an external decomposition M ≃ₗ[A] ⨁ i, N i, with the summands N i abstract modules of their own, cannot apply them without first transporting every summand into the submodule lattice of M and rebuilding the independence data by hand. This file does that transport once and restates both halves against external direct sums.

Main results

• TauCeti.exists_iSupIndep_linearEquiv_of_directSum: an external decomposition M ≃ₗ[A] ⨁ i, N i induces an internal one, a family of submodules of M that is iSupIndep, spans M, and whose i-th member is isomorphic to N i. This is the transport the two theorems below run on, and it is stated separately because it is what a client needs in order to reach any other statement about internal decompositions.
• TauCeti.IsIndecomposableModule.exists_nonempty_linearEquiv_of_directSum: an indecomposable module isomorphic to ⨁ i, N i is isomorphic to one of the summands N i.
• TauCeti.exists_linearEquiv_directSum_isIndecomposableModule: existence, externally: an Artinian module is isomorphic to a direct sum of indecomposable modules.
• TauCeti.exists_equiv_linearEquiv_of_directSum: the Krull-Schmidt theorem, externally: two decompositions M ≃ₗ[A] ⨁ i, N i and M ≃ₗ[A] ⨁ j, Q j of a module of finite length into indecomposable summands are matched by a bijection ι ≃ κ under which corresponding summands are isomorphic, with TauCeti.exists_equiv_linearEquiv_of_directSum_of_isLocalRing_end in Azumaya's generality and TauCeti.card_eq_card_of_directSum for the number of summands.
• TauCeti.exists_equiv_linearEquiv_of_directSumEquiv: the same for two abstract families of summands compared by an isomorphism (⨁ i, N i) ≃ₗ[A] ⨁ j, Q j, with no ambient module.

Implementation notes

The transport goes through LinearMap.range (DirectSum.lof A ι N i), the copy of N i inside ⨁ i, N i. That these ranges span is Mathlib's DFinsupp.iSup_range_lsingle, DirectSum.lof being by definition DFinsupp.lsingle; that they are independent is the one private lemma below, read off the components. Their images under e.symm are the internal decomposition of M, independent by LinearMap.iSupIndep_map. The transport is stated existentially rather than as a named family of submodules, so that DecidableEq ι — which DirectSum.lof needs but no statement here does — can be produced by classical inside the proof instead of appearing as a hypothesis. This matches the choice made in TauCeti/RingTheory/KrullSchmidt/Uniqueness.lean to spell decompositions as iSupIndep together with ⨆ i, P i = ⊤ rather than as DirectSum.IsInternal.

Comparing two abstract families N and Q directly, with no ambient module, is the case M := ⨁ i, N i, taking the first equivalence to be LinearEquiv.refl; that is TauCeti.exists_equiv_linearEquiv_of_directSumEquiv. The statements are given with an ambient M rather than only in that special case because the finiteness hypothesis is then read on the direct sum itself, which is not where a client holds it.

The transport lemmas need no subtraction, so they are stated for a semimodule over a semiring; the decomposition theorems are over a ring, which is the generality of the internal statements they consume.

References

This supplies the external interface to Layer 2 ("the Krull-Schmidt theorem") of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md, whose uniqueness bullet asks for the theorem to be proved "at the module level with submodules and linear equivalences", then transported.

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

An external decomposition induces an internal one

theorem TauCeti.exists_iSupIndep_linearEquiv_of_directSum {A : Type u} [Semiring A] {M : Type v} [AddCommMonoid M] [Module A M] {ι : Type w} {N : ι → Type y} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module A (N i)] (e : M ≃ₗ[A] DirectSum ι fun (i : ι) => N i) : ∃ (P : ι → Submodule A M), iSupIndep P ∧ ⨆ (i : ι), P i = ⊤ ∧ ∀ (i : ι), Nonempty (N i ≃ₗ[A] ↥(P i))

An external direct-sum decomposition induces an internal one. An isomorphism M ≃ₗ[A] ⨁ i, N i carries the copies of the summands to a family of submodules of M that is independent, spans M, and reproduces the N i up to isomorphism.

This is the transport that lets the internal statements of the Krull-Schmidt theorem be applied to an external decomposition; TauCeti.exists_equiv_linearEquiv_of_directSum is that application.

theorem TauCeti.IsIndecomposableModule.exists_nonempty_linearEquiv_of_directSum {A : Type u} [Semiring A] {M : Type v} [AddCommMonoid M] [Module A M] {ι : Type w} {N : ι → Type y} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module A (N i)] (h : IsIndecomposableModule A M) (e : M ≃ₗ[A] DirectSum ι fun (i : ι) => N i) : ∃ (i : ι), Nonempty (M ≃ₗ[A] N i)

An indecomposable direct sum has a single summand: a module isomorphic to ⨁ i, N i that is indecomposable is isomorphic to one of the N i, namely to the unique nonzero summand.

The two halves of the Krull-Schmidt theorem, externally

theorem TauCeti.exists_linearEquiv_directSum_isIndecomposableModule {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] [IsArtinian A M] : ∃ (s : Finset (Submodule A M)), (∀ N ∈ s, IsIndecomposableModule A ↥N) ∧ Nonempty (M ≃ₗ[A] DirectSum ↥s fun (N : ↥s) => ↥↑N)

Existence of an indecomposable decomposition, externally: an Artinian module — in particular one of finite length — is isomorphic to the direct sum of a finite family of indecomposable modules.

The summands are produced as submodules of M, by TauCeti.exists_isInternal_isIndecomposableModule; the point of this form is that the conclusion is a linear equivalence with a direct sum, which is what TauCeti.exists_equiv_linearEquiv_of_directSum consumes.

theorem TauCeti.exists_equiv_linearEquiv_of_directSum_of_isLocalRing_end {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {ι : Type w} {κ : Type x} [Finite ι] [Finite κ] {N : ι → Type y} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module A (N i)] {Q : κ → Type z} [(j : κ) → AddCommGroup (Q j)] [(j : κ) → Module A (Q j)] (eN : M ≃ₗ[A] DirectSum ι fun (i : ι) => N i) (eQ : M ≃ₗ[A] DirectSum κ fun (j : κ) => Q j) (hN : ∀ (i : ι), IsLocalRing (Module.End A (N i))) (hQ : ∀ (j : κ), IsIndecomposableModule A (Q j)) : ∃ (e : ι ≃ κ), ∀ (i : ι), Nonempty (N i ≃ₗ[A] Q (e i))

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

No finiteness hypothesis on M is needed; for a module of finite length Fitting's lemma supplies the locality hypothesis, which is TauCeti.exists_equiv_linearEquiv_of_directSum below.

theorem TauCeti.exists_equiv_linearEquiv_of_directSumEquiv {A : Type u} [Ring A] {ι : Type w} {κ : Type x} [Finite ι] [Finite κ] {N : ι → Type y} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module A (N i)] {Q : κ → Type z} [(j : κ) → AddCommGroup (Q j)] [(j : κ) → Module A (Q j)] (e : (DirectSum ι fun (i : ι) => N i) ≃ₗ[A] DirectSum κ fun (j : κ) => Q j) (hN : ∀ (i : ι), IsLocalRing (Module.End A (N i))) (hQ : ∀ (j : κ), IsIndecomposableModule A (Q j)) : ∃ (f : ι ≃ κ), ∀ (i : ι), Nonempty (N i ≃ₗ[A] Q (f i))

The Krull-Schmidt theorem for two abstract families of summands: a direct sum of modules with local endomorphism rings that is isomorphic to a direct sum of indecomposable modules has its summands matched by a bijection of the index sets.

This is TauCeti.exists_equiv_linearEquiv_of_directSum_of_isLocalRing_end with the ambient module taken to be the first direct sum; it is the form to use when no ambient module is in play.

theorem TauCeti.exists_equiv_linearEquiv_of_directSum {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {ι : Type w} {κ : Type x} [Finite ι] [Finite κ] {N : ι → Type y} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module A (N i)] {Q : κ → Type z} [(j : κ) → AddCommGroup (Q j)] [(j : κ) → Module A (Q j)] [IsNoetherian A M] [IsArtinian A M] (eN : M ≃ₗ[A] DirectSum ι fun (i : ι) => N i) (eQ : M ≃ₗ[A] DirectSum κ fun (j : κ) => Q j) (hN : ∀ (i : ι), IsIndecomposableModule A (N i)) (hQ : ∀ (j : κ), IsIndecomposableModule A (Q j)) : ∃ (e : ι ≃ κ), ∀ (i : ι), Nonempty (N i ≃ₗ[A] Q (e i))

The Krull-Schmidt theorem for external direct sums. Two decompositions of a module of finite length as a direct sum of indecomposable modules are matched by a bijection of their index sets under which corresponding summands are isomorphic.

TauCeti.exists_linearEquiv_directSum_isIndecomposableModule supplies such a decomposition, and TauCeti.exists_equiv_linearEquiv_of_iSupIndep is the same statement for families of submodules of M.

theorem TauCeti.card_eq_card_of_directSum {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {ι : Type w} {κ : Type x} [Finite ι] [Finite κ] {N : ι → Type y} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module A (N i)] {Q : κ → Type z} [(j : κ) → AddCommGroup (Q j)] [(j : κ) → Module A (Q j)] [IsNoetherian A M] [IsArtinian A M] (eN : M ≃ₗ[A] DirectSum ι fun (i : ι) => N i) (eQ : M ≃ₗ[A] DirectSum κ fun (j : κ) => Q j) (hN : ∀ (i : ι), IsIndecomposableModule A (N i)) (hQ : ∀ (j : κ), IsIndecomposableModule A (Q j)) : Nat.card ι = Nat.card κ

Two decompositions of a module of finite length as a direct sum of indecomposable modules have the same number of summands.