Spectra of standard syntomic algebras

If S is a standard syntomic R-algebra of relative dimension n, then every fibre κ(p) ⊗[R] S of Spec S ⟶ Spec R has Krull dimension at most n, so the morphism Spec S ⟶ Spec R has relative dimension at most n in the sense of TauCeti.AlgebraicGeometry.RelativeDimensionLE. This connects the algebraic local models of syntomic morphisms to the scheme-level fibre-dimension API used to define families of curves.

Main results

• TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.relativeDimensionLE_SpecMap: the spectrum of a standard syntomic algebra of relative dimension n has relative dimension at most n.

instance TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.relativeDimensionLE_SpecMap (n : ℕ) (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [h : IsStandardSyntomicOfRelativeDimension n R S] : AlgebraicGeometry.RelativeDimensionLE n (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))

The morphism Spec S ⟶ Spec R of a standard syntomic R-algebra S of relative dimension n has relative dimension at most n.