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 σ to P.ι. 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 σ 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.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 : σ.
• PreSubmersivePresentation.jacobian: The determinant of P.differential.
• PreSubmersivePresentation.jacobiMatrix: If σ 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) (ι : Type w) (σ : Type t) [CommRing R] [CommRing S] [Algebra R S] extends Algebra.Presentation R S ι σ : Type (max (max (max t u) v) w)

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

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

• val : ι → S
• σ' : S → MvPolynomial ι R
• aeval_val_σ' (s : S) : (MvPolynomial.aeval self.val) (self.σ' s) = s
• algebra : Algebra (MvPolynomial ι R) S
• algebraMap_eq : algebraMap (MvPolynomial ι R) S = ↑(MvPolynomial.aeval self.val)
• relation : σ → self.Ring
• span_range_relation_eq_ker : Ideal.span (Set.range self.relation) = self.ker
• map : σ → ι

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

• map_inj : Function.Injective self.map

theorem Algebra.PreSubmersivePresentation.card_relations_le_card_vars_of_isFinite {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) [Finite ι] : Nat.card σ ≤ Nat.card ι

@[reducible, inline]

noncomputable abbrev Algebra.PreSubmersivePresentation.basis {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) [Finite σ] : Basis σ P.Ring (σ → P.Ring)

The standard basis of σ → P.ring.

Equations

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

noncomputable def Algebra.PreSubmersivePresentation.differential {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) [Finite σ] : (σ → P.Ring) →ₗ[P.Ring] σ → P.Ring

The differential of a P : PreSubmersivePresentation is a P.Ring-linear map on σ → 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 : σ.

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 : σ) => (MvPolynomial.pderiv (P.map i)) (P.relation j)

noncomputable def Algebra.PreSubmersivePresentation.aevalDifferential {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) [Finite σ] : (σ → S) →ₗ[S] σ → S

PreSubmersivePresentation.differential pushed forward to S via aeval P.val.

Equations

• P.aevalDifferential = ((Pi.basisFun S σ).constr S) fun (j i : σ) => (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map i)) (P.relation j))

@[simp]

theorem Algebra.PreSubmersivePresentation.aevalDifferential_single {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) [Finite σ] [DecidableEq σ] (i j : σ) : P.aevalDifferential (Pi.single i 1) j = (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map j)) (P.relation i))

noncomputable def Algebra.PreSubmersivePresentation.jacobian {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) [Finite σ] : 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} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) [Fintype σ] [DecidableEq σ] : Matrix σ σ P.Ring

If σ 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} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) [Fintype σ] [DecidableEq σ] : P.jacobian = (algebraMap P.Ring S) P.jacobiMatrix.det

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

theorem Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) [Fintype σ] [DecidableEq σ] : LinearMap.toMatrix' P.aevalDifferential = (MvPolynomial.aeval P.val).mapMatrix P.jacobiMatrix

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

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.

@[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)) : (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] : PreSubmersivePresentation R S Unit Unit

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

Equations

• Algebra.PreSubmersivePresentation.localizationAway S r = { toPresentation := Algebra.Presentation.localizationAway S r, map := fun (x : Unit) => (), map_inj := ⋯ }

@[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✝ : Unit) : (localizationAway S r).map x✝ = ()

@[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] : (localizationAway S r).jacobiMatrix = Matrix.diagonal fun (x : Unit) => 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] : (localizationAway S r).jacobian = (algebraMap R S) r

noncomputable def Algebra.PreSubmersivePresentation.comp {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : PreSubmersivePresentation S T ι' σ') (P : PreSubmersivePresentation R S ι σ) : 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

