Flatness of a module sheaf over a morphism

Scheme.Modules.IsFlatOver p M says that M is flat over the base along p : X ⟶ S, stalkwise: at every point of X, the stalk of M is flat as a module over the corresponding stalk of S, restricted along the local-ring map p induces.

This is a property of one module sheaf and one morphism. It needs no derived category, no moduli problem and no perfectness notion, and it is used before any of them: Tor-amplitude models, geometric fibers and base-change arguments all ask for flat terms. It lives with X.Modules for that reason — the carrier in its public type is a module sheaf, and moduleStalkFunctor, the only other repository construction it mentions, is the neighbouring Modules/Pullback/Stalk.lean.

Flatness over the identity is equivalent to flatness at each module stalk, and is preserved by indexed coproducts of module sheaves.

It previously sat in Moduli/PerfectComplex/Relative.lean, where its first consumer was; see docs/architecture/cutover-ledger.md, finding 11.

Not a morphism-flatness predicate

Mathlib.AlgebraicGeometry.Morphisms.Flat is a different subject: it asks that the morphism be flat, which is this condition for the structure sheaf alone. Nothing here specializes to or is implied by that class, and no instance relates them.

def AlgebraicGeometry.Scheme.Modules.IsFlatOver {X S : Scheme} (p : X ⟶ S) (M : X.Modules) : Prop

A module sheaf on X is flat over S when every stalk, restricted along the local-ring map induced by p, is a flat module over the corresponding stalk of S.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.Modules.isFlatOverId_iff_stalkwiseFlat (X : Scheme) (M : X.Modules) : IsFlatOver (CategoryTheory.CategoryStruct.id X) M ↔ ∀ (x : ↥X), Module.Flat ↑(X.presheaf.stalk x) ↑((moduleStalkFunctor X x).obj M)

The identity morphism induces identity maps on stalk rings, and ModuleCat.restrictScalarsId'App removes the scalar-restriction bookkeeping.

theorem AlgebraicGeometry.Scheme.Modules.isFlatOverId_coprod (X : Scheme) {I : Type u} (G : I → X.Modules) (hG : ∀ (i : I), IsFlatOver (CategoryTheory.CategoryStruct.id X) (G i)) : IsFlatOver (CategoryTheory.CategoryStruct.id X) (∐ G)

The stalk of a sheaf coproduct is a direct sum of its module stalks. Direct sums of flat modules are flat, so identity-relative flatness is closed under coproducts.