Documentation

TauCeti.Algebra.Module.ProjectiveCover.Multiplicity

Hom out of a projective cover counts composition factors #

Let k be a field, A a k-algebra, S a simple A-module and f : P →ₗ[A] S a projective cover of S. This file proves the multiplicity formula

dim_k Hom_A(P, M) = [M : S] · dim_k End_A(S),

for every A-module M that is finite-dimensional over k, where [M : S] is the Jordan--Hölder multiplicity TauCeti.jordanHolderMultiplicity. It is the integral pairing between projectives and modules made explicit: reading dim_k Hom_A(P, -) off a finite-dimensional module returns its S-multiplicity, scaled by the dimension of the division algebra D = End_A(S). Over a splitting field D is k and the scale disappears, so the hom dimension is the multiplicity; over a general field the scale is genuinely there, which is why the raw hom dimension is not the multiplicity coordinate.

Two facts drive the proof. Since P is projective, Hom_A(P, -) is exact, so dim_k Hom_A(P, -) is additive in short exact sequences. Since the kernel of a projective cover is superfluous, it lies in the radical of P, which every map into a simple module annihilates; precomposition with f therefore identifies Hom_A(S, T) with Hom_A(P, T) for every simple T, and Schur's lemma evaluates the latter. Induction along a composition series of M adds up the factors.

The identification is TauCeti.IsProjectiveCover.homEquivOfIsSemisimpleModule in TauCeti/Algebra/Module/ProjectiveCover/Basic.lean, and the additivity is TauCeti.finrank_linearMap_quotient_add_finrank_linearMap in TauCeti/Algebra/Module/Projective/LinearMap.lean.

Main results #

References #

The multiplicity formula #

source
theorem TauCeti.IsProjectiveCover.finrank_linearMap_eq_finrank_end {k : Type u_1} {A : Type u_2} {P : Type u_3} {S : Type u_4} [Field k] [Ring A] [Algebra k A] [AddCommGroup P] [Module A P] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] {T : Type u_5} [AddCommGroup T] [Module k T] [Module A T] [IsScalarTower k A T] [IsSimpleModule A T] {f : P →ₗ[A] S} (hf : IsProjectiveCover f) (e : T ≃ₗ[A] S) :
Module.finrank k (P →ₗ[A] T) = Module.finrank k (Module.End A S)

The diagonal value of the projective/simple pairing. If the simple module T is isomorphic to S, the hom space out of a projective cover of S has the dimension of the division algebra End_A(S).

source
theorem TauCeti.IsProjectiveCover.finrank_linearMap_eq_zero {k : Type u_1} {A : Type u_2} {P : Type u_3} {S : Type u_4} [Field k] [Ring A] [Algebra k A] [AddCommGroup P] [Module A P] [AddCommGroup S] [Module A S] [IsSimpleModule A S] {T : Type u_5} [AddCommGroup T] [Module k T] [Module A T] [IsScalarTower k A T] [IsSimpleModule A T] {f : P →ₗ[A] S} (hf : IsProjectiveCover f) (he : IsEmpty (T ≃ₗ[A] S)) :
Module.finrank k (P →ₗ[A] T) = 0

The off-diagonal value of the projective/simple pairing. Between a projective cover of S and a simple module not isomorphic to S the hom space vanishes, by Schur's lemma.

source
theorem TauCeti.IsProjectiveCover.finrank_linearMap_eq_jordanHolderMultiplicity_mul_finrank_end {k : Type u_1} {A : Type u_2} {P : Type u_3} {S : Type u_4} [Field k] [Ring A] [Algebra k A] [AddCommGroup P] [Module A P] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [IsSimpleModule A S] [Module k P] [IsScalarTower k A P] [FiniteDimensional k P] {f : P →ₗ[A] S} (hf : IsProjectiveCover f) (M : Type w) [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [FiniteDimensional k M] [IsNoetherian A M] [IsArtinian A M] :
Module.finrank k (P →ₗ[A] M) = jordanHolderMultiplicity A M S * Module.finrank k (Module.End A S)

The multiplicity formula. For a projective cover f : P →ₗ[A] S of a simple module S and an A-module M that is finite-dimensional over k, the dimension of Hom_A(P, M) is the Jordan--Hölder multiplicity of S in M, scaled by the dimension of the division algebra End_A(S).

The Noetherian and Artinian hypotheses on M follow from FiniteDimensional k M, but are binders here because TauCeti.jordanHolderMultiplicity A M S does not elaborate without them, so a caller holds them already in order to state the conclusion.

source
theorem TauCeti.IsProjectiveCover.finrank_linearMap_eq_jordanHolderMultiplicity {k : Type u_1} {A : Type u_2} {P : Type u_3} {S : Type u_4} [Field k] [Ring A] [Algebra k A] [AddCommGroup P] [Module A P] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [IsSimpleModule A S] [Module k P] [IsScalarTower k A P] [FiniteDimensional k P] {f : P →ₗ[A] S} (hf : IsProjectiveCover f) (hend : Module.finrank k (Module.End A S) = 1) (M : Type w) [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [FiniteDimensional k M] [IsNoetherian A M] [IsArtinian A M] :
Module.finrank k (P →ₗ[A] M) = jordanHolderMultiplicity A M S

The split form of the multiplicity formula. When the simple module S is absolutely simple -- its endomorphism algebra is one-dimensional -- the dimension of Hom_A(P, M) is the Jordan--Hölder multiplicity of S in M on the nose.

source
theorem TauCeti.IsProjectiveCover.finrank_linearMap_eq_jordanHolderMultiplicity_of_isAlgClosed {k : Type u_1} {A : Type u_2} {P : Type u_3} {S : Type u_4} [Field k] [Ring A] [Algebra k A] [AddCommGroup P] [Module A P] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [IsSimpleModule A S] [Module k P] [IsScalarTower k A P] [FiniteDimensional k P] [IsAlgClosed k] [FiniteDimensional k S] {f : P →ₗ[A] S} (hf : IsProjectiveCover f) (M : Type w) [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [FiniteDimensional k M] [IsNoetherian A M] [IsArtinian A M] :
Module.finrank k (P →ₗ[A] M) = jordanHolderMultiplicity A M S

Over an algebraically closed field a finite-dimensional simple module is absolutely simple, so the dimension of Hom_A(P, M) is the Jordan--Hölder multiplicity of S in M.