• Q.comp P = { toPresentation := Q.comp P.toPresentation, map := Sum.elim (fun (rq : σ') => Sum.inl (Q.map rq)) fun (rp : σ) => Sum.inr (P.map rp), map_inj := ⋯ }

@[simp]

theorem Algebra.PreSubmersivePresentation.comp_map {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : PreSubmersivePresentation S T ι' σ') (P : PreSubmersivePresentation R S ι σ) (a✝ : σ' ⊕ σ) : (Q.comp P).map a✝ = Sum.elim (fun (rq : σ') => Sum.inl (Q.map rq)) (fun (rp : σ) => Sum.inr (P.map rp)) a✝

theorem Algebra.PreSubmersivePresentation.toPresentation_comp {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : PreSubmersivePresentation S T ι' σ') (P : PreSubmersivePresentation R S ι σ) : (Q.comp P).toPresentation = Q.comp P.toPresentation

theorem Algebra.PreSubmersivePresentation.toGenerators_comp {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : PreSubmersivePresentation S T ι' σ') (P : PreSubmersivePresentation R S ι σ) : (Q.comp P).toGenerators = Q.comp P.toGenerators

theorem Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : PreSubmersivePresentation S T ι' σ') (P : PreSubmersivePresentation R S ι σ) [Finite ι] [Finite ι'] [Finite σ] [Finite σ'] : (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} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : PreSubmersivePresentation S T ι' σ') (P : PreSubmersivePresentation R S ι σ) [Finite σ] [Finite σ'] : (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} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] (P : PreSubmersivePresentation R S ι σ) : 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 := ⋯ }

theorem Algebra.PreSubmersivePresentation.baseChange_toPresentation {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) : (baseChange R P).toPresentation = Presentation.baseChange R P.toPresentation

theorem Algebra.PreSubmersivePresentation.baseChange_ring {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) : (baseChange R P).Ring = P.Ring

@[simp]

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

noncomputable def Algebra.PreSubmersivePresentation.reindex {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ) : PreSubmersivePresentation R S ι' σ'

Given a pre-submersive presentation P and equivalences ι' ≃ ι and σ' ≃ σ, this is the induced pre-sumbersive presentation with variables indexed by ι and relations indexed by `κ

Equations

• P.reindex e f = { toPresentation := P.reindex e f, map := ⇑e.symm ∘ P.map ∘ ⇑f, map_inj := ⋯ }

@[simp]

theorem Algebra.PreSubmersivePresentation.reindex_toPresentation {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ) : (P.reindex e f).toPresentation = P.reindex e f

theorem Algebra.PreSubmersivePresentation.reindex_map {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ) (a✝ : σ') : (P.reindex e f).map a✝ = (⇑e.symm ∘ P.map ∘ ⇑f) a✝

theorem Algebra.PreSubmersivePresentation.jacobiMatrix_reindex {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ) [Fintype σ'] [DecidableEq σ'] [Fintype σ] [DecidableEq σ] : (P.reindex e f).jacobiMatrix = ((Matrix.reindex f.symm f.symm) P.jacobiMatrix).map ⇑(MvPolynomial.rename ⇑e.symm)

@[simp]

theorem Algebra.PreSubmersivePresentation.jacobian_reindex {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ) [Finite σ] [Finite σ'] : (P.reindex e f).jacobian = P.jacobian

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

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

• val : ι → S
• σ' : S → MvPolynomial ι R
• aeval_val_σ' (s : S) : (MvPolynomial.aeval self.val) (self.σ' s) = s
• algebra : Algebra (MvPolynomial ι R) S
• algebraMap_eq : algebraMap (MvPolynomial ι R) S = ↑(MvPolynomial.aeval self.val)
• relation : σ → self.Ring
• span_range_relation_eq_ker : Ideal.span (Set.range self.relation) = self.ker
• map : σ → ι
• map_inj : Function.Injective self.map
• jacobian_isUnit : IsUnit self.jacobian

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

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 := ⋯ }

noncomputable def Algebra.SubmersivePresentation.id (R : Type u) [CommRing R] : SubmersivePresentation R R PEmpty.{w + 1} PEmpty.{t + 1}

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} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] {T : Type u_1} {ι' : Type u_2} {σ' : Type u_3} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Finite σ'] (Q : SubmersivePresentation S T ι' σ') (P : SubmersivePresentation R S ι σ) : 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 := ⋯ }

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

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 := ⋯ }

noncomputable def Algebra.SubmersivePresentation.baseChange {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (T : Type u_1) [CommRing T] [Algebra R T] (P : SubmersivePresentation R S ι σ) : 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

• Algebra.SubmersivePresentation.baseChange T P = { toPreSubmersivePresentation := Algebra.PreSubmersivePresentation.baseChange T P.toPreSubmersivePresentation, jacobian_isUnit := ⋯ }

noncomputable def Algebra.SubmersivePresentation.reindex {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} [Finite σ'] (e : ι' ≃ ι) (f : σ' ≃ σ) : SubmersivePresentation R S ι' σ'

Given a submersive presentation P and equivalences ι ≃ P.vars and κ ≃ σ, this is the induced sumbersive presentation with variables indexed by ι and relations indexed by `κ

Equations

• P.reindex e f = { toPreSubmersivePresentation := P.reindex e f, jacobian_isUnit := ⋯ }

@[simp]

theorem Algebra.SubmersivePresentation.reindex_toPreSubmersivePresentation {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} [Finite σ'] (e : ι' ≃ ι) (f : σ' ≃ σ) : (P.reindex e f).toPreSubmersivePresentation = P.reindex e f

noncomputable def Algebra.SubmersivePresentation.aevalDifferentialEquiv {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) : (σ → S) ≃ₗ[S] σ → S

If P is submersive, PreSubmersivePresentation.aevalDifferential is an isomorphism.

Equations

• P.aevalDifferentialEquiv = LinearEquiv.ofIsUnitDet ⋯

@[simp]

theorem Algebra.SubmersivePresentation.aevalDifferentialEquiv_apply {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) [Finite σ] (x : σ → S) : P.aevalDifferentialEquiv x = P.aevalDifferential x

noncomputable def Algebra.SubmersivePresentation.basisDeriv {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) : Basis σ S (σ → S)

If P is a submersive presentation, the partial derivatives of P.relation i by P.map j form a basis of σ → S.

Equations

• P.basisDeriv = (Pi.basisFun S σ).map P.aevalDifferentialEquiv

@[simp]

theorem Algebra.SubmersivePresentation.basisDeriv_apply {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (i j : σ) : P.basisDeriv i j = (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map j)) (P.relation i))

theorem Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) : LinearIndependent S fun (i j : σ) => (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map j)) (P.relation i))

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)