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 preserves injectivity in the ring's universe (or higher).

Implementation notes

In Module.Flat.iff_rTensor_preserves_injective_linearMap, we require that the universe level of the ring is lower than or equal to that of the module. This requirement is to make sure ideals of the ring can be lifted to the universe of the module. It is unclear if this lemma also holds when the module lives in a lower universe.

TODO

• Generalize flatness to noncommutative rings.

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))

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.out {R : Type u} {M : Type v} : ∀ {inst : CommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M} [self : 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)

Equations

• ⋯ = inst

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

Equations

• ⋯ = ⋯

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_4) {N : Type u_5} {P : Type u_6} [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.

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.

Equations

• ⋯ = ⋯

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

Free R-modules over discrete types are flat.

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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.

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] : 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.rTensor M L)

M is flat if and only if f ⊗ 𝟙 M is injective whenever f is an injective linear map.

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] : 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.

theorem Module.Flat.lTensor_exact {R : Type u} (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Small.{v, u} R] [flat : Module.Flat R M] ⦃N : Type v⦄ ⦃N' : Type v⦄ ⦃N'' : Type v⦄ [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)

theorem Module.Flat.rTensor_exact {R : Type u} (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Small.{v, u} R] [flat : Module.Flat R M] ⦃N : Type v⦄ ⦃N' : Type v⦄ ⦃N'' : Type v⦄ [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)

theorem Module.Flat.iff_lTensor_exact {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Small.{v, u} R] : 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 a left exact functor.

theorem Module.Flat.iff_rTensor_exact {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Small.{v, u} R] : 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 a left exact functor.