A homogeneous universal hyperplane restriction without denominators. The normal A cuts out A₀x₀+ΣAᵢxᵢ=0; the chart A₀≠0 is represented by x₀=−ΣAᵢxᵢ and xᵢ=A₀xᵢ before evaluating a degree-d equation.

noncomputable def CCDN.universalHyperplaneRestriction {σ : Type u_1} [Fintype σ] : MvPolynomial (Option σ) ℤ →ₐ[ℤ] MvPolynomial σ (MvPolynomial (Option σ) ℤ)

The universal restriction of an integer polynomial to the hyperplane A none * x_none + ∑ A (some j) * x j = 0, whose normal coefficients A are indeterminates, without denominators: it substitutes x_none ↦ -∑ A (some j) * x j and x j ↦ A none * x j.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CCDN.scaledHyperplaneRestriction {K : Type u_1} {σ : Type u_2} [CommRing K] [Fintype σ] (A : Option σ → K) : MvPolynomial (Option σ) K →ₐ[K] MvPolynomial σ K

The restriction of a polynomial to the hyperplane A none * x_none + ∑ A (some j) * x j = 0 without denominators, obtained by substituting x_none ↦ -∑ A (some j) * x j and x j ↦ A none * x j.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.universalHyperplaneRestriction_specialize {K : Type u_1} {σ : Type u_2} [CommRing K] [Fintype σ] (A : Option σ → K) (f : MvPolynomial (Option σ) ℤ) : (MvPolynomial.map (MvPolynomial.eval₂Hom (Int.castRingHom K) A)) (universalHyperplaneRestriction f) = (scaledHyperplaneRestriction A) ((MvPolynomial.map (Int.castRingHom K)) f)

Specializing the coefficient indeterminates of the universal hyperplane restriction at a normal vector A gives the scaled hyperplane restriction for A.

theorem CCDN.universalHyperplaneRestriction_coefficientwiseHomogeneous {σ : Type u_1} [Fintype σ] {d : ℕ} {f : MvPolynomial (Option σ) ℤ} (hf : f.IsHomogeneous d) : CoefficientwiseHomogeneous (universalHyperplaneRestriction f) d

The universal hyperplane restriction of a homogeneous polynomial of degree d has coefficients that are homogeneous of degree d in the normal coefficients.

theorem CCDN.scaledHyperplaneRestriction_homogeneous {K : Type u_1} {σ : Type u_2} [CommRing K] [Fintype σ] (A : Option σ → K) {d : ℕ} {f : MvPolynomial (Option σ) K} (hf : f.IsHomogeneous d) : ((scaledHyperplaneRestriction A) f).IsHomogeneous d

The scaled hyperplane restriction preserves homogeneity of degree d.

theorem CCDN.scaledHyperplaneRestriction_eq_graph {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] (A : Option σ → K) (hA : A none ≠ 0) {d : ℕ} {f : MvPolynomial (Option σ) K} (hf : f.IsHomogeneous d) : (scaledHyperplaneRestriction A) f = MvPolynomial.C (A none ^ d) * (graphHyperplaneRestriction fun (i : σ) => -A (some i) / A none) f

For A none ≠ 0 and f homogeneous of degree d, the scaled hyperplane restriction of f is A none ^ d times its restriction to the graph hyperplane x_none = ∑ -(A (some i) / A none) * x i.

theorem CCDN.scaledHyperplaneRestriction_normalized {K : Type u_1} {σ : Type u_2} [CommRing K] [Fintype σ] (a : σ → K) (f : MvPolynomial (Option σ) K) : (scaledHyperplaneRestriction fun (i : Option σ) => i.elim 1 fun (j : σ) => -a j) f = (graphHyperplaneRestriction a) f

The scaled hyperplane restriction for the normal vector (1, -a) is the restriction to the graph hyperplane x_none = ∑ a i * x i.