Nonzerodivisors in flat algebras

A flat algebra A over a commutative ring R is torsion-free: multiplication by a nonzerodivisor of R is injective on A (Module.Flat.isSMulRegular_of_nonZeroDivisors). For a commutative A this says that the structure map sends nonzerodivisors of R to nonzerodivisors of A. Over a Bezout domain, such as a discrete valuation ring, torsion-freeness is also sufficient for flatness, so a commutative algebra over a Bezout domain is flat exactly when every nonzero scalar becomes a nonzerodivisor.

Main results

• Module.Flat.algebraMap_mem_nonZeroDivisors: the image of a nonzerodivisor of R in a flat commutative R-algebra is a nonzerodivisor.
• Module.Flat.flat_iff_algebraMap_mem_nonZeroDivisors_of_isBezout: over a Bezout domain, a commutative algebra is flat exactly when the structure map sends nonzero elements to nonzerodivisors.

theorem Module.Flat.algebraMap_mem_nonZeroDivisors {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Flat R A] {r : R} (hr : r ∈ nonZeroDivisors R) : (algebraMap R A) r ∈ nonZeroDivisors A

The structure map of a flat commutative algebra sends nonzerodivisors to nonzerodivisors.

theorem Module.Flat.flat_iff_algebraMap_mem_nonZeroDivisors_of_isBezout {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [IsDomain R] [IsBezout R] : Flat R A ↔ ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∈ nonZeroDivisors A

Over a Bezout domain, a commutative algebra is flat exactly when the structure map sends every nonzero element to a nonzerodivisor.