Extensions of flat modules

In a short exact sequence 0 → M → N → P → 0 of modules over a commutative ring, if M and P are flat, then N is flat. This allows flatness of a quotient to be established from simpler subquotients without requiring the ambient module to be flat. Likewise, if N and P are flat, then so is M: a submodule of a flat module with flat quotient is flat.

Main results

• Function.Exact.flat_of_injective_of_surjective: the middle term of a short exact sequence with flat outer terms is flat.
• Module.Flat.of_exact_of_lTensor_quotient_injective: for an exact pair M → N → P → 0 with N flat, the cokernel P is flat when M → N stays injective after tensoring with every R ⧸ I.
• Function.Exact.flat_left_of_injective_of_surjective: the first term of a short exact sequence whose other two terms are flat is flat.

theorem Function.Exact.flat_of_injective_of_surjective {R : Type u} {M : Type v} {N : Type w} {P : Type x} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Exact ⇑f ⇑g) (hf : Injective ⇑f) (hg : Surjective ⇑g) [Module.Flat R M] [Module.Flat R P] : Module.Flat R N

The middle term of a short exact sequence with flat outer terms is flat.

theorem Module.Flat.of_exact_of_lTensor_quotient_injective {R : Type u} {M : Type v} {N : Type w} {P : Type x} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [Flat R N] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (hexact : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) (hf : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) f)) : Flat R P

A cokernel is flat when the presentation stays injective modulo ideals. Let f : M → N and g : N → P be exact with g surjective and N flat over R. If id ⊗ f : (R ⧸ I) ⊗[R] M → (R ⧸ I) ⊗[R] N is injective for every finitely generated ideal I, then P is flat over R. In terms of Tor, the hypothesis kills the image of Tor₁(R ⧸ I, P) in (R ⧸ I) ⊗[R] M, and flatness of N makes Tor₁(R ⧸ I, P) → (R ⧸ I) ⊗[R] M injective. No flatness of M and no injectivity of f is needed.

theorem Function.Exact.flat_left_of_injective_of_surjective {R : Type u} {M : Type v} {N : Type w} {P : Type x} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Exact ⇑f ⇑g) (hf : Injective ⇑f) (hg : Surjective ⇑g) [Module.Flat R N] [Module.Flat R P] : Module.Flat R M

The first term of a short exact sequence whose middle and last terms are flat is flat.