feat(AlgebraicGeometry/Modules): flat sheaves of modules

Define relative flatness of a sheaf of modules `F` on a scheme `X` over a
base `S` via a morphism `f : X ⟶ S` (`AlgebraicGeometry.IsRelativeFlat`):
for every point `x`, the stalk `F_x` is flat over the local ring
`𝒪_{S, f(x)}` acting through `f.stalkMap x`.

Main results:
* `isRelativeFlat_tilde_iff` and `isRelativeFlat_tilde_iff_of_algebra`: the
  affine criteria identifying relative flatness of `M^~` with flatness of `M`.
* `IsRelativeFlat.comp`: transitivity along a flat base.
* `isRelativeFlat_comp_isOpenImmersion_iff`: locality on the base.
* `isRelativeFlat_iff_forall_openCover`: locality on the source.

Also adds supporting flatness lemmas to `RingTheory`:
* `Module.Flat.tensor_tower` (`RingTheory/Flat/Stability`)
* `Module.flat_iff_forall_localizedModule_prime`,
  `Module.Flat.localizedModule_base`,
  `Module.flat_iff_forall_localizedModule_prime_of_algebra`
  (`RingTheory/Flat/Localization`)
* `Module.Flat.trans_compHom`, `Module.Flat.compHom_bijective_iff`
  (`RingTheory/RingHom/Flat`)

Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Author: 3 people

Mathlib.lean

@@ -1396,6 +1396,7 @@ public import Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
 public import Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
 public import Mathlib.AlgebraicGeometry.Limits
 public import Mathlib.AlgebraicGeometry.LimitsOver
+public import Mathlib.AlgebraicGeometry.Modules.Flat
 public import Mathlib.AlgebraicGeometry.Modules.Presheaf
 public import Mathlib.AlgebraicGeometry.Modules.Sheaf
 public import Mathlib.AlgebraicGeometry.Modules.Tilde