Syntomic morphisms of fixed relative dimension

A syntomic morphism of relative dimension n is locally on affine charts standard syntomic of relative dimension n. These morphisms are flat and locally finitely presented, are local on both source and target, and are stable under arbitrary base change. They have relative dimension at most n. The affine criterion connects the scheme property to the existing algebraic complete-intersection presentations.

The consequences SyntomicOfRelativeDimension.flat n f and SyntomicOfRelativeDimension.locallyOfFinitePresentation n f take the dimension explicitly, since it is absent from their conclusions. For downstream typeclass-based APIs, install them locally with have := SyntomicOfRelativeDimension.flat n f and have := SyntomicOfRelativeDimension.locallyOfFinitePresentation n f.

This construction follows the local-chart API of Mathlib's SmoothOfRelativeDimension in Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean, by Christian Merten. The mathematical reference is the Stacks Project, Syntomic morphisms. Syntomic relative curves provide the complete-intersection input to the singular-locus criterion for nodal families.

class TauCeti.AlgebraicGeometry.SyntomicOfRelativeDimension (n : ℕ) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Prop

A scheme morphism is syntomic of relative dimension n if each source point has affine source and target neighborhoods on which the induced ring map is standard syntomic of relative dimension n.

• exists_isStandardSyntomicOfRelativeDimension (x : ↥X) : ∃ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (_ : x ∈ ↑V) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), IsStandardSyntomicOfRelativeDimension n (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e))

theorem TauCeti.AlgebraicGeometry.syntomicOfRelativeDimension_iff (n : ℕ) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : SyntomicOfRelativeDimension n f ↔ ∀ (x : ↥X), ∃ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (_ : x ∈ ↑V) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), IsStandardSyntomicOfRelativeDimension n (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e))

instance TauCeti.AlgebraicGeometry.instHasRingHomPropertySyntomicOfRelativeDimensionLocallyIsStandardSyntomicOfRelativeDimension (n : ℕ) : AlgebraicGeometry.HasRingHomProperty (@SyntomicOfRelativeDimension n) fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.Locally (@IsStandardSyntomicOfRelativeDimension n)

The affine ring property of syntomic morphisms is locally standard syntomic.

theorem TauCeti.AlgebraicGeometry.SyntomicOfRelativeDimension.exists_isStandardSyntomicOfRelativeDimension_appLE_top (n : ℕ) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffine Y] [SyntomicOfRelativeDimension n f] (x : ↥X) : ∃ (V : ↑X.affineOpens) (_ : x ∈ ↑V) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ⊤), IsStandardSyntomicOfRelativeDimension n (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f ⊤ (↑V) e))

Over an affine target, every source point has a standard syntomic affine chart over the global sections of the target.

instance TauCeti.AlgebraicGeometry.syntomicOfRelativeDimension_isStableUnderBaseChange (n : ℕ) : CategoryTheory.MorphismProperty.IsStableUnderBaseChange (@SyntomicOfRelativeDimension n)

Syntomic morphisms of fixed relative dimension are stable under arbitrary base change.

instance TauCeti.AlgebraicGeometry.instRespectsIsoSchemeSyntomicOfRelativeDimension (n : ℕ) : CategoryTheory.MorphismProperty.RespectsIso (@SyntomicOfRelativeDimension n)

Syntomicity of fixed relative dimension is invariant under isomorphisms.

instance TauCeti.AlgebraicGeometry.instIsZariskiLocalAtSourceSyntomicOfRelativeDimension (n : ℕ) : AlgebraicGeometry.IsZariskiLocalAtSource (@SyntomicOfRelativeDimension n)

Syntomicity of fixed relative dimension is local on the source.

instance TauCeti.AlgebraicGeometry.instIsZariskiLocalAtTargetSyntomicOfRelativeDimension (n : ℕ) : AlgebraicGeometry.IsZariskiLocalAtTarget (@SyntomicOfRelativeDimension n)

Syntomicity of fixed relative dimension is local on the target.

instance TauCeti.AlgebraicGeometry.instRespectsSchemeSyntomicOfRelativeDimensionIsOpenImmersion (n : ℕ) : CategoryTheory.MorphismProperty.Respects (@SyntomicOfRelativeDimension n) AlgebraicGeometry.IsOpenImmersion

Restricting the source to an open subscheme preserves syntomicity and relative dimension.

@[instance 900]

instance TauCeti.AlgebraicGeometry.instSyntomicOfRelativeDimensionOfNatNatOfIsOpenImmersion {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] : SyntomicOfRelativeDimension 0 f

Open immersions, including identities, are syntomic of relative dimension zero.

theorem TauCeti.AlgebraicGeometry.SyntomicOfRelativeDimension.flat (n : ℕ) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [SyntomicOfRelativeDimension n f] : AlgebraicGeometry.Flat f

Syntomic morphisms are flat.

theorem TauCeti.AlgebraicGeometry.SyntomicOfRelativeDimension.locallyOfFinitePresentation (n : ℕ) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [SyntomicOfRelativeDimension n f] : AlgebraicGeometry.LocallyOfFinitePresentation f

Syntomic morphisms are locally of finite presentation.

instance TauCeti.AlgebraicGeometry.syntomicOfRelativeDimension_SpecMap {n : ℕ} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsStandardSyntomicOfRelativeDimension n R S] : SyntomicOfRelativeDimension n (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))

A standard syntomic algebra gives a syntomic morphism on spectra.

@[simp]

theorem TauCeti.AlgebraicGeometry.syntomicOfRelativeDimension_SpecMap_iff (n : ℕ) {R S : CommRingCat} (φ : R ⟶ S) : SyntomicOfRelativeDimension n (AlgebraicGeometry.Spec.map φ) ↔ RingHom.Locally (@IsStandardSyntomicOfRelativeDimension n) (CommRingCat.Hom.hom φ)

The affine criterion for syntomicity is localization on the source of the induced ring map.

instance TauCeti.AlgebraicGeometry.instSyntomicOfRelativeDimensionFstScheme (n : ℕ) {X Y S : AlgebraicGeometry.Scheme} (g : X ⟶ S) (h : Y ⟶ S) [SyntomicOfRelativeDimension n h] : SyntomicOfRelativeDimension n (CategoryTheory.Limits.pullback.fst g h)

Pulling back a syntomic morphism preserves its relative dimension.

instance TauCeti.AlgebraicGeometry.instSyntomicOfRelativeDimensionSndScheme (n : ℕ) {X Y S : AlgebraicGeometry.Scheme} (g : X ⟶ S) (h : Y ⟶ S) [SyntomicOfRelativeDimension n g] : SyntomicOfRelativeDimension n (CategoryTheory.Limits.pullback.snd g h)

Pulling back a syntomic morphism preserves its relative dimension.

@[instance 100]

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

A syntomic morphism of relative dimension n has all fibres of dimension at most n.