Additivity of the Jordan-Hölder multiplicities

The Jordan-Hölder multiplicity [M : S] counts the factors isomorphic to S in a composition series of M. This file proves that it is additive in a short exact sequence: for a submodule p of a module M of finite length,

[M : S] = [p : S] + [M ⧸ p : S].

Both the composition factors of p and those of M ⧸ p are composition factors of M, and no others are, so a single count splits in two.

The proof glues a composition series of p and a composition series of M ⧸ p into one series of M: the lower half is carried along the injective map p.subtype by TauCeti.mapCompositionSeriesOfInjective and the upper half along the surjective map p.mkQ by TauCeti.comapCompositionSeriesOfSurjective, both of TauCeti/RingTheory/CompositionSeries/Basic.lean; that these transports preserve every multiplicity is TauCeti.compositionMultiplicity_mapCompositionSeriesOfInjective and TauCeti.compositionMultiplicity_comapCompositionSeriesOfSurjective, of TauCeti/RingTheory/CompositionSeries/Multiplicity.lean. The two resulting series meet at p and are glued with RelSeries.smash, whose castAdd/natAdd index lemmas split the count of factors isomorphic to S into the two halves.

Main results

• TauCeti.compositionMultiplicity_smash: the multiplicities of two composition series glued end to end add.
• TauCeti.jordanHolderMultiplicity_eq_submodule_add_quotient: additivity, [M : S] = [p : S] + [M ⧸ p : S].
• TauCeti.jordanHolderMultiplicity_eq_add_of_exact: the same statement for a short exact sequence 0 → A → M → B → 0.
• TauCeti.jordanHolderMultiplicity_le_of_injective and TauCeti.jordanHolderMultiplicity_le_of_surjective: a submodule and a quotient — more generally the source of an injective map into M and the target of a surjective map out of M — each contribute at most M's multiplicity.
• TauCeti.jordanHolderMultiplicity_prod: [M × N : S] = [M : S] + [N : S].
• TauCeti.jordanHolderMultiplicity_pi: additivity on a finite product of modules.

References

This file refines Mathlib's Module.length_eq_add_of_exact (Mathlib/RingTheory/Length.lean, by Andrew Yang) from counting the factors of a composition series to counting those isomorphic to a fixed simple module S, and follows its proof plan: the same two transports along an injective and a surjective map, the same RelSeries.smash gluing, and the same map_bot/comap_top endpoint bookkeeping. The monotonicity and product corollaries below are likewise the multiplicity analogues of Module.length_le_of_injective, Module.length_le_of_surjective and Module.length_prod. What is new is that the transports are shown to preserve each factor's isomorphism class and not merely the number of factors: the identification of the subquotients is TauCeti.mapSubquotientEquivOfInjective and TauCeti.comapSubquotientEquivOfSurjective of TauCeti/Algebra/Module/Submodule/Quotient.lean, and the resulting factor-by-factor comparison is TauCeti.isCompositionFactorAt_mapCompositionSeriesOfInjective_iff and its surjective counterpart in TauCeti/RingTheory/CompositionSeries/Multiplicity.lean; TauCeti/RingTheory/CompositionSeries/Basic.lean supplies the transports themselves.

The additivity of [Pᵢ : Sⱼ] is what makes the Cartan matrix of a finite-dimensional algebra computable, in Layer 3 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md ("The Cartan matrix of an algebra"); TauCeti/RingTheory/CompositionSeries/Multiplicity.lean supplies the multiplicity itself.

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

Gluing two composition series

@[simp]

