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.comp: 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 : Prop

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

• out : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(TensorProduct.lift (LinearMap.lsmul R M ∘ₗ Submodule.subtype I))
• 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] : Module.FaithfullyFlat R M ↔ Module.Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤

theorem Module.FaithfullyFlat.submodule_ne_top {R : Type u} {M : Type v} : ∀ {inst : CommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M} [self : Module.FaithfullyFlat R M] ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤

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

Equations

• ⋯ = ⋯

theorem Module.FaithfullyFlat.iff_flat_and_proper_ideal (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Module.FaithfullyFlat R M ↔ Module.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] : Module.FaithfullyFlat R M ↔ Module.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 : Module.FaithfullyFlat R M] (N : Type u_1) [AddCommGroup N] [Module R N] [Nontrivial N] : Nontrivial (TensorProduct R N M)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem Module.FaithfullyFlat.rTensor_reflects_triviality (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Module.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] [Module.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] : Module.FaithfullyFlat R M ↔ Module.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] : Module.FaithfullyFlat R M ↔ Module.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] : Module.FaithfullyFlat R M ↔ Module.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] : Module.FaithfullyFlat R M ↔ Module.Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Subsingleton (TensorProduct R M N) → Subsingleton N

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 : Module.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 : Module.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 : Module.FaithfullyFlat R M] (ex : Function.Exact ⇑(LinearMap.lTensor M l12) ⇑(LinearMap.lTensor M l23)) : Function.Exact ⇑l12 ⇑l23

theorem Module.FaithfullyFlat.exact_iff_rTensor_exact (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [fl : Module.FaithfullyFlat R M] {N1 : Type (max u v)} [AddCommGroup N1] [Module R N1] {N2 : Type (max u v)} [AddCommGroup N2] [Module R N2] {N3 : Type (max u v)} [AddCommGroup N3] [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_rTensor_exact (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Module.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] : Module.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 : Module.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 : Module.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.

theorem Module.FaithfullyFlat.iff_zero_iff_lTensor_zero (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Module.FaithfullyFlat R M ↔ Module.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] : Module.FaithfullyFlat R M ↔ Module.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.of_linearEquiv (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [fl : Module.FaithfullyFlat R M] (M' : Type u_1) [AddCommGroup M'] [Module R M'] (e : M' ≃ₗ[R] M) : Module.FaithfullyFlat R M'

An R-module linearly equivalent to a faithfully flat R-module is faithfully flat.

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] [Module.FaithfullyFlat R S] [Module.FaithfullyFlat S M] : Module.FaithfullyFlat R M

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