The universal affine plane

The universal affine two-plane has independent coordinates for its base point and both directions. Its specializations are affine-plane restrictions; its polynomial coefficients are the objects to be counted. Every coefficient of the universal restriction has degree in the plane parameters bounded by the total degree of the original equation.

@[reducible, inline]

abbrev CCDN.PlaneParameters (σ : Type u_1) : Type u_1

Indices of the parameters of an affine plane in the affine space with coordinates σ: the pair (i, 0) indexes the i-th coordinate of the base point, and (i, 1), (i, 2) those of the two direction vectors.

Equations

• CCDN.PlaneParameters σ = (σ × Fin 3)

noncomputable def CCDN.universalPlaneMap (K : Type u_1) (σ : Type u_2) [CommRing K] : MvPolynomial σ K →ₐ[K] MvPolynomial (Fin 2) (MvPolynomial (PlaneParameters σ) K)

All affine planes a+xb+yc, with every coordinate an independent parameter.

Equations

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

noncomputable def CCDN.universalPlanePolynomial {K : Type u_1} {σ : Type u_2} [CommRing K] (f : MvPolynomial σ K) : Polynomial (Polynomial (MvPolynomial (PlaneParameters σ) K))

The restriction of f to the universal affine plane, viewed as a bivariate polynomial whose coefficients are polynomials in the plane parameters.

Equations

• CCDN.universalPlanePolynomial f = (CCDN.bivariatePolynomialEquiv (MvPolynomial (CCDN.PlaneParameters σ) K)) ((CCDN.universalPlaneMap K σ) f)

def CCDN.planeParameterEval {K : Type u_1} {A : Type u_2} {σ : Type u_3} [CommRing K] [CommRing A] (φ : K →+* A) (a b c : σ → A) : MvPolynomial (PlaneParameters σ) K →+* A

Evaluate all three blocks of affine-plane parameters.

Equations

• CCDN.planeParameterEval φ a b c = MvPolynomial.eval₂Hom φ fun (i : CCDN.PlaneParameters σ) => ![a i.1, b i.1, c i.1] i.2

theorem CCDN.universalPlaneMap_specialize {K : Type u_1} {A : Type u_2} {σ : Type u_3} [CommRing K] [CommRing A] (φ : K →+* A) (a b c : σ → A) (f : MvPolynomial σ K) : (MvPolynomial.map (planeParameterEval φ a b c)) ((universalPlaneMap K σ) f) = (MvPolynomial.eval₂Hom (MvPolynomial.C.comp φ) fun (i : σ) => MvPolynomial.C (a i) + MvPolynomial.C (b i) * MvPolynomial.X 0 + MvPolynomial.C (c i) * MvPolynomial.X 1) f

Universal specialization is exactly the displayed affine substitution.

theorem CCDN.universalPlanePolynomial_specialize {K : Type u_1} {A : Type u_2} {σ : Type u_3} [CommRing K] [CommRing A] (φ : K →+* A) (a b c : σ → A) (f : MvPolynomial σ K) : (bivariateMap (planeParameterEval φ a b c)) (universalPlanePolynomial f) = (bivariatePolynomialEquiv A) ((MvPolynomial.eval₂Hom (MvPolynomial.C.comp φ) fun (i : σ) => MvPolynomial.C (a i) + MvPolynomial.C (b i) * MvPolynomial.X 0 + MvPolynomial.C (c i) * MvPolynomial.X 1) f)

Specializing the plane parameters of the universal plane restriction of f to a base point a and directions b, c gives the restriction of f to the plane a + x • b + y • c.

theorem CCDN.closedForm_minor_smul {R : Type u_1} [CommRing R] (u : R) (d r : ℕ) (f : Polynomial (Polynomial R)) (a : Fin r → ℕ × ℕ) (c : Fin r → ClosedFormColumns d) : ((closedFormCoefficientMatrix d (u • f)).submatrix a c).det = u ^ r * ((closedFormCoefficientMatrix d f).submatrix a c).det

Scaling f by u multiplies every minor of order r of its closed-form coefficient matrix by u ^ r.

theorem CCDN.commAlgEquiv_coeff_coeff {K : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommRing K] (f : MvPolynomial σ (MvPolynomial τ K)) (m : σ →₀ ℕ) (n : τ →₀ ℕ) : (((MvPolynomial.commAlgEquiv K σ τ) f).coeff n).coeff m = (f.coeff m).coeff n

Under commAlgEquiv, which swaps the two sets of variables of an iterated multivariate polynomial ring, the coefficient of n in the coefficient of m is the coefficient of m in the coefficient of n.

theorem CCDN.universalPlanePolynomial_coefficient_degree {K : Type u_1} {σ : Type u_2} [CommRing K] (f : MvPolynomial σ K) (i j : ℕ) : (((universalPlanePolynomial f).coeff i).coeff j).totalDegree ≤ f.totalDegree

Each coefficient of the universal plane restriction of f has total degree at most the total degree of f in all plane parameters together.