Commit 2024-11-16 08:30 2c6b8bbf

View on Github →

feat: tensor product of two flat modules is flat (#18745) Add the missing Flat R (M ⊗[R] N) instance. Add two lemmas relating flatness to injectivity of mapIncl. Clean up the file Flat/Stability, renaming Flat.comp to Flat.trans. Also rename Algebra.Flat.comp and FaithfullyFlat.comp.

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

added theorem LinearMap.rTensor_tensor

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

added theorem TensorProduct.AlgebraTensorModule.rTensor_tensor

Modified Mathlib/RingTheory/Flat/Algebra.lean

deleted theorem Algebra.Flat.comp

added theorem Algebra.Flat.trans

Modified Mathlib/RingTheory/Flat/Basic.lean

added theorem Module.Flat.tensorProduct_mapIncl_injective_of_left

added theorem Module.Flat.tensorProduct_mapIncl_injective_of_right

Modified Mathlib/RingTheory/Flat/FaithfullyFlat.lean

deleted theorem Module.FaithfullyFlat.comp

added theorem Module.FaithfullyFlat.trans

Modified Mathlib/RingTheory/Flat/Stability.lean

deleted theorem Module.Flat.comp

modified theorem Module.Flat.isBaseChange

modified theorem Module.Flat.of_isLocalizedModule

added theorem Module.Flat.trans