diff --git a/Mathlib.lean b/Mathlib.lean
index 4308c4d1d9eeb9..57c4f7a5f99e50 100644
--- a/Mathlib.lean
+++ b/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
diff --git a/Mathlib/Algebra/Module/RingHom.lean b/Mathlib/Algebra/Module/RingHom.lean
index 6df2b99a7a5b87..247ba89e9be9b9 100644
--- a/Mathlib/Algebra/Module/RingHom.lean
+++ b/Mathlib/Algebra/Module/RingHom.lean
@@ -60,9 +60,12 @@ abbrev Module.compHom [Semiring S] (f : S →+* R) : Module S M :=
     -- Somehow, now that `SMul` is heterogeneous, it can't unfold earlier fields of a definition for
     -- use in later fields.  See
     -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Heterogeneous.20scalar.20multiplication
-    -- TODO(jmc): there should be a rw-lemma `smul_comp` close to `SMulZeroClass.compFun`
     add_smul := fun r s x => show f (r + s) • x = f r • x + f s • x by simp [add_smul] }
 
+lemma Module.compHom_smul [Semiring S] (f : S →+* R) (s : S) (m : M) :
+    letI := Module.compHom M f; s • m = f s • m :=
+  rfl
+
 end AddCommMonoid
 
 /-- A ring homomorphism `f : R →+* M` defines a module structure by `r • x = f r * x`.
