Commit 2025-02-12 21:23 bdd34c37

View on Github →

feat(RingTheory/FaithfullyFlat): equivalent characterizations for algebras (#20725) Let B be an A-algebra. Then

B is faithfully flat over A if and only if it is flat and induces a surjective map on prime spectra.
If B is flat and local over A, it is faithfully flat. Co-authored by: Sihan Su ssh@stu.pku.edu.cn Co-authored by: Yi Song sif4delta0@mail.ustc.edu.cn

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Exact.lean

added theorem LinearMap.exact_zero_iff_injective

added theorem LinearMap.exact_zero_iff_surjective

Created Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean

added theorem Ideal.comap_map_eq_self_of_faithfullyFlat

added theorem Ideal.comap_surjective_of_faithfullyFlat

added theorem Ideal.exists_isPrime_liesOver_of_faithfullyFlat

added theorem Module.FaithfullyFlat.of_flat_of_isLocalHom

added theorem Module.FaithfullyFlat.of_specComap_surjective

added theorem Module.FaithfullyFlat.tensorProduct_mk_injective

added theorem PrimeSpectrum.specComap_surjective_of_faithfullyFlat

Modified Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean

deleted theorem Module.FaithfullyFlat.exact_iff_rTensor_exact

added theorem Module.FaithfullyFlat.lTensor_exact_iff_exact

added theorem Module.FaithfullyFlat.lTensor_injective_iff_injective

added theorem Module.FaithfullyFlat.lTensor_surjective_iff_surjective

added theorem Module.FaithfullyFlat.rTensor_exact_iff_exact

Modified Mathlib/RingTheory/Spectrum/Prime/RingHom.lean

added theorem PrimeSpectrum.mem_range_comap_iff

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

added theorem Algebra.TensorProduct.mk_one_injective_of_isScalarTower