Presentations on subrings

In this file we establish the API for realising a presentation over a subring of R. We define a property HasCoeffs R₀ for a presentation P to mean the (sub)ring R₀ contains the coefficients of the relations of P. subring R₀ of R that contains the coefficients of the relations In this case there exists a model of S over R₀, i.e., there exists an R₀-algebra S₀ such that S is isomorphic to R ⊗[R₀] S₀.

If the presentation is finite, R₀ may be chosen as a Noetherian ring. In this case, this API can be used to remove Noetherian hypothesis in certain cases.

def Algebra.Presentation.coeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) : Set R

The coefficients of a presentation are the coefficients of the relations.

Equations

• P.coeffs = ⋃ (i : σ), ↑(MvPolynomial.coeffs (P.relation i))

theorem Algebra.Presentation.coeffs_relation_subset_coeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (x : σ) : ↑(MvPolynomial.coeffs (P.relation x)) ⊆ P.coeffs

theorem Algebra.Presentation.finite_coeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} [Finite σ] : P.coeffs.Finite

def Algebra.Presentation.core {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) : Subalgebra ℤ R

The core of a presentation is the subalgebra generated by the coefficients of the relations.

Equations

• P.core = Algebra.adjoin ℤ P.coeffs

theorem Algebra.Presentation.coeffs_subset_core {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) : P.coeffs ⊆ ↑P.core

theorem Algebra.Presentation.coeffs_relation_subset_core {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (x : σ) : ↑(MvPolynomial.coeffs (P.relation x)) ⊆ ↑P.core

def Algebra.Presentation.Core {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) : Type u_1

The core coerced to a type for performance reasons.

Equations

• P.Core = ↥P.core

instance Algebra.Presentation.instCommRingCore {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} : CommRing P.Core

Equations

• Algebra.Presentation.instCommRingCore = P.core.toCommRing

instance Algebra.Presentation.instCore {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} : Algebra P.Core R

Equations

• Algebra.Presentation.instCore = P.core.toAlgebra

instance Algebra.Presentation.instFaithfulSMulCore {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} : FaithfulSMul P.Core R

instance Algebra.Presentation.instCore_1 {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} : Algebra P.Core S

Equations

• Algebra.Presentation.instCore_1 = P.core.toAlgebra

instance Algebra.Presentation.instIsScalarTowerCore {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} : IsScalarTower P.Core R S

instance Algebra.Presentation.instFiniteTypeIntCoreOfFinite {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} [Finite σ] : FiniteType ℤ P.Core

class Algebra.Presentation.HasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] : Prop

A ring R₀ has the coefficients of the presentation P if the coefficients of the relations of P lie in the image of R₀ in R. The smallest subring of R satisfying this is given by Algebra.Presentation.Core P.

• coeffs_subset_range : P.coeffs ⊆ Set.range ⇑(algebraMap R₀ R)

instance Algebra.Presentation.instHasCoeffsCore {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} : P.HasCoeffs P.Core

