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.
• Define flat R-algebras
• Define flat ring homomorphisms
  • Show that the identity is flat
  • Show that composition of flat morphisms is flat
• 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.

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

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

Equations

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

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

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

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.

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.

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

• (_ : Module.Flat R (DirectSum ι fun (i : ι) => M i)) = (_ : Module.Flat R (DirectSum ι fun (i : ι) => M i))

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

Free R-modules over discrete types are flat.

Equations

• (_ : Module.Flat R (ι →₀ R)) = (_ : Module.Flat R (ι →₀ R))

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

Equations

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

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

Equations

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