theorem TauCeti.isCompositionFactorAt_smash_castAdd_iff {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {S : Type v''} [AddCommGroup S] [Module R S] (p q : CompositionSeries (Submodule R M)) (h : RelSeries.last p = RelSeries.head q) (i : Fin p.length) : IsCompositionFactorAt (RelSeries.smash p q h) (Fin.castAdd q.length i) S ↔ IsCompositionFactorAt p i S

The factors of the first half of a glued series are the factors of the first series.

@[simp]

theorem TauCeti.isCompositionFactorAt_smash_natAdd_iff {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {S : Type v''} [AddCommGroup S] [Module R S] (p q : CompositionSeries (Submodule R M)) (h : RelSeries.last p = RelSeries.head q) (i : Fin q.length) : IsCompositionFactorAt (RelSeries.smash p q h) (Fin.natAdd p.length i) S ↔ IsCompositionFactorAt q i S

The factors of the second half of a glued series are the factors of the second series.

@[simp]

theorem TauCeti.compositionMultiplicity_smash {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {S : Type v''} [AddCommGroup S] [Module R S] (p q : CompositionSeries (Submodule R M)) (h : RelSeries.last p = RelSeries.head q) : compositionMultiplicity (RelSeries.smash p q h) S = compositionMultiplicity p S + compositionMultiplicity q S

Gluing adds multiplicities. Two composition series joined end to end count every module as often as the two of them together.

Additivity of the Jordan-Hölder multiplicity

theorem TauCeti.jordanHolderMultiplicity_eq_submodule_add_quotient {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {S : Type v''} [AddCommGroup S] [Module R S] [IsNoetherian R M] [IsArtinian R M] (p : Submodule R M) : jordanHolderMultiplicity R M S = jordanHolderMultiplicity R (↥p) S + jordanHolderMultiplicity R (M ⧸ p) S

The Jordan-Hölder multiplicity is additive. For a submodule p of a module of finite length, [M : S] = [p : S] + [M ⧸ p : S]: a composition series of p, pushed into M along p.subtype, and one of M ⧸ p, pulled back along p.mkQ, meet at p and glue to a composition series of M.

theorem TauCeti.jordanHolderMultiplicity_eq_add_of_exact {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {S : Type v''} [AddCommGroup S] [Module R S] [IsNoetherian R M] [IsArtinian R M] {A : Type w} [AddCommGroup A] [Module R A] [IsNoetherian R A] [IsArtinian R A] {B : Type w'} [AddCommGroup B] [Module R B] [IsNoetherian R B] [IsArtinian R B] (f : A →ₗ[R] M) (g : M →ₗ[R] B) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (hfg : Function.Exact ⇑f ⇑g) : jordanHolderMultiplicity R M S = jordanHolderMultiplicity R A S + jordanHolderMultiplicity R B S

Additivity in a short exact sequence 0 → A → M → B → 0: the multiplicity of S in the middle term is the sum of its multiplicities in the two ends.

Mathematically the finiteness of A and of B follows from that of M, through A ≃ₗ[R] range f and M ⧸ ker g ≃ₗ[R] B. The assumptions are nevertheless binders here rather than facts derived in the proof, because jordanHolderMultiplicity R A S and jordanHolderMultiplicity R B S carry them in their own signatures: the conclusion does not elaborate without them, so a caller holds them already in order to state it.

theorem TauCeti.jordanHolderMultiplicity_le_of_injective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {S : Type v''} [AddCommGroup S] [Module R S] [IsNoetherian R M] [IsArtinian R M] {A : Type w} [AddCommGroup A] [Module R A] [IsNoetherian R A] [IsArtinian R A] (f : A →ₗ[R] M) (hf : Function.Injective ⇑f) : jordanHolderMultiplicity R A S ≤ jordanHolderMultiplicity R M S

A module that embeds in M contributes at most M's multiplicity. As for TauCeti.jordanHolderMultiplicity_eq_add_of_exact, the finiteness of A follows from that of M and is a binder only because jordanHolderMultiplicity R A S — which already occurs in the statement a caller is trying to prove — does not elaborate without it.

theorem TauCeti.jordanHolderMultiplicity_le_of_surjective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {S : Type v''} [AddCommGroup S] [Module R S] [IsNoetherian R M] [IsArtinian R M] {B : Type w'} [AddCommGroup B] [Module R B] [IsNoetherian R B] [IsArtinian R B] (g : M →ₗ[R] B) (hg : Function.Surjective ⇑g) : jordanHolderMultiplicity R B S ≤ jordanHolderMultiplicity R M S

A quotient of M contributes at most M's multiplicity. As for TauCeti.jordanHolderMultiplicity_eq_add_of_exact, the finiteness of B follows from that of M and is a binder only because jordanHolderMultiplicity R B S — which already occurs in the statement a caller is trying to prove — does not elaborate without it.

@[simp]

theorem TauCeti.jordanHolderMultiplicity_prod {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v'} [AddCommGroup N] [Module R N] {S : Type v''} [AddCommGroup S] [Module R S] [IsNoetherian R M] [IsArtinian R M] [IsNoetherian R N] [IsArtinian R N] : jordanHolderMultiplicity R (M × N) S = jordanHolderMultiplicity R M S + jordanHolderMultiplicity R N S

Additivity on a binary product: [M × N : S] = [M : S] + [N : S].

@[simp]

theorem TauCeti.jordanHolderMultiplicity_pi {R : Type u} [Ring R] {S : Type v''} [AddCommGroup S] [Module R S] {ι : Type u_1} [Fintype ι] (N : ι → Type u_2) [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module R (N i)] [∀ (i : ι), IsNoetherian R (N i)] [∀ (i : ι), IsArtinian R (N i)] : jordanHolderMultiplicity R ((i : ι) → N i) S = ∑ i : ι, jordanHolderMultiplicity R (N i) S

The Jordan-Hölder multiplicity in a finite product is the sum of the multiplicities in its factors. This is the multiplicity analogue of Module.length_pi_of_fintype.