Tensoring with a flat module is an exact functor

In this file we prove that tensoring with a flat module is an exact functor.

Main results

• Module.Flat.iff_lTensor_preserves_shortComplex_exact: an R-module M is flat if and only if for every exact sequence A ⟶ B ⟶ C, M ⊗ A ⟶ M ⊗ B ⟶ M ⊗ C is also exact.

• Module.Flat.iff_rTensor_preserves_shortComplex_exact: an R-module M is flat if and only if for every short exact sequence A ⟶ B ⟶ C, A ⊗ M ⟶ B ⊗ M ⟶ C ⊗ M is also exact.

TODO

• Prove that tensoring with a flat module is an exact functor in the sense that it preserves both finite limits and colimits.
• Relate flatness with Tor

theorem Module.Flat.lTensor_shortComplex_exact {R : Type u} [CommRing R] (M : ModuleCat R) [Flat R ↑M] (C : CategoryTheory.ShortComplex (ModuleCat R)) (hC : C.Exact) : (C.map (CategoryTheory.MonoidalCategory.tensorLeft M)).Exact

theorem Module.Flat.rTensor_shortComplex_exact {R : Type u} [CommRing R] (M : ModuleCat R) [Flat R ↑M] (C : CategoryTheory.ShortComplex (ModuleCat R)) (hC : C.Exact) : (C.map (CategoryTheory.MonoidalCategory.tensorRight M)).Exact

theorem Module.Flat.iff_lTensor_preserves_shortComplex_exact {R : Type u} [CommRing R] (M : ModuleCat R) : Flat R ↑M ↔ ∀ (C : CategoryTheory.ShortComplex (ModuleCat R)), C.Exact → (C.map (CategoryTheory.MonoidalCategory.tensorLeft M)).Exact

theorem Module.Flat.iff_rTensor_preserves_shortComplex_exact {R : Type u} [CommRing R] (M : ModuleCat R) : Flat R ↑M ↔ ∀ (C : CategoryTheory.ShortComplex (ModuleCat R)), C.Exact → (C.map (CategoryTheory.MonoidalCategory.tensorRight M)).Exact