Scalar extension preserves the filtered Hilbert polynomial. Coefficient-linear functionals descend elements of the extended ideal. A functional nonzero on a leading coefficient preserves its leading exponent.
theorem
CCDN.standardExponents_scalar_extension
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{n : ℕ}
(I : Ideal (MvPolynomial (Fin n) K))
(m : MonomialOrder (Fin n))
:
Extending scalars along a field extension K → L does not change the standard exponents of an
ideal.
theorem
CCDN.filteredHilbertPolynomial_scalar_extension
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{n : ℕ}
(I : Ideal (MvPolynomial (Fin n) K))
:
Extending scalars along a field extension K → L preserves the filtered Hilbert polynomial of
an ideal.
theorem
CCDN.hasAffineDimensionDegree_scalar_extension
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{n m d : ℕ}
{J : Ideal (MvPolynomial (Fin n) K)}
(h : HasAffineDimensionDegree J m d)
:
HasAffineDimensionDegree (Ideal.map (MvPolynomial.map (algebraMap K L)) J) m d
Affine dimension and degree are preserved by extending the coefficient field.
theorem
CCDN.hasProjectiveDimensionDegree_scalar_extension
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{n m d : ℕ}
{J : Ideal (MvPolynomial (Fin n) K)}
(h : HasProjectiveDimensionDegree J m d)
:
HasProjectiveDimensionDegree (Ideal.map (MvPolynomial.map (algebraMap K L)) J) m d
Projective dimension and degree are preserved by extending the coefficient field.