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.

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

@[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.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)