Krull-Schmidt multiplicities of an indecomposable module

A module of finite length is an internal direct sum of finitely many indecomposable submodules, and the Krull-Schmidt theorem matches any two such decompositions summand by summand. Counting how often a fixed module N occurs among the summands is therefore an invariant of the module alone: the multiplicity of N in M. This file builds that count.

It is the direct-sum analogue of the Jordan-Hölder count TauCeti.jordanHolderMultiplicity, and is well defined for the same reason: the existence theorem TauCeti.exists_isInternal_isIndecomposableModule produces a decomposition, and the uniqueness theorem TauCeti.exists_equiv_linearEquiv_of_finset matches any two of them by a bijection under which corresponding summands are isomorphic, so the two counts agree.

The count is taken with Nat.card, over the subtype of members of the decomposition that are copies of N, so no decidability of "is a copy of N" is needed in the definition.

Multiplicity is additive on direct sums, which is what makes it a coordinate on a Grothendieck group of modules: the classes of the indecomposable modules are independent because their multiplicities are the Kronecker delta.

Main definitions

• TauCeti.decompositionMultiplicity: the number of members of a finite set of submodules that are copies of a given module.
• TauCeti.indecomposableMultiplicity: the multiplicity of a module N among the indecomposable summands of a module M of finite length.

Main results

• TauCeti.decompositionMultiplicity_eq_of_isInternal: the count is a Krull-Schmidt invariant — two indecomposable decompositions contain the same number of copies of every module. This is what makes TauCeti.indecomposableMultiplicity well defined, and TauCeti.decompositionMultiplicity_eq_indecomposableMultiplicity says that every indecomposable decomposition computes it.
• TauCeti.indecomposableMultiplicity_eq_of_linearEquiv and TauCeti.indecomposableMultiplicity_congr: the multiplicity depends on each of the two modules only through its isomorphism class.
• TauCeti.isIndecomposableModule_of_indecomposableMultiplicity_ne_zero: only an indecomposable module occurs, and TauCeti.indecomposableMultiplicity_self and TauCeti.indecomposableMultiplicity_eq_zero_of_isEmpty_linearEquiv: an indecomposable module occurs exactly once in itself and not at all in a nonisomorphic indecomposable module. TauCeti.indecomposableMultiplicity_eq_ite reads the last two as a Kronecker delta on a pairwise nonisomorphic indecomposable family.
• TauCeti.indecomposableMultiplicity_prod: multiplicity is additive on direct sums, with TauCeti.indecomposableMultiplicity_eq_add_of_isCompl the internal form.

References

• Ibrahim Assem, Daniel Simson, and Andrzej Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter I, Section 4.

Counting the copies of a module in a finite set of submodules

noncomputable def TauCeti.decompositionMultiplicity {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] (s : Finset (Submodule A M)) (N : Type w) [AddCommGroup N] [Module A N] : ℕ

The number of members of the finite set of submodules s that are copies of N. When s is a decomposition of M into indecomposable submodules this is the multiplicity of N in M, by TauCeti.decompositionMultiplicity_eq_indecomposableMultiplicity.

Equations

• TauCeti.decompositionMultiplicity s N = Nat.card { P : Submodule A M // P ∈ s ∧ Nonempty (↥P ≃ₗ[A] N) }

theorem TauCeti.decompositionMultiplicity_def {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (s : Finset (Submodule A M)) : decompositionMultiplicity s N = Nat.card { P : Submodule A M // P ∈ s ∧ Nonempty (↥P ≃ₗ[A] N) }

The defining equation of TauCeti.decompositionMultiplicity: it is the number of members of s admitting a linear equivalence with N. This is what introduces and eliminates the count, whose body is not exposed to importing modules.

theorem TauCeti.decompositionMultiplicity_eq_card_filter {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] (s : Finset (Submodule A M)) (N : Type w) [AddCommGroup N] [Module A N] [DecidablePred fun (P : Submodule A M) => Nonempty (↥P ≃ₗ[A] N)] : decompositionMultiplicity s N = {P ∈ s | Nonempty (↥P ≃ₗ[A] N)}.card

The count, as the cardinality of the corresponding Finset.filter. The definition itself is taken with Nat.card over a subtype, so that it needs no decidability hypothesis; this is the form in which the counting arguments run.

theorem TauCeti.decompositionMultiplicity_congr {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] {N' : Type w'} [AddCommGroup N'] [Module A N'] (s : Finset (Submodule A M)) (e : N ≃ₗ[A] N') : decompositionMultiplicity s N = decompositionMultiplicity s N'

The count depends on N only through its isomorphism class.

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

The count is a Krull-Schmidt invariant: two decompositions of a module of finite length into indecomposable submodules contain the same number of copies of every module.

theorem TauCeti.decompositionMultiplicity_union {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] [DecidableEq (Submodule A M)] {s t : Finset (Submodule A M)} (hst : Disjoint s t) : decompositionMultiplicity (s ∪ t) N = decompositionMultiplicity s N + decompositionMultiplicity t N

The counts over two disjoint finite sets of submodules add.

Transport along an injective linear map

theorem TauCeti.decompositionMultiplicity_image {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {M' : Type v'} [AddCommGroup M'] [Module A M'] {N : Type w} [AddCommGroup N] [Module A N] [DecidableEq (Submodule A M')] {f : M →ₗ[A] M'} (hf : Function.Injective ⇑f) (s : Finset (Submodule A M)) : decompositionMultiplicity (Finset.image (Submodule.map f) s) N = decompositionMultiplicity s N

Pushing a finite set of submodules forward along an injective linear map does not change how many of its members are copies of N.

The multiplicity of an indecomposable module

noncomputable def TauCeti.indecomposableMultiplicity (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] [IsArtinian A M] (N : Type w) [AddCommGroup N] [Module A N] : ℕ

The multiplicity of N in M: the number of copies of N among the summands of a decomposition of the finite-length module M into indecomposable submodules. Every such decomposition computes it, by TauCeti.decompositionMultiplicity_eq_indecomposableMultiplicity.

Equations

• TauCeti.indecomposableMultiplicity A M N = TauCeti.decompositionMultiplicity ⋯.choose N

theorem TauCeti.decompositionMultiplicity_eq_indecomposableMultiplicity {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] [IsNoetherian A M] [IsArtinian A M] {s : Finset (Submodule A M)} (hs : ∀ P ∈ s, IsIndecomposableModule A ↥P) (hsi : DirectSum.IsInternal fun (P : ↥s) => ↑P) : decompositionMultiplicity s N = indecomposableMultiplicity A M N

Every indecomposable decomposition computes the multiplicity.

theorem TauCeti.decompositionMultiplicity_eq_indecomposableMultiplicity_of_supIndep {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] [IsNoetherian A M] [IsArtinian A M] {s : Finset (Submodule A M)} (hs : ∀ P ∈ s, IsIndecomposableModule A ↥P) (hsi : s.SupIndep id) (hsup : s.sup id = ⊤) : decompositionMultiplicity s N = indecomposableMultiplicity A M N

An independent, spanning finite set of indecomposable submodules computes the multiplicity. This is TauCeti.decompositionMultiplicity_eq_indecomposableMultiplicity in the packaging that TauCeti.exists_finset_isIndecomposableModule_supIndep_sup_eq produces.

theorem TauCeti.indecomposableMultiplicity_congr {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] {N' : Type w'} [AddCommGroup N'] [Module A N'] [IsArtinian A M] (e : N ≃ₗ[A] N') : indecomposableMultiplicity A M N = indecomposableMultiplicity A M N'

The multiplicity depends on N only through its isomorphism class.

theorem TauCeti.indecomposableMultiplicity_eq_of_linearEquiv {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {M' : Type v'} [AddCommGroup M'] [Module A M'] {N : Type w} [AddCommGroup N] [Module A N] [IsNoetherian A M] [IsArtinian A M] (f : M ≃ₗ[A] M') : indecomposableMultiplicity A M N = indecomposableMultiplicity A M' N

The multiplicity depends on the ambient module only through its isomorphism class.

@[simp]

theorem TauCeti.indecomposableMultiplicity_eq_zero_of_subsingleton {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] [IsArtinian A M] [Subsingleton M] : indecomposableMultiplicity A M N = 0

A zero module has no indecomposable summands.

theorem TauCeti.isIndecomposableModule_of_indecomposableMultiplicity_ne_zero {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] [IsArtinian A M] (h : indecomposableMultiplicity A M N ≠ 0) : IsIndecomposableModule A N

Only an indecomposable module has a nonzero multiplicity: the summands counted are indecomposable by construction.

@[simp]

theorem TauCeti.indecomposableMultiplicity_eq_zero_of_not_isIndecomposableModule {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] [IsArtinian A M] (hN : ¬IsIndecomposableModule A N) : indecomposableMultiplicity A M N = 0

A non-indecomposable module has zero multiplicity in every Artinian module.

theorem TauCeti.indecomposableMultiplicity_self {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] [IsArtinian A M] (hM : IsIndecomposableModule A M) (e : M ≃ₗ[A] N) : indecomposableMultiplicity A M N = 1

An indecomposable module occurs exactly once in itself.

theorem TauCeti.indecomposableMultiplicity_eq_zero_of_isEmpty_linearEquiv {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] [IsArtinian A M] (hM : IsIndecomposableModule A M) (he : IsEmpty (M ≃ₗ[A] N)) : indecomposableMultiplicity A M N = 0

A nonisomorphic module does not occur in an indecomposable module.

@[simp]

theorem TauCeti.indecomposableMultiplicity_eq_ite {A : Type u} [Ring A] {I : Type u_1} [DecidableEq I] {P : I → Type w} [(i : I) → AddCommGroup (P i)] [(i : I) → Module A (P i)] [∀ (i : I), IsArtinian A (P i)] (hind : ∀ (i : I), IsIndecomposableModule A (P i)) (hnoniso : Pairwise fun (i j : I) => IsEmpty (P i ≃ₗ[A] P j)) (i j : I) : indecomposableMultiplicity A (P j) (P i) = if j = i then 1 else 0

The multiplicities inside a pairwise nonisomorphic indecomposable family are the Kronecker delta: a member occurs once in itself and not at all in any other member.

Additivity

@[simp]

theorem TauCeti.indecomposableMultiplicity_prod {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {M' : Type v'} [AddCommGroup M'] [Module A M'] {N : Type w} [AddCommGroup N] [Module A N] [IsNoetherian A M] [IsArtinian A M] [IsNoetherian A M'] [IsArtinian A M'] : indecomposableMultiplicity A (M × M') N = indecomposableMultiplicity A M N + indecomposableMultiplicity A M' N

Multiplicity is additive on direct sums.

theorem TauCeti.indecomposableMultiplicity_eq_add_of_isCompl {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] [IsNoetherian A M] [IsArtinian A M] {T T' : Submodule A M} (h : IsCompl T T') : indecomposableMultiplicity A M N = indecomposableMultiplicity A (↥T) N + indecomposableMultiplicity A (↥T') N

Multiplicity is additive on an internal direct sum decomposition into two summands.

theorem TauCeti.indecomposableMultiplicity_eq_add_of_exact_of_rightInverse {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] [IsNoetherian A M] [IsArtinian A M] {M₁ : Type u_1} [AddCommGroup M₁] [Module A M₁] [IsNoetherian A M₁] [IsArtinian A M₁] {M₃ : Type u_2} [AddCommGroup M₃] [Module A M₃] [IsNoetherian A M₃] [IsArtinian A M₃] {f : M₁ →ₗ[A] M} {g : M →ₗ[A] M₃} {σ : M₃ →ₗ[A] M} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (hσ : Function.LeftInverse ⇑g ⇑σ) : indecomposableMultiplicity A M N = indecomposableMultiplicity A M₁ N + indecomposableMultiplicity A M₃ N

Multiplicity is additive on a split short exact sequence 0 → M₁ → M → M₃ → 0, the splitting being given by a right inverse σ of the surjection.