A hyperplane written as x₀ = ∑ aᵢxᵢ. A full-degree irreducible plane contained in that hyperplane certifies irreducibility of the entire hyperplane restriction.

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

The restriction of a polynomial in the coordinates x_none and x i to the hyperplane x_none = ∑ a i * x i, as a polynomial in the remaining coordinates x i.

Equations

• CCDN.graphHyperplaneRestriction a = MvPolynomial.aeval fun (i : Option σ) => i.elim (∑ j : σ, MvPolynomial.C (a j) * MvPolynomial.X j) MvPolynomial.X

theorem CCDN.graphHyperplaneRestriction_totalDegree_le {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] (a : σ → K) (f : MvPolynomial (Option σ) K) : ((graphHyperplaneRestriction a) f).totalDegree ≤ f.totalDegree

Restriction to a graph hyperplane does not increase the total degree.

theorem CCDN.graphHyperplaneRestriction_eval {K : Type u_1} {σ : Type u_2} [CommRing K] [Fintype σ] (a x : σ → K) (f : MvPolynomial (Option σ) K) : (MvPolynomial.eval x) ((graphHyperplaneRestriction a) f) = (MvPolynomial.eval fun (i : Option σ) => i.elim (∑ j : σ, a j * x j) x) f

Evaluating the restriction of f to the hyperplane x_none = ∑ a j * x j at x is evaluating f at the point of the hyperplane lying over x.

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

Restriction to a graph hyperplane preserves homogeneity of degree d.

theorem CCDN.graphHyperplaneRestriction_map {K : Type u_1} {L : Type u_2} {σ : Type u_3} [CommRing K] [CommRing L] [Fintype σ] (φ : K →+* L) (a : σ → K) (f : MvPolynomial (Option σ) K) : (MvPolynomial.map φ) ((graphHyperplaneRestriction a) f) = (graphHyperplaneRestriction (⇑φ ∘ a)) ((MvPolynomial.map φ) f)

Restriction to the graph hyperplane commutes with applying a ring homomorphism φ to the coefficients, the hyperplane coefficients a being mapped by φ as well.

theorem CCDN.graphHyperplaneRestriction_homogeneousComponent {K : Type u_1} {σ : Type u_2} [CommRing K] [Fintype σ] (a : σ → K) (f : MvPolynomial (Option σ) K) (d : ℕ) : (graphHyperplaneRestriction a) ((MvPolynomial.homogeneousComponent d) f) = (MvPolynomial.homogeneousComponent d) ((graphHyperplaneRestriction a) f)

Restriction to a graph hyperplane commutes with taking the homogeneous component of degree d.

theorem CCDN.graphHyperplaneRestriction_irreducible_of_plane {K : Type u_1} {σ : Type u_2} [Field K] [Infinite K] [Fintype σ] (f : MvPolynomial (Option σ) K) (a : σ → K) (v : PlaneParameters (Option σ) → K) (hv : ∀ (j : Fin 3), v (none, j) = ∑ i : σ, a i * v (some i, j)) (hir : Irreducible (universalPlaneSection f v)) (hdegree : bivariateTotalDegree (universalPlaneSection f v) = f.totalDegree) : ((graphHyperplaneRestriction a) f).totalDegree = f.totalDegree ∧ Irreducible ((graphHyperplaneRestriction a) f)

Full degree and irreducibility of a concrete contained plane force both properties for the containing hyperplane.