Radial scaling records the homogeneous components as coefficients of a single polynomial.
noncomputable def
CCDN.quotientRadialMap
{K : Type u_1}
{σ : Type u_2}
[Field K]
(I : Ideal (MvPolynomial σ K))
:
The K-algebra map sending f to ∑ n, [f_n] T ^ n, where f_n is the degree-n
homogeneous component of f and [·] its class modulo I; it lands in the homogeneous
coordinate algebra projectiveCoordinateAlgebra I.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CCDN.quotientRadialMap_coeff
{K : Type u_1}
{σ : Type u_2}
[Field K]
(I : Ideal (MvPolynomial σ K))
(f : MvPolynomial σ K)
(n : ℕ)
:
(↑((quotientRadialMap I) f)).coeff n = (Ideal.Quotient.mk I) ((MvPolynomial.homogeneousComponent n) f)
The coefficient of T ^ n in the radial image of f is the class modulo I of the
degree-n homogeneous component of f.
theorem
CCDN.quotientRadialMap_homogeneous
{K : Type u_1}
{σ : Type u_2}
[Field K]
(I : Ideal (MvPolynomial σ K))
(f : MvPolynomial σ K)
(n : ℕ)
(hf : f.IsHomogeneous n)
:
The radial image of a homogeneous polynomial f of degree n is the class of f
placed in degree n of the homogeneous coordinate algebra.