Faithful flatness of ring homomorphisms

Scalar extension Algebra.TensorProduct.lTensor preserves faithful flatness of algebra homomorphisms, via the pushout identification used by Mathlib's RingHom.Flat.lTensor. A finite family of flat ring homomorphisms f i : R →+* S i combines into a faithfully flat ring homomorphism RingHom.pi f : R →+* ∀ i, S i as soon as every maximal ideal of R stays proper under some f i.

Main results

• RingHom.FaithfullyFlat.lTensor: scalar extension preserves faithful flatness.
• RingHom.FaithfullyFlat.pi_of_exists_map_ne_top: the criterion above.

theorem RingHom.FaithfullyFlat.lTensor {R : Type u_1} {S : Type u_2} (A : Type u_3) {B : Type u_4} {D : Type u_5} [CommSemiring R] [CommSemiring S] [Algebra R S] [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [CommRing B] [Algebra R B] [CommRing D] [Algebra R D] {f : B →ₐ[R] D} (hf : f.FaithfullyFlat) : (Algebra.TensorProduct.lTensor A f).FaithfullyFlat

Tensoring an algebra homomorphism with an algebra preserves faithful flatness.

theorem RingHom.FaithfullyFlat.pi_of_exists_map_ne_top {R : Type u_1} {ι : Type u_2} [CommRing R] [_root_.Finite ι] {S : ι → Type u_3} [(i : ι) → CommRing (S i)] {f : (i : ι) → R →+* S i} (hf : ∀ (i : ι), (f i).Flat) (h : ∀ (m : Ideal R), m.IsMaximal → ∃ (i : ι), Ideal.map (f i) m ≠ ⊤) : (RingHom.pi f).FaithfullyFlat

A finite product of flat ring homomorphisms is faithfully flat as soon as no maximal ideal becomes the unit ideal under every factor. No single f i need be faithfully flat: each maximal ideal m of R only has to stay proper under some f i, and which one may depend on m. Since m is maximal, m.map (f i) ≠ ⊤ holds exactly when some prime of S i lies over m.

This is Module.FaithfullyFlat.pi_of_exists_submodule_ne_top for the R-algebra structures induced by the f i, with its condition m • ⊤ ≠ ⊤ rephrased as m.map (f i) ≠ ⊤. The finiteness of ι cannot be dropped: an infinite product of flat modules need not be flat.