theorem Algebra.Presentation.coeffs_subset_range {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : P.coeffs ⊆ Set.range ⇑(algebraMap R₀ R)

theorem Algebra.Presentation.HasCoeffs.of_isScalarTower {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] {R₁ : Type u_6} [CommRing R₁] [Algebra R₀ R₁] [Algebra R₁ R] [IsScalarTower R₀ R₁ R] [Algebra R₁ S] [IsScalarTower R₁ R S] : P.HasCoeffs R₁

instance Algebra.Presentation.instHasCoeffsSubtypeMemSubalgebraAdjoin {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (s : Set R) : P.HasCoeffs ↥(adjoin R₀ s)

theorem Algebra.Presentation.HasCoeffs.coeffs_relation_mem_range {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (x : σ) : ↑(MvPolynomial.coeffs (P.relation x)) ⊆ Set.range ⇑(algebraMap R₀ R)

theorem Algebra.Presentation.HasCoeffs.relation_mem_range_map {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (x : σ) : P.relation x ∈ Set.range ⇑(MvPolynomial.map (algebraMap R₀ R))

noncomputable def Algebra.Presentation.relationOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (r : σ) : MvPolynomial ι R₀

The r-th relation of P as a polynomial in R₀. This is the (arbitrary) choice of a pre-image under the map R₀[X] → R[X].

Equations

• Algebra.Presentation.relationOfHasCoeffs R₀ r = Exists.choose ⋯

theorem Algebra.Presentation.map_relationOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (r : σ) : (MvPolynomial.map (algebraMap R₀ R)) (relationOfHasCoeffs R₀ r) = P.relation r

@[simp]

theorem Algebra.Presentation.aeval_val_relationOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (r : σ) : (MvPolynomial.aeval P.val) (relationOfHasCoeffs R₀ r) = 0

@[simp]

theorem Algebra.Presentation.algebraTensorAlgEquiv_symm_relation {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (r : σ) : (MvPolynomial.algebraTensorAlgEquiv R₀ R).symm (P.relation r) = 1 ⊗ₜ[R₀] relationOfHasCoeffs R₀ r

@[reducible, inline]

abbrev Algebra.Presentation.ModelOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : Type (max (max u_3 u_5) u_5 u_3)

The model of S over a R₀ that contains the coefficients of P is R₀[X] quotiented by the same relations.

Equations

• Algebra.Presentation.ModelOfHasCoeffs R₀ = (MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Algebra.Presentation.relationOfHasCoeffs R₀)))

instance Algebra.Presentation.instFinitePresentationModelOfHasCoeffsOfFinite {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] [Finite ι] [Finite σ] : FinitePresentation R₀ (ModelOfHasCoeffs R₀)

noncomputable def Algebra.Presentation.tensorModelOfHasCoeffsHom {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : TensorProduct R₀ R (ModelOfHasCoeffs R₀) →ₐ[R] S

(Implementation detail): The underlying AlgHom of tensorModelOfHasCoeffsEquiv.

Equations

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

@[simp]

theorem Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (x : R) (y : MvPolynomial ι R₀) : (P.tensorModelOfHasCoeffsHom R₀) (x ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (relationOfHasCoeffs R₀)))) y) = (algebraMap R S) x * (MvPolynomial.aeval P.val) y

noncomputable def Algebra.Presentation.tensorModelOfHasCoeffsInv {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : S →ₐ[R] TensorProduct R₀ R (ModelOfHasCoeffs R₀)

(Implementation detail): The inverse of tensorModelOfHasCoeffsHom.

Equations

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

@[simp]

theorem Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (x : MvPolynomial ι R₀) : (P.tensorModelOfHasCoeffsInv R₀) ((MvPolynomial.aeval P.val) x) = 1 ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (relationOfHasCoeffs R₀)))) x

noncomputable def Algebra.Presentation.tensorModelOfHasCoeffsEquiv {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : TensorProduct R₀ R (ModelOfHasCoeffs R₀) ≃ₐ[R] S

The natural isomorphism R ⊗[R₀] S₀ ≃ₐ[R] S.

Equations

• Algebra.Presentation.tensorModelOfHasCoeffsEquiv R₀ = AlgEquiv.ofAlgHom (P.tensorModelOfHasCoeffsHom R₀) (P.tensorModelOfHasCoeffsInv R₀) ⋯ ⋯

@[simp]

theorem Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (x : R) (y : MvPolynomial ι R₀) : (tensorModelOfHasCoeffsEquiv R₀) (x ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (relationOfHasCoeffs R₀)))) y) = (algebraMap R S) x * (MvPolynomial.aeval P.val) y

@[simp]

theorem Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] {P : Presentation R S ι σ} (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (x : MvPolynomial ι R₀) : (tensorModelOfHasCoeffsEquiv R₀).symm ((MvPolynomial.aeval P.val) x) = 1 ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (relationOfHasCoeffs R₀)))) x

noncomputable def Algebra.PreSubmersivePresentation.ofHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : PreSubmersivePresentation R₀ (Presentation.ModelOfHasCoeffs R₀) ι σ

The presubmersive presentation on P.ModelOfHasCoeffs R₀ provided P.HasCoeffs R₀.

Equations

• P.ofHasCoeffs R₀ = { toPresentation := Algebra.Presentation.naive (Function.surjInv ⋯) ⋯, map := P.map, map_inj := ⋯ }

@[simp]

theorem Algebra.PreSubmersivePresentation.ofHasCoeffs_σ' {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (b : MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀))) : (P.ofHasCoeffs R₀).σ' b = Function.surjInv ⋯ b

@[simp]

theorem Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (a : MvPolynomial ι R₀) (a✝ : Quotient (Submodule.quotientRel (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀))))) : SMul.smul a a✝ = Quotient.map' (fun (x : MvPolynomial ι R₀) => a * x) ⋯ a✝

@[simp]

