Faithfully flat modules

A module M over a commutative ring R is faithfully flat if it is flat and IM ≠ M whenever I is a maximal ideal of R.

Main declaration

• Module.FaithfullyFlat: the predicate asserting that an R-module M is faithfully flat.

Main theorems

• Module.FaithfullyFlat.iff_flat_and_proper_ideal: an R-module M is faithfully flat iff it is flat and for all proper ideals I of R, I • M ≠ M.

• Module.FaithfullyFlat.iff_flat_and_rTensor_faithful: an R-module M is faithfully flat iff it is flat and tensoring with M is faithful, i.e. N ≠ 0 implies N ⊗ M ≠ 0.

• Module.FaithfullyFlat.iff_flat_and_lTensor_faithful: an R-module M is faithfully flat iff it is flat and tensoring with M is faithful, i.e. N ≠ 0 implies M ⊗ N ≠ 0.

• Module.FaithfullyFlat.iff_exact_iff_rTensor_exact: an R-module M is faithfully flat iff tensoring with M preserves and reflects exact sequences, i.e. the sequence N₁ → N₂ → N₃ is exact iff the sequence N₁ ⊗ M → N₂ ⊗ M → N₃ ⊗ M is exact.

• Module.FaithfullyFlat.iff_exact_iff_lTensor_exact: an R-module M is faithfully flat iff tensoring with M preserves and reflects exact sequences, i.e. the sequence N₁ → N₂ → N₃ is exact iff the sequence M ⊗ N₁ → M ⊗ N₂ → M ⊗ N₃ is exact.

• Module.FaithfullyFlat.iff_zero_iff_lTensor_zero: an R-module M is faithfully flat iff for all linear maps f : N → N', f = 0 iff M ⊗ f = 0.

• Module.FaithfullyFlat.iff_zero_iff_rTensor_zero: an R-module M is faithfully flat iff for all linear maps f : N → N', f = 0 iff f ⊗ M = 0.

• Module.FaithfullyFlat.of_linearEquiv: modules linearly equivalent to a flat modules are flat

• Module.FaithfullyFlat.trans: if S is R-faithfully flat and M is S-faithfully flat, then M is R-faithfully flat.

• Module.FaithfullyFlat.self: the R-module R is faithfully flat.

class Module.FaithfullyFlat (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] extends Module.Flat R M : Prop

A module M over a commutative ring R is faithfully flat if it is flat and, for all R-linear maps f : N → N' such that id ⊗ f = 0, we have f = 0.

• out ⦃P : Type u⦄ [AddCommMonoid P] [Module R P] [Module.Finite R P] (N : Submodule R P) : N.FG → Function.Injective ⇑(LinearMap.rTensor M N.subtype)
• submodule_ne_top ⦃m : Ideal R⦄ : m.IsMaximal → m • ⊤ ≠ ⊤

