Flat morphisms: restrictions and generic points

Flatness on an open subset of the target is equivalent to flatness of the original stalk maps at all points lying over that open subset.

A flat morphism of schemes is generalizing: every generization of the image of a point lifts to a generization of that point. Between irreducible schemes this forces the generic point of the source to map to the generic point of the target, since the generic point of the target generizes the image of the generic point of the source, and the generic point of the source has no proper generization. This is the dominance of a flat morphism between irreducible schemes, for instance of a flat model of a curve over a discrete valuation ring, whose generic point lies in the generic fibre.

Main results

• AlgebraicGeometry.Scheme.Hom.flat_restrict_iff: the stalk criterion for flatness of a restriction.
• AlgebraicGeometry.Scheme.Hom.genericPoint_eq_of_flat: a flat morphism between irreducible schemes sends the generic point to the generic point.

References

• The Stacks Project, Lemma 29.25.9, flat morphisms are generalizing.

theorem AlgebraicGeometry.Scheme.Hom.genericPoint_eq_of_flat {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IrreducibleSpace ↥X] [IrreducibleSpace ↥Y] : f (genericPoint ↥X) = genericPoint ↥Y

A flat morphism between irreducible schemes sends the generic point to the generic point.

theorem AlgebraicGeometry.Scheme.Hom.flat_restrict_iff {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : Flat (f ∣_ U) ↔ ∀ (x : ↥X), f x ∈ U → (CommRingCat.Hom.hom (stalkMap f x)).Flat

Flatness of a restriction is equivalent to flatness of the original stalk maps at all points lying above the chosen open subset of the target.