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.
Instances For
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
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.
Instances For
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.
Instances For
@[implicit_reducible]
@[implicit_reducible]
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
@[implicit_reducible]
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]
:
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)
Instances
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)
:
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].
Instances For
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.
Instances For
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₀]
:
(Implementation detail): The underlying AlgHom of tensorModelOfHasCoeffsEquiv.
Instances For
@[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₀]
:
(Implementation detail): The inverse of tensorModelOfHasCoeffsHom.
Instances For
@[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₀]
:
The natural isomorphism R ⊗[R₀] S₀ ≃ₐ[R] S.
Instances For
@[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₀]
:
The presubmersive presentation on P.ModelOfHasCoeffs R₀ provided P.HasCoeffs R₀.
Instances For
@[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_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_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_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
@[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_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)
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.
Instances For
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
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]
:
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
Instances
@[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₀.
Instances For
@[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₀.
Instances For
@[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₀.
Instances For
@[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₀.