diff --git a/MathlibStaging.lean b/MathlibStaging.lean
index 4ca4307..14d8432 100644
--- a/MathlibStaging.lean
+++ b/MathlibStaging.lean
@@ -1,8 +1,14 @@
+import MathlibStaging.Algebra.Category.ModuleCat.Flat
 import MathlibStaging.Algebra.Category.ModuleCat.Presheaf
 import MathlibStaging.Algebra.Category.ModuleCat.Presheaf.Submodule
+import MathlibStaging.Algebra.Module.RingHom
 import MathlibStaging.Algebra.Module.Submodule.Map
+import MathlibStaging.AlgebraicGeometry.Modules.Flat
 import MathlibStaging.Init
 import MathlibStaging.Linter.Staging
 import MathlibStaging.Meta.Overrides
 import MathlibStaging.Meta.Upstreamed
 import MathlibStaging.Meta.UpstreamedExt
+import MathlibStaging.RingTheory.Flat.Localization
+import MathlibStaging.RingTheory.Flat.Stability
+import MathlibStaging.RingTheory.RingHom.Flat
diff --git a/MathlibStaging/Algebra/Category/ModuleCat/Flat.lean b/MathlibStaging/Algebra/Category/ModuleCat/Flat.lean
new file mode 100644
index 0000000..c1d6056
--- /dev/null
+++ b/MathlibStaging/Algebra/Category/ModuleCat/Flat.lean
@@ -0,0 +1,77 @@
+/-
+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.Algebra.Category.ModuleCat.ChangeOfRings
+public import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
+public import Mathlib.RingTheory.RingHom.Flat
+public import MathlibStaging.RingTheory.RingHom.Flat
+public import MathlibStaging.Init
+
+/-!
+# Flat modules, as a property of objects of `ModuleCat R`
+
+We define `ModuleCat.flat R : ObjectProperty (ModuleCat R)`, the property of objects of
+`ModuleCat R` given by `Module.Flat`, show that it is closed under isomorphisms and record its
+interaction with restriction of scalars (`ModuleCat.restrictScalars`):
+
+* `ModuleCat.flat_restrictScalars`: restriction of scalars along a flat ring homomorphism
+  preserves flatness.
+* `ModuleCat.flat_restrictScalars_iff_of_bijective`: restriction of scalars along a bijective
+  ring homomorphism preserves and reflects flatness.
+* `ModuleCat.flat_restrictScalars_comp_iff`: restricting scalars along a composition agrees with
+  successively restricting scalars.
+-/
+
+@[expose] public section
+
+open CategoryTheory
+
+universe v u
+
+namespace ModuleCat
+
+variable (R : Type u) [CommRing R]
+
+/-- Flat modules, as a property of objects of `ModuleCat R`. -/
+def flat : ObjectProperty (ModuleCat.{v} R) :=
+  fun M ↦ Module.Flat R M
+
+variable {R}
+
+@[simp]
+lemma flat_iff (M : ModuleCat.{v} R) : flat R M ↔ Module.Flat R M :=
+  Iff.rfl
+
+instance : (flat R).IsClosedUnderIsomorphisms where
+  of_iso e hM := (Module.Flat.equiv_iff e.toLinearEquiv).mp hM
+
+section RestrictScalars
+
+variable {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]
+
+/-- Restriction of scalars along a flat ring homomorphism preserves flatness. -/
+lemma flat_restrictScalars {φ : R →+* S} (hφ : φ.Flat) {M : ModuleCat.{v} S} (hM : flat S M) :
+    flat R ((restrictScalars φ).obj M) :=
+  Module.Flat.trans_compHom φ hφ hM
+
+/-- Restriction of scalars along a bijective ring homomorphism preserves and reflects
+flatness. -/
+lemma flat_restrictScalars_iff_of_bijective {φ : R →+* S} (hφ : Function.Bijective φ)
+    (M : ModuleCat.{v} S) :
+    flat R ((restrictScalars φ).obj M) ↔ flat S M :=
+  Module.Flat.compHom_bijective_iff φ hφ
+
+/-- Restricting scalars along a composition of ring homomorphisms is flat if and only if
+successively restricting scalars is. -/
+lemma flat_restrictScalars_comp_iff (f : R →+* S) (g : S →+* T) (M : ModuleCat.{v} T) :
+    flat R ((restrictScalars (g.comp f)).obj M) ↔
+      flat R ((restrictScalars f).obj ((restrictScalars g).obj M)) :=
+  ObjectProperty.prop_iff_of_iso _ (restrictScalarsComp'App f g (g.comp f) rfl M)
+
+end RestrictScalars
+
+end ModuleCat
diff --git a/MathlibStaging/Algebra/Module/RingHom.lean b/MathlibStaging/Algebra/Module/RingHom.lean
new file mode 100644
index 0000000..ac657e8
--- /dev/null
+++ b/MathlibStaging/Algebra/Module/RingHom.lean
@@ -0,0 +1,22 @@
+/-
+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.Algebra.Module.RingHom
+public import MathlibStaging.Init
+
+/-!
+-/
+
+@[expose] public section
+
+variable {R S M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
+
+/-- The scalar action of `Module.compHom M f` (restriction of scalars along a ring
+homomorphism `f : S →+* R`) is given by `s • m = f s • m`. -/
+lemma Module.compHom_smul [Semiring S] (f : S →+* R) (s : S) (m : M) :
+    letI := Module.compHom M f; s • m = f s • m :=
+  rfl
diff --git a/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean b/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean
new file mode 100644
index 0000000..f015419
--- /dev/null
+++ b/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean
@@ -0,0 +1,416 @@
+/-
+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
+public import MathlibStaging.Algebra.Category.ModuleCat.Flat
+public import MathlibStaging.Algebra.Module.RingHom
+public import MathlibStaging.RingTheory.Flat.Localization
+public import MathlibStaging.Init
+
+/-!
+# Flat sheaves of modules
+
+We say that an `𝒪_X`-module `F` is *flat* if for every point `x ∈ X`, the stalk `F_x` is a flat
+module over the local ring `𝒪_{X, x}`. This is the *absolute* notion, over the structure sheaf of
+`X` itself.
+
+More generally, given a morphism of schemes `f : X ⟶ S`, 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`. Conceptually this is the absolute flatness
+of the restriction of scalars of `F` to the inverse-image structure sheaf `f⁻¹𝒪_S`; the absolute
+notion is the special case `f = 𝟙 X` (`flatOver_id_iff`).
+
+## 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.stalk`: the stalk `F_x`, bundled as an object of the category
+  of modules over the local ring `𝒪_{X, x}`.
+* `AlgebraicGeometry.Scheme.Modules.FlatAt`: the pointwise (absolute) flatness condition at a point,
+  `F_x` is flat over `𝒪_{X, x}`.
+* `AlgebraicGeometry.Scheme.Modules.Flat`: the class asserting (absolute) flatness, defined as
+  `∀ x, FlatAt F x`.
+* `AlgebraicGeometry.Scheme.Modules.FlatAtOver`/`FlatOver`: the relative pointwise condition and
+  class, flatness of `F` over a base `S` via `f : X ⟶ S`, phrased via `ModuleCat.flat` and
+  restriction of scalars along the stalk map.
+
+## Main results
+
+* `AlgebraicGeometry.Scheme.Modules.flatOver_id_iff`: `F` is flat over the base via the identity
+  morphism `𝟙 X` iff it is (absolutely) flat.
+* `AlgebraicGeometry.Scheme.Modules.flatOver_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.flatOver_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.FlatOver.comp`: flatness is preserved under composition with a
+  flat morphism of the base.
+* `AlgebraicGeometry.Scheme.Modules.flatOver_comp_isOpenImmersion_iff`: flatness is local on the
+  base.
+* `AlgebraicGeometry.Scheme.Modules.flatOver_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`.
+
+We pin the `PresheafOfModules`-instance explicitly rather than via `inferInstance`: `Stalk.lean`
+registers two definitionally-equal `Module (X.presheaf.stalk x) _` instances, and the downstream
+germ-level rewrites (e.g. via `PresheafOfModules.germ_smul`) only match against this one. -/
+abbrev 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 stalk `F_x` of an `𝒪_X`-module `F` at a point `x ∈ X`, bundled as an object of the
+category of modules over the local ring `𝒪_{X, x}`, with the module structure `stalkModule`. -/
+def stalk {X : Scheme.{u}} (F : X.Modules) (x : X) : ModuleCat (X.presheaf.stalk x) :=
+  @ModuleCat.of _ _ (F.presheaf.stalk x) _ (stalkModule F x)
+
+/-- The pointwise flatness condition at a single point `x ∈ X`: the stalk `F_x` is flat over the
+local ring `𝒪_{X, x}`. -/
+def FlatAt {X : Scheme.{u}} (F : X.Modules) (x : X) : Prop :=
+  ModuleCat.flat (X.presheaf.stalk x) (F.stalk x)
+
+/-- A sheaf of modules `F` on a scheme `X` is *flat* if for every point `x ∈ X`, the stalk `F_x`
+is flat over the local ring `𝒪_{X, x}`, i.e. if `FlatAt F x` holds at every point. -/
+class Flat {X : Scheme.{u}} (F : X.Modules) : Prop where
+  flatAt : ∀ x : X, FlatAt F x
+
+/-- `Flat F` holds iff the pointwise condition `FlatAt F x` holds for all `x`. -/
+theorem flat_iff_forall_flatAt {X : Scheme.{u}} (F : X.Modules) :
+    Flat F ↔ ∀ x : X, FlatAt F x :=
+  ⟨fun h ↦ h.flatAt, fun h ↦ ⟨h⟩⟩
+
+/-! ### Relative flatness over a base
+
+`Flat` above is *absolute*: it is flatness of `F` over its own structure sheaf `𝒪_X`. To talk about
+flatness of `F` over a base `S` via a morphism `f : X ⟶ S`, we restrict scalars of each stalk `F_x`
+along the stalk map `f.stalkMap x : 𝒪_{S, f(x)} ⟶ 𝒪_{X, x}`.
+
+Conceptually this is the absolute flatness (`Flat`) of the restriction of scalars of `F` to the
+inverse-image structure sheaf `f⁻¹𝒪_S` (whose stalk at `x` is `𝒪_{S, f(x)}`). We phrase it
+stalk-wise directly, as Mathlib does not yet provide the inverse-image sheaf of rings and its stalk
+identification. -/
+
+/-- The pointwise flatness condition of `F` over a base `S` (via `f : X ⟶ S`) 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 FlatAtOver {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (x : X) : Prop :=
+  ModuleCat.flat (S.presheaf.stalk (f.base x))
+    ((ModuleCat.restrictScalars (f.stalkMap x).hom).obj (F.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 `FlatAtOver f F x` holds at
+every point. -/
+class FlatOver {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) : Prop where
+  flatAt : ∀ x : X, FlatAtOver f F x
+
+/-- `FlatOver f F` holds iff the pointwise condition `FlatAtOver f F x` holds for all `x`. -/
+theorem flatOver_iff_forall_flatAtOver {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) :
+    FlatOver f F ↔ ∀ x : X, FlatAtOver f F x :=
+  ⟨fun h ↦ h.flatAt, fun h ↦ ⟨h⟩⟩
+
+/-- Flatness of `F` over its own structure sheaf, `Flat F`, is the special case of relative
+flatness `FlatOver f F` for the identity morphism `f = 𝟙 X`. Under the identity stalk map the
+restriction of scalars is the identity, so the two pointwise conditions agree. -/
+theorem flatAtOver_id {X : Scheme.{u}} (F : X.Modules) (x : X) :
+    FlatAtOver (𝟙 X) F x ↔ FlatAt F x := by
+  have hf : ((𝟙 X : X ⟶ X).stalkMap x).hom = RingHom.id (X.presheaf.stalk x) := by
+    rw [Scheme.Hom.stalkMap_id]; exact CommRingCat.hom_id
+  exact ObjectProperty.prop_iff_of_iso _ (ModuleCat.restrictScalarsId'App _ hf (F.stalk x))
+
+/-- `F` is flat over the base via the identity morphism `𝟙 X` iff it is (absolutely) flat. -/
+theorem flatOver_id_iff {X : Scheme.{u}} (F : X.Modules) :
+    FlatOver (𝟙 X) F ↔ Flat F := by
+  rw [flatOver_iff_forall_flatAtOver, flat_iff_forall_flatAt]
+  exact forall_congr' fun x ↦ flatAtOver_id F x
+
+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
+
+/-- The local ring `𝒪_{Spec R, x}` is the localization of `R` at the prime `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}`. This re-exposes the
+canonical `PresheafOfModules`-instance: typeclass search does not otherwise find it through the
+`SheafOfModules.presheaf` projection, so the downstream `IsScalarTower`/flatness statements rely on
+it being registered here. -/
+instance instModuleStalk (x : PrimeSpectrum.Top R) :
+    Module ((Spec R).presheaf.stalk x) ((tilde M).presheaf.stalk x) :=
+  Scheme.Modules.stalkModule (tilde M) x
+
+/-- The actions of `R` and the local ring `𝒪_{Spec R, x}` on the stalk `(M^~)_x` are compatible. -/
+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. -/
+
+/-- The underlying ring homomorphism of the stalk map of a composition factors as the composition
+of the underlying ring homomorphisms of the stalk maps. -/
+lemma stalkMap_comp_hom {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
+    ((f ≫ g).stalkMap x).hom = (f.stalkMap x).hom.comp (g.stalkMap (f.base x)).hom := by
+  rw [Scheme.Hom.stalkMap_comp]
+  exact CommRingCat.hom_comp _ _
+
+/-- **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 FlatOver.comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (F : X.Modules)
+    [hf : FlatOver f F] [AlgebraicGeometry.Flat g] : FlatOver (f ≫ g) F := by
+  refine ⟨fun x ↦ ?_⟩
+  simp only [FlatAtOver]
+  rw [stalkMap_comp_hom f g x]
+  exact (ModuleCat.flat_restrictScalars_comp_iff _ _ _).mpr
+    (ModuleCat.flat_restrictScalars (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 flatOver_comp_isOpenImmersion_iff {X V S : Scheme.{u}} (g : X ⟶ V) (j : V ⟶ S)
+    [IsOpenImmersion j] (F : X.Modules) :
+    FlatOver (g ≫ j) F ↔ FlatOver g F := by
+  simp only [flatOver_iff_forall_flatAtOver]
+  refine forall_congr' fun x ↦ ?_
+  simp only [FlatAtOver]
+  rw [stalkMap_comp_hom g j x]
+  exact (ModuleCat.flat_restrictScalars_comp_iff _ _ _).trans
+    (ModuleCat.flat_restrictScalars_iff_of_bijective
+      ((ConcreteCategory.isIso_iff_bijective (j.stalkMap (g.base x))).mp inferInstance) _)
+
+/-! ### 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 flatAtOver_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
+    FlatAtOver (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
+  have : 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
+  have : IsScalarTower R S ((tilde M).presheaf.stalk x) :=
+    IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl
+  have : 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]
+  exact Iff.trans
+    (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))
+    (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 flatOver_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
+    FlatOver (Spec.map f) (tilde M) ↔ Module.Flat R M := by
+  letI := f.hom.toAlgebra
+  letI : Module R M := Module.compHom M f.hom
+  have : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl
+  rw [flatOver_iff_forall_flatAtOver]
+  refine ⟨fun h ↦ (Module.flat_iff_forall_localizedModule_maximal_of_algebra (R := R) (S := S)
+      (M := M)).mpr fun q _ ↦ (flatAtOver_tilde_algebra_iff f M ⟨q, inferInstance⟩).mp
+        (h ⟨q, inferInstance⟩),
+    fun hM x ↦ (flatAtOver_tilde_algebra_iff f M x).mpr
+      (Module.Flat.localizedModule_base M x.asIdeal.primeCompl)⟩
+
+/-- **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 `flatOver_tilde_iff_of_algebra` for the identity ring
+map `𝟙 R`. -/
+theorem flatOver_tilde_iff {R : CommRingCat.{u}} (M : ModuleCat.{u} R) :
+    FlatOver (𝟙 (Spec R)) (tilde M) ↔ Module.Flat R M := by
+  rw [← Spec.map_id R]
+  exact flatOver_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`). -/
+
+-- The `rw`s below rewrite scalar actions on stalks whose module instance enters the goal as a
+-- `letI`-bound local instance, while `PresheafOfModules.germ_smul` phrases the action through the
+-- canonical instance. These are defeq but not syntactically equal, so `rw` needs the relaxed defeq.
+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
+    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
+
+/-- For an open immersion `ι : U ⟶ X` and a point `u ∈ U`, the stalk of the restriction `F|_U`
+at `u`, with scalars restricted along the (iso) stalk map `ι.stalkMap u`, is isomorphic in
+`ModuleCat 𝒪_{X, ι u}` to the stalk of `F` at `ι u`. -/
+def restrictStalkModuleIso {U X : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion ι]
+    (F : X.Modules) (u : U) :
+    (ModuleCat.restrictScalars (ι.stalkMap u).hom).obj ((F.restrict ι).stalk u) ≅
+      F.stalk (ι.base u) :=
+  (AddEquiv.toLinearEquiv
+    (M := (ModuleCat.restrictScalars (ι.stalkMap u).hom).obj ((F.restrict ι).stalk u))
+    (M₂ := F.stalk (ι.base u))
+    ((Scheme.Modules.restrictStalkNatIso ι u).app F).addCommGroupIsoToAddEquiv
+    (fun c m ↦ restrictStalkNatIso_hom_smul ι F u c m)).toModuleIso
+
+/-- **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 flatAtOver_restrict_iff {U X S : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion ι]
+    (f : X ⟶ S) (F : X.Modules) (u : U) :
+    FlatAtOver (ι ≫ f) (F.restrict ι) u ↔ FlatAtOver f F (ι.base u) := by
+  simp only [FlatAtOver]
+  rw [stalkMap_comp_hom ι f u]
+  exact (ModuleCat.flat_restrictScalars_comp_iff _ _ _).trans
+    (ObjectProperty.prop_iff_of_iso _
+      ((ModuleCat.restrictScalars (f.stalkMap (ι.base u)).hom).mapIso
+        (restrictStalkModuleIso ι F u)))
+
+/-- 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 flatOver_restrict_iff {U X S : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion ι]
+    (f : X ⟶ S) (F : X.Modules) :
+    FlatOver (ι ≫ f) (F.restrict ι) ↔ ∀ u : U, FlatAtOver f F (ι.base u) := by
+  rw [flatOver_iff_forall_flatAtOver]
+  exact forall_congr' fun u ↦ flatAtOver_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 flatOver_iff_forall_openCover {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules)
+    (𝒰 : X.OpenCover) :
+    FlatOver f F ↔ ∀ i, FlatOver (𝒰.f i ≫ f) (F.restrict (𝒰.f i)) := by
+  simp_rw [flatOver_restrict_iff, flatOver_iff_forall_flatAtOver]
+  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/MathlibStaging/RingTheory/Flat/Localization.lean b/MathlibStaging/RingTheory/Flat/Localization.lean
new file mode 100644
index 0000000..c31dec7
--- /dev/null
+++ b/MathlibStaging/RingTheory/Flat/Localization.lean
@@ -0,0 +1,41 @@
+/-
+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.RingTheory.Flat.Localization
+public import MathlibStaging.RingTheory.Flat.Stability
+public import MathlibStaging.Init
+
+/-!
+-/
+
+@[expose] public section
+
+open scoped TensorProduct
+
+/-- 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
+  have : Module.Flat S (Localization q) := IsLocalization.flat (Localization q) q
+  have : 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 maximal ideals of `S`.** For an `R`-algebra `S`
+and an `S`-module `M`, `M` is flat over `R` iff its localization at every maximal ideal of `S` is
+flat over `R`. -/
+theorem Module.flat_iff_forall_localizedModule_maximal_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.IsMaximal], Module.Flat R (LocalizedModule q.primeCompl M) := by
+  refine ⟨fun _ q _ ↦ Module.Flat.localizedModule_base M q.primeCompl, fun h ↦ ?_⟩
+  exact Module.flat_of_isLocalized_maximal S M (fun P _ ↦ LocalizedModule P.primeCompl M)
+    (fun P _ ↦ LocalizedModule.mkLinearMap P.primeCompl M) fun P _ ↦ h P
diff --git a/MathlibStaging/RingTheory/Flat/Stability.lean b/MathlibStaging/RingTheory/Flat/Stability.lean
new file mode 100644
index 0000000..366c63e
--- /dev/null
+++ b/MathlibStaging/RingTheory/Flat/Stability.lean
@@ -0,0 +1,61 @@
+/-
+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.RingTheory.Flat.Stability
+public import MathlibStaging.Init
+
+/-!
+-/
+
+@[expose] public section
+
+open scoped TensorProduct
+
+namespace Module.Flat
+
+section TensorTower
+
+/-- **Flatness of a tensor product over a tower.** If `A` is a flat `S`-module and `M` is a flat
+`R`-module (where `R → S` is an algebra and `A`, `M` carry compatible scalar towers), then
+`A ⊗[S] M` is a flat `R`-module. -/
+theorem tensor_tower {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
+    (A : Type*) [AddCommGroup A] [Module S A] [Module 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/MathlibStaging/RingTheory/RingHom/Flat.lean b/MathlibStaging/RingTheory/RingHom/Flat.lean
new file mode 100644
index 0000000..92d3177
--- /dev/null
+++ b/MathlibStaging/RingTheory/RingHom/Flat.lean
@@ -0,0 +1,52 @@
+/-
+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.RingTheory.RingHom.Flat
+public import MathlibStaging.Init
+
+/-!
+-/
+
+@[expose] public section
+
+/-- 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 φ
+  have : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl
+  have : Module.Flat R S := hφ
+  exact Module.Flat.trans R S M
+
+/-- If the algebra map `R → S` is bijective, then an `S`-module `M` is flat over `R` (via the tower)
+iff it is flat over `S`. -/
+theorem Module.Flat.iff_of_bijective_algebraMap {R S : Type*} [CommRing R] [CommRing S]
+    [Algebra R S] (hb : Function.Bijective (algebraMap R S)) (M : Type*) [AddCommGroup M]
+    [Module R M] [Module S M] [IsScalarTower R S M] :
+    Module.Flat R M ↔ Module.Flat S M := by
+  let e : R ≃+* S := RingEquiv.ofBijective (algebraMap R S) hb
+  refine ⟨fun hM ↦ ?_, fun hM ↦ ?_⟩
+  · letI : Algebra S R := e.symm.toRingHom.toAlgebra
+    haveI : IsScalarTower S R M := IsScalarTower.of_algebraMap_smul fun s x ↦ by
+      have h : (algebraMap R S) (e.symm s) = s := e.apply_symm_apply s
+      rw [show algebraMap S R s = e.symm s from rfl, ← algebraMap_smul (A := S) (e.symm s) x, h]
+    haveI : Module.Flat S R := RingHom.Flat.of_bijective (f := e.symm.toRingHom) e.symm.bijective
+    exact Module.Flat.trans S R M
+  · haveI : Module.Flat R S :=
+      Module.Flat.of_linearEquiv (LinearEquiv.ofBijective (Algebra.linearMap R S) hb).symm
+    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
+  letI := φ.toAlgebra
+  letI := Module.compHom M φ
+  haveI : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl
+  exact Module.Flat.iff_of_bijective_algebraMap hφ M