Standard smooth algebras

In this file we define standard smooth algebras. For this we introduce the notion of a PreSubmersivePresentation. This is a presentation P that has fewer relations than generators. More precisely there exists an injective map from P.rels to P.vars. To such a presentation we may associate a jacobian. P is then a submersive presentation, if its jacobian is invertible.

Finally, a standard smooth algebra is an algebra that admits a submersive presentation.

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.

• PreSubmersivePresentation: A Presentation of S as R-algebra, equipped with an injective map P.map from P.rels to P.vars. This map is used to define the differential of a presubmersive presentation.

For a presubmersive presentation P of S over R we make the following definitions:

• PreSubmersivePresentation.differential: A linear endomorphism of P.rels → P.Ring sending the j-th standard basis vector, corresponding to the j-th relation, to the vector of partial derivatives of P.relation j with respect to the coordinates P.map i for i : P.rels.
• PreSubmersivePresentation.jacobian: The determinant of P.differential.
• PreSubmersivePresentation.jacobiMatrix: If P.rels has a Fintype instance, we may form the matrix corresponding to P.differential. Its determinant is P.jacobian.
• SubmersivePresentation: A submersive presentation is a finite, presubmersive presentation P with in S invertible jacobian.

Furthermore, for algebras we define:

• 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.

Finally, for ring homomorphisms we define:

• RingHom.IsStandardSmooth: A ring homomorphism R →+* S is standard smooth if S is standard smooth as R-algebra.
• RingHom.IsStandardSmoothOfRelativeDimension n: A ring homomorphism R →+* S is standard smooth of relative dimension n if S is standard smooth of relative dimension n as R-algebra.

TODO

• Show that the canonical presentation for localization away from an element is standard smooth of relative dimension 0.
• Show that the composition of submersive presentations of relative dimensions n and m is submersive of relative dimension n + m.
• Show that the module of Kaehler differentials of a standard smooth R-algebra S of relative dimension n is S-free of rank n. In particular this shows that the relative dimension is independent of the choice of the standard smooth presentation.
• Show that standard smooth algebras are smooth. This relies on the computation of the module of Kaehler differentials.
• Show that locally on the target, smooth algebras are standard smooth.

Implementation details

Standard smooth algebras and ring homomorphisms feature 4 universe levels: The universe levels of the rings involved and the universe levels of the types of the variables and relations.

Notes

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

structure Algebra.PreSubmersivePresentation (R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S] extends Algebra.Presentation : Type (max (max (max (t + 1) u) v) (w + 1))

A PreSubmersivePresentation of an R-algebra S is a Presentation with finitely-many relations equipped with an injective map : relations → vars.

This map determines how the differential of P is constructed. See PreSubmersivePresentation.differential for details.

• vars : Type w
• val : self.vars → S
• σ' : S → MvPolynomial self.vars R
• aeval_val_σ' : ∀ (s : S), (MvPolynomial.aeval self.val) (self.σ' s) = s
• rels : Type t
• relation : self.rels → self.Ring
• span_range_relation_eq_ker : Ideal.span (Set.range self.relation) = self.ker
• map : self.rels → self.vars

  A map from the relations type to the variables type. Used to compute the differential.

• map_inj : Function.Injective self.map
• relations_finite : Finite self.rels

