Standard syntomic algebras

An R-algebra S is a relative global complete intersection if it has a presentation S = R[x₁, …, x_m] ⧸ (f₁, …, f_c) such that every nonempty fibre κ(p) ⊗[R] S has Krull dimension m - c; it is standard syntomic if moreover S is flat over R. Standard syntomic algebras are the local models of syntomic morphisms (flat, locally finitely presented local complete intersections): a ring map is syntomic exactly when it is standard syntomic locally on the source. Standard smooth algebras and the local model R[x, y] ⧸ (xy - a) of a node are standard syntomic, and a family of nodal curves is a syntomic morphism of relative dimension one.

We record the relative dimension m - c, which is the dimension of the nonempty fibres, and require m = n + c for a presentation with m generators and c relations. Note that Mathlib's Algebra.Presentation.dimension is the truncated difference m - c; demanding m = n + c instead excludes presentations with more relations than generators, so that, for example, k[x, y] ⧸ (x², xy, y²), which is flat over the field k with fibre of dimension zero but is not a complete intersection, is not standard syntomic of relative dimension zero.

Main definitions

• TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension n R S: S is flat over R, has a finite presentation with n + c generators and c relations, and every nontrivial fibre κ(p) ⊗[R] S has Krull dimension n.

Main results

• TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.ringKrullDim_tensorProduct_of_field: the dimension condition holds for all fibres over fields, not just over residue fields: if R → K is a ring map to a field and K ⊗[R] S is nontrivial, it has Krull dimension n.
• TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.isPureDimensional_primeSpectrum: over a field, the spectrum of a standard syntomic algebra of relative dimension n is pure-dimensional of dimension n, since it is a global complete intersection.
• TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.baseChange: standard syntomic algebras of relative dimension n are stable under arbitrary base change.
• TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.of_algEquiv: invariance under isomorphism.
• TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.mvPolynomial: a polynomial algebra in finitely many variables is standard syntomic of relative dimension the number of variables.

References

• The Stacks Project, Commutative Algebra, Section Syntomic morphisms: the definitions of relative global complete intersections and of standard syntomic ring maps, and the characterization of syntomic ring maps as those that are standard syntomic locally on the source.
• The shape of the definition, a class asserting the existence of a presentation with a prescribed number of generators and relations, and its basic API (mvPolynomial, mvPolynomial_fin, baseChange) are modelled on Mathlib's Algebra.IsStandardSmoothOfRelativeDimension in Mathlib/RingTheory/Smooth/StandardSmooth.lean, by Jung Tao Cheng, Christian Merten and Andrew Yang.

class TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension (n : ℕ) (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Prop

An R-algebra S is standard syntomic of relative dimension n if it is flat over R and has a finite presentation S = R[x₁, …, x_{n+c}] ⧸ (f₁, …, f_c) which is a relative global complete intersection: every nontrivial fibre κ(p) ⊗[R] S over a prime p of R has Krull dimension n. The fibre condition does not depend on the presentation.

• flat : Module.Flat R S

  A standard syntomic algebra is flat.

• exists_presentation : ∃ (ι : Type) (σ : Type) (_ : Finite ι) (_ : Finite σ) (x : Algebra.Presentation R S ι σ), Nat.card ι = n + Nat.card σ

  A presentation with n + c generators and c relations.

• ringKrullDim_fiber (p : Ideal R) [p.IsPrime] [Nontrivial (p.Fiber S)] : ringKrullDim (p.Fiber S) = ↑n

  Every nonempty fibre has Krull dimension n.

theorem Algebra.Presentation.isStandardSyntomicOfRelativeDimension {n : ℕ} {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] {ι : Type w} {σ : Type u_1} [Finite ι] [Finite σ] (P : Presentation R S ι σ) (hP : Nat.card ι = n + Nat.card σ) (hfib : ∀ (p : Ideal R) [inst : p.IsPrime] [Nontrivial (p.Fiber S)], ringKrullDim (p.Fiber S) = ↑n) : TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension n R S

A finite presentation of a flat algebra with n + c generators and c relations, all of whose nontrivial fibres have Krull dimension n, exhibits it as standard syntomic of relative dimension n.

theorem TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.finitePresentation {n : ℕ} {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [h : IsStandardSyntomicOfRelativeDimension n R S] : Algebra.FinitePresentation R S

A standard syntomic algebra is of finite presentation.

theorem TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.ringKrullDim_fiber_le {n : ℕ} {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [h : IsStandardSyntomicOfRelativeDimension n R S] (p : Ideal R) [p.IsPrime] : ringKrullDim (p.Fiber S) ≤ ↑n

Every fibre of a standard syntomic algebra of relative dimension n has Krull dimension at most n; the empty fibres have dimension ⊥.

theorem TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.ringKrullDim_tensorProduct_of_field {n : ℕ} {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [h : IsStandardSyntomicOfRelativeDimension n R S] (K : Type w) [Field K] [Algebra R K] [Nontrivial (TensorProduct R K S)] : ringKrullDim (TensorProduct R K S) = ↑n

The fibres of a standard syntomic algebra of relative dimension n over arbitrary fields have Krull dimension n: if R → K is a ring map to a field and K ⊗[R] S is nontrivial, then it has Krull dimension n.

theorem TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.isPureDimensional_primeSpectrum (n : ℕ) (k : Type u) (A : Type v) [Field k] [CommRing A] [Algebra k A] [hA : IsStandardSyntomicOfRelativeDimension n k A] : IsPureDimensional n (PrimeSpectrum A)

Over a field k, the spectrum of a standard syntomic algebra of relative dimension n is pure-dimensional of dimension n: every irreducible component has dimension n.

theorem TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.of_algEquiv {n : ℕ} {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [h : IsStandardSyntomicOfRelativeDimension n R S] {S' : Type u_1} [CommRing S'] [Algebra R S'] (e : S ≃ₐ[R] S') : IsStandardSyntomicOfRelativeDimension n R S'

Standard syntomic algebras of relative dimension n are invariant under isomorphism.

instance TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.baseChange {n : ℕ} {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [h : IsStandardSyntomicOfRelativeDimension n R S] (T : Type w) [CommRing T] [Algebra R T] : IsStandardSyntomicOfRelativeDimension n T (TensorProduct R T S)

Standard syntomic algebras of relative dimension n are stable under base change.

theorem TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.mvPolynomial (R : Type u) [CommRing R] (ι : Type w) [Finite ι] : IsStandardSyntomicOfRelativeDimension (Nat.card ι) R (MvPolynomial ι R)

A polynomial algebra in finitely many variables indexed by ι is standard syntomic of relative dimension Nat.card ι.

instance TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.mvPolynomial_fin (n : ℕ) (R : Type u) [CommRing R] : IsStandardSyntomicOfRelativeDimension n R (MvPolynomial (Fin n) R)

A polynomial algebra in n variables is standard syntomic of relative dimension n.