Transporting a composition series along a linear map

An injective linear map f : M →ₗ[R] N carries the submodules of M to submodules of N and preserves coverings (Submodule.map_covBy_of_injective), and a surjective one pulls the submodules of N back and preserves coverings (Submodule.comap_covBy_of_surjective), so each carries a composition series to a composition series: TauCeti.mapCompositionSeriesOfInjective and TauCeti.comapCompositionSeriesOfSurjective. That the transported series keeps the factors themselves, and not just their number, is the identification of subquotients TauCeti.mapSubquotientEquivOfInjective, respectively TauCeti.comapSubquotientEquivOfSurjective, of TauCeti.Algebra.Module.Submodule.Quotient.

Taking f to be a linear equivalence, this is what makes an invariant read off a composition series an invariant of the isomorphism class of the ambient module; the Jordan-Hölder multiplicities of TauCeti.RingTheory.CompositionSeries.Multiplicity are the consumer this was written for, and TauCeti.RingTheory.CompositionSeries.Additivity is the consumer that needs the two one-sided forms, for the inclusion of a submodule and the projection onto a quotient.

Main definitions

• TauCeti.mapCompositionSeriesOfInjective: the image of a composition series under an injective linear map.
• TauCeti.comapCompositionSeriesOfSurjective: the preimage of a composition series under a surjective linear map.

References

The two transports are exactly the anonymous lets inside the proof of Mathlib's Module.length_eq_add_of_exact (Mathlib/RingTheory/Length.lean, by Andrew Yang), packaged here as named definitions with an API so that they can be shown to preserve the factors themselves and not just their number.

def TauCeti.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)) : CompositionSeries (Submodule R N)

The image of a composition series of M under an injective linear map f : M →ₗ[R] N.

Equations

• TauCeti.mapCompositionSeriesOfInjective f hf s = RelSeries.map s { toFun := fun (A : Submodule R M) => Submodule.map f A, map_rel' := ⋯ }

@[simp]

theorem TauCeti.mapCompositionSeriesOfInjective_length {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)) : (mapCompositionSeriesOfInjective f hf s).length = s.length

@[simp]

theorem TauCeti.mapCompositionSeriesOfInjective_apply {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 + 1)) : (mapCompositionSeriesOfInjective f hf s).toFun i = Submodule.map f (s.toFun (Fin.cast ⋯ i))

The term of the transported series at an index is the image of the term of s at that same index, transported along TauCeti.mapCompositionSeriesOfInjective_length.

@[simp]

theorem TauCeti.head_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)) : RelSeries.head (mapCompositionSeriesOfInjective f hf s) = Submodule.map f (RelSeries.head s)

@[simp]

theorem TauCeti.last_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)) : RelSeries.last (mapCompositionSeriesOfInjective f hf s) = Submodule.map f (RelSeries.last s)

def TauCeti.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)) : CompositionSeries (Submodule R M)

The preimage of a composition series of N under a surjective linear map f : M →ₗ[R] N.

Equations

• TauCeti.comapCompositionSeriesOfSurjective f hf s = RelSeries.map s { toFun := fun (A : Submodule R N) => Submodule.comap f A, map_rel' := ⋯ }

@[simp]

theorem TauCeti.comapCompositionSeriesOfSurjective_length {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)) : (comapCompositionSeriesOfSurjective f hf s).length = s.length

@[simp]

theorem TauCeti.comapCompositionSeriesOfSurjective_apply {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 + 1)) : (comapCompositionSeriesOfSurjective f hf s).toFun i = Submodule.comap f (s.toFun (Fin.cast ⋯ i))

The term of the transported series at an index is the preimage of the term of s at that same index, transported along TauCeti.comapCompositionSeriesOfSurjective_length.

@[simp]

theorem TauCeti.head_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)) : RelSeries.head (comapCompositionSeriesOfSurjective f hf s) = Submodule.comap f (RelSeries.head s)

@[simp]

theorem TauCeti.last_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)) : RelSeries.last (comapCompositionSeriesOfSurjective f hf s) = Submodule.comap f (RelSeries.last s)