Homogeneous coefficient descent and homogeneous top factors.
theorem
CCDN.polynomialCoefficientLinear_homogeneous
{k : Type u_1}
{K : Type u_2}
[Field k]
[Field K]
[Algebra k K]
{n d : ℕ}
(φ : K →ₗ[k] k)
(f : MvPolynomial (Fin n) K)
(hf : f.IsHomogeneous d)
:
((polynomialCoefficientLinear φ) f).IsHomogeneous d
Applying a linear map φ : K → k to the coefficients of a homogeneous polynomial of
degree d gives a homogeneous polynomial of degree d.
theorem
CCDN.exists_nonzero_homogeneous_linear_descent
{k : Type u_1}
{K : Type u_2}
[Field k]
[Field K]
[Algebra k K]
{n d : ℕ}
(f : MvPolynomial (Fin n) K)
(hf : f ≠ 0)
(hhom : f.IsHomogeneous d)
:
∃ (g : MvPolynomial (Fin n) k),
g ≠ 0 ∧ g.IsHomogeneous d ∧ ∀ (x : Fin n → k), (MvPolynomial.eval (⇑(algebraMap k K) ∘ x)) f = 0 → (MvPolynomial.eval x) g = 0
A nonzero homogeneous polynomial f of degree d over an extension field K of k yields
a nonzero homogeneous polynomial g of degree d over k that vanishes at every k-point
where f vanishes.
theorem
CCDN.top_homogeneousComponent_mul
{K : Type u_1}
{σ : Type u_2}
[CommRing K]
(g h : MvPolynomial σ K)
:
The homogeneous component of g * h in degree g.totalDegree + h.totalDegree is the
product of the top-degree homogeneous components of g and h.
theorem
CCDN.homogeneous_factorization_top
{K : Type u_1}
{σ : Type u_2}
[Field K]
{f g h : MvPolynomial σ K}
{d : ℕ}
(hf : f.IsHomogeneous d)
(hf0 : f ≠ 0)
(hg : g ≠ 0)
(hh : h ≠ 0)
(he : f = g * h)
:
g.totalDegree + h.totalDegree = d ∧ f = (MvPolynomial.homogeneousComponent g.totalDegree) g * (MvPolynomial.homogeneousComponent h.totalDegree) h
A factorization of a homogeneous equation can be replaced by homogeneous factors of the same respective total degrees.