Parallel affine slices preserve the good leading hyperplane section. Rational restriction equations can then be replaced by integer polynomials without changing their zero sets or total degrees.

noncomputable def CCDN.optionCoordinateShift {K : Type u_1} [CommRing K] {n : ℕ} (c : K) : MvPolynomial (Option (Fin n)) K →ₐ[K] MvPolynomial (Option (Fin n)) K

The K-algebra automorphism of K[x_none, x_0, …, x_{n-1}] translating the distinguished coordinate x_none by the constant c and fixing the other coordinates.

Equations

• CCDN.optionCoordinateShift c = MvPolynomial.aeval fun (i : Option (Fin n)) => i.elim (MvPolynomial.X none + MvPolynomial.C c) fun (j : Fin n) => MvPolynomial.X (some j)

noncomputable def CCDN.affineGraphHyperplaneSlice {K : Type u_1} [CommRing K] {n : ℕ} (a : Fin n → K) (c : K) (f : MvPolynomial (Option (Fin n)) K) : MvPolynomial (Fin n) K

The restriction of f to the affine hyperplane x_none = ∑ a j * x j + c, written as a polynomial in the remaining coordinates x j.

Equations

• CCDN.affineGraphHyperplaneSlice a c f = (CCDN.graphHyperplaneRestriction a) ((CCDN.optionCoordinateShift c) f)

theorem CCDN.affineGraphHyperplaneSlice_eval {K : Type u_1} [CommRing K] {n : ℕ} (a : Fin n → K) (c : K) (f : MvPolynomial (Option (Fin n)) K) (x : Fin n → K) : (MvPolynomial.eval x) (affineGraphHyperplaneSlice a c f) = (MvPolynomial.eval fun (i : Option (Fin n)) => i.elim (∑ j : Fin n, a j * x j + c) x) f

Evaluating the affine slice affineGraphHyperplaneSlice a c f at x is evaluating f at the point of the hyperplane x_none = ∑ a j * x j + c lying over x.

theorem CCDN.affineGraphHyperplaneSlice_top {K : Type u_1} [CommRing K] [Nontrivial K] {n : ℕ} (a : Fin n → K) (c : K) (f : MvPolynomial (Option (Fin n)) K) : (MvPolynomial.homogeneousComponent f.totalDegree) (affineGraphHyperplaneSlice a c f) = (graphHyperplaneRestriction a) ((MvPolynomial.homogeneousComponent f.totalDegree) f)

The degree-f.totalDegree component of an affine slice of f is the restriction of the top form of f to the parallel linear hyperplane x_none = ∑ a j * x j.

theorem CCDN.affineGraphHyperplaneSlice_degree {K : Type u_1} [Field K] {n : ℕ} (a : Fin n → K) (c : K) (f : MvPolynomial (Option (Fin n)) K) (htop : (graphHyperplaneRestriction a) ((MvPolynomial.homogeneousComponent f.totalDegree) f) ≠ 0) : (affineGraphHyperplaneSlice a c f).totalDegree = f.totalDegree

A nonzero restriction of the top form prevents degree loss at every parallel affine level.