Commit 2024-03-02 17:21 146948d7

View on Github →

feat(RingTheory/Flat/Basic): a module is flat iff tensoring preserves injectivity of linear maps (#9120)

Estimated changes

Modified Mathlib/Algebra/Module/CharacterModule.lean

added theorem CharacterModule.dual_rTensor_conj_homEquiv

modified theorem CharacterModule.dual_surjective_iff_injective

added theorem rTensor_injective_iff_lcomp_surjective

Modified Mathlib/Algebra/Module/Injective.lean

modified theorem Module.ulift_injective_of_injective

Modified Mathlib/LinearAlgebra/TensorProduct.lean

added theorem LinearMap.lid_comp_rTensor

Modified Mathlib/RingTheory/Flat/Basic.lean

added theorem Module.Flat.iff_characterModule_baer

added theorem Module.Flat.iff_characterModule_injective

added theorem Module.Flat.iff_rTensor_preserves_injective_linearMap

added theorem Module.Flat.injective_characterModule_iff_rTensor_preserves_injective_linearMap

modified theorem Module.Flat.lTensor_inj_iff_rTensor_inj

added theorem Module.Flat.preserves_injective_linearMap