Commit 2025-09-27 16:22 ad69e75c

feat(Mathlib/AlgebraicGeometry/Morphisms/Flat): add simple properties of flat maps (#30021) This PR adds two lemmas for faithfully flat ring maps and flat surjective scheme morphisms.

• RingHom.FaithfullyFlat.injective: Proves that a faithfully flat ring map is injective. (This is built on the pre-existing lemma Module.FaithfullyFlat.tensorProduct_mk_injective, which states that If `B` is a faithfully flat `A`-module and `M` is any `A`-module, the canonical map `M →ₗ[A] B ⊗[A] M` is injective.)
• AlgebraicGeometry.Flat.epi_of_flat_surjective: Proves that a flat surjective morphism of schemes is an epimorphism in the category of schemes. For this, Mathlib/AlgebraicGeometry/Morphisms/Flat.lean now imports Mathlib.RingTheory.RingHom.FaithfullyFlat to use the former.