Symmetric Laurent polynomials

A Laurent polynomial fixed by inversion is a polynomial in T + T⁻¹, over any commutative ring. The proof uses Mathlib's rescaled Chebyshev polynomials, which express Tⁿ + T⁻ⁿ without dividing by two. Consequently the result applies to integer coefficients and to rings of characteristic two.

The shifted generator T + T⁻¹ - 2 is convenient for converting a symmetric Alexander polynomial to the square of the Conway variable.

The rescaled Chebyshev polynomials of the second kind give the companion identity (T - T⁻¹) Sₙ(T + T⁻¹) = Tⁿ⁺¹ - T⁻ⁿ⁻¹ for the antisymmetric Laurent polynomials.

Finally, a family of symmetric Laurent polynomials whose coefficients are read off a nested power series that is symmetric in its two variables consists of constants (LaurentPolynomial.eq_C_coeff_zero_of_coeff_swap).

@[simp]

theorem Polynomial.Chebyshev.eval₂_C_add_T_neg {R : Type u_1} [CommRing R] (n : ℕ) : eval₂ LaurentPolynomial.C (LaurentPolynomial.T 1 + LaurentPolynomial.T (-1)) (C R ↑n) = LaurentPolynomial.T ↑n + LaurentPolynomial.T (-↑n)

The rescaled Chebyshev polynomial expresses a pair of opposite Laurent powers.

@[simp]

theorem Polynomial.Chebyshev.T_sub_T_neg_mul_eval₂_S_add_T_neg {R : Type u_1} [CommRing R] (n : ℕ) : (LaurentPolynomial.T 1 - LaurentPolynomial.T (-1)) * eval₂ LaurentPolynomial.C (LaurentPolynomial.T 1 + LaurentPolynomial.T (-1)) (S R ↑n) = LaurentPolynomial.T (↑n + 1) - LaurentPolynomial.T (-(↑n + 1))

The rescaled Chebyshev polynomial of the second kind expresses a difference of opposite Laurent powers, once multiplied by T - T⁻¹.

@[simp]

theorem LaurentPolynomial.coeff_trunc {R : Type u_1} [Semiring R] (p : LaurentPolynomial R) (n : ℕ) : (trunc p).coeff n = p.coeff ↑n

Truncation retains every coefficient of nonnegative exponent.

@[simp]

theorem LaurentPolynomial.toLaurent_trunc_add_invert {R : Type u_1} [CommRing R] (p : LaurentPolynomial R) : Polynomial.toLaurent (trunc p) + invert (Polynomial.toLaurent (trunc (invert p))) - C (p.coeff 0) = p

Split a Laurent polynomial into its nonnegative and negative powers, correcting the double-counted constant term.

theorem Polynomial.eval₂_comp_X_sq_eq_laurent_eval₂ {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (q : Polynomial R) (f : R →+* S) (s : Sˣ) : eval₂ f (↑s⁻¹ - ↑s) (q.comp (X ^ 2)) = (LaurentPolynomial.eval₂ f (s ^ 2)) (eval₂ LaurentPolynomial.C (LaurentPolynomial.T 1 + LaurentPolynomial.T (-1) - 2) q)

Substitution of s⁻¹ - s in q(X²) agrees with evaluating the Laurent polynomial q(T + T⁻¹ - 2) at T = s², under any coefficient homomorphism.

theorem Polynomial.exists_eval₂_add_T_neg {R : Type u_1} [CommRing R] (p : Polynomial R) : ∃ (q : Polynomial R), eval₂ LaurentPolynomial.C (LaurentPolynomial.T 1 + LaurentPolynomial.T (-1)) q = toLaurent p + LaurentPolynomial.invert (toLaurent p) - LaurentPolynomial.C (p.coeff 0)

The positive and reflected negative parts of an ordinary polynomial, with the constant counted once, are a polynomial in T + T⁻¹.

theorem LaurentPolynomial.invert_eq_self_iff_exists_eval₂ {R : Type u_1} [CommRing R] (p : LaurentPolynomial R) : invert p = p ↔ ∃ (q : Polynomial R), Polynomial.eval₂ C (T 1 + T (-1)) q = p

A Laurent polynomial is fixed by inversion exactly when it is an ordinary polynomial in T + T⁻¹. This holds without inverting two.

theorem LaurentPolynomial.exists_eval₂_add_T_neg_sub_two {R : Type u_1} [CommRing R] {p : LaurentPolynomial R} (hp : invert p = p) : ∃ (q : Polynomial R), Polynomial.eval₂ C (T 1 + T (-1) - 2) q = p

A symmetric Laurent polynomial can also be expressed in the shifted generator T + T⁻¹ - 2, the square of the Conway variable after doubling exponents.

theorem LaurentPolynomial.eq_C_coeff_zero_of_coeff_swap {R : Type u_1} [Semiring R] {G : PowerSeries (PowerSeries R)} {L : ℕ → LaurentPolynomial R} (hcoe : ∀ (N : ℕ) (k : ℤ), (L N).coeff k = if k + ↑N < 0 then 0 else (PowerSeries.coeff (k + ↑N).natAbs) ((PowerSeries.coeff N) G)) (hsymm : ∀ (N : ℕ) (k : ℤ), (L N).coeff (-k) = (L N).coeff k) (hswap : ∀ (a b : ℕ), (PowerSeries.coeff a) ((PowerSeries.coeff b) G) = (PowerSeries.coeff b) ((PowerSeries.coeff a) G)) (N : ℕ) : L N = C ((L N).coeff 0)

If the Laurent polynomials L N are symmetric, and the coefficient of uᵏ in L N is the coefficient of vᵏ⁺ᴺ read off a series G that is symmetric in its two variables, then each L N is constant. This is the induction in the formal Liouville theorem for the Tate curve.