theorem Module.faithfullyFlat_iff (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : FaithfullyFlat R M ↔ Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤

instance Module.FaithfullyFlat.self (R : Type u) [CommRing R] : FaithfullyFlat R R

theorem Module.FaithfullyFlat.iff_flat_and_proper_ideal (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : FaithfullyFlat R M ↔ Flat R M ∧ ∀ (I : Ideal R), I ≠ ⊤ → I • ⊤ ≠ ⊤

theorem Module.FaithfullyFlat.iff_flat_and_ideal_smul_eq_top (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : FaithfullyFlat R M ↔ Flat R M ∧ ∀ (I : Ideal R), I • ⊤ = ⊤ → I = ⊤

instance Module.FaithfullyFlat.rTensor_nontrivial (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [fl : FaithfullyFlat R M] (N : Type u_1) [AddCommGroup N] [Module R N] [Nontrivial N] : Nontrivial (TensorProduct R N M)

instance Module.FaithfullyFlat.lTensor_nontrivial (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [FaithfullyFlat R M] (N : Type u_1) [AddCommGroup N] [Module R N] [Nontrivial N] : Nontrivial (TensorProduct R M N)

theorem Module.FaithfullyFlat.rTensor_reflects_triviality (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [FaithfullyFlat R M] (N : Type u_1) [AddCommGroup N] [Module R N] [h : Subsingleton (TensorProduct R N M)] : Subsingleton N

theorem Module.FaithfullyFlat.lTensor_reflects_triviality (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [FaithfullyFlat R M] (N : Type u_1) [AddCommGroup N] [Module R N] [Subsingleton (TensorProduct R M N)] : Subsingleton N

theorem Module.FaithfullyFlat.iff_flat_and_rTensor_faithful (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : FaithfullyFlat R M ↔ Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (TensorProduct R N M)

theorem Module.FaithfullyFlat.iff_flat_and_rTensor_reflects_triviality (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : FaithfullyFlat R M ↔ Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Subsingleton (TensorProduct R N M) → Subsingleton N

theorem Module.FaithfullyFlat.iff_flat_and_lTensor_faithful (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : FaithfullyFlat R M ↔ Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (TensorProduct R M N)

theorem Module.FaithfullyFlat.iff_flat_and_lTensor_reflects_triviality (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : FaithfullyFlat R M ↔ Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Subsingleton (TensorProduct R M N) → Subsingleton N

theorem Module.FaithfullyFlat.of_linearEquiv (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_1} [AddCommGroup N] [Module R N] [FaithfullyFlat R M] (e : N ≃ₗ[R] M) : FaithfullyFlat R N

If M is a faithfully flat R-module and N is R-linearly isomorphic to M, then N is faithfully flat.

instance Module.FaithfullyFlat.directSum (R : Type u) [CommRing R] {ι : Type u_1} [Nonempty ι] (M : ι → Type u_2) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), FaithfullyFlat R (M i)] : FaithfullyFlat R (DirectSum ι fun (i : ι) => M i)

A direct sum of faithfully flat R-modules is faithfully flat.

instance Module.FaithfullyFlat.finsupp (R : Type u) [CommRing R] (ι : Type v) [Nonempty ι] : FaithfullyFlat R (ι →₀ R)

Free R-modules over discrete types are flat.

instance Module.FaithfullyFlat.instOfNontrivialOfFree (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial M] [Free R M] : FaithfullyFlat R M

Any free, nontrivial R-module is flat.

@[simp]

theorem Module.FaithfullyFlat.subsingleton_tensorProduct_iff_right (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_1} [AddCommGroup N] [Module R N] [FaithfullyFlat R M] : Subsingleton (TensorProduct R M N) ↔ Subsingleton N

@[simp]

theorem Module.FaithfullyFlat.subsingleton_tensorProduct_iff_left (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_1} [AddCommGroup N] [Module R N] [FaithfullyFlat R N] : Subsingleton (TensorProduct R M N) ↔ Subsingleton M

@[simp]

theorem Module.FaithfullyFlat.nontrivial_tensorProduct_iff_right (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_1} [AddCommGroup N] [Module R N] [FaithfullyFlat R M] : Nontrivial (TensorProduct R M N) ↔ Nontrivial N

@[simp]

theorem Module.FaithfullyFlat.nontrivial_tensorProduct_iff_left (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_1} [AddCommGroup N] [Module R N] [FaithfullyFlat R N] : Nontrivial (TensorProduct R M N) ↔ Nontrivial M

Faithfully flat modules and exact sequences

In this section we prove that an R-module M is faithfully flat iff tensoring with M preserves and reflects exact sequences.

Let N₁ -l₁₂-> N₂ -l₂₃-> N₃ be two linear maps.

• We first show that if N₁ ⊗ M -> N₂ ⊗ M -> N₃ ⊗ M is exact, then N₁ -l₁₂-> N₂ -l₂₃-> N₃ is a complex, i.e. range l₁₂ ≤ ker l₂₃. This is range_le_ker_of_exact_rTensor.
• Then in rTensor_reflects_exact, we show ker l₂₃ = range l₁₂ by considering the cohomology ker l₂₃ ⧸ range l₁₂. This shows that when M is faithfully flat, - ⊗ M reflects exact sequences. For details, see comments in the proof. Since M is flat, - ⊗ M preserves exact sequences.

On the other hand, if - ⊗ M preserves and reflects exact sequences, then M is faithfully flat.

• M is flat because - ⊗ M preserves exact sequences.
• We need to show that if N ⊗ M = 0 then N = 0. Consider the sequence N -0-> N -0-> 0. After tensoring with M, we get N ⊗ M -0-> N ⊗ M -0-> 0 which is exact because N ⊗ M = 0. Since - ⊗ M reflects exact sequences, N = 0.

theorem Module.FaithfullyFlat.range_le_ker_of_exact_rTensor (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] {N1 : Type u_1} [AddCommGroup N1] [Module R N1] {N2 : Type u_2} [AddCommGroup N2] [Module R N2] {N3 : Type u_3} [AddCommGroup N3] [Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3) [fl : FaithfullyFlat R M] (ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)) : LinearMap.range l12 ≤ LinearMap.ker l23

If M is faithfully flat, then exactness of N₁ ⊗ M -> N₂ ⊗ M -> N₃ ⊗ M implies that the composition N₁ -> N₂ -> N₃ is 0.

Implementation detail, please use rTensor_reflects_exact instead.

theorem Module.FaithfullyFlat.rTensor_reflects_exact (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] {N1 : Type u_1} [AddCommGroup N1] [Module R N1] {N2 : Type u_2} [AddCommGroup N2] [Module R N2] {N3 : Type u_3} [AddCommGroup N3] [Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3) [fl : FaithfullyFlat R M] (ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)) : Function.Exact ⇑l12 ⇑l23

theorem Module.FaithfullyFlat.lTensor_reflects_exact (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] {N1 : Type u_1} [AddCommGroup N1] [Module R N1] {N2 : Type u_2} [AddCommGroup N2] [Module R N2] {N3 : Type u_3} [AddCommGroup N3] [Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3) [fl : FaithfullyFlat R M] (ex : Function.Exact ⇑(LinearMap.lTensor M l12) ⇑(LinearMap.lTensor M l23)) : Function.Exact ⇑l12 ⇑l23

@[simp]

theorem Module.FaithfullyFlat.rTensor_exact_iff_exact (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] {N1 : Type u_1} [AddCommGroup N1] [Module R N1] {N2 : Type u_2} [AddCommGroup N2] [Module R N2] {N3 : Type u_3} [AddCommGroup N3] [Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3) [FaithfullyFlat R M] : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23) ↔ Function.Exact ⇑l12 ⇑l23

@[simp]

theorem Module.FaithfullyFlat.lTensor_exact_iff_exact (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] {N1 : Type u_1} [AddCommGroup N1] [Module R N1] {N2 : Type u_2} [AddCommGroup N2] [Module R N2] {N3 : Type u_3} [AddCommGroup N3] [Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3) [FaithfullyFlat R M] : Function.Exact ⇑(LinearMap.lTensor M l12) ⇑(LinearMap.lTensor M l23) ↔ Function.Exact ⇑l12 ⇑l23

@[simp]

theorem Module.FaithfullyFlat.lTensor_injective_iff_injective (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_4} {N' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N'] (f : N →ₗ[R] N') [FaithfullyFlat R M] : Function.Injective ⇑(LinearMap.lTensor M f) ↔ Function.Injective ⇑f

@[simp]

theorem Module.FaithfullyFlat.lTensor_surjective_iff_surjective (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_4} {N' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N'] (f : N →ₗ[R] N') [FaithfullyFlat R M] : Function.Surjective ⇑(LinearMap.lTensor M f) ↔ Function.Surjective ⇑f

theorem Module.FaithfullyFlat.iff_exact_iff_rTensor_exact (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : FaithfullyFlat R M ↔ ∀ {N1 : Type (max u v)} [inst : AddCommGroup N1] [inst_1 : Module R N1] {N2 : Type (max u v)} [inst_2 : AddCommGroup N2] [inst_3 : Module R N2] {N3 : Type (max u v)} [inst_4 : AddCommGroup N3] [inst_5 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3), Function.Exact ⇑l12 ⇑l23 ↔ Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)

theorem Module.FaithfullyFlat.iff_exact_iff_lTensor_exact (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : FaithfullyFlat R M ↔ ∀ {N1 : Type (max u v)} [inst : AddCommGroup N1] [inst_1 : Module R N1] {N2 : Type (max u v)} [inst_2 : AddCommGroup N2] [inst_3 : Module R N2] {N3 : Type (max u v)} [inst_4 : AddCommGroup N3] [inst_5 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3), Function.Exact ⇑l12 ⇑l23 ↔ Function.Exact ⇑(LinearMap.lTensor M l12) ⇑(LinearMap.lTensor M l23)

Faithfully flat modules and linear maps

In this section we prove that an R-module M is faithfully flat iff the following holds:

• M is flat
• for any R-linear map f : N → N', f = 0 iff f ⊗ 𝟙M = 0 iff 𝟙M ⊗ f = 0

theorem Module.FaithfullyFlat.zero_iff_lTensor_zero (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [h : FaithfullyFlat R M] {N : Type u_1} [AddCommGroup N] [Module R N] {N' : Type u_2} [AddCommGroup N'] [Module R N'] (f : N →ₗ[R] N') : f = 0 ↔ LinearMap.lTensor M f = 0

If M is a faithfully flat module, then for all linear maps f, the map id ⊗ f = 0, if and only if f = 0.

theorem Module.FaithfullyFlat.zero_iff_rTensor_zero (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [h : FaithfullyFlat R M] {N : Type u_1} [AddCommGroup N] [Module R N] {N' : Type u_2} [AddCommGroup N'] [Module R N'] (f : N →ₗ[R] N') : f = 0 ↔ LinearMap.rTensor M f = 0

If M is a faithfully flat module, then for all linear maps f, the map f ⊗ id = 0, if and only if f = 0.

@[simp]

theorem Module.FaithfullyFlat.one_tmul_eq_zero_iff (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] {A : Type u_1} [Ring A] [Algebra R A] [FaithfullyFlat R A] (m : M) : 1 ⊗ₜ[R] m = 0 ↔ m = 0

If A is a faithfully flat R-algebra, and m is a term of an R-module M, then 1 ⊗ₜ[R] m = 0 if and only if m = 0.

theorem Module.FaithfullyFlat.iff_zero_iff_lTensor_zero (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : FaithfullyFlat R M ↔ Flat R M ∧ ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0

An R-module M is faithfully flat iff it is flat and for all linear maps f, the map id ⊗ f = 0, if and only if f = 0.

theorem Module.FaithfullyFlat.iff_zero_iff_rTensor_zero (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : FaithfullyFlat R M ↔ Flat R M ∧ ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0

An R-module M is faithfully flat iff it is flat and for all linear maps f, the map id ⊗ f = 0, if and only if f = 0.

theorem Module.FaithfullyFlat.trans (R : Type u_1) [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] (M : Type u_3) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [FaithfullyFlat R S] [FaithfullyFlat S M] : FaithfullyFlat R M

If S is a faithfully flat R-algebra, then any faithfully flat S-Module is faithfully flat as an R-module.

@[deprecated Module.FaithfullyFlat.trans (since := "2024-11-08")]

theorem Module.FaithfullyFlat.comp (R : Type u_1) [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] (M : Type u_3) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [FaithfullyFlat R S] [FaithfullyFlat S M] : FaithfullyFlat R M

Alias of Module.FaithfullyFlat.trans.

---

If S is a faithfully flat R-algebra, then any faithfully flat S-Module is faithfully flat as an R-module.

instance Module.FaithfullyFlat.instTensorProduct (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (S : Type u_1) [CommRing S] [Algebra R S] [FaithfullyFlat R M] : FaithfullyFlat S (TensorProduct R S M)

Faithful flatness is preserved by arbitrary base change.

theorem Module.Flat.of_flat_tensorProduct (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (S : Type u_1) [CommRing S] [Algebra R S] [FaithfullyFlat R S] [Flat S (TensorProduct R S M)] : Flat R M

Flat descends along faithfully flat ring maps.

theorem Module.Flat.iff_flat_tensorProduct (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (S : Type u_1) [CommRing S] [Algebra R S] [FaithfullyFlat R S] : Flat S (TensorProduct R S M) ↔ Flat R M