Flat modules

M is flat if · ⊗ M preserves finite limits (equivalently, pullbacks, or equalizers). If R is a ring, an R-module M is flat if and only if it is mono-flat, and to show a module is flat, it suffices to check inclusions of finitely generated ideals into R. See https://stacks.math.columbia.edu/tag/00HD.

Main theorems

• Module.Flat.iff_characterModule_injective: CharacterModule M is an injective module iff M is flat.
• Module.Flat.iff_lTensor_injective, Module.Flat.iff_rTensor_injective, Module.Flat.iff_lTensor_injective', Module.Flat.iff_rTensor_injective': A module M over a ring R 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.

theorem Module.Flat.injective_characterModule_iff_rTensor_preserves_injective_linearMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] : 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'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.rTensor M f)

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

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

CharacterModule M is an injective module iff M is flat. See [Lam64] for a self-contained proof.

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

CharacterModule M is Baer iff M is flat.

theorem Module.Flat.iff_rTensor_injective' {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] : 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.

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

The lTensor-variant of iff_rTensor_injective'. .

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

A module M over a ring R 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_lTensor_injective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] : 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_lift_lsmul_comp_subtype_injective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] : Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(TensorProduct.lift (LinearMap.lsmul R M ∘ₗ Submodule.subtype I))

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