Flatness of homogeneous morphisms

Suppose automorphisms of the source and target commute with a scheme morphism and act transitively on the closed points of the target. Over a Jacobson target, flatness above one nonempty open subset then implies flatness everywhere. The translates of that open cover the target: their complement is closed and has no closed points. Flatness is checked on all stalks, including those at nonclosed points.

Combining this propagation result with generic flatness proves that a finite-type homogeneous morphism to a reduced locally Noetherian Jacobson scheme is flat. This is the translation argument used for orbit morphisms and homogeneous spaces. The automorphisms need not be supplied as a group action; only the commuting squares and transitivity are used.

The proof uses Scheme.Hom.flat_restrict_iff, Scheme.Hom.exists_dense_open_flat, and Mathlib's invariance of ring-map flatness under isomorphisms.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 1.65(a), flatness of equivariant morphisms; §§7.c–7.f, orbits and homogeneous spaces.

theorem AlgebraicGeometry.Scheme.Hom.flat_stalkMap_iff_of_isos {X Y : Scheme} (f : X ⟶ Y) (a : X ≅ X) (b : Y ≅ Y) (h : CategoryTheory.CategoryStruct.comp a.hom f = CategoryTheory.CategoryStruct.comp f b.hom) (x : ↥X) : (CommRingCat.Hom.hom (stalkMap f (a.hom x))).Flat ↔ (CommRingCat.Hom.hom (stalkMap f x)).Flat

A commuting square of scheme isomorphisms preserves flatness at corresponding source stalks.

theorem AlgebraicGeometry.Scheme.Hom.flat_restrict_preimage_iff_of_isos {X Y : Scheme} (f : X ⟶ Y) (a : X ≅ X) (b : Y ≅ Y) (h : CategoryTheory.CategoryStruct.comp a.hom f = CategoryTheory.CategoryStruct.comp f b.hom) (U : Y.Opens) : Flat (f ∣_ (TopologicalSpace.Opens.map b.hom.base).obj U) ↔ Flat (f ∣_ U)

Flatness above an open subset is preserved by compatible source and target translations. The translated open is the inverse image under the target isomorphism.

theorem AlgebraicGeometry.Scheme.Hom.flat_of_transitive_closedPoints {X Y : Scheme} (f : X ⟶ Y) [JacobsonSpace ↥Y] {ι : Type v} (a : ι → (X ≅ X)) (b : ι → (Y ≅ Y)) (hcomm : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a i).hom f = CategoryTheory.CategoryStruct.comp f (b i).hom) (htrans : ∀ (y z : ↥Y), y ∈ closedPoints ↥Y → z ∈ closedPoints ↥Y → ∃ (i : ι), (b i).hom y = z) (U : Y.Opens) (hU : (↑U).Nonempty) (hflat : Flat (f ∣_ U)) : Flat f

If compatible automorphisms act transitively on the closed points of a Jacobson target, flatness above any one nonempty open subset implies global flatness. No finite-type, reducedness, or surjectivity assumption on the morphism is needed.

theorem AlgebraicGeometry.Scheme.Hom.flat_of_transitive_closedPoints_of_finiteType {X Y : Scheme} (f : X ⟶ Y) [JacobsonSpace ↥Y] [IsLocallyNoetherian Y] [IsReduced Y] [QuasiCompact f] [LocallyOfFiniteType f] {ι : Type v} (a : ι → (X ≅ X)) (b : ι → (Y ≅ Y)) (hcomm : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a i).hom f = CategoryTheory.CategoryStruct.comp f (b i).hom) (htrans : ∀ (y z : ↥Y), y ∈ closedPoints ↥Y → z ∈ closedPoints ↥Y → ∃ (i : ι), (b i).hom y = z) : Flat f

A finite-type morphism to a reduced locally Noetherian Jacobson scheme is flat if compatible source and target automorphisms act transitively on the target's closed points. The target may be empty or disconnected.