diff --git a/Mathlib/AlgebraicGeometry/Modules/Flat.lean b/Mathlib/AlgebraicGeometry/Modules/Flat.lean
new file mode 100644
index 00000000000000..54c5747e880441
--- /dev/null
+++ b/Mathlib/AlgebraicGeometry/Modules/Flat.lean
@@ -0,0 +1,356 @@
+/-
+Copyright (c) 2026 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+module
+
+public import Mathlib.AlgebraicGeometry.Modules.Tilde
+public import Mathlib.AlgebraicGeometry.Morphisms.Flat
+
+/-!
+# Flat sheaves of modules
+
+Given a morphism of schemes `f : X ⟶ S` and an `𝒪_X`-module `F`, we say that `F` is
+*flat* over `S` (via `f`) if for every point `x ∈ X`, the stalk `F_x` is a flat module over the
+local ring `𝒪_{S, f(x)}`, where `𝒪_{S, f(x)}` acts on `F_x` through the local ring homomorphism
+`f.stalkMap x : 𝒪_{S, f(x)} ⟶ 𝒪_{X, x}` induced by `f`.
+
+## Main definitions
+
+* `AlgebraicGeometry.Scheme.Modules.stalkModule`: the canonical module structure of the local
+  ring `𝒪_{X, x}` on the stalk `F_x` of an `𝒪_X`-module `F`.
+* `AlgebraicGeometry.Scheme.Modules.FlatAt`: the pointwise flatness condition at a point.
+* `AlgebraicGeometry.Scheme.Modules.Flat`: the class asserting flatness, defined as
+  `∀ x, FlatAt f F x`.
+
+## Main results
+
+* `AlgebraicGeometry.Scheme.Modules.flat_tilde_iff`: for a commutative ring `R` and an `R`-module
+  `M`, the sheaf `M^~` on `Spec R` is flat over `Spec R` (via the identity morphism) if and only if
+  `M` is a flat `R`-module.
+* `AlgebraicGeometry.Scheme.Modules.flat_tilde_iff_of_algebra`: the same criterion for a ring map
+  `f : R ⟶ S` and an `S`-module `M`: the sheaf `M^~` on `Spec S` is flat over `Spec R`
+  (via `Spec.map f`) if and only if `M` is flat as an `R`-module.
+* `AlgebraicGeometry.Scheme.Modules.Flat.comp`: flatness is preserved under composition with a
+  flat morphism of the base.
+* `AlgebraicGeometry.Scheme.Modules.flat_comp_isOpenImmersion_iff`: flatness is local on the base.
+* `AlgebraicGeometry.Scheme.Modules.flat_iff_forall_openCover`: flatness is local on the source.
+-/
+
+@[expose] public noncomputable section
+
+universe u
+
+open CategoryTheory TopologicalSpace Opposite
+
+namespace AlgebraicGeometry
+
+namespace Scheme.Modules
+
+/-! ### Flatness of a sheaf of modules -/
+
+/-- The canonical module structure of the local ring `𝒪_{X, x}` (the stalk of the structure
+sheaf at `x`) on the stalk `F_x` of an `𝒪_X`-module `F`. -/
+@[reducible]
+def stalkModule {X : Scheme.{u}} (F : X.Modules) (x : X) :
+    Module (X.presheaf.stalk x) (F.presheaf.stalk x) :=
+  PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
+    (R := X.presheaf) F.val x
+
+/-- The pointwise flatness condition at a single point `x ∈ X`: the stalk `F_x` is flat over the
+local ring `𝒪_{S, f(x)}`, where the latter acts by restriction of scalars along the stalk map
+`f.stalkMap x`. -/
+def FlatAt {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (x : X) : Prop :=
+  letI := stalkModule F x
+  letI : Module (S.presheaf.stalk (f.base x)) (F.presheaf.stalk x) :=
+    Module.compHom (F.presheaf.stalk x) (f.stalkMap x).hom
+  Module.Flat (S.presheaf.stalk (f.base x)) (F.presheaf.stalk x)
+
+/-- A sheaf of modules `F` on a scheme `X` is *flat* over `S` via a morphism `f : X ⟶ S` if for
+every point `x ∈ X`, the stalk `F_x` is flat over the local ring `𝒪_{S, f(x)}` (acting by
+restriction of scalars along the stalk map `f.stalkMap x`), i.e. if `FlatAt f F x` holds at every
+point. -/
+class Flat {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) : Prop where
+  flatAt : ∀ x : X, FlatAt f F x
+
+/-- `Flat f F` holds iff the pointwise condition `FlatAt f F x` holds for all `x`. -/
+theorem flat_iff_forall_flatAt {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) :
+    Flat f F ↔ ∀ x : X, FlatAt f F x :=
+  ⟨fun h ↦ h.flatAt, fun h ↦ ⟨h⟩⟩
+
+end Scheme.Modules
+
+namespace Tilde
+
+variable {R : CommRingCat.{u}} (M : ModuleCat.{u} R)
+
+/-- The local ring `𝒪_{Spec R, x}` is an `R`-algebra (it is the localization of `R` at the prime
+corresponding to `x`). -/
+instance instAlgebraStalk (x : PrimeSpectrum.Top R) :
+    Algebra R ((Spec R).presheaf.stalk x) :=
+  StructureSheaf.stalkAlgebra R x
+
+instance instIsLocalizationStalk (x : PrimeSpectrum.Top R) :
+    IsLocalization.AtPrime ((Spec R).presheaf.stalk x) x.asIdeal :=
+  StructureSheaf.IsLocalization.to_stalk R x
+
+/-- The stalk `(M^~)_x` is a module over the local ring `𝒪_{Spec R, x}`. -/
+instance instModuleStalk (x : PrimeSpectrum.Top R) :
+    Module ((Spec R).presheaf.stalk x) ((tilde M).presheaf.stalk x) :=
+  Scheme.Modules.stalkModule (tilde M) x
+
+instance instScalarTowerStalk (x : PrimeSpectrum.Top R) :
+    IsScalarTower R ((Spec R).presheaf.stalk x) ((tilde M).presheaf.stalk x) :=
+  IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl
+
+end Tilde
+
+namespace Scheme.Modules
+
+/-! ### Transitivity and base-locality of flatness
+
+We relate `Flat` to flat morphisms of schemes (`AlgebraicGeometry.Flat`), proving that flatness is
+transitive along a flat base change and that flatness is local on the base. -/
+
+/-- **Transitivity along a flat base.** If a sheaf of modules `F` on `X` is flat over `Y` via
+`f : X ⟶ Y`, and `g : Y ⟶ Z` is a flat morphism of schemes, then `F` is flat over `Z` via the
+composite `f ≫ g`. -/
+theorem Flat.comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (F : X.Modules)
+    [hf : Flat f F] [AlgebraicGeometry.Flat g] : Flat (f ≫ g) F := by
+  refine ⟨fun x ↦ ?_⟩
+  simp only [FlatAt]
+  letI := stalkModule F x
+  letI : Module (Y.presheaf.stalk (f.base x)) (F.presheaf.stalk x) :=
+    Module.compHom (F.presheaf.stalk x) (f.stalkMap x).hom
+  have hmap : ((f ≫ g).stalkMap x).hom
+      = (f.stalkMap x).hom.comp (g.stalkMap (f.base x)).hom := by
+    rw [Scheme.Hom.stalkMap_comp]; rfl
+  rw [congrArg (Module.compHom (F.presheaf.stalk x)) hmap]
+  exact Module.Flat.trans_compHom (g.stalkMap (f.base x)).hom
+    (AlgebraicGeometry.Flat.stalkMap g (f.base x)) (hf.flatAt x)
+
+/-- **Flatness is local on the base.** If `j : V ⟶ S` is an open immersion and `g : X ⟶ V`, then
+`F` is flat over `S` via `g ≫ j` if and only if it is flat over `V` via `g`. In other words,
+flatness over the base only depends on the base through an open neighbourhood of the image. -/
+theorem flat_comp_isOpenImmersion_iff {X V S : Scheme.{u}} (g : X ⟶ V) (j : V ⟶ S)
+    [IsOpenImmersion j] (F : X.Modules) :
+    Flat (g ≫ j) F ↔ Flat g F := by
+  have hbij : ∀ x : X, Function.Bijective (j.stalkMap (g.base x)).hom := fun x ↦
+    (ConcreteCategory.isIso_iff_bijective (j.stalkMap (g.base x))).mp inferInstance
+  refine ⟨fun h ↦ ⟨fun x ↦ ?_⟩, fun h ↦ ⟨fun x ↦ ?_⟩⟩
+  all_goals
+    simp only [FlatAt]
+    letI := stalkModule F x
+    letI : Module (V.presheaf.stalk (g.base x)) (F.presheaf.stalk x) :=
+      Module.compHom (F.presheaf.stalk x) (g.stalkMap x).hom
+    have hmap : ((g ≫ j).stalkMap x).hom
+        = (g.stalkMap x).hom.comp (j.stalkMap (g.base x)).hom := by
+      rw [Scheme.Hom.stalkMap_comp]; rfl
+    have hcompHom := congrArg (Module.compHom (F.presheaf.stalk x)) hmap
+  · have hx := h.flatAt x
+    simp only [FlatAt] at hx
+    rw [hcompHom] at hx
+    exact (Module.Flat.compHom_bijective_iff (j.stalkMap (g.base x)).hom (hbij x)).1 hx
+  · rw [hcompHom]
+    exact Module.Flat.trans_compHom (j.stalkMap (g.base x)).hom
+      (RingHom.Flat.of_bijective (hbij x)) (h.flatAt x)
+
+/-! ### The affine criterion for an `R`-algebra `S` and an `S`-module `M`
+
+We generalise `flat_tilde_iff` from the identity morphism on `Spec R` to the morphism
+`Spec S ⟶ Spec R` induced by an `R`-algebra `S`, applied to the sheaf `M^~` of an `S`-module `M`
+(which is in particular an `R`-module). The result: `M^~` is flat over `Spec R` iff `M` is flat as
+an `R`-module. -/
+
+/-- The pointwise flatness condition for `M^~` (with `M` an `S`-module, for a ring map `f : R ⟶ S`)
+over `Spec R` at a prime `x` of `S` is equivalent to the localization `M_x` being flat over `R`
+(with `R` acting on `M` by restriction of scalars along `f`). -/
+theorem flatAt_tilde_algebra_iff {R S : CommRingCat.{u}} (f : R ⟶ S) (M : ModuleCat.{u} S)
+    (x : PrimeSpectrum S) :
+    letI := f.hom.toAlgebra
+    letI : Module R M := Module.compHom M f.hom
+    letI : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl
+    FlatAt (Spec.map f) (tilde M) x ↔
+      Module.Flat R (LocalizedModule x.asIdeal.primeCompl M) := by
+  letI := f.hom.toAlgebra
+  letI : Module R M := Module.compHom M f.hom
+  haveI : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl
+  letI : Module ((Spec R).presheaf.stalk ((Spec.map f).base x)) ((tilde M).presheaf.stalk x) :=
+    Module.compHom ((tilde M).presheaf.stalk x) ((Spec.map f).stalkMap x).hom
+  letI : Module R ((tilde M).presheaf.stalk x) :=
+    Module.compHom ((tilde M).presheaf.stalk x) f.hom
+  have hsquare : ∀ r : R, ((Spec.map f).stalkMap x).hom
+        (algebraMap R ((Spec R).presheaf.stalk ((Spec.map f).base x)) r)
+      = algebraMap S ((Spec S).presheaf.stalk x) (f.hom r) := fun r ↦
+    AlgebraicGeometry.stalkMap_toStalk_apply f x r
+  haveI : IsScalarTower R S ((tilde M).presheaf.stalk x) :=
+    IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl
+  haveI : IsScalarTower R ((Spec R).presheaf.stalk ((Spec.map f).base x))
+      ((tilde M).presheaf.stalk x) := by
+    refine IsScalarTower.of_algebraMap_smul fun r n ↦ ?_
+    rw [Module.compHom_smul, hsquare r, Module.compHom_smul, algebraMap_smul]
+  simp only [FlatAt]
+  rw [Module.flat_iff_of_isLocalization ((Spec R).presheaf.stalk ((Spec.map f).base x))
+      ((Spec.map f).base x).asIdeal.primeCompl ((tilde M).presheaf.stalk x)]
+  exact Module.Flat.equiv_iff
+    ((IsLocalizedModule.linearEquiv x.asIdeal.primeCompl (tilde.toStalk M x).hom
+      (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)).restrictScalars R)
+
+/-- **The affine case for an `R`-algebra `S`.** For a ring map `f : R ⟶ S` (an `R`-algebra `S`) and
+an `S`-module `M` (hence also an `R`-module, by restriction of scalars), the sheaf `M^~` on `Spec S`
+is flat over `Spec R` (via `Spec.map f`) if and only if `M` is a flat `R`-module. -/
+theorem flat_tilde_iff_of_algebra {R S : CommRingCat.{u}} (f : R ⟶ S) (M : ModuleCat.{u} S) :
+    letI := f.hom.toAlgebra
+    letI : Module R M := Module.compHom M f.hom
+    Flat (Spec.map f) (tilde M) ↔ Module.Flat R M := by
+  letI := f.hom.toAlgebra
+  letI : Module R M := Module.compHom M f.hom
+  haveI : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl
+  rw [flat_iff_forall_flatAt,
+    Module.flat_iff_forall_localizedModule_prime_of_algebra (R := R) (S := S) (M := M)]
+  refine ⟨fun h q _ ↦ (flatAt_tilde_algebra_iff f M ⟨q, ‹_›⟩).mp (h ⟨q, ‹_›⟩),
+    fun h x ↦ (flatAt_tilde_algebra_iff f M x).mpr (h x.asIdeal)⟩
+
+/-- **The affine case.** For a commutative ring `R` and an `R`-module `M`, the quasi-coherent
+sheaf `M^~` on `Spec R` is flat over `Spec R` (via the identity morphism) if and only if `M` is a
+flat `R`-module. This is the special case of `flat_tilde_iff_of_algebra` for the identity ring
+map `𝟙 R`. -/
+theorem flat_tilde_iff {R : CommRingCat.{u}} (M : ModuleCat.{u} R) :
+    Flat (𝟙 (Spec R)) (tilde M) ↔ Module.Flat R M := by
+  rw [← Spec.map_id R]
+  exact flat_tilde_iff_of_algebra (𝟙 R) M
+
+/-! ### Flatness is local on the source (open covers)
+
+We show that flatness can be checked on the members of an open cover of the source: for an open
+cover `{Uᵢ}` of `X`, the module `F` is flat over `S` (via `f : X ⟶ S`) iff each restriction
+`F|_{Uᵢ}` is flat over `S` (via `Uᵢ ⟶ X ⟶ S`). -/
+
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+/-- The additive isomorphism `(F.restrict ι)_u ≅ F_{ι u}` coming from `restrictStalkNatIso` is
+semilinear over the (iso) stalk map `ι.stalkMap u : 𝒪_{X,ι u} ⟶ 𝒪_{U,u}`: scaling by
+`ι.stalkMap u c` on the restriction side corresponds to scaling by `c` on `F`. -/
+theorem restrictStalkNatIso_hom_smul {U X : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion ι]
+    (F : X.Modules) (u : U) (c : X.presheaf.stalk (ι.base u))
+    (m : (F.restrict ι).presheaf.stalk u) :
+    letI := stalkModule (F.restrict ι) u
+    letI := stalkModule F (ι.base u)
+    let Φ : (F.restrict ι).presheaf.stalk u → F.presheaf.stalk (ι.base u) :=
+      fun z ↦ (Scheme.Modules.restrictStalkNatIso ι u).hom.app F z
+    Φ ((ι.stalkMap u).hom c • m) = c • Φ m := by
+  letI := stalkModule (F.restrict ι) u
+  letI := stalkModule F (ι.base u)
+  intro Φ
+  obtain ⟨V, hV, t, rfl⟩ := X.presheaf.exists_germ_eq c
+  obtain ⟨W, hW, s, rfl⟩ := (F.restrict ι).presheaf.exists_germ_eq m
+  rw [Scheme.Hom.germ_stalkMap_apply ι V u hV t]
+  set W' : U.Opens := W ⊓ ι ⁻¹ᵁ V with hW'def
+  have huW' : u ∈ W' := ⟨hW, hV⟩
+  rw [← TopCat.Presheaf.germ_res_apply U.presheaf (homOfLE inf_le_right : W' ⟶ ι ⁻¹ᵁ V) u huW'
+        (ι.app V t),
+      ← TopCat.Presheaf.germ_res_apply (F.restrict ι).presheaf (homOfLE inf_le_left : W' ⟶ W) u
+        huW' s]
+  -- combine the `𝒪_U`-side scalar action into a single germ of a section
+  have lemL : U.presheaf.germ W' u huW' (U.presheaf.map (homOfLE inf_le_right).op (ι.app V t))
+      • (F.restrict ι).presheaf.germ W' u huW'
+        ((F.restrict ι).presheaf.map (homOfLE inf_le_left).op s)
+      = (F.restrict ι).presheaf.germ W' u huW'
+        (U.presheaf.map (homOfLE inf_le_right).op (ι.app V t)
+          • (F.restrict ι).presheaf.map (homOfLE inf_le_left).op s) :=
+    (PresheafOfModules.germ_smul (R := U.presheaf) (F.restrict ι).val u W' huW' _ _).symm
+  rw [lemL]
+  -- push `Φ` through germs of the restricted module
+  have hΦ : ∀ (A : U.Opens) (h : u ∈ A) (z : Γ(F.restrict ι, A)),
+      Φ ((F.restrict ι).presheaf.germ A u h z)
+        = F.presheaf.germ (ι ''ᵁ A) (ι.base u) ⟨u, h, rfl⟩ z := by
+    intro A h z
+    have e1 : Φ ((F.restrict ι).presheaf.germ A u h z)
+        = ((F.restrict ι).presheaf.germ A u h
+            ≫ (Scheme.Modules.restrictStalkNatIso ι u).hom.app F) z := rfl
+    rw [e1]
+    exact DFunLike.congr_fun (congrArg ConcreteCategory.hom
+      (Scheme.Modules.germ_restrictStalkNatIso_hom_app ι u F h)) z
+  rw [hΦ, hΦ, Scheme.Modules.restrict_map]
+  -- align the `𝒪_X`-germ of `t` over `ι ''ᵁ W'` and combine the `F`-side action
+  have hsub : ι ''ᵁ W' ≤ V := by rintro _ ⟨p, hp, rfl⟩; exact hp.2
+  rw [← TopCat.Presheaf.germ_res_apply X.presheaf (homOfLE hsub : ι ''ᵁ W' ⟶ V) (ι.base u)
+        ⟨u, huW', rfl⟩ t]
+  have lemR : X.presheaf.germ (ι ''ᵁ W') (ι.base u) ⟨u, huW', rfl⟩
+        (X.presheaf.map (homOfLE hsub).op t)
+      • F.presheaf.germ (ι ''ᵁ W') (ι.base u) ⟨u, huW', rfl⟩
+        (F.presheaf.map (ι.opensFunctor.map (homOfLE inf_le_left)).op s)
+      = F.presheaf.germ (ι ''ᵁ W') (ι.base u) ⟨u, huW', rfl⟩
+        (X.presheaf.map (homOfLE hsub).op t
+          • F.presheaf.map (ι.opensFunctor.map (homOfLE inf_le_left)).op s) :=
+    (PresheafOfModules.germ_smul (R := X.presheaf) F.val (ι.base u) (ι ''ᵁ W') ⟨u, huW', rfl⟩
+      _ _).symm
+  -- the structure-sheaf identity comparing the two scalars
+  have F2 : (ι.appIso W').inv
+        (U.presheaf.map (homOfLE (inf_le_right : W' ≤ ι ⁻¹ᵁ V)).op (ι.app V t))
+      = X.presheaf.map (homOfLE hsub).op t := by
+    have F2mor : ι.app V ≫ U.presheaf.map (homOfLE (inf_le_right : W' ≤ ι ⁻¹ᵁ V)).op
+          ≫ (ι.appIso W').inv = X.presheaf.map (homOfLE hsub).op := by
+      rw [Scheme.Hom.appIso_inv_naturality, Scheme.Hom.app_appIso_inv_assoc, ← Functor.map_comp]
+      rfl
+    rw [← F2mor]; rfl
+  -- conclude: both germs are of the same section of `F`, using the scalar identity `F2`
+  refine Eq.trans (congrArg _ ?_) lemR.symm
+  exact congrArg
+    (· • F.presheaf.map (ι.opensFunctor.map (homOfLE (inf_le_left : W ⊓ ι ⁻¹ᵁ V ≤ W))).op s) F2
+
+/-- **Pointwise comparison under restriction to an open subscheme.** For an open immersion
+`ι : U ⟶ X`, the flatness of the restricted module `F|_U` at `u` (over `S`, via `ι ≫ f`) is
+equivalent to the flatness of `F` at `ι(u)`. This holds because the stalk map of an open immersion
+is an isomorphism, so restriction does not change the stalk data. -/
+theorem flatAt_restrict_iff {U X S : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion ι]
+    (f : X ⟶ S) (F : X.Modules) (u : U) :
+    FlatAt (ι ≫ f) (F.restrict ι) u ↔ FlatAt f F (ι.base u) := by
+  letI := stalkModule (F.restrict ι) u
+  letI := stalkModule F (ι.base u)
+  let Φe : (F.restrict ι).presheaf.stalk u ≃+ F.presheaf.stalk (ι.base u) :=
+    ((Scheme.Modules.restrictStalkNatIso ι u).app F).addCommGroupIsoToAddEquiv
+  letI : Module (S.presheaf.stalk (f.base (ι.base u))) ((F.restrict ι).presheaf.stalk u) :=
+    Module.compHom ((F.restrict ι).presheaf.stalk u) ((ι ≫ f).stalkMap u).hom
+  letI : Module (S.presheaf.stalk (f.base (ι.base u))) (F.presheaf.stalk (ι.base u)) :=
+    Module.compHom (F.presheaf.stalk (ι.base u)) (f.stalkMap (ι.base u)).hom
+  let e : (F.restrict ι).presheaf.stalk u ≃ₗ[S.presheaf.stalk (f.base (ι.base u))]
+      F.presheaf.stalk (ι.base u) :=
+    Φe.toLinearEquiv (by
+      intro b m
+      -- `change` normalizes the two stalk-map base points `(ι ≫ f) u` and `f (ι u)`, which are
+      -- only equal up to `Scheme.Hom.comp_base`, into a form where `hb` applies.
+      change Φe (((ι ≫ f).stalkMap u).hom b • m) = (f.stalkMap (ι.base u)).hom b • Φe m
+      have hb : ((ι ≫ f).stalkMap u).hom b
+          = (ι.stalkMap u).hom ((f.stalkMap (ι.base u)).hom b) := by
+        rw [Scheme.Hom.stalkMap_comp]; rfl
+      rw [hb]
+      exact restrictStalkNatIso_hom_smul ι F u _ m)
+  change Module.Flat (S.presheaf.stalk (f.base (ι.base u))) ((F.restrict ι).presheaf.stalk u)
+      ↔ Module.Flat (S.presheaf.stalk (f.base (ι.base u))) (F.presheaf.stalk (ι.base u))
+  exact Module.Flat.equiv_iff e
+
+/-- Flatness of the restriction of `F` to an open subscheme `U` (via `ι ≫ f`) is equivalent to the
+pointwise flatness of `F` at every point of `U`. -/
+theorem flat_restrict_iff {U X S : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion ι]
+    (f : X ⟶ S) (F : X.Modules) :
+    Flat (ι ≫ f) (F.restrict ι) ↔ ∀ u : U, FlatAt f F (ι.base u) := by
+  rw [flat_iff_forall_flatAt]
+  exact forall_congr' fun u ↦ flatAt_restrict_iff ι f F u
+
+/-- **Flatness is local on the source.** For an open cover `𝒰` of `X`, the module `F` is flat over
+`S` (via `f`) if and only if for every member `Uᵢ` of the cover, the restriction `F|_{Uᵢ}` is flat
+over `S` (via `𝒰.f i ≫ f`). -/
+theorem flat_iff_forall_openCover {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules)
+    (𝒰 : X.OpenCover) :
+    Flat f F ↔ ∀ i, Flat (𝒰.f i ≫ f) (F.restrict (𝒰.f i)) := by
+  simp_rw [flat_restrict_iff, flat_iff_forall_flatAt]
+  refine ⟨fun h i u ↦ h _, fun h x ↦ ?_⟩
+  obtain ⟨u, hu⟩ := 𝒰.covers x
+  rw [← hu]
+  exact h (𝒰.idx x) u
+
+end Scheme.Modules
+
+end AlgebraicGeometry
diff --git a/Mathlib/RingTheory/Flat/Localization.lean b/Mathlib/RingTheory/Flat/Localization.lean
index 1b54ac43aa720a..d0074d760d6d81 100644
--- a/Mathlib/RingTheory/Flat/Localization.lean
+++ b/Mathlib/RingTheory/Flat/Localization.lean
@@ -103,6 +103,45 @@ theorem flat_of_localized_span
 
 end Module
 
+/-- A module `N` over a commutative ring `R` is flat if and only if its localization at every
+prime ideal is flat over `R`. -/
+theorem Module.flat_iff_forall_localizedModule_prime (R : Type*) [CommRing R] (N : Type*)
+    [AddCommGroup N] [Module R N] :
+    Module.Flat R N ↔
+      ∀ (p : Ideal R) [p.IsPrime], Module.Flat R (LocalizedModule p.primeCompl N) := by
+  refine ⟨fun _ p _ ↦ ?_, fun h ↦ Module.flat_of_localized_maximal _ fun P hP ↦ ?_⟩
+  · have : Module.Flat (Localization p.primeCompl) (LocalizedModule p.primeCompl N) :=
+      Module.Flat.localizedModule _
+    have : Module.Flat R (Localization p.primeCompl) := IsLocalization.flat _ p.primeCompl
+    exact Module.Flat.trans R (Localization p.primeCompl) _
+  · haveI := hP.isPrime
+    exact h P
+
+/-- Localising an `R`-flat module (which is also a module over an `R`-algebra `S`) at a submonoid
+of `S` yields again an `R`-flat module. -/
+theorem Module.Flat.localizedModule_base {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
+    (M : Type*) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
+    (q : Submonoid S) [Module.Flat R M] :
+    Module.Flat R (LocalizedModule q M) := by
+  have e : LocalizedModule q M ≃ₗ[R] (Localization q ⊗[S] M) :=
+    (LocalizedModule.equivTensorProduct q M).restrictScalars R
+  haveI : Module.Flat S (Localization q) := IsLocalization.flat (Localization q) q
+  haveI : Module.Flat R (Localization q ⊗[S] M) := Module.Flat.tensor_tower (Localization q) M
+  exact Module.Flat.of_linearEquiv e
+
+/-- **Local–global flatness over a base, indexed by primes of `S`.** For an `R`-algebra `S` and an
+`S`-module `M`, `M` is flat over `R` iff its localization at every prime of `S` is flat over `R`. -/
+theorem Module.flat_iff_forall_localizedModule_prime_of_algebra {R S : Type*} [CommRing R]
+    [CommRing S] [Algebra R S] (M : Type*) [AddCommGroup M] [Module R M] [Module S M]
+    [IsScalarTower R S M] :
+    Module.Flat R M ↔
+      ∀ (q : Ideal S) [q.IsPrime], Module.Flat R (LocalizedModule q.primeCompl M) := by
+  refine ⟨fun _ q _ ↦ Module.Flat.localizedModule_base M q.primeCompl, fun h ↦ ?_⟩
+  refine Module.flat_of_isLocalized_maximal S M (fun P _ ↦ LocalizedModule P.primeCompl M)
+    (fun P _ ↦ LocalizedModule.mkLinearMap P.primeCompl M) fun P hP ↦ ?_
+  haveI := hP.isPrime
+  exact h P
+
 variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
 
 instance [Module.Flat A B] (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p]
diff --git a/Mathlib/RingTheory/Flat/Stability.lean b/Mathlib/RingTheory/Flat/Stability.lean
index 3c6aa197c93543..cc6f14a99f65aa 100644
--- a/Mathlib/RingTheory/Flat/Stability.lean
+++ b/Mathlib/RingTheory/Flat/Stability.lean
@@ -131,4 +131,41 @@ instance {A : Type*} [CommSemiring A] [Algebra R A] [Flat R A] (S : Submonoid R)
 
 end Localization
 
+section TensorTower
+
+/-- **Flatness of a tensor product over a tower.** If `A` is a flat `S`-algebra and `M` is a flat
+`R`-module (where `R → S → A` is a tower), then `A ⊗[S] M` is a flat `R`-module. -/
+theorem tensor_tower {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
+    (A : Type*) [CommRing A] [Algebra S A] [Algebra R A] [IsScalarTower R S A] [Flat S A]
+    (M : Type*) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [Flat R M] :
+    Flat R (A ⊗[S] M) := by
+  rw [iff_lTensor_preserves_injective_linearMap]
+  intro N N' _ _ _ _ f hf
+  let g : M ⊗[R] N →ₗ[S] M ⊗[R] N' := TensorProduct.AlgebraTensorModule.lTensor S M f
+  have hg : Function.Injective g := by
+    have hcoe : (g : M ⊗[R] N → M ⊗[R] N') = LinearMap.lTensor M f := by ext x; rfl
+    rw [hcoe]
+    exact lTensor_preserves_injective_linearMap (M := M) f hf
+  have hbot : Function.Injective (LinearMap.lTensor A g) :=
+    lTensor_preserves_injective_linearMap (M := A) g hg
+  let eN := TensorProduct.AlgebraTensorModule.assoc R S S A M N
+  let eN' := TensorProduct.AlgebraTensorModule.assoc R S S A M N'
+  have hsqL : eN'.toLinearMap.restrictScalars R ∘ₗ LinearMap.lTensor (A ⊗[S] M) f
+      = (LinearMap.lTensor A g).restrictScalars R ∘ₗ eN.toLinearMap.restrictScalars R := by
+    apply TensorProduct.ext'
+    intro w n
+    induction w using TensorProduct.induction_on with
+    | zero => simp
+    | tmul x y => simp [eN, eN', g, TensorProduct.AlgebraTensorModule.assoc_tmul,
+        TensorProduct.AlgebraTensorModule.lTensor_tmul]
+    | add a b ha hb => simp [TensorProduct.add_tmul, map_add, ha, hb]
+  have hsq : (eN' : _ → _) ∘ LinearMap.lTensor (A ⊗[S] M) f
+      = LinearMap.lTensor A g ∘ (eN : _ → _) := by
+    simpa using congrArg (fun L : _ →ₗ[R] _ ↦ (L : _ → _)) hsqL
+  have hcomp : Function.Injective ((eN' : _ → _) ∘ LinearMap.lTensor (A ⊗[S] M) f) := by
+    rw [hsq]; exact hbot.comp eN.injective
+  exact hcomp.of_comp
+
+end TensorTower
+
 end Module.Flat
diff --git a/Mathlib/RingTheory/RingHom/Flat.lean b/Mathlib/RingTheory/RingHom/Flat.lean
index 721195176b5a4a..b990453baf1120 100644
--- a/Mathlib/RingTheory/RingHom/Flat.lean
+++ b/Mathlib/RingTheory/RingHom/Flat.lean
@@ -270,3 +270,28 @@ lemma RingHom.Flat.mapOfCompatibleSMul {R S : Type u} (T A : Type u)
         (CommRingCat.isPushout_tensorProduct R T A).isoPushout.symm
     · exact (CommRingCat.isPushout_tensorProduct S T A).isoPushout.symm
     all_goals ext <;> simp
+
+/-- If `M` is an `S`-module that is flat over `S`, and `φ : R →+* S` is a flat ring homomorphism,
+then `M` is flat over `R` for the module structure obtained by restricting scalars along `φ`. -/
+theorem Module.Flat.trans_compHom {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S)
+    {M : Type*} [AddCommGroup M] [Module S M] (hφ : RingHom.Flat φ) (hM : Module.Flat S M) :
+    letI := Module.compHom M φ; Module.Flat R M := by
+  letI := φ.toAlgebra
+  letI := Module.compHom M φ
+  haveI : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl
+  haveI : Module.Flat R S := hφ
+  exact Module.Flat.trans R S M
+
+/-- Restricting scalars along a bijective ring homomorphism preserves and reflects flatness. -/
+theorem Module.Flat.compHom_bijective_iff {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S)
+    (hφ : Function.Bijective φ) {M : Type*} [AddCommGroup M] [Module S M] :
+    (letI := Module.compHom M φ; Module.Flat R M) ↔ Module.Flat S M := by
+  refine ⟨fun hM ↦ ?_, fun hM ↦ Module.Flat.trans_compHom φ (.of_bijective hφ) hM⟩
+  letI := Module.compHom M φ
+  let e : R ≃+* S := RingEquiv.ofBijective φ hφ
+  have key := Module.Flat.trans_compHom e.symm.toRingHom (.of_bijective e.symm.bijective) hM
+  have h : (inferInstanceAs (Module S M)) = Module.compHom M e.symm.toRingHom :=
+    Module.ext' _ _ fun s m ↦ by
+      change s • m = e (e.symm s) • m
+      rw [e.apply_symm_apply]
+  rwa [← h] at key