theorem Algebra.PreSubmersivePresentation.ofHasCoeffs_map {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (a✝ : σ) : (P.ofHasCoeffs R₀).map a✝ = P.map a✝

@[simp]

theorem Algebra.PreSubmersivePresentation.ofHasCoeffs_val {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (i : ι) : (P.ofHasCoeffs R₀).val i = (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (MvPolynomial.X i)

@[simp]

theorem Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (a✝ : MvPolynomial ι R₀) : Algebra.algebraMap a✝ = (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) a✝

@[simp]

theorem Algebra.PreSubmersivePresentation.ofHasCoeffs_relation {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (r : σ) : (P.ofHasCoeffs R₀).relation r = Presentation.relationOfHasCoeffs R₀ r

theorem Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) [DecidableEq σ] [Fintype σ] : ∃ (v : σ → MvPolynomial ι R), ∑ i : σ, v i * P.relation i = P.jacobiMatrix.det * P.σ ↑⋯.unit⁻¹ - 1

noncomputable def Algebra.SubmersivePresentation.jacobianRelations {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (s : σ) : MvPolynomial ι R

An arbitrarily chosen relation exhibiting the fact that P.jacobian is invertible.

Equations

• P.jacobianRelations s = ⋯.choose s

theorem Algebra.SubmersivePresentation.jacobianRelations_spec {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) [DecidableEq σ] [Fintype σ] : ∑ i : σ, P.jacobianRelations i * P.relation i = P.jacobiMatrix.det * P.σ ↑⋯.unit⁻¹ - 1

def Algebra.SubmersivePresentation.coeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) : Set R

The set of coefficients that is enough to descend a submersive presentation P.

Equations

• P.coeffs = P.coeffs ∪ ↑(MvPolynomial.coeffs (P.σ ↑⋯.unit⁻¹)) ∪ ⋃ (i : σ), ↑(P.jacobianRelations i).coeffs

theorem Algebra.SubmersivePresentation.finite_coeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) : P.coeffs.Finite

theorem Algebra.SubmersivePresentation.coeffs_toPresentation_subset_coeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) : P.coeffs ⊆ P.coeffs

class Algebra.SubmersivePresentation.HasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] : Prop

A type class witnessing the fact that R₀ contains enough coefficients to descend P to a submersive presentation.

• coeffs_subset_range : P.coeffs ⊆ ↑(algebraMap R₀ R).range

@[instance 100]

instance Algebra.SubmersivePresentation.instHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : P.HasCoeffs R₀

noncomputable def Algebra.SubmersivePresentation.jacobianOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : MvPolynomial ι R₀

The jacobian of a presentation in the smaller coefficient ring, provided P.HasCoeffs R₀.

Equations

• P.jacobianOfHasCoeffs R₀ = (P.ofHasCoeffs R₀).jacobiMatrix.det

@[simp]

theorem Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] [Fintype σ] [DecidableEq σ] : (MvPolynomial.map (algebraMap R₀ R)) (P.jacobianOfHasCoeffs R₀) = P.jacobiMatrix.det

@[simp]

theorem Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : (MvPolynomial.aeval P.val) (P.jacobianOfHasCoeffs R₀) = P.jacobian

noncomputable def Algebra.SubmersivePresentation.invJacobianOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : MvPolynomial ι R₀

The inverse jacobian of a presentation in the smaller coefficient ring, provided P.HasCoeffs R₀.

Equations

• P.invJacobianOfHasCoeffs R₀ = Exists.choose ⋯

@[simp]

theorem Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : (MvPolynomial.map (algebraMap R₀ R)) (P.invJacobianOfHasCoeffs R₀) = P.σ ↑⋯.unit⁻¹

@[simp]

theorem Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : (MvPolynomial.aeval P.val) (P.invJacobianOfHasCoeffs R₀) = ↑⋯.unit⁻¹

noncomputable def Algebra.SubmersivePresentation.jacobianRelationsOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (i : σ) : MvPolynomial ι R₀

An arbitrarily chosen relation exhibiting the fact that P.jacobian is invertible, provided P.HasCoeffs R₀.

Equations

• P.jacobianRelationsOfHasCoeffs R₀ i = Exists.choose ⋯

@[simp]

theorem Algebra.SubmersivePresentation.map_jacobianRelationsOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] (i : σ) : (MvPolynomial.map (algebraMap R₀ R)) (P.jacobianRelationsOfHasCoeffs R₀ i) = P.jacobianRelations i

theorem Algebra.SubmersivePresentation.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] [FaithfulSMul R₀ R] [Fintype σ] : ∑ i : σ, P.jacobianRelationsOfHasCoeffs R₀ i * Presentation.relationOfHasCoeffs R₀ i = P.jacobianOfHasCoeffs R₀ * P.invJacobianOfHasCoeffs R₀ - 1

noncomputable def Algebra.SubmersivePresentation.ofHasCoeffs {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] [FaithfulSMul R₀ R] : SubmersivePresentation R₀ (Presentation.ModelOfHasCoeffs R₀) ι σ

The submersive presentation on P.ModelOfHasCoeffs R₀ provided P.HasCoeffs R₀.

Equations

• P.ofHasCoeffs R₀ = { toPreSubmersivePresentation := P.ofHasCoeffs R₀, jacobian_isUnit := ⋯ }