Syntomic morphisms of relative dimension n have pure relative dimension n

A morphism f : X ⟶ Y that is syntomic of relative dimension n has pure relative dimension n: every irreducible component of every nonempty fibre has dimension exactly n. In particular a syntomic relative curve, such as a family of nodal curves or a smooth relative curve, has the pure one-dimensional fibres on which the relative singular locus Fitt₁(Ω_{X/S}) is defined.

Both conditions are fibrewise, and the fibre X_y ⟶ Spec κ(y) is again syntomic of relative dimension n, so it suffices to treat a scheme X over a field k. Pure relative dimension is local on the source for morphisms locally of finite type, and X is covered by affine opens whose rings are standard syntomic k-algebras of relative dimension n. Such an algebra is a global complete intersection k[x₁, …, x_{n+c}] ⧸ (f₁, …, f_c) of dimension at most n, so its spectrum is pure-dimensional of dimension n (TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.isPureDimensional_primeSpectrum).

Since smooth morphisms of relative dimension n are syntomic of relative dimension n (TauCeti.AlgebraicGeometry.SyntomicOfRelativeDimension.of_smoothOfRelativeDimension), this also gives pure relative dimension n for smooth morphisms.

Main declarations

• TauCeti.AlgebraicGeometry.PureRelativeDimension.of_syntomicOfRelativeDimension: a morphism syntomic of relative dimension n has pure relative dimension n.

References

• The Stacks Project, Commutative Algebra, Section Syntomic morphisms: global complete intersections over a field and their dimension.

@[instance 100]

instance TauCeti.AlgebraicGeometry.PureRelativeDimension.of_syntomicOfRelativeDimension {n : ℕ} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [SyntomicOfRelativeDimension n f] : PureRelativeDimension n f

A morphism syntomic of relative dimension n has pure relative dimension n: every irreducible component of every nonempty fibre has dimension n.