Relationships between flatness and torsionfreeness.

We show that flat implies torsion-free, and that they're the same concept for rings satisfying a certain property, including Dedekind domains and valuation rings.

Main theorems

• Module.Flat.isSMulRegular_of_nonZeroDivisors: Scalar multiplication by a nonzerodivisor of R is injective on a flat R-module.
• Module.Flat.torsion_eq_bot: Torsion R M = ⊥ if M is a flat R-module.
• Module.Flat.flat_iff_torsion_eq_bot_of_valuationRing_localized_maximal: if localizing R at the complement of any maximal ideal is a valuation ring then Torsion R M = ⊥ iff M is a flat R-module.

theorem Module.Flat.isSMulRegular_of_isRegular {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {r : R} (hr : IsRegular r) [Flat R M] : IsSMulRegular M r

Scalar multiplication m ↦ r • m by a regular r is injective on a flat module.

theorem Module.Flat.isSMulRegular_of_nonZeroDivisors {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {r : R} (hr : r ∈ nonZeroDivisors R) [Flat R M] : IsSMulRegular M r

Scalar multiplication m ↦ r • m by a nonzerodivisor r is injective on a flat module.

theorem Module.Flat.torsion_eq_bot {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Flat R M] : Submodule.torsion R M = ⊥

Flat modules have no torsion.

theorem Module.Flat.flat_iff_torsion_eq_bot_of_isBezout {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsBezout R] [IsDomain R] : Flat R M ↔ Submodule.torsion R M = ⊥

If R is Bezout then an R-module is flat iff it has no torsion.

theorem Module.Flat.flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximal {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsDomain R] (h : ∀ (P : Ideal R) [inst : P.IsMaximal], ValuationRing (Localization P.primeCompl)) : Flat R M ↔ Submodule.torsion R M = ⊥

If every localization of R at a maximal ideal is a valuation ring then an R-module is flat iff it has no torsion.

theorem IsDedekindDomain.flat_iff_torsion_eq_bot {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsDedekindDomain R] : Module.Flat R M ↔ Submodule.torsion R M = ⊥

If R is a Dedekind domain then an R-module is flat iff it has no torsion.

instance Module.Flat.instOfIsDedekindDomainOfNoZeroSMulDivisors {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsDedekindDomain R] [NoZeroSMulDivisors R M] : Flat R M