Commit 2025-01-17 07:37 66e14198

feat(RingTheory): flatness over a semiring (#19115) A module over a ring is said to be flat if tensoring with it preserves injective linear maps. The same definition remains reasonable over a semiring, because (1) injective linear maps still coincides with monomorphisms over a semiring*; (2) projective modules (in particular, free modules) and localizations are still examples of flat modules over a semiring; (3) we recently fixed the definition of linear independence over semirings (#18426), and flatness of S/R means (1:S) ⊗[R] · preserves linear independence. In fact (2) is the main motivation for this PR: it allows us to unify results about free modules (e.g. polynomial algebras) and localizations over a semiring. There is a caveat in the definition: injective linear maps need to come from a particular universe, as we can't quantify over all universes. Over a ring, using Baer's criterion and character modules, we may restrict to inclusion maps of (f.g.) ideals, and that was the definition adopted in Mathlib. However, the proof doesn't work over a semiring due to three difficulties: (1) Baer's criterion for injective modules doesn't work over a semiring; (2) Q/Z isn't an injective object in the category of AddCommMonoids, in fact this category doesn't have enough injectives; (3) homs into Q/Z does not distinguish points in an AddCommMonoid. However, we can still show that it suffices to consider injective linear maps between modules in the same universe as the semiring, using the fact that every module is the direct limit of its f.g. submodules, and that taking tensor products commutes with taking direct limits: of course, f.g. modules fit in the same universe as the semiring. We therefore change the definition of flatness to state preservation of injectivity of inclusion of f.g. submodules into f.g. modules in the same universe as the semiring. As we reorder the lemmas in Flat/Basic.lean, We also change all the iff lemmas to use implicit arguments; several other files need to be fixed for this reason, and as we fix them, we also generalize them to CommSemirings and in some cases golf the proofs. (*) There are more epimorphisms than surjective homs, e.g. the inclusion of N in Z.