Generic flatness

A finite-type morphism to a reduced locally Noetherian scheme is flat over a dense open subset of the target. The source need not be reduced. This provides the initial open set from which flatness of a homogeneous orbit morphism can be propagated by translations.

The argument uses Module.freeLocus_mem_nhds_of_mem_minimalPrimes on a finite affine cover of the source above each affine open of the target. Freeness over the base at a prime implies flatness of all source stalks above that prime.

References

• The Stacks Project, Tag 0529, generic flatness.
• H. Matsumura, Commutative Ring Theory, Theorem 24.1, generic freeness.

theorem PrimeSpectrum.flat_stalkMap_specMap_of_comap_mem_freeLocus {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (q : PrimeSpectrum S) (hq : comap (algebraMap R S) q ∈ Module.freeLocus R S) : (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) q)).Flat

Freeness of an algebra at a base prime implies flatness of the corresponding scheme morphism at every source prime above it.

theorem AlgebraicGeometry.Scheme.Hom.exists_dense_open_flat_of_target_spec {X : Scheme} {R : CommRingCat} [IsNoetherianRing ↑R] [_root_.IsReduced ↑R] (f : X ⟶ Spec R) [QuasiCompact f] [LocallyOfFiniteType f] : ∃ (U : (Spec R).Opens), Dense ↑U ∧ Flat (f ∣_ U)

A finite-type morphism to the spectrum of a reduced Noetherian ring is flat over a dense open subset of the spectrum.

theorem AlgebraicGeometry.Scheme.Hom.exists_dense_open_flat_of_isAffine {X Y : Scheme} [IsAffine Y] [IsLocallyNoetherian Y] [IsReduced Y] (f : X ⟶ Y) [QuasiCompact f] [LocallyOfFiniteType f] : ∃ (U : Y.Opens), Dense ↑U ∧ Flat (f ∣_ U)

A finite-type morphism to a reduced locally Noetherian affine scheme is flat over a dense open subset of the target.

theorem AlgebraicGeometry.Scheme.Hom.exists_dense_open_flat {X Y : Scheme} [IsLocallyNoetherian Y] [IsReduced Y] (f : X ⟶ Y) [QuasiCompact f] [LocallyOfFiniteType f] : ∃ (U : Y.Opens), Dense ↑U ∧ Flat (f ∣_ U)

Generic flatness. A finite-type morphism to a reduced locally Noetherian scheme is flat over a dense open subset of its target. Neither reducedness of the source nor separatedness of the morphism is required.