The Krull-Schmidt theorem for biproducts in ModuleCat

TauCeti.exists_linearEquiv_directSum_isIndecomposableModule and TauCeti.exists_equiv_linearEquiv_of_directSum are the two halves of the Krull-Schmidt theorem in their external module form: a module of finite length is a direct sum ⨁ i, N i of indecomposable modules, and any two such direct-sum decompositions are matched by a bijection of their index sets under which corresponding summands are isomorphic. A client who works with representations meets the theorem in its categorical form instead, with CategoryTheory.Limits.biproduct in place of DirectSum and isomorphisms of objects in place of linear equivalences. This file restates both halves in that form for ModuleCat A.

The transport is TauCeti.biproductDirectSumEquiv, which identifies the carrier of a finite biproduct with the external direct sum of the carriers of the summands, together with TauCeti.indecomposable_iff_isIndecomposableModule, which carries indecomposability across.

Main results

• TauCeti.exists_indecomposable_iso_biproduct: existence, categorically: an Artinian object of ModuleCat A is isomorphic to a finite biproduct of indecomposable objects.
• TauCeti.exists_equiv_iso_of_iso_biproduct: the Krull-Schmidt theorem, categorically: two isomorphisms of an object of finite length with finite biproducts of indecomposable objects are matched by a bijection of the index sets under which corresponding summands are isomorphic.
• TauCeti.exists_equiv_iso_of_biproduct_iso: the same with no ambient object, for an isomorphism between two biproducts.
• TauCeti.card_eq_card_of_iso_biproduct and TauCeti.eq_of_iso_biproduct_fin: in particular the two decompositions have the same number of summands.
• TauCeti.card_iso_eq_card_iso_of_iso_biproduct: the number of summands isomorphic to a fixed object is the same in any two such decompositions, so the multiplicity of an indecomposable summand is an invariant.

Implementation notes

The index types are taken in Type, the generality of Mathlib's ModuleCat.biproductIsoPi, while the summands stay in the universe v of the ambient object; nothing is lost, because an index type of a finite biproduct can be replaced by Fin n, which is what the existence theorem produces.

References

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

The two halves of the Krull-Schmidt theorem, categorically

theorem TauCeti.exists_indecomposable_iso_biproduct {A : Type u} [Ring A] (X : ModuleCat A) [IsArtinian A ↑X] : ∃ (n : ℕ) (P : Fin n → ModuleCat A), (∀ (i : Fin n), CategoryTheory.Indecomposable (P i)) ∧ Nonempty (X ≅ ⨁ P)

Existence of an indecomposable decomposition, categorically: an Artinian object of ModuleCat A — in particular one of finite length — is isomorphic to a finite biproduct of indecomposable objects.

The index type is produced as Fin n, so the statement stays inside the index universe in which ModuleCat.biproductIsoPi, and hence TauCeti.biproductDirectSumEquiv, is available.

theorem TauCeti.exists_equiv_iso_of_iso_biproduct {A : Type u} [Ring A] {ι κ : Type} [Finite ι] [Finite κ] {P : ι → ModuleCat A} {Q : κ → ModuleCat A} {X : ModuleCat A} [IsNoetherian A ↑X] [IsArtinian A ↑X] (eP : X ≅ ⨁ P) (eQ : X ≅ ⨁ Q) (hP : ∀ (i : ι), CategoryTheory.Indecomposable (P i)) (hQ : ∀ (j : κ), CategoryTheory.Indecomposable (Q j)) : ∃ (e : ι ≃ κ), ∀ (i : ι), Nonempty (P i ≅ Q (e i))

The Krull-Schmidt theorem for biproducts in ModuleCat A. If an object of finite length is isomorphic to a finite biproduct of indecomposable objects in two ways, the two families of summands are matched by a bijection of their index sets under which corresponding summands are isomorphic.

TauCeti.exists_indecomposable_iso_biproduct supplies such an isomorphism, and TauCeti.exists_equiv_linearEquiv_of_directSum is the same statement for external direct sums of modules.

theorem TauCeti.exists_equiv_iso_of_biproduct_iso {A : Type u} [Ring A] {ι κ : Type} [Finite ι] [Finite κ] {P : ι → ModuleCat A} {Q : κ → ModuleCat A} [IsNoetherian A ↑(⨁ P)] [IsArtinian A ↑(⨁ P)] (e : ⨁ P ≅ ⨁ Q) (hP : ∀ (i : ι), CategoryTheory.Indecomposable (P i)) (hQ : ∀ (j : κ), CategoryTheory.Indecomposable (Q j)) : ∃ (f : ι ≃ κ), ∀ (i : ι), Nonempty (P i ≅ Q (f i))

The Krull-Schmidt theorem with no ambient object: an isomorphism between two finite biproducts of indecomposable objects of finite length matches their summands by a bijection of the index sets.

theorem TauCeti.card_eq_card_of_iso_biproduct {A : Type u} [Ring A] {ι κ : Type} [Finite ι] [Finite κ] {P : ι → ModuleCat A} {Q : κ → ModuleCat A} {X : ModuleCat A} [IsNoetherian A ↑X] [IsArtinian A ↑X] (eP : X ≅ ⨁ P) (eQ : X ≅ ⨁ Q) (hP : ∀ (i : ι), CategoryTheory.Indecomposable (P i)) (hQ : ∀ (j : κ), CategoryTheory.Indecomposable (Q j)) : Nat.card ι = Nat.card κ

Two decompositions of an object of finite length as a biproduct of indecomposable objects have the same number of summands.

theorem TauCeti.card_iso_eq_card_iso_of_iso_biproduct {A : Type u} [Ring A] {ι κ : Type} [Finite ι] [Finite κ] {P : ι → ModuleCat A} {Q : κ → ModuleCat A} {X : ModuleCat A} [IsNoetherian A ↑X] [IsArtinian A ↑X] (eP : X ≅ ⨁ P) (eQ : X ≅ ⨁ Q) (hP : ∀ (i : ι), CategoryTheory.Indecomposable (P i)) (hQ : ∀ (j : κ), CategoryTheory.Indecomposable (Q j)) (N : ModuleCat A) : Nat.card { i : ι // Nonempty (P i ≅ N) } = Nat.card { j : κ // Nonempty (Q j ≅ N) }

The multiplicity of an indecomposable summand is well defined: the number of summands isomorphic to a fixed object N is the same in any two indecomposable biproduct decompositions of an object of finite length. This is what makes "the indecomposable summands of X, with multiplicity" an invariant of X; TauCeti.indecomposableMultiplicity is the module-level counterpart.

theorem TauCeti.eq_of_iso_biproduct_fin {A : Type u} [Ring A] {X : ModuleCat A} [IsNoetherian A ↑X] [IsArtinian A ↑X] {m n : ℕ} {P : Fin m → ModuleCat A} {Q : Fin n → ModuleCat A} (eP : X ≅ ⨁ P) (eQ : X ≅ ⨁ Q) (hP : ∀ (i : Fin m), CategoryTheory.Indecomposable (P i)) (hQ : ∀ (j : Fin n), CategoryTheory.Indecomposable (Q j)) : m = n

The number of summands of an indecomposable biproduct decomposition of an object of finite length is well defined: two Fin-indexed decompositions have the same length. This is the form in which TauCeti.exists_indecomposable_iso_biproduct produces its decompositions.