Flat modules

A module M over a commutative ring R is flat if for all finitely generated ideals I of R, the canonical map I ⊗ M →ₗ M is injective.

This is equivalent to the claim that for all injective R-linear maps f : M₁ → M₂ the induced map M₁ ⊗ M → M₂ ⊗ M is injective. See https://stacks.math.columbia.edu/tag/00HD.

Main declaration

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

Main theorems

• Module.Flat.of_retract: retracts of flat modules are flat
• Module.Flat.of_linearEquiv: modules linearly equivalent to a flat modules are flat
• Module.Flat.directSum: arbitrary direct sums of flat modules are flat
• Module.Flat.of_free: free modules are flat
• Module.Flat.of_projective: projective modules are flat
• Module.Flat.preserves_injective_linearMap: If M is a flat module then tensoring with M preserves injectivity of linear maps. This lemma is fully universally polymorphic in all arguments, i.e. R, M and linear maps N → N' can all have different universe levels.
• Module.Flat.iff_rTensor_preserves_injective_linearMap: a module is flat iff tensoring modules in the higher universe preserves injectivity .
• Module.Flat.lTensor_exact: If M is a flat module then tensoring with M is an exact functor. This lemma is fully universally polymorphic in all arguments, i.e. R, M and linear maps N → N' → N'' can all have different universe levels.
• Module.Flat.iff_lTensor_exact: a module is flat iff tensoring modules in the higher universe is an exact functor.

TODO

• Generalize flatness to noncommutative rings.

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

An R-module M is flat if for all finitely generated ideals I of R, the canonical map I ⊗ M →ₗ M is injective.

• out ⦃I : Ideal R⦄ : I.FG → Function.Injective ⇑(TensorProduct.lift (LinearMap.lsmul R M ∘ₗ Submodule.subtype I))

theorem Module.flat_iff (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(TensorProduct.lift (LinearMap.lsmul R M ∘ₗ Submodule.subtype I))

instance Module.Flat.instSubalgebraToSubmodule {R : Type u} [CommRing R] {S : Type v} [Ring S] [Algebra R S] (A : Subalgebra R S) [Module.Flat R ↥A] : Module.Flat R ↥(Subalgebra.toSubmodule A)

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

theorem Module.Flat.iff_rTensor_injective (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I))

An R-module M is flat iff for all finitely generated ideals I of R, the tensor product of the inclusion I → R and the identity M → M is injective. See iff_rTensor_injective' to extend to all ideals I. -

theorem Module.Flat.iff_rTensor_injective' (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I))

An R-module M is flat iff for all ideals I of R, the tensor product of the inclusion I → R and the identity M → M is injective. See iff_rTensor_injective to restrict to finitely generated ideals I. -

@[deprecated LinearMap.lTensor_inj_iff_rTensor_inj]

