Submersive presentations

In this file we define PreSubmersivePresentation. This is a presentation P that has fewer relations than generators. More precisely there exists an injective map from σ to ι. To such a presentation we may associate a Jacobian. P is then a submersive presentation, if its Jacobian is invertible.

Algebras that admit such a presentation are called standard smooth. See Mathlib.RingTheory.Smooth.StandardSmooth for applications.

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

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 σ] : Module.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-submersive 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

noncomputable def Algebra.PreSubmersivePresentation.naive {R : Type u} {ι : Type w} {σ : Type t} [CommRing R] {v : ι → MvPolynomial σ R} (a : ι → σ) (ha : Function.Injective a) (s : MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R := Function.surjInv ⋯) (hs : ∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x := by apply Function.surjInv_eq) : PreSubmersivePresentation R (MvPolynomial σ R ⧸ Ideal.span (Set.range v)) σ ι

The naive pre-submersive presentation of a quotient R[Xᵢ] ⧸ (vⱼ). If the definitional equality of the section matters, it can be explicitly provided.

To construct the associated submersive presentation, use PreSubmersivePresentation.jacobiMatrix_naive.

Equations

• Algebra.PreSubmersivePresentation.naive a ha s hs = { toPresentation := Algebra.Presentation.naive s hs, map := a, map_inj := ha }

@[simp]

theorem Algebra.PreSubmersivePresentation.naive_toPresentation {R : Type u} {ι : Type w} {σ : Type t} [CommRing R] {v : ι → MvPolynomial σ R} (a : ι → σ) (ha : Function.Injective a) (s : MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R := Function.surjInv ⋯) (hs : ∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x := by apply Function.surjInv_eq) : (naive a ha s hs).toPresentation = Presentation.naive s hs

@[simp]

theorem Algebra.PreSubmersivePresentation.jacobiMatrix_naive {R : Type u} {ι : Type w} {σ : Type t} [CommRing R] {v : ι → MvPolynomial σ R} (a : ι → σ) (ha : Function.Injective a) (s : MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R := Function.surjInv ⋯) (hs : ∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x := by apply Function.surjInv_eq) [Fintype ι] [DecidableEq ι] (i j : ι) : (naive a ha s hs).jacobiMatrix i j = (MvPolynomial.pderiv (a i)) (v j)

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 ι' ≃ ι and σ' ≃ σ, this is the induced submersive 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 ι σ) : Module.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))