Full-degree monic positioning of an irreducible hypersurface at a smooth point, using an invertible affine change and a nonzero scalar.

noncomputable def CCDN.normalizedHypersurfaceCoordinates {K : Type u_1} {σ : Type u_2} [Field K] (a b : Option σ → K) (hb : b none ≠ 0) (f : MvPolynomial (Option σ) K) : MvPolynomial (Option σ) K

Normalize the leading scalar of the explicit affine coordinate change.

Equations

• CCDN.normalizedHypersurfaceCoordinates a b hb f = MvPolynomial.C ((MvPolynomial.eval b) ((MvPolynomial.homogeneousComponent f.totalDegree) f))⁻¹ * (CCDN.hypersurfaceAffineCoordinates a b hb) f

theorem CCDN.normalizedHypersurfaceCoordinates_monic {K : Type u_1} {σ : Type u_2} [Field K] (a b : Option σ → K) (hb : b none ≠ 0) (f : MvPolynomial (Option σ) K) (hdir : (MvPolynomial.eval b) ((MvPolynomial.homogeneousComponent f.totalDegree) f) ≠ 0) : ((MvPolynomial.optionEquivLeft K σ) (normalizedHypersurfaceCoordinates a b hb f)).Monic

If the leading form of f does not vanish at the direction b, then the normalized affine coordinate change of f is monic as a polynomial in the distinguished variable none.

structure CCDN.IsMonicSmoothAtOrigin {K : Type u_1} {σ : Type u_2} [Field K] (g : MvPolynomial (Option σ) K) (d : ℕ) : Prop

The equation g is in position for the generic-plane minor: it is irreducible, monic of degree d in the distinguished variable none, of total degree at most d, and passes through the origin, where its derivative in the distinguished variable does not vanish.

• irreducible : Irreducible g

  The equation is irreducible.

• monic : ((MvPolynomial.optionEquivLeft K σ) g).Monic

  The equation is monic in the distinguished variable none.

• natDegree_eq : ((MvPolynomial.optionEquivLeft K σ) g).natDegree = d

  The equation has degree d in the distinguished variable none.

• totalDegree_le : g.totalDegree ≤ d

  The equation has total degree at most d.

• eval_zero : (MvPolynomial.eval 0) g = 0

  The equation vanishes at the origin.

• pderiv_ne_zero : (MvPolynomial.eval 0) ((MvPolynomial.pderiv none) g) ≠ 0

  The partial derivative in the distinguished variable none does not vanish at the origin.

theorem CCDN.exists_monic_smooth_hypersurface_coordinates {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 f.totalDegree) : ∃ (a : Option σ → K) (b : Option σ → K) (hb : b none ≠ 0), (MvPolynomial.eval b) ((MvPolynomial.homogeneousComponent f.totalDegree) f) ≠ 0 ∧ IsMonicSmoothAtOrigin (normalizedHypersurfaceCoordinates a b hb f) f.totalDegree

Smooth-point existence and direction avoidance discharge all positioning hypotheses: the coordinates and the nonzero scalar are actually constructed.

theorem CCDN.exists_positioned_genericPlane_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)) : ∃ (a : Option σ → K) (b : Option σ → K) (hb : b none ≠ 0), (MvPolynomial.eval b) ((MvPolynomial.homogeneousComponent f.totalDegree) f) ≠ 0 ∧ (closedFormCoefficientMatrix f.totalDegree (genericPlanePolynomial (normalizedHypersurfaceCoordinates a b hb f))).HasNonzeroMinor (2 * f.totalDegree ^ 2 - 1)

Every irreducible positive-degree hypersurface in characteristic zero or larger than 2*d^2 has an explicitly positioned generic-plane family with a nonzero slope minor.