Submodules of free modules over principal ideal rings without zero divisors

Every submodule of a free module over a principal ideal ring without zero divisors is free, without a finiteness hypothesis on the ambient module. The ring need not be commutative: as in IsPrincipalIdealRing, it suffices that every left ideal is principal. The construction well-orders an ambient basis and chooses a pivot for each nonzero left ideal of possible leading coordinates. The pivots form a basis of the submodule by elimination of the greatest coordinate in the finite support of each vector.

This is the arbitrary-rank form of Lang, Algebra, Chapter III, Theorem 7.1. Mathlib's Submodule.nonempty_basis_of_pid is the finite-rank form. A projective module embeds in a free module, so every submodule of a projective module is free as well (Submodule.free_of_projective_of_isPrincipalIdealRing), and so is every module that injects into a projective module (Module.Free.of_injective_of_projective_of_isPrincipalIdealRing).

theorem Submodule.free_of_isPrincipalIdealRing {R : Type u_1} {M : Type u_2} [Ring R] [NoZeroDivisors R] [IsPrincipalIdealRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) [Module.Free R M] : Module.Free R ↥N

Every submodule of a free module over a principal ideal ring without zero divisors is free, with no finiteness assumption on either module.

theorem Submodule.free_of_projective_of_isPrincipalIdealRing {R : Type u_1} {M : Type u_2} [Ring R] [NoZeroDivisors R] [IsPrincipalIdealRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) [Module.Projective R M] : Module.Free R ↥N

Every submodule of a projective module over a principal ideal ring without zero divisors is free.

theorem Module.Free.of_injective_of_projective_of_isPrincipalIdealRing {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [NoZeroDivisors R] [IsPrincipalIdealRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Projective R M] (f : N →ₗ[R] M) (hf : Function.Injective ⇑f) : Free R N

A module that injects into a projective module over a principal ideal ring without zero divisors is free.