Primitive submodules over principal ideal domains #
A submodule of a torsion-free module over a principal ideal domain is primitive when its quotient has no torsion. When the quotient is finitely generated, such a submodule is exactly a direct summand. In particular, an injective homomorphism of finite free abelian groups is primitive precisely when its image has a complement.
Main results #
Submodule.isTorsionFree_quotient_of_smul_mem: a saturated submodule has torsion-free quotient.Submodule.exists_isCompl_iff_isTorsionFree_quotient: the direct-summand criterion.
References #
- V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.5.
theorem
Submodule.isTorsionFree_quotient_of_smul_mem
{R : Type u_1}
[Ring R]
{M : Type u}
[AddCommGroup M]
[Module R M]
(S : Submodule R M)
(hS : ∀ (c : R) (z : M), c ≠ 0 → c • z ∈ S → z ∈ S)
:
Module.IsTorsionFree R (M ⧸ S)
If a submodule contains every element with a nonzero multiple in it, its quotient is torsion-free.
theorem
Submodule.exists_isCompl_iff_isTorsionFree_quotient
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsPrincipalIdealRing R]
{M : Type u}
[AddCommGroup M]
[Module R M]
[Module.IsTorsionFree R M]
(S : Submodule R M)
[Module.Finite R (M ⧸ S)]
:
A submodule of a torsion-free module over a PID with finitely generated quotient has torsion-free quotient if and only if it admits a complementary submodule.