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 . This result is not yet formalised.

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

TODO #

Show that tensoring with a flat module preserves injective morphisms. Show that this is equivalent to be flat. See . To do this, it is probably a good idea to think about a suitable categorical induction principle that should be applied to the category of R-modules, and that will take care of the administrative side of the proof.
Show that flatness is stable under base change (aka extension of scalars) For base change, it will be very useful to have a "characteristic predicate" instead of relying on the construction A ⊗ B. Indeed, such a predicate should allow us to treat both A[X] and A ⊗ R[X] as the base change of R[X] to A. (Similar examples exist with Fin n → R, R × R, ℤ[i] ⊗ ℝ, etc...)
Generalize flatness to noncommutative rings.

source

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⦄, Ideal.FG I → Function.Injective ⇑(TensorProduct.lift (LinearMap.lsmul R M ∘ₗ Submodule.subtype I))

Instances

source

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

Module.Flat R R

Equations

(_ : Module.Flat R R) = (_ : Module.Flat R R)

source

theorem Module.Flat.iff_rTensor_injective (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] :

Module.Flat R M ↔ ∀ ⦃I : Ideal R⦄, Ideal.FG I → 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. -

source

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

source

theorem Module.Flat.lTensor_inj_iff_rTensor_inj (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] {N : Type u_1} {P : Type u_2} [AddCommGroup N] [AddCommGroup P] [Module R N] [Module R P] (f : N →ₗ[R] P) :

Function.Injective ⇑(LinearMap.lTensor M f) ↔ Function.Injective ⇑(LinearMap.rTensor M f)

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

source

theorem Module.Flat.iff_lTensor_injective (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] :

Module.Flat R M ↔ ∀ ⦃I : Ideal R⦄, Ideal.FG I → Function.Injective ⇑(LinearMap.lTensor M (Submodule.subtype I))

The lTensor-variant of iff_rTensor_injective. .

source

theorem Module.Flat.iff_lTensor_injective' (R : Type u) [CommRing R] (M : Type v) [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'. .

source

theorem Module.Flat.of_retract (R : Type u) [CommRing R] (M : Type v) [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.

source

theorem Module.Flat.of_linearEquiv (R : Type u) [CommRing R] (M : Type v) [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.

source

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