Syntomic morphisms are detected on fibres

A morphism f : X ⟶ Y is syntomic of relative dimension n exactly when it is flat and locally of finite presentation and each of its fibres f.fiber y ⟶ Spec κ(y) over a residue field is syntomic of relative dimension n (TauCeti.AlgebraicGeometry.syntomicOfRelativeDimension_iff_flat_and_fiberToSpecResidueField).

Both sides are local on the source and the target, so the converse direction reduces to a morphism Spec A ⟶ Spec R, where it is the fibrewise criterion for standard syntomic ring maps (TauCeti.locally_isStandardSyntomicOfRelativeDimension_of_fiber): the fibre of Spec A ⟶ Spec R over a prime p is Spec (κ(p) ⊗[R] A) ⟶ Spec κ(p) (AlgebraicGeometry.Spec.fiberToSpecResidueFieldIso).

Main results

• TauCeti.AlgebraicGeometry.SyntomicOfRelativeDimension.of_fiberToSpecResidueField: a flat morphism locally of finite presentation whose fibres are syntomic of relative dimension n is syntomic of relative dimension n.
• TauCeti.AlgebraicGeometry.syntomicOfRelativeDimension_iff_flat_and_fiberToSpecResidueField: the fibrewise characterization of syntomic morphisms of relative dimension n.

References

• The Stacks Project, Morphisms of Schemes, Section Syntomic morphisms: a flat morphism locally of finite presentation is syntomic if and only if its fibres are local complete intersections.

theorem TauCeti.AlgebraicGeometry.SyntomicOfRelativeDimension.of_fiberToSpecResidueField {n : ℕ} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f] [AlgebraicGeometry.LocallyOfFinitePresentation f] (h : ∀ (y : ↥Y), SyntomicOfRelativeDimension n (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f y)) : SyntomicOfRelativeDimension n f

The fibrewise criterion for syntomic morphisms. A flat morphism locally of finite presentation, each of whose fibres f.fiber y ⟶ Spec κ(y) over a residue field is syntomic of relative dimension n, is syntomic of relative dimension n.

theorem TauCeti.AlgebraicGeometry.syntomicOfRelativeDimension_iff_flat_and_fiberToSpecResidueField {n : ℕ} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : SyntomicOfRelativeDimension n f ↔ AlgebraicGeometry.Flat f ∧ AlgebraicGeometry.LocallyOfFinitePresentation f ∧ ∀ (y : ↥Y), SyntomicOfRelativeDimension n (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f y)

A morphism is syntomic of relative dimension n exactly when it is flat and locally of finite presentation and each of its fibres f.fiber y ⟶ Spec κ(y) over a residue field is syntomic of relative dimension n.