Standard smooth algebras are standard syntomic

A standard smooth algebra of relative dimension n is standard syntomic of relative dimension n. Thus smooth local charts are also syntomic local charts, with the same dimension. This comparison supplies the complete-intersection condition for smooth families of curves.

A submersive presentation has an injection from its relations to its variables, so its dimension is an exact difference rather than a truncated one. Smoothness supplies flatness. After base change to a residue field, the standard smooth dimension theorem supplies the dimension of every nonempty fibre. No Noetherian or nontriviality assumption on the base or algebra is required.

References

• Stacks Project, Lemma 10.137.9, Tag 00TA: smooth ring maps are syntomic.
• The construction uses Mathlib's Algebra.SubmersivePresentation and Algebra.IsStandardSmoothOfRelativeDimension by Jung Tao Cheng, Christian Merten and Andrew Yang, and the existing TauCeti.ringKrullDim_eq_of_isStandardSmoothOfRelativeDimension.

instance TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.of_standardSmooth (n : ℕ) (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] [h : Algebra.IsStandardSmoothOfRelativeDimension n R S] : IsStandardSyntomicOfRelativeDimension n R S

A standard smooth algebra is standard syntomic of the same relative dimension.