Two-variable polynomials substituted into three variables

For a polynomial g(X, Y) in two variables, this file computes the coefficient of XⁱYʲZᵏ in the four three-variable polynomials g(X + Y, Z), g(X, Y + Z), g(X, Y) and g(Y, Z) in terms of the coefficients of g. These are the four terms of the additive 2-cocycle identity g(X, Y) + g(X + Y, Z) = g(X, Y + Z) + g(Y, Z), so these formulas turn that identity into linear equations on the coefficients of g.

Main results

• MvPolynomial.coeff_add_pow_mul_X_pow_fin_three, MvPolynomial.coeff_X_pow_mul_X_pow_fin_three: the coefficients of (X a + X b) ^ m * X c ^ k and X a ^ m * X c ^ k for distinct a, b, c : Fin 3.
• MvPolynomial.coeff_aeval_X_add_X_X: the coefficient of XⁱYʲZᵏ in g(X + Y, Z) is (i + j).choose i times that of Xⁱ⁺ʲYᵏ in g.
• MvPolynomial.coeff_aeval_X_X_add_X: the coefficient of XⁱYʲZᵏ in g(X, Y + Z) is (j + k).choose j times that of XⁱYʲ⁺ᵏ in g.
• MvPolynomial.coeff_aeval_X_zero_X_one, MvPolynomial.coeff_aeval_X_one_X_two: the coefficients of g(X, Y) and g(Y, Z).

theorem MvPolynomial.coeff_add_pow_mul_X_pow_fin_three {R : Type u_1} [CommSemiring R] {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (m k : ℕ) (d : Fin 3 →₀ ℕ) : ((X a + X b) ^ m * X c ^ k).coeff d = if d a + d b = m ∧ d c = k then ↑(m.choose (d a)) else 0

The coefficients of (X a + X b) ^ m * X c ^ k in three variables a, b, c.

theorem MvPolynomial.coeff_X_pow_mul_X_pow_fin_three {R : Type u_1} [CommSemiring R] {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (m k : ℕ) (d : Fin 3 →₀ ℕ) : (X a ^ m * X c ^ k).coeff d = if d a = m ∧ d b = 0 ∧ d c = k then 1 else 0

The coefficients of X a ^ m * X c ^ k in three variables a, b, c.

theorem MvPolynomial.coeff_aeval_X_add_X_X {R : Type u_1} [CommSemiring R] (g : MvPolynomial (Fin 2) R) (d : Fin 3 →₀ ℕ) : ((aeval ![X 0 + X 1, X 2]) g).coeff d = ↑((d 0 + d 1).choose (d 0)) * g.coeff (Finsupp.single 0 (d 0 + d 1) + Finsupp.single 1 (d 2))

The coefficient of XⁱYʲZᵏ in g(X + Y, Z) is (i + j).choose i times that of Xⁱ⁺ʲYᵏ in g.

theorem MvPolynomial.coeff_aeval_X_X_add_X {R : Type u_1} [CommSemiring R] (g : MvPolynomial (Fin 2) R) (d : Fin 3 →₀ ℕ) : ((aeval ![X 0, X 1 + X 2]) g).coeff d = ↑((d 1 + d 2).choose (d 1)) * g.coeff (Finsupp.single 0 (d 0) + Finsupp.single 1 (d 1 + d 2))

The coefficient of XⁱYʲZᵏ in g(X, Y + Z) is (j + k).choose j times that of XⁱYʲ⁺ᵏ in g.

theorem MvPolynomial.coeff_aeval_X_zero_X_one {R : Type u_1} [CommSemiring R] (g : MvPolynomial (Fin 2) R) (d : Fin 3 →₀ ℕ) : ((aeval ![X 0, X 1]) g).coeff d = if d 2 = 0 then g.coeff (Finsupp.single 0 (d 0) + Finsupp.single 1 (d 1)) else 0

The coefficient of XⁱYʲZᵏ in g(X, Y) is that of XⁱYʲ in g if k = 0, and 0 otherwise.

theorem MvPolynomial.coeff_aeval_X_one_X_two {R : Type u_1} [CommSemiring R] (g : MvPolynomial (Fin 2) R) (d : Fin 3 →₀ ℕ) : ((aeval ![X 1, X 2]) g).coeff d = if d 0 = 0 then g.coeff (Finsupp.single 0 (d 1) + Finsupp.single 1 (d 2)) else 0

The coefficient of XⁱYʲZᵏ in g(Y, Z) is that of XʲYᵏ in g if i = 0, and 0 otherwise.