 Saturated sublattice

A subgroup $L\subseteq M$ of a finitely generated free abelian group is saturated if $am\in L$ for a nonzero integer $a$ implies $m\in L$. Equivalently $M/L$ is torsion-free. It is then free abelian and the quotient map splits, so $L$ is a direct summand. Intersecting $M$ with a real linear subspace always gives a saturated sublattice.

// Target: algebra.bigb