Smooth morphisms are syntomic #
A smooth morphism of relative dimension n is syntomic of relative dimension n over an
arbitrary scheme base. Its standard smooth affine charts are standard syntomic charts of the
same dimension. In particular, smooth relative curves satisfy the complete-intersection
condition in the singular-locus characterization of nodal families.
The comparison is a low-priority instance, so the syntomic base-change and locality API applies to smooth morphisms without separately choosing complete-intersection presentations.
Main results #
TauCeti.AlgebraicGeometry.SyntomicOfRelativeDimension.of_smoothOfRelativeDimension: smooth morphisms are syntomic with the same relative dimension.
References #
- Stacks Project, Lemma 10.137.9, Tag 00TA:
smooth ring maps are syntomic. The algebraic comparison is provided by
TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.of_standardSmooth.
@[instance 100]
instance
TauCeti.AlgebraicGeometry.SyntomicOfRelativeDimension.of_smoothOfRelativeDimension
{n : ℕ}
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[AlgebraicGeometry.SmoothOfRelativeDimension n f]
:
A smooth morphism of relative dimension n is syntomic of relative dimension n.