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 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) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] extends Algebra.Presentation R S : 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.card_relations_le_card_vars_of_isFinite {R : Type u} {S : Type v} [CommRing R] [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} {S : Type v} [CommRing R] [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} {S : Type v} [CommRing R] [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} {S : Type v} [CommRing R] [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} {S : Type v} [CommRing R] [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} {S : Type v} [CommRing R] [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} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) [Fintype P.rels] [DecidableEq P.rels] (i j : P.rels) : P.jacobiMatrix i j = (MvPolynomial.pderiv (P.map i)) (P.relation j)

noncomputable def Algebra.PreSubmersivePresentation.ofBijectiveAlgebraMap {R : Type u} {S : Type v} [CommRing R] [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} {S : Type v} [CommRing R] [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} {S : Type v} [CommRing R] [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})

@[simp]

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

noncomputable def Algebra.PreSubmersivePresentation.localizationAway {R : Type u} (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : Algebra.PreSubmersivePresentation R S

If S is the localization of R at r, this is the canonical submersive presentation of S as R-algebra.

Equations

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

@[simp]

theorem Algebra.PreSubmersivePresentation.localizationAway_map {R : Type u} (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] (x✝ : (Algebra.Presentation.localizationAway S r).rels) : (Algebra.PreSubmersivePresentation.localizationAway S r).map x✝ = ()

instance Algebra.PreSubmersivePresentation.instFintypeRelsLocalizationAway {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : Fintype (Algebra.PreSubmersivePresentation.localizationAway S r).rels

Equations

• Algebra.PreSubmersivePresentation.instFintypeRelsLocalizationAway r = inferInstanceAs (Fintype Unit)

instance Algebra.PreSubmersivePresentation.instDecidableEqRelsLocalizationAway {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : DecidableEq (Algebra.PreSubmersivePresentation.localizationAway S r).rels

Equations

• Algebra.PreSubmersivePresentation.instDecidableEqRelsLocalizationAway r = inferInstanceAs (DecidableEq Unit)

@[simp]

theorem Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : (Algebra.PreSubmersivePresentation.localizationAway S r).jacobiMatrix = Matrix.diagonal fun (x : (Algebra.PreSubmersivePresentation.localizationAway S r).rels) => MvPolynomial.C r

@[simp]

theorem Algebra.PreSubmersivePresentation.localizationAway_jacobian {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : (Algebra.PreSubmersivePresentation.localizationAway S r).jacobian = (algebraMap R S) r

noncomputable def Algebra.PreSubmersivePresentation.comp {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] (Q : Algebra.PreSubmersivePresentation S T) (P : Algebra.PreSubmersivePresentation R S) : Algebra.PreSubmersivePresentation R T

Given an R-algebra S and an S-algebra T with pre-submersive presentations, this is the canonical pre-submersive presentation of T as an R-algebra.

Equations

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

@[simp]

theorem Algebra.PreSubmersivePresentation.comp_map {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] (Q : Algebra.PreSubmersivePresentation S T) (P : Algebra.PreSubmersivePresentation R S) (a✝ : Q.rels ⊕ P.rels) : (Q.comp P).map a✝ = Sum.elim (fun (rq : Q.rels) => Sum.inl (Q.map rq)) (fun (rp : P.rels) => Sum.inr (P.map rp)) a✝

theorem Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_3} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.PreSubmersivePresentation S T) (P : Algebra.PreSubmersivePresentation R S) [Q.IsFinite] [P.IsFinite] : (Q.comp P).dimension = Q.dimension + P.dimension

The dimension of the composition of two finite submersive presentations is the sum of the dimensions.

Jacobian of composition

Let S be an R-algebra and T be an S-algebra with presentations P and Q respectively. In this section we compute the jacobian of the composition of Q and P to be the product of the jacobians. For this we use a block decomposition of the jacobi matrix and show that the upper-right block vanishes, the upper-left block has determinant jacobian of Q and the lower-right block has determinant jacobian of P.

@[simp]

theorem Algebra.PreSubmersivePresentation.comp_jacobian_eq_jacobian_smul_jacobian {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] (Q : Algebra.PreSubmersivePresentation S T) (P : Algebra.PreSubmersivePresentation R S) : (Q.comp P).jacobian = P.jacobian • Q.jacobian

The jacobian of the composition of presentations is the product of the jacobians.

noncomputable def Algebra.PreSubmersivePresentation.baseChange {R : Type u} {S : Type v} [CommRing R] [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 := ⋯ }

@[simp]

theorem Algebra.PreSubmersivePresentation.baseChange_jacobian {R : Type u} {S : Type v} [CommRing R] [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) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] extends Algebra.PreSubmersivePresentation R S : 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

noncomputable def Algebra.SubmersivePresentation.ofBijectiveAlgebraMap {R : Type u} {S : Type v} [CommRing R] [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.comp {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] (Q : Algebra.SubmersivePresentation S T) (P : Algebra.SubmersivePresentation R S) : Algebra.SubmersivePresentation R T

Given an R-algebra S and an S-algebra T with submersive presentations, this is the canonical submersive presentation of T as an R-algebra.

Equations

• Q.comp P = { toPreSubmersivePresentation := Q.comp P.toPreSubmersivePresentation, jacobian_isUnit := ⋯, isFinite := ⋯ }

noncomputable def Algebra.SubmersivePresentation.localizationAway {R : Type u} (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : Algebra.SubmersivePresentation R S

If S is the localization of R at r, this is the canonical submersive presentation of S as R-algebra.

Equations

• Algebra.SubmersivePresentation.localizationAway S r = { toPreSubmersivePresentation := Algebra.PreSubmersivePresentation.localizationAway S r, jacobian_isUnit := ⋯, isFinite := ⋯ }

noncomputable def Algebra.SubmersivePresentation.baseChange (R : Type u) (S : Type v) [CommRing R] [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) (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 : Nonempty (Algebra.SubmersivePresentation R S)

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

theorem Algebra.IsStandardSmoothOfRelativeDimension.isStandardSmooth (n : ℕ) {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsStandardSmoothOfRelativeDimension n R S] : Algebra.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)) : Algebra.IsStandardSmoothOfRelativeDimension 0 R S

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

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] [Algebra.IsStandardSmooth R S] [Algebra.IsStandardSmooth S T] : Algebra.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] [Algebra.IsStandardSmoothOfRelativeDimension n R S] [Algebra.IsStandardSmoothOfRelativeDimension m S T] : Algebra.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] : Algebra.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] : Algebra.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] [Algebra.IsStandardSmooth R S] : Algebra.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] [Algebra.IsStandardSmoothOfRelativeDimension n R S] : Algebra.IsStandardSmoothOfRelativeDimension n T (TensorProduct R T S)