Bounded integral shears give full outer degree.

theorem CCDN.bivariatePolynomialEquiv_X_zero {R : Type u_1} [CommRing R] : (bivariatePolynomialEquiv R) (MvPolynomial.X 0) = Polynomial.X

Variable zero corresponds to the outer variable of the nested polynomial ring.

theorem CCDN.bivariatePolynomialEquiv_X_one {R : Type u_1} [CommRing R] : (bivariatePolynomialEquiv R) (MvPolynomial.X 1) = Polynomial.C Polynomial.X

Variable one corresponds to the inner variable of the nested polynomial ring.

theorem CCDN.bivariatePolynomialEquiv_C {R : Type u_1} [CommRing R] (a : R) : (bivariatePolynomialEquiv R) (MvPolynomial.C a) = Polynomial.C (Polynomial.C a)

Constants correspond to constants of the nested polynomial ring.

noncomputable def CCDN.bivariateShear (R : Type u_1) [CommRing R] (a : R) : Polynomial (Polynomial R) ≃ₐ[R] Polynomial (Polynomial R)

The integral shear in nested polynomial coordinates.

Equations

• CCDN.bivariateShear R a = (CCDN.bivariatePolynomialEquiv R).symm.trans ((CCDN.planeShear R a).trans (CCDN.bivariatePolynomialEquiv R))

theorem CCDN.bivariate_exponent_eq_iff (m : Fin 2 →₀ ℕ) (i j : ℕ) : Finsupp.cons i (Finsupp.single 0 j) = m ↔ m 0 = i ∧ m 1 = j

A two-variable exponent vector m equals Finsupp.cons i (Finsupp.single 0 j) if and only if its components are i and j.

theorem CCDN.bivariateShear_irreducible_iff {R : Type u_1} [CommRing R] (a : R) (f : Polynomial (Polynomial R)) : Irreducible ((bivariateShear R a) f) ↔ Irreducible f

A plane shear preserves irreducibility of bivariate polynomials.

theorem CCDN.exists_bounded_full_outer_shear (f : Polynomial (Polynomial ℤ)) (hf : f ≠ 0) : ∃ a ≤ bivariateTotalDegree f, ((bivariateShear ℤ ↑a) f).natDegree = bivariateTotalDegree f ∧ bivariateTotalDegree ((bivariateShear ℤ ↑a) f) = bivariateTotalDegree f

Every nonzero integer plane equation admits a shear with parameter in 0,...,d whose outer degree is exactly its original total degree.

theorem CCDN.bivariatePolynomialEquiv_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (f : MvPolynomial (Fin 2) R) : (bivariateMap φ) ((bivariatePolynomialEquiv R) f) = (bivariatePolynomialEquiv S) ((MvPolynomial.map φ) f)

The identification of two-variable polynomials with nested polynomials commutes with applying a coefficient ring homomorphism.

theorem CCDN.bivariateShear_equiv {R : Type u_1} [CommRing R] (a : R) (f : MvPolynomial (Fin 2) R) : (bivariateShear R a) ((bivariatePolynomialEquiv R) f) = (bivariatePolynomialEquiv R) ((planeShear R a) f)

The nested plane shear corresponds to the plane shear of two-variable polynomials.

theorem CCDN.bivariateShear_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (a : R) (f : Polynomial (Polynomial R)) : (bivariateMap φ) ((bivariateShear R a) f) = (bivariateShear S (φ a)) ((bivariateMap φ) f)

Applying a coefficient ring homomorphism φ commutes with shearing, the shear parameter a becoming φ a.

theorem CCDN.bivariateBadReduction_shear_iff (a : ℤ) (f : Polynomial (Polynomial ℤ)) (d p : ℕ) : BivariateBadReduction ((bivariateShear ℤ a) f) d p ↔ BivariateBadReduction f d p

Shearing does not change the set of bad primes, including reductions where the degree drops.