theorem Module.Flat.lTensor_inj_iff_rTensor_inj {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : Function.Injective ⇑(LinearMap.lTensor M f) ↔ Function.Injective ⇑(LinearMap.rTensor M f)

Alias of LinearMap.lTensor_inj_iff_rTensor_inj.

---

Given a linear map f : N → P, f ⊗ M is injective if and only if M ⊗ f is injective.

theorem Module.Flat.iff_lTensor_injective (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(LinearMap.lTensor M (Submodule.subtype I))

The lTensor-variant of iff_rTensor_injective. .

theorem Module.Flat.iff_lTensor_injective' (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(LinearMap.lTensor M (Submodule.subtype I))

The lTensor-variant of iff_rTensor_injective'. .

theorem Module.Flat.of_retract (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (N : Type w) [AddCommGroup N] [Module R N] [f : Module.Flat R M] (i : N →ₗ[R] M) (r : M →ₗ[R] N) (h : r ∘ₗ i = LinearMap.id) : Module.Flat R N

A retract of a flat R-module is flat.

theorem Module.Flat.of_linearEquiv (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (N : Type w) [AddCommGroup N] [Module R N] [f : Module.Flat R M] (e : N ≃ₗ[R] M) : Module.Flat R N

A R-module linearly equivalent to a flat R-module is flat.

theorem Module.Flat.equiv_iff (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (N : Type w) [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) : Module.Flat R M ↔ Module.Flat R N

If an R-module M is linearly equivalent to another R-module N, then M is flat if and only if N is flat.

instance Module.Flat.ulift (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] : Module.Flat R (ULift.{v', v} M)

theorem Module.Flat.of_ulift (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R (ULift.{v', v} M)] : Module.Flat R M

instance Module.Flat.shrink (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', v} M] [Module.Flat R M] : Module.Flat R (Shrink.{v', v} M)

theorem Module.Flat.of_shrink (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', v} M] [Module.Flat R (Shrink.{v', v} M)] : Module.Flat R M

instance Module.Flat.directSum (R : Type u) [CommRing R] (ι : Type v) (M : ι → Type w) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [F : ∀ (i : ι), Module.Flat R (M i)] : Module.Flat R (DirectSum ι fun (i : ι) => M i)

A direct sum of flat R-modules is flat.

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

Free R-modules over discrete types are flat.

instance Module.Flat.of_free (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] : Module.Flat R M

theorem Module.Flat.of_projective_surjective (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (ι : Type w) [Module.Projective R M] (p : (ι →₀ R) →ₗ[R] M) (hp : Function.Surjective ⇑p) : Module.Flat R M

A projective module with a discrete type of generator is flat

instance Module.Flat.of_projective (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [h : Module.Projective R M] : Module.Flat R M

theorem Module.Flat.injective_characterModule_iff_rTensor_preserves_injective_linearMap (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Module.Injective R (CharacterModule M) ↔ ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (L : N →ₗ[R] N'), Function.Injective ⇑L → Function.Injective ⇑(LinearMap.rTensor M L)

Define the character module of M to be M →+ ℚ ⧸ ℤ. The character module of M is an injective module if and only if L ⊗ 𝟙 M is injective for any linear map L in the same universe as M.

theorem Module.Flat.iff_characterModule_baer {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ Module.Baer R (CharacterModule M)

CharacterModule M is Baer iff M is flat.

theorem Module.Flat.iff_characterModule_injective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Small.{v, u} R] : Module.Flat R M ↔ Module.Injective R (CharacterModule M)

CharacterModule M is an injective module iff M is flat.

theorem Module.Flat.rTensor_preserves_injective_linearMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [h : Module.Flat R M] (L : N →ₗ[R] N') (hL : Function.Injective ⇑L) : Function.Injective ⇑(LinearMap.rTensor M L)

If M is a flat module, then f ⊗ 𝟙 M is injective for all injective linear maps f.

@[deprecated Module.Flat.rTensor_preserves_injective_linearMap]

theorem Module.Flat.preserves_injective_linearMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [h : Module.Flat R M] (L : N →ₗ[R] N') (hL : Function.Injective ⇑L) : Function.Injective ⇑(LinearMap.rTensor M L)

Alias of Module.Flat.rTensor_preserves_injective_linearMap.

---

If M is a flat module, then f ⊗ 𝟙 M is injective for all injective linear maps f.

instance Module.Flat.instTensorProduct {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] {S : Type u_1} [CommRing S] [Algebra R S] [Module S M] [IsScalarTower R S M] [Module.Flat S M] [Module.Flat R N] : Module.Flat S (TensorProduct R M N)

theorem Module.Flat.lTensor_preserves_injective_linearMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [Module.Flat R M] (L : N →ₗ[R] N') (hL : Function.Injective ⇑L) : Function.Injective ⇑(LinearMap.lTensor M L)

If M is a flat module, then 𝟙 M ⊗ f is injective for all injective linear maps f.

theorem Module.Flat.iff_rTensor_preserves_injective_linearMap' (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] [Small.{v', v} M] : Module.Flat R M ↔ ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.rTensor M f)

M is flat if and only if f ⊗ 𝟙 M is injective whenever f is an injective linear map. See Module.Flat.iff_rTensor_preserves_injective_linearMap to specialize the universe of N, N', N'' to Type (max u v).

theorem Module.Flat.iff_rTensor_preserves_injective_linearMap (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ ⦃N N' : Type (max u v)⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.rTensor M f)

M is flat if and only if f ⊗ 𝟙 M is injective whenever f is an injective linear map. See Module.Flat.iff_rTensor_preserves_injective_linearMap' to generalize the universe of N, N', N'' to any universe that is higher than R and M.

theorem Module.Flat.iff_lTensor_preserves_injective_linearMap' (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] [Small.{v', v} M] : Module.Flat R M ↔ ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (L : N →ₗ[R] N'), Function.Injective ⇑L → Function.Injective ⇑(LinearMap.lTensor M L)

M is flat if and only if 𝟙 M ⊗ f is injective whenever f is an injective linear map. See Module.Flat.iff_lTensor_preserves_injective_linearMap to specialize the universe of N, N', N'' to Type (max u v).

theorem Module.Flat.iff_lTensor_preserves_injective_linearMap (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ ⦃N N' : Type (max u v)⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)

M is flat if and only if 𝟙 M ⊗ f is injective whenever f is an injective linear map. See Module.Flat.iff_lTensor_preserves_injective_linearMap' to generalize the universe of N, N', N'' to any universe that is higher than R and M.

theorem Module.Flat.lTensor_exact {R : Type u} (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] ⦃N : Type u_1⦄ ⦃N' : Type u_2⦄ ⦃N'' : Type u_3⦄ [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [Module R N] [Module R N'] [Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄ (exact : Function.Exact ⇑f ⇑g) : Function.Exact ⇑(LinearMap.lTensor M f) ⇑(LinearMap.lTensor M g)

If M is flat then M ⊗ - is an exact functor.

theorem Module.Flat.rTensor_exact {R : Type u} (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] ⦃N : Type u_1⦄ ⦃N' : Type u_2⦄ ⦃N'' : Type u_3⦄ [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [Module R N] [Module R N'] [Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄ (exact : Function.Exact ⇑f ⇑g) : Function.Exact ⇑(LinearMap.rTensor M f) ⇑(LinearMap.rTensor M g)

If M is flat then - ⊗ M is an exact functor.

theorem Module.Flat.iff_lTensor_exact' {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] [Small.{v', v} M] : Module.Flat R M ↔ ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄, Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.lTensor M f) ⇑(LinearMap.lTensor M g)

M is flat if and only if M ⊗ - is an exact functor. See Module.Flat.iff_lTensor_exact to specialize the universe of N, N', N'' to Type (max u v).

theorem Module.Flat.iff_lTensor_exact {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ ⦃N N' N'' : Type (max u v)⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄, Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.lTensor M f) ⇑(LinearMap.lTensor M g)

M is flat if and only if M ⊗ - is an exact functor. See Module.Flat.iff_lTensor_exact' to generalize the universe of N, N', N'' to any universe that is higher than R and M.

theorem Module.Flat.iff_rTensor_exact' {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] [Small.{v', v} M] : Module.Flat R M ↔ ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄, Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.rTensor M f) ⇑(LinearMap.rTensor M g)

M is flat if and only if - ⊗ M is an exact functor. See Module.Flat.iff_rTensor_exact to specialize the universe of N, N', N'' to Type (max u v).

theorem Module.Flat.iff_rTensor_exact {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ ⦃N N' N'' : Type (max u v)⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄, Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.rTensor M f) ⇑(LinearMap.rTensor M g)

M is flat if and only if - ⊗ M is an exact functor. See Module.Flat.iff_rTensor_exact' to generalize the universe of N, N', N'' to any universe that is higher than R and M.

theorem Module.Flat.tensorProduct_mapIncl_injective_of_right {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] (p : Submodule R M) (q : Submodule R N) [Module.Flat R M] [Module.Flat R ↥q] : Function.Injective ⇑(TensorProduct.mapIncl p q)

If p and q are submodules of M and N respectively, and M and q are flat, then p ⊗ q → M ⊗ N is injective.

theorem Module.Flat.tensorProduct_mapIncl_injective_of_left {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] (p : Submodule R M) (q : Submodule R N) [Module.Flat R ↥p] [Module.Flat R N] : Function.Injective ⇑(TensorProduct.mapIncl p q)

If p and q are submodules of M and N respectively, and N and p are flat, then p ⊗ q → M ⊗ N is injective.

theorem Algebra.TensorProduct.includeLeft_injective {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommRing R] [Ring A] [Algebra R A] [Ring B] [Algebra R B] [CommSemiring S] [Algebra S A] [SMulCommClass R S A] [Module.Flat R A] (hb : Function.Injective ⇑(algebraMap R B)) : Function.Injective ⇑Algebra.TensorProduct.includeLeft

theorem Algebra.TensorProduct.includeRight_injective {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommRing R] [Ring A] [Algebra R A] [Ring B] [Algebra R B] [Module.Flat R B] (ha : Function.Injective ⇑(algebraMap R A)) : Function.Injective ⇑Algebra.TensorProduct.includeRight

theorem TensorProduct.nontrivial_of_linearMap_injective_of_flat_left (R : Type u_1) [CommRing R] (M : Type u_2) (N : Type u_3) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : R →ₗ[R] N) (h : Function.Injective ⇑f) [Module.Flat R M] [Nontrivial M] : Nontrivial (TensorProduct R M N)

If M, N are R-modules, there exists an injective R-linear map from R to N, and M is a nontrivial flat R-module, then M ⊗[R] N is nontrivial.

theorem TensorProduct.nontrivial_of_linearMap_injective_of_flat_right (R : Type u_1) [CommRing R] (M : Type u_2) (N : Type u_3) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : R →ₗ[R] M) (h : Function.Injective ⇑f) [Module.Flat R N] [Nontrivial N] : Nontrivial (TensorProduct R M N)

If M, N are R-modules, there exists an injective R-linear map from R to M, and N is a nontrivial flat R-module, then M ⊗[R] N is nontrivial.

theorem Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_flat_left (R : Type u_1) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (h : Function.Injective ⇑(algebraMap R B)) [Module.Flat R A] [Nontrivial A] : Nontrivial (TensorProduct R A B)

If A, B are R-algebras, R injects into B, and A is a nontrivial flat R-algebra, then A ⊗[R] B is nontrivial.

theorem Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_flat_right (R : Type u_1) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (h : Function.Injective ⇑(algebraMap R A)) [Module.Flat R B] [Nontrivial B] : Nontrivial (TensorProduct R A B)

If A, B are R-algebras, R injects into A, and B is a nontrivial flat R-algebra, then A ⊗[R] B is nontrivial.