Standard smooth algebras

A standard smooth algebra is an algebra that admits a SubmersivePresentation. A standard smooth algebra is of relative dimension n if it admits a submersive presentation of dimension n.

While every standard smooth algebra is smooth, the converse does not hold. But if S is R-smooth, then S is R-standard smooth locally on S, i.e. there exists a set { t } of S that generates the unit ideal, such that Sₜ is R-standard smooth for every t (TODO, see below).

Main definitions

All of these are in the Algebra namespace. Let S be an R-algebra.

• Algebra.IsStandardSmooth: S is R-standard smooth if S admits a submersive R-presentation.
• Algebra.IsStandardSmooth.relativeDimension: If S is R-standard smooth this is the dimension of an arbitrary submersive R-presentation of S. This is independent of the choice of the presentation (TODO, see below).
• Algebra.IsStandardSmoothOfRelativeDimension n: S is R-standard smooth of relative dimension n if it admits a submersive R-presentation of dimension n.

Main results

• Algebra.IsStandardSmoothOfRelativeDimension.mvPolynomial: If ι is finite, the polynomial algebra MvPolynomial ι R is R-standard smooth of relative dimension Nat.card ι.
• Standard smoothness is stable under composition (Algebra.IsStandardSmooth.trans), base change (Algebra.IsStandardSmooth.baseChange) and localization away from an element (Algebra.IsStandardSmooth.localization_away), and similarly for standard smoothness of a fixed relative dimension.
• Algebra.IsStandardSmooth.finitePresentation: A standard smooth algebra is of finite presentation.

TODO

• Show that locally on the target, smooth algebras are standard smooth.

Notes

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

class Algebra.IsStandardSmooth (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Prop

An R-algebra S is called standard smooth, if there exists a submersive presentation.

• out : ∃ (ι : Type) (σ : Type) (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation R S ι σ)

theorem Algebra.SubmersivePresentation.isStandardSmooth {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] [Finite ι] (P : SubmersivePresentation R S ι σ) : IsStandardSmooth R S

noncomputable def Algebra.IsStandardSmooth.relativeDimension (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] [IsStandardSmooth R S] : ℕ

The relative dimension of a standard smooth R-algebra S is the dimension of an arbitrarily chosen submersive R-presentation of S.

Note: If S is non-trivial, this number is independent of the choice of the presentation as it is equal to the S-rank of Ω[S/R] (see IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential).

Equations

• Algebra.IsStandardSmooth.relativeDimension R S = ⋯.some.dimension

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

An R-algebra S is called standard smooth of relative dimension n, if there exists a submersive presentation of dimension n.

• out : ∃ (ι : Type) (σ : Type) (x : Finite σ) (_ : Finite ι) (P : SubmersivePresentation R S ι σ), P.dimension = n

theorem Algebra.SubmersivePresentation.isStandardSmoothOfRelativeDimension {n : ℕ} {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] [Finite ι] (P : SubmersivePresentation R S ι σ) (hP : P.dimension = n) : IsStandardSmoothOfRelativeDimension n R S

theorem Algebra.IsStandardSmoothOfRelativeDimension.isStandardSmooth (n : ℕ) {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [H : IsStandardSmoothOfRelativeDimension n R S] : IsStandardSmooth R S

theorem Algebra.IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (h : Function.Bijective ⇑(algebraMap R S)) : IsStandardSmoothOfRelativeDimension 0 R S

instance Algebra.IsStandardSmoothOfRelativeDimension.id (R : Type u) [CommRing R] : IsStandardSmoothOfRelativeDimension 0 R R

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

The polynomial algebra MvPolynomial ι R is standard smooth over R of relative dimension Nat.card ι, for a finite type ι.

instance Algebra.IsStandardSmoothOfRelativeDimension.mvPolynomial_fin {R : Type u} [CommRing R] {n : ℕ} : IsStandardSmoothOfRelativeDimension n R (MvPolynomial (Fin n) R)

The polynomial algebra MvPolynomial (Fin n) R is standard smooth over R of relative dimension n.

instance Algebra.IsStandardSmooth.mvPolynomial {R : Type u} (ι : Type w) [CommRing R] [Finite ι] : IsStandardSmooth R (MvPolynomial ι R)

The polynomial algebra MvPolynomial ι R is standard smooth over R when ι is finite.

@[instance 100]

instance Algebra.IsStandardSmooth.finitePresentation {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [IsStandardSmooth R S] : FinitePresentation R S

theorem Algebra.IsStandardSmooth.of_algEquiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] (e : S ≃ₐ[R] T) [IsStandardSmooth R S] : IsStandardSmooth R T

theorem Algebra.IsStandardSmoothOfRelativeDimension.of_algEquiv (n : ℕ) {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] (e : S ≃ₐ[R] T) [IsStandardSmoothOfRelativeDimension n R S] : IsStandardSmoothOfRelativeDimension n R T

theorem Algebra.IsStandardSmooth.trans (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsStandardSmooth R S] [IsStandardSmooth S T] : IsStandardSmooth R T

theorem Algebra.IsStandardSmoothOfRelativeDimension.trans (n m : ℕ) (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsStandardSmoothOfRelativeDimension n R S] [IsStandardSmoothOfRelativeDimension m S T] : IsStandardSmoothOfRelativeDimension (m + n) R T

theorem Algebra.IsStandardSmooth.localization_away {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : IsStandardSmooth R S

theorem Algebra.IsStandardSmoothOfRelativeDimension.localization_away {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : IsStandardSmoothOfRelativeDimension 0 R S

instance Algebra.IsStandardSmooth.baseChange {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] [IsStandardSmooth R S] : IsStandardSmooth T (TensorProduct R T S)

instance Algebra.IsStandardSmoothOfRelativeDimension.baseChange (n : ℕ) {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] [IsStandardSmoothOfRelativeDimension n R S] : IsStandardSmoothOfRelativeDimension n T (TensorProduct R T S)

@[instance 100]

instance Algebra.instIsStandardSmoothOfSubsingleton {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Subsingleton S] : IsStandardSmooth R S

@[instance 100]

instance Algebra.instIsStandardSmoothOfRelativeDimensionOfNatNatOfSubsingleton {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Subsingleton S] : IsStandardSmoothOfRelativeDimension 0 R S