feat(AlgebraicGeometry/Modules): flat sheaves of modules

Define flatness of a sheaf of modules `F` on a scheme `X` over a base `S`
via a morphism `f : X ⟶ S`: `Scheme.Modules.FlatAt f F x` is the pointwise
condition that the stalk `F_x` is flat over `𝒪_{S, f(x)}` (acting through
`f.stalkMap x`), and `Scheme.Modules.Flat f F` asserts `∀ x, FlatAt f F x`.

Main results:
* `Scheme.Modules.flat_tilde_iff` / `flat_tilde_iff_of_algebra`: affine
  criteria identifying flatness of `M^~` with flatness of `M`.
* `Scheme.Modules.Flat.comp`: transitivity along a flat base.
* `Scheme.Modules.flat_comp_isOpenImmersion_iff`: locality on the base.
* `Scheme.Modules.flat_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