Properties of faithfully flat algebras

An A-algebra B is faithfully flat if B is faithfully flat as an A-module. In this file we give equivalent characterizations of faithful flatness in the algebra case.

Main results

Let B be a faithfully flat A-algebra:

• Ideal.comap_map_eq_self_of_faithfullyFlat: the contraction of the extension of any ideal of A to B is the ideal itself.
• Module.FaithfullyFlat.tensorProduct_mk_injective: The natural map M →ₗ[A] B ⊗[A] M is injective for any A-module M.
• PrimeSpectrum.comap_surjective_of_faithfullyFlat: The map on prime spectra induced by a faithfully flat ring map is surjective. See also Ideal.exists_isPrime_liesOver_of_faithfullyFlat for a version stated in terms of Ideal.LiesOver.

Conversely, let B be a flat A-algebra:

• Module.FaithfullyFlat.of_comap_surjective: B is faithfully flat over A, if the induced map on prime spectra is surjective.
• Module.FaithfullyFlat.of_flat_of_isLocalHom: flat + local implies faithfully flat

theorem Module.FaithfullyFlat.of_comap_surjective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Flat A B] (h : Function.Surjective (PrimeSpectrum.comap (algebraMap A B))) : FaithfullyFlat A B

If A →+* B is flat and surjective on prime spectra, B is a faithfully flat A-algebra.

@[deprecated Module.FaithfullyFlat.of_comap_surjective (since := "2025-12-10")]

theorem Module.FaithfullyFlat.of_specComap_surjective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Flat A B] (h : Function.Surjective (PrimeSpectrum.comap (algebraMap A B))) : FaithfullyFlat A B

Alias of Module.FaithfullyFlat.of_comap_surjective.

---

If A →+* B is flat and surjective on prime spectra, B is a faithfully flat A-algebra.

theorem Module.FaithfullyFlat.of_flat_of_isLocalHom {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsLocalRing A] [IsLocalRing B] [Flat A B] [IsLocalHom (algebraMap A B)] : FaithfullyFlat A B

If A is local and B is a local and flat A-algebra, then B is faithfully flat.

theorem Module.FaithfullyFlat.tensorProduct_mk_injective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [FaithfullyFlat A B] (M : Type u_3) [AddCommGroup M] [Module A M] : Function.Injective ⇑((TensorProduct.mk A B M) 1)

If B is a faithfully flat A-module and M is any A-module, the canonical map M →ₗ[A] B ⊗[A] M is injective.

instance Module.FaithfullyFlat.faithfulSMul {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [FaithfullyFlat A B] : FaithfulSMul A B

theorem Ideal.comap_map_eq_self_of_faithfullyFlat {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Module.FaithfullyFlat A B] (I : Ideal A) : comap (algebraMap A B) (map (algebraMap A B) I) = I

If B is a faithfully flat A-algebra, the preimage of the pushforward of any ideal I is again I.

theorem Ideal.comap_surjective_of_faithfullyFlat {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Module.FaithfullyFlat A B] : Function.Surjective (comap (algebraMap A B))

If B is a faithfully-flat A-algebra, every ideal in A is the preimage of some ideal in B.

theorem Ideal.exists_isPrime_liesOver_of_faithfullyFlat {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Module.FaithfullyFlat A B] (p : Ideal A) [p.IsPrime] : ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p

If B is faithfully flat over A, every prime of A comes from a prime of B.

theorem PrimeSpectrum.comap_surjective_of_faithfullyFlat {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Module.FaithfullyFlat A B] : Function.Surjective (comap (algebraMap A B))

If B is a faithfully flat A-algebra, the induced map on the prime spectrum is surjective.

@[deprecated PrimeSpectrum.comap_surjective_of_faithfullyFlat (since := "2025-12-10")]

theorem PrimeSpectrum.specComap_surjective_of_faithfullyFlat {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Module.FaithfullyFlat A B] : Function.Surjective (comap (algebraMap A B))

Alias of PrimeSpectrum.comap_surjective_of_faithfullyFlat.

---

If B is a faithfully flat A-algebra, the induced map on the prime spectrum is surjective.