theorem Algebra.PreSubmersivePresentation.map_inj {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (self : Algebra.PreSubmersivePresentation R S) : Function.Injective self.map

theorem Algebra.PreSubmersivePresentation.relations_finite {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (self : Algebra.PreSubmersivePresentation R S) : Finite self.rels

theorem Algebra.PreSubmersivePresentation.card_relations_le_card_vars_of_isFinite {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) [P.IsFinite] : Nat.card P.rels ≤ Nat.card P.vars

@[reducible, inline]

noncomputable abbrev Algebra.PreSubmersivePresentation.basis {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) : Basis P.rels P.Ring (P.rels → P.Ring)

The standard basis of P.rels → P.ring.

Equations

• P.basis = Pi.basisFun P.Ring P.rels

noncomputable def Algebra.PreSubmersivePresentation.differential {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) : (P.rels → P.Ring) →ₗ[P.Ring] P.rels → P.Ring

The differential of a P : PreSubmersivePresentation is a P.Ring-linear map on P.rels → P.Ring:

The j-th standard basis vector, corresponding to the j-th relation of P, is mapped to the vector of partial derivatives of P.relation j with respect to the coordinates P.map i for all i : P.rels.

The determinant of this map is the jacobian of P used to define when a PreSubmersivePresentation is submersive. See PreSubmersivePresentation.jacobian.

Equations

• P.differential = (P.basis.constr P.Ring) fun (j i : P.rels) => (MvPolynomial.pderiv (P.map i)) (P.relation j)

noncomputable def Algebra.PreSubmersivePresentation.jacobian {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) : S

The jacobian of a P : PreSubmersivePresentation is the determinant of P.differential viewed as element of S.

Equations

• P.jacobian = (algebraMap P.Ring S) (LinearMap.det P.differential)

noncomputable def Algebra.PreSubmersivePresentation.jacobiMatrix {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) [Fintype P.rels] [DecidableEq P.rels] : Matrix P.rels P.rels P.Ring

If P.rels has a Fintype and DecidableEq instance, the differential of P can be expressed in matrix form.

Equations

• P.jacobiMatrix = (LinearMap.toMatrix P.basis P.basis) P.differential

theorem Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) [Fintype P.rels] [DecidableEq P.rels] : P.jacobian = (algebraMap P.Ring S) P.jacobiMatrix.det

theorem Algebra.PreSubmersivePresentation.jacobiMatrix_apply {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) [Fintype P.rels] [DecidableEq P.rels] (i : P.rels) (j : P.rels) : P.jacobiMatrix i j = (MvPolynomial.pderiv (P.map i)) (P.relation j)

noncomputable def Algebra.PreSubmersivePresentation.ofBijectiveAlgebraMap {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (h : Function.Bijective ⇑(algebraMap R S)) : Algebra.PreSubmersivePresentation R S

If algebraMap R S is bijective, the empty generators are a pre-submersive presentation with no relations.

Equations

• One or more equations did not get rendered due to their size.

instance Algebra.PreSubmersivePresentation.instFintypeVarsOfBijectiveAlgebraMap {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (h : Function.Bijective ⇑(algebraMap R S)) : Fintype (Algebra.PreSubmersivePresentation.ofBijectiveAlgebraMap h).vars

Equations

• Algebra.PreSubmersivePresentation.instFintypeVarsOfBijectiveAlgebraMap h = inferInstanceAs (Fintype PEmpty.{?u.42 + 1} )

instance Algebra.PreSubmersivePresentation.instFintypeRelsOfBijectiveAlgebraMap {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (h : Function.Bijective ⇑(algebraMap R S)) : Fintype (Algebra.PreSubmersivePresentation.ofBijectiveAlgebraMap h).rels

Equations

• Algebra.PreSubmersivePresentation.instFintypeRelsOfBijectiveAlgebraMap h = inferInstanceAs (Fintype PEmpty.{?u.42 + 1} )

theorem Algebra.PreSubmersivePresentation.ofBijectiveAlgebraMap_jacobian {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (h : Function.Bijective ⇑(algebraMap R S)) : (Algebra.PreSubmersivePresentation.ofBijectiveAlgebraMap h).jacobian = 1

noncomputable def Algebra.PreSubmersivePresentation.baseChange {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] (P : Algebra.PreSubmersivePresentation R S) : Algebra.PreSubmersivePresentation T (TensorProduct R T S)

If P is a pre-submersive presentation of S over R and T is an R-algebra, we obtain a natural pre-submersive presentation of T ⊗[R] S over T.

Equations

• Algebra.PreSubmersivePresentation.baseChange T P = { toPresentation := Algebra.Presentation.baseChange T P.toPresentation, map := P.map, map_inj := ⋯, relations_finite := ⋯ }

theorem Algebra.PreSubmersivePresentation.baseChange_jacobian {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] (P : Algebra.PreSubmersivePresentation R S) : (Algebra.PreSubmersivePresentation.baseChange T P).jacobian = 1 ⊗ₜ[R] P.jacobian

structure Algebra.SubmersivePresentation (R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S] extends Algebra.PreSubmersivePresentation : Type (max (max (max (t + 1) u) v) (w + 1))

A PreSubmersivePresentation is submersive if its jacobian is a unit in S and the presentation is finite.

• vars : Type w
• val : self.vars → S
• σ' : S → MvPolynomial self.vars R
• aeval_val_σ' : ∀ (s : S), (MvPolynomial.aeval self.val) (self.σ' s) = s
• rels : Type t
• relation : self.rels → self.Ring
• span_range_relation_eq_ker : Ideal.span (Set.range self.relation) = self.ker
• map : self.rels → self.vars
• map_inj : Function.Injective self.map
• relations_finite : Finite self.rels
• jacobian_isUnit : IsUnit self.jacobian
• isFinite : self.IsFinite

theorem Algebra.SubmersivePresentation.jacobian_isUnit {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (self : Algebra.SubmersivePresentation R S) : IsUnit self.jacobian

theorem Algebra.SubmersivePresentation.isFinite {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (self : Algebra.SubmersivePresentation R S) : self.IsFinite

noncomputable def Algebra.SubmersivePresentation.ofBijectiveAlgebraMap {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (h : Function.Bijective ⇑(algebraMap R S)) : Algebra.SubmersivePresentation R S

If algebraMap R S is bijective, the empty generators are a submersive presentation with no relations.

Equations

• Algebra.SubmersivePresentation.ofBijectiveAlgebraMap h = { toPreSubmersivePresentation := Algebra.PreSubmersivePresentation.ofBijectiveAlgebraMap h, jacobian_isUnit := ⋯, isFinite := ⋯ }

noncomputable def Algebra.SubmersivePresentation.id (R : Type u) [CommRing R] : Algebra.SubmersivePresentation R R

The canonical submersive R-presentation of R with no generators and no relations.

Equations

• Algebra.SubmersivePresentation.id R = Algebra.SubmersivePresentation.ofBijectiveAlgebraMap ⋯

noncomputable def Algebra.SubmersivePresentation.baseChange (R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] (P : Algebra.SubmersivePresentation R S) : Algebra.SubmersivePresentation T (TensorProduct R T S)

If P is a submersive presentation of S over R and T is an R-algebra, we obtain a natural submersive presentation of T ⊗[R] S over T.

Equations

• One or more equations did not get rendered due to their size.

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

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

• out : Nonempty (Algebra.SubmersivePresentation R S)

theorem Algebra.IsStandardSmooth.out {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [self : Algebra.IsStandardSmooth R S] : Nonempty (Algebra.SubmersivePresentation R S)

noncomputable def Algebra.IsStandardSmooth.relativeDimension (R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S] [Algebra.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] (TODO).

Equations

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

class Algebra.IsStandardSmoothOfRelativeDimension (n : ℕ) (R : Type u) [CommRing R] (S : Type v) [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 : ∃ (P : Algebra.SubmersivePresentation R S), P.dimension = n

theorem Algebra.IsStandardSmoothOfRelativeDimension.out {n : ℕ} {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [self : Algebra.IsStandardSmoothOfRelativeDimension n R S] : ∃ (P : Algebra.SubmersivePresentation R S), P.dimension = n

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

def RingHom.IsStandardSmooth {R : Type u} [CommRing R] {S : Type v} [CommRing S] (f : R →+* S) : Prop

A ring homomorphism R →+* S is standard smooth if S is standard smooth as R-algebra.

Equations

• f.IsStandardSmooth = Algebra.IsStandardSmooth R S

def RingHom.IsStandardSmoothOfRelativeDimension (n : ℕ) {R : Type u} [CommRing R] {S : Type v} [CommRing S] (f : R →+* S) : Prop

A ring homomorphism R →+* S is standard smooth of relative dimension n if S is standard smooth of relative dimension n as R-algebra.

Equations

• RingHom.IsStandardSmoothOfRelativeDimension n f = Algebra.IsStandardSmoothOfRelativeDimension n R S

theorem RingHom.IsStandardSmoothOfRelativeDimension.isStandardSmooth (n : ℕ) {R : Type u} [CommRing R] {S : Type v} [CommRing S] (f : R →+* S) (hf : RingHom.IsStandardSmoothOfRelativeDimension n f) : f.IsStandardSmooth