The constructed positioned family is a specialization of the universal family of all affine planes. Its nonzero minor therefore proves that a universal parameter polynomial is nonzero.
noncomputable def
CCDN.genericTransverseDirection
(K : Type u_1)
(F : Type u_2)
(σ : Type u_3)
[Field K]
[Field F]
[Algebra (MvPolynomial σ K) F]
:
Option σ → F
The second direction has zero first coordinate and generic transverse slopes.
Equations
- CCDN.genericTransverseDirection K F σ i = i.elim 0 fun (j : σ) => (algebraMap (MvPolynomial σ K) F) (MvPolynomial.X j)
Instances For
theorem
CCDN.normalized_genericPlane_universal_specialization
{K : Type u_1}
{F : Type u_2}
{σ : Type u_3}
[Field K]
[Field F]
[Algebra K F]
[Algebra (MvPolynomial σ K) F]
[IsScalarTower K (MvPolynomial σ K) F]
(a b : Option σ → K)
(hb : b none ≠ 0)
(f : MvPolynomial (Option σ) K)
:
(bivariateMap (algebraMap (MvPolynomial σ K) F)) (genericPlanePolynomial (normalizedHypersurfaceCoordinates a b hb f)) = (algebraMap K F) ((MvPolynomial.eval b) ((MvPolynomial.homogeneousComponent f.totalDegree) f))⁻¹ • (bivariateMap
(planeParameterEval (algebraMap K F) (⇑(algebraMap K F) ∘ a) (⇑(algebraMap K F) ∘ b)
(genericTransverseDirection K F σ)))
(universalPlanePolynomial f)
Monic normalization changes the specialized equation only by a scalar.
theorem
CCDN.exists_universalPlane_minor
{K : Type u_1}
{σ : Type u_2}
[Field K]
[IsAlgClosed K]
[Finite σ]
(f : MvPolynomial (Option σ) K)
(hf : Irreducible f)
(hpos : 0 < f.totalDegree)
(hchar : CharZeroOrGT K (2 * f.totalDegree ^ 2))
:
(closedFormCoefficientMatrix f.totalDegree (universalPlanePolynomial f)).HasNonzeroMinor (2 * f.totalDegree ^ 2 - 1)
Every irreducible positive-degree hypersurface over an algebraically closed field of characteristic zero or >2*d^2 has a nonzero minor in the UNIVERSAL affine-plane parameter ring, not merely in a family through a fixed line.