Dominant morphisms to curves are flat

A dominant morphism f : X ⟶ Y from an integral scheme to a scheme whose local rings are valuation rings is flat. At a point x of X, the stalk map 𝒪_{Y,f x} → 𝒪_{X,x} is injective, because a section of 𝒪_Y killed by f vanishes on the dense image of f; so the domain 𝒪_{X,x} is a torsion-free module over the valuation ring 𝒪_{Y,f x}, and torsion-free modules over a valuation ring are flat.

The local rings of a scheme smooth over a field are regular, and when its dimension is at most one they are fields or discrete valuation rings. Hence every dominant morphism from an integral scheme to a curve smooth over a field is flat. Since a nonconstant morphism between proper integral curves over a field is dominant, this applies to nonconstant morphisms of smooth projective curves over a field, such as the projective model of an elliptic curve. A morphism that is smooth of relative dimension one supplies the smoothness and dimension hypotheses through TauCeti.AlgebraicGeometry.SyntomicOfRelativeDimension.relativeDimensionLE.

The hypotheses on f and on Y are needed. The inclusion of a closed point into a curve is not dominant and not flat. The closed point Spec k ⟶ Spec k[ε]/(ε²) is dominant and not flat; there the target is not reduced, although its only local ring is a principal ideal ring.

Main results

• AlgebraicGeometry.Scheme.Hom.stalkMap_injective_of_isDominant: the stalk maps of a dominant morphism from an integral scheme to a scheme with reduced local rings are injective.
• AlgebraicGeometry.Scheme.Hom.flat_of_isDominant_of_valuationRing: a dominant morphism from an integral scheme to a scheme whose local rings are valuation rings is flat.
• AlgebraicGeometry.Scheme.Hom.flat_of_isDominant_of_smooth: a dominant morphism from an integral scheme to a scheme smooth over a field, of dimension at most one, is flat.

References

• R. Hartshorne, Algebraic Geometry, Proposition III.9.7, for flatness over a regular integral scheme of dimension one.

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_injective_of_isDominant {X Y : Scheme} (f : X ⟶ Y) [IsIntegral X] [IsDominant f] (x : ↥X) [_root_.IsReduced ↑(Y.presheaf.stalk (f x))] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (stalkMap f x))

The stalk maps of a dominant morphism from an integral scheme to a scheme with reduced local rings (for instance a reduced scheme) are injective.

theorem AlgebraicGeometry.Scheme.Hom.flat_stalkMap_of_isDominant {X Y : Scheme} (f : X ⟶ Y) [IsIntegral X] [IsDominant f] (x : ↥X) [IsDomain ↑(Y.presheaf.stalk (f x))] [ValuationRing ↑(Y.presheaf.stalk (f x))] : (CommRingCat.Hom.hom (stalkMap f x)).Flat

At a point where the target has a valuation ring as local ring, the stalk map of a dominant morphism from an integral scheme is flat.

theorem AlgebraicGeometry.Scheme.Hom.flat_of_isDominant_of_valuationRing {X Y : Scheme} (f : X ⟶ Y) [IsIntegral X] [IsDominant f] [∀ (y : ↥Y), IsDomain ↑(Y.presheaf.stalk y)] [∀ (y : ↥Y), ValuationRing ↑(Y.presheaf.stalk y)] : Flat f

A dominant morphism to a scheme with valuation rings as local rings is flat. If X is integral and every local ring of Y is a valuation ring, as for a Dedekind scheme, then a dominant morphism X ⟶ Y is flat.

theorem AlgebraicGeometry.Scheme.Hom.flat_of_isDominant_of_smooth {X Y : Scheme} {K : Type u} [Field K] (f : X ⟶ Y) (g : Y ⟶ Spec ↧K) [Smooth g] [TauCeti.AlgebraicGeometry.RelativeDimensionLE 1 g] [IsIntegral X] [IsDominant f] : Flat f

A dominant morphism to a smooth curve over a field is flat. If Y is smooth over a field K with all fibres of dimension at most one, then every dominant morphism from an integral scheme to Y is flat. The local rings of Y are regular of dimension at most one, hence valuation rings.