Jordan-Hölder multiplicities of a simple module

A composition series of a module M cuts M into simple subquotients, its factors, and the Jordan-Hölder theorem says that two composition series with the same endpoints have the same factors up to a permutation. Counting how often a fixed simple module S occurs among them is therefore an invariant of M alone: the multiplicity [M : S] of S in M. This file builds that count.

Mathlib has everything the construction rests on and nothing built on it: the Jordan-Hölder theorem CompositionSeries.jordan_holder in the abstract lattice form, the recognition isFiniteLength_iff_exists_compositionSeries of the modules that admit a composition series from ⊥ to ⊤, the identification JordanHolderLattice.Iso.linearEquiv of the abstract interval isomorphism with a linear equivalence of subquotients, and Module.length, which records only the number of factors — and, with it, Module.length_compositionSeries, which is what pins down the length of a composition series of a subsingleton or a simple module below. The multiplicity of an individual simple module is not there.

The count is taken with Nat.card, over the subtype of indices whose factor is a copy of S, so no decidability of "is a copy of S" is needed. The factor at an index i is spelled out as the subquotient ↥(s i.succ) ⧸ Submodule.comap (s i.succ).subtype (s i.castSucc), in the exact form that JordanHolderLattice.Iso.linearEquiv produces, rather than being wrapped in a definition of its own; that keeps the interface between this file and Mathlib's Jordan-Hölder machinery a definitional identity.

Main definitions

• TauCeti.IsCompositionFactorAt: the factor of a composition series at an index is a copy of a given module.
• TauCeti.compositionMultiplicity: the number of indices of a composition series whose factor is a copy of a given module.
• TauCeti.jordanHolderMultiplicity: the multiplicity [M : S], the same count for a composition series of M running from ⊥ to ⊤.

Main results

• TauCeti.compositionMultiplicity_eq_of_head_eq_of_last_eq: the multiplicity is a Jordan-Hölder invariant — two composition series with the same endpoints count every module the same number of times. This is what makes TauCeti.jordanHolderMultiplicity well defined, and TauCeti.compositionMultiplicity_eq_jordanHolderMultiplicity says that every composition series from ⊥ to ⊤ computes it.
• TauCeti.IsCompositionFactorAt.isSimpleModule: the factors are simple, so the multiplicity of a module that is not simple vanishes (TauCeti.jordanHolderMultiplicity_eq_zero_of_not_isSimpleModule).
• TauCeti.jordanHolderMultiplicity_eq_of_linearEquiv: the multiplicity is an invariant of the isomorphism class of the ambient module, which is what makes [Pᵢ : Sⱼ] well posed for a projective cover, an object defined only up to isomorphism. The transport of a composition series along an injective or a surjective linear map that this rests on is TauCeti.RingTheory.CompositionSeries.Basic.
• TauCeti.jordanHolderMultiplicity_eq_one_of_isSimpleModule_of_linearEquiv and TauCeti.jordanHolderMultiplicity_eq_zero_of_isEmpty_linearEquiv_of_isSimpleModule: a simple module contains itself once and nothing else, the anti-vacuity check on the count.
• TauCeti.jordanHolderMultiplicity_congr: the multiplicity depends on S only through its isomorphism class.

References

The Jordan-Hölder multiplicities [Pᵢ : Sⱼ] are what the Cartan matrix of a finite-dimensional algebra is defined by, in Layer 3 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md ("The Cartan matrix of an algebra", "defined primarily by the Jordan-Hölder multiplicities Cᵢⱼ = [Pᵢ : Sⱼ] of Sⱼ in the projective cover Pᵢ, well-defined by Jordan-Hölder"); this file supplies that multiplicity and its well-definedness.

• Assem, Simson and Skowroński, Elements of the Representation Theory of Associative Algebras I, §I.4 and §III.3.

The factors of a composition series

def TauCeti.IsCompositionFactorAt {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (s : CompositionSeries (Submodule R M)) (i : Fin s.length) (S : Type w) [AddCommGroup S] [Module R S] : Prop

The factor of the composition series s at the index i is a copy of S: the subquotient s i.succ / s i.castSucc is linearly equivalent to S.

Equations

• TauCeti.IsCompositionFactorAt s i S = Nonempty ((↥(s.toFun i.succ) ⧸ Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc)) ≃ₗ[R] S)

theorem TauCeti.isCompositionFactorAt_iff {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {s : CompositionSeries (Submodule R M)} {i : Fin s.length} {S : Type w} [AddCommGroup S] [Module R S] : IsCompositionFactorAt s i S ↔ Nonempty ((↥(s.toFun i.succ) ⧸ Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc)) ≃ₗ[R] S)

The defining property of TauCeti.IsCompositionFactorAt: it is the existence of a linear equivalence between the subquotient at the index and the given module. This is what introduces and eliminates the predicate.

theorem TauCeti.IsCompositionFactorAt.congr {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {s : CompositionSeries (Submodule R M)} {i : Fin s.length} {S : Type w} [AddCommGroup S] [Module R S] {T : Type w'} [AddCommGroup T] [Module R T] (h : IsCompositionFactorAt s i S) (e : S ≃ₗ[R] T) : IsCompositionFactorAt s i T

Being a factor at a given index only depends on the isomorphism class of the module.

theorem TauCeti.isCompositionFactorAt_congr {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {s : CompositionSeries (Submodule R M)} {i : Fin s.length} {S : Type w} [AddCommGroup S] [Module R S] {T : Type w'} [AddCommGroup T] [Module R T] (e : S ≃ₗ[R] T) : IsCompositionFactorAt s i S ↔ IsCompositionFactorAt s i T

Being a factor at a given index only depends on the isomorphism class of the module.

theorem TauCeti.isCompositionFactorAt_congr_of_eq {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {S : Type w} [AddCommGroup S] [Module R S] {s t : CompositionSeries (Submodule R M)} {i : Fin s.length} {j : Fin t.length} (hsucc : s.toFun i.succ = t.toFun j.succ) (hcast : s.toFun i.castSucc = t.toFun j.castSucc) : IsCompositionFactorAt s i S ↔ IsCompositionFactorAt t j S

Two composition series with the same two submodules at an index have the same factor there. The equalities are enough: the subquotient is built from the two submodules alone.

theorem TauCeti.isSimpleModule_subquotient {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (s : CompositionSeries (Submodule R M)) (i : Fin s.length) : IsSimpleModule R (↥(s.toFun i.succ) ⧸ Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc))

The factors of a composition series are simple: each step of a composition series is a covering, and a covering pair of submodules has simple quotient.

theorem TauCeti.IsCompositionFactorAt.isSimpleModule {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {s : CompositionSeries (Submodule R M)} {i : Fin s.length} {S : Type w} [AddCommGroup S] [Module R S] (h : IsCompositionFactorAt s i S) : IsSimpleModule R S

A module that occurs as a factor of a composition series is simple.

The multiplicity along a fixed composition series

noncomputable def TauCeti.compositionMultiplicity {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (s : CompositionSeries (Submodule R M)) (S : Type w) [AddCommGroup S] [Module R S] : ℕ

The number of indices at which the composition series s has a factor isomorphic to S.

Equations

• TauCeti.compositionMultiplicity s S = Nat.card { i : Fin s.length // TauCeti.IsCompositionFactorAt s i S }

theorem TauCeti.compositionMultiplicity_def {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (s : CompositionSeries (Submodule R M)) (S : Type w) [AddCommGroup S] [Module R S] : compositionMultiplicity s S = Nat.card { i : Fin s.length // IsCompositionFactorAt s i S }

The defining formula for TauCeti.compositionMultiplicity, so that it can be evaluated on a concrete composition series.

theorem TauCeti.compositionMultiplicity_eq_sum_ite {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (s : CompositionSeries (Submodule R M)) (S : Type w) [AddCommGroup S] [Module R S] [(i : Fin s.length) → Decidable (IsCompositionFactorAt s i S)] : compositionMultiplicity s S = ∑ i : Fin s.length, if IsCompositionFactorAt s i S then 1 else 0

The multiplicity along a fixed composition series as a sum of indicators, the form in which it splits along a decomposition of the index set.

theorem TauCeti.compositionMultiplicity_ne_zero_iff {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (s : CompositionSeries (Submodule R M)) (S : Type w) [AddCommGroup S] [Module R S] : compositionMultiplicity s S ≠ 0 ↔ ∃ (i : Fin s.length), IsCompositionFactorAt s i S

S occurs in s — the multiplicity is nonzero — exactly when some index carries a copy of S.

theorem TauCeti.compositionMultiplicity_le_length {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (s : CompositionSeries (Submodule R M)) (S : Type w) [AddCommGroup S] [Module R S] : compositionMultiplicity s S ≤ s.length

theorem TauCeti.compositionMultiplicity_eq_zero_of_not_isSimpleModule {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (s : CompositionSeries (Submodule R M)) (S : Type w) [AddCommGroup S] [Module R S] (hS : ¬IsSimpleModule R S) : compositionMultiplicity s S = 0

Only simple modules occur as factors, so everything else has multiplicity zero.

theorem TauCeti.compositionMultiplicity_congr {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {S : Type w} [AddCommGroup S] [Module R S] {T : Type w'} [AddCommGroup T] [Module R T] (s : CompositionSeries (Submodule R M)) (e : S ≃ₗ[R] T) : compositionMultiplicity s S = compositionMultiplicity s T

The multiplicity along a fixed composition series depends on S only through its isomorphism class.

theorem TauCeti.compositionMultiplicity_eq_of_equivalent {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {s₁ s₂ : CompositionSeries (Submodule R M)} (h : s₁.Equivalent s₂) (S : Type w) [AddCommGroup S] [Module R S] : compositionMultiplicity s₁ S = compositionMultiplicity s₂ S

Equivalent composition series have the same multiplicities. The bijection of indices underlying the equivalence matches the factors up to isomorphism, so it restricts to a bijection between the indices carrying a copy of S.

theorem TauCeti.compositionMultiplicity_eq_of_head_eq_of_last_eq {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {s₁ s₂ : CompositionSeries (Submodule R M)} (hhead : RelSeries.head s₁ = RelSeries.head s₂) (hlast : RelSeries.last s₁ = RelSeries.last s₂) (S : Type w) [AddCommGroup S] [Module R S] : compositionMultiplicity s₁ S = compositionMultiplicity s₂ S

The multiplicity is a Jordan-Hölder invariant. Two composition series with the same first and last term count every module the same number of times.

The multiplicity of a simple module in a module of finite length

noncomputable def TauCeti.jordanHolderMultiplicity (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [IsNoetherian R M] [IsArtinian R M] (S : Type w) [AddCommGroup S] [Module R S] : ℕ

The Jordan-Hölder multiplicity [M : S]: the number of factors isomorphic to S in a composition series of M running from ⊥ to ⊤. By TauCeti.compositionMultiplicity_eq_jordanHolderMultiplicity any such series computes it, so the choice of series below is immaterial.

Equations

• TauCeti.jordanHolderMultiplicity R M S = TauCeti.compositionMultiplicity ⋯.choose S

theorem TauCeti.compositionMultiplicity_eq_jordanHolderMultiplicity {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsNoetherian R M] [IsArtinian R M] (s : CompositionSeries (Submodule R M)) (hbot : RelSeries.head s = ⊥) (htop : RelSeries.last s = ⊤) (S : Type w) [AddCommGroup S] [Module R S] : compositionMultiplicity s S = jordanHolderMultiplicity R M S

Every composition series from ⊥ to ⊤ computes the multiplicity.

theorem TauCeti.jordanHolderMultiplicity_ne_zero_iff {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsNoetherian R M] [IsArtinian R M] (s : CompositionSeries (Submodule R M)) (hbot : RelSeries.head s = ⊥) (htop : RelSeries.last s = ⊤) (S : Type w) [AddCommGroup S] [Module R S] : jordanHolderMultiplicity R M S ≠ 0 ↔ ∃ (i : Fin s.length), IsCompositionFactorAt s i S

S is a composition factor of M — the multiplicity [M : S] is nonzero — exactly when some index of a composition series from ⊥ to ⊤ carries a copy of S.

theorem TauCeti.jordanHolderMultiplicity_congr {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {S : Type w} [AddCommGroup S] [Module R S] {T : Type w'} [AddCommGroup T] [Module R T] [IsNoetherian R M] [IsArtinian R M] (e : S ≃ₗ[R] T) : jordanHolderMultiplicity R M S = jordanHolderMultiplicity R M T

The multiplicity [M : S] depends on S only through its isomorphism class.

theorem TauCeti.jordanHolderMultiplicity_eq_zero_of_not_isSimpleModule {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsNoetherian R M] [IsArtinian R M] (S : Type w) [AddCommGroup S] [Module R S] (hS : ¬IsSimpleModule R S) : jordanHolderMultiplicity R M S = 0

Only simple modules occur as composition factors.

Transport along an injective or a surjective linear map

@[simp]

theorem TauCeti.isCompositionFactorAt_mapCompositionSeriesOfInjective_iff {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v'} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Injective ⇑f) (s : CompositionSeries (Submodule R M)) (i : Fin (mapCompositionSeriesOfInjective f hf s).length) (S : Type w) [AddCommGroup S] [Module R S] : IsCompositionFactorAt (mapCompositionSeriesOfInjective f hf s) i S ↔ IsCompositionFactorAt s (Fin.cast ⋯ i) S

Transporting a composition series along an injective linear map does not change which module sits at an index; the index is transported along TauCeti.mapCompositionSeriesOfInjective_length.

@[simp]

theorem TauCeti.isCompositionFactorAt_comapCompositionSeriesOfSurjective_iff {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v'} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) (s : CompositionSeries (Submodule R N)) (i : Fin (comapCompositionSeriesOfSurjective f hf s).length) (S : Type w) [AddCommGroup S] [Module R S] : IsCompositionFactorAt (comapCompositionSeriesOfSurjective f hf s) i S ↔ IsCompositionFactorAt s (Fin.cast ⋯ i) S

Transporting a composition series along a surjective linear map does not change which module sits at an index; the index is transported along TauCeti.comapCompositionSeriesOfSurjective_length.

@[simp]

theorem TauCeti.compositionMultiplicity_mapCompositionSeriesOfInjective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v'} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Injective ⇑f) (s : CompositionSeries (Submodule R M)) (S : Type w) [AddCommGroup S] [Module R S] : compositionMultiplicity (mapCompositionSeriesOfInjective f hf s) S = compositionMultiplicity s S

An injective map preserves multiplicities: the image of a composition series counts every module the same number of times as the series itself.

@[simp]

theorem TauCeti.compositionMultiplicity_comapCompositionSeriesOfSurjective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v'} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) (s : CompositionSeries (Submodule R N)) (S : Type w) [AddCommGroup S] [Module R S] : compositionMultiplicity (comapCompositionSeriesOfSurjective f hf s) S = compositionMultiplicity s S

A surjective map preserves multiplicities: the preimage of a composition series counts every module the same number of times as the series itself.

theorem TauCeti.jordanHolderMultiplicity_eq_of_linearEquiv {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v'} [AddCommGroup N] [Module R N] [IsNoetherian R M] [IsArtinian R M] [IsNoetherian R N] [IsArtinian R N] (e : M ≃ₗ[R] N) (S : Type w) [AddCommGroup S] [Module R S] : jordanHolderMultiplicity R M S = jordanHolderMultiplicity R N S

The multiplicity only depends on the isomorphism class of the ambient module.

Modules of length zero and one

theorem TauCeti.compositionSeries_length_eq_zero_of_subsingleton {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Subsingleton M] (s : CompositionSeries (Submodule R M)) : s.length = 0

A composition series of a subsingleton module is a single point.

theorem TauCeti.compositionMultiplicity_eq_zero_of_subsingleton {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Subsingleton M] (s : CompositionSeries (Submodule R M)) (S : Type w) [AddCommGroup S] [Module R S] : compositionMultiplicity s S = 0

A subsingleton module has no composition factors at all.

theorem TauCeti.jordanHolderMultiplicity_eq_zero_of_subsingleton {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Subsingleton M] (S : Type w) [AddCommGroup S] [Module R S] : jordanHolderMultiplicity R M S = 0

Every multiplicity [M : S] in a subsingleton module M vanishes.

theorem TauCeti.nonempty_linearEquiv_subquotient_of_eq_bot_of_eq_top {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {A B : Submodule R M} (hA : A = ⊥) (hB : B = ⊤) : Nonempty ((↥B ⧸ Submodule.comap B.subtype A) ≃ₗ[R] M)

The bottom-to-top subquotient of a module is the module itself.

theorem TauCeti.compositionSeries_length_eq_one_of_isSimpleModule {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSimpleModule R M] {s : CompositionSeries (Submodule R M)} (hbot : RelSeries.head s = ⊥) (htop : RelSeries.last s = ⊤) : s.length = 1

A composition series of a simple module from ⊥ to ⊤ has a single step.

theorem TauCeti.isCompositionFactorAt_iff_of_isSimpleModule {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSimpleModule R M] {s : CompositionSeries (Submodule R M)} (hbot : RelSeries.head s = ⊥) (htop : RelSeries.last s = ⊤) (i : Fin s.length) (S : Type w) [AddCommGroup S] [Module R S] : IsCompositionFactorAt s i S ↔ Nonempty (M ≃ₗ[R] S)

The single factor of a simple module is that module. Every index of a composition series of a simple module running from ⊥ to ⊤ carries the module itself.

theorem TauCeti.compositionMultiplicity_eq_one_of_isSimpleModule_of_linearEquiv {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSimpleModule R M] {s : CompositionSeries (Submodule R M)} (hbot : RelSeries.head s = ⊥) (htop : RelSeries.last s = ⊤) (S : Type w) [AddCommGroup S] [Module R S] (e : M ≃ₗ[R] S) : compositionMultiplicity s S = 1

A simple module contains exactly one copy of itself, counted along a fixed composition series of it running from ⊥ to ⊤.

theorem TauCeti.compositionMultiplicity_eq_zero_of_isEmpty_linearEquiv_of_isSimpleModule {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSimpleModule R M] {s : CompositionSeries (Submodule R M)} (hbot : RelSeries.head s = ⊥) (htop : RelSeries.last s = ⊤) (S : Type w) [AddCommGroup S] [Module R S] (he : IsEmpty (M ≃ₗ[R] S)) : compositionMultiplicity s S = 0

A simple module contains no copy of a module it is not isomorphic to, counted along a fixed composition series of it running from ⊥ to ⊤.

theorem TauCeti.jordanHolderMultiplicity_eq_one_of_isSimpleModule_of_linearEquiv {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSimpleModule R M] (S : Type w) [AddCommGroup S] [Module R S] (e : M ≃ₗ[R] S) : jordanHolderMultiplicity R M S = 1

A simple module contains exactly one copy of itself: the multiplicity [M : S] of a simple module M in itself is 1.

theorem TauCeti.jordanHolderMultiplicity_eq_zero_of_isEmpty_linearEquiv_of_isSimpleModule {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSimpleModule R M] (S : Type w) [AddCommGroup S] [Module R S] (he : IsEmpty (M ≃ₗ[R] S)) : jordanHolderMultiplicity R M S = 0

A simple module contains no copy of a module it is not isomorphic to: the multiplicity [M : S] vanishes for a simple M admitting no linear equivalence with S.