mathlib documentation


Laurent polynomials #

We introduce Laurent polynomials over a semiring R. Mathematically, they are expressions of the form $$ \sum_{i \in \mathbb{Z}} a_i T ^ i $$ where the sum extends over a finite subset of . Thus, negative exponents are allowed. The coefficients come from the semiring R and the variable T commutes with everything.

Since we are going to convert back and forth between polynomials and Laurent polynomials, we decided to maintain some distinction by using the symbol T, rather than X, as the variable for Laurent polynomials

Notation #

The symbol R[T;T⁻¹] stands for laurent_polynomial R. We also define

Implementation notes #

We define Laurent polynomials as add_monoid_algebra R ℤ. Thus, they are essentially finsupps ℤ →₀ R. This choice differs from the current irreducible design of polynomial, that instead shields away the implementation via finsupps. It is closer to the original definition of polynomials.

As a consequence, laurent_polynomial plays well with polynomials, but there is a little roughness in establishing the API, since the finsupp implementation of polynomial R is well-shielded.

Unlike the case of polynomials, I felt that the exponent notation was not too easy to use, as only natural exponents would be allowed. Moreover, in the end, it seems likely that we should aim to perform computations on exponents in anyway and separating this via the symbol T seems convenient.

I made a heavy use of simp lemmas, aiming to bring Laurent polynomials to the form C a * T n. Any comments or suggestions for improvements is greatly appreciated!

Future work #

Lots is missing! -- (Riccardo) add inclusion into Laurent series. -- (Riccardo) giving a morphism (as R-alg, so in the commutative case) from R[T,T⁻¹] to S is the same as choosing a unit of S. -- A "better" definition of trunc would be as an R-linear map. This works: -- lean -- def trunc : R[T;T⁻¹] →[R] R[X] := -- begin -- refine (_ : add_monoid_algebra R ℕ →[R] R[X]).comp _, -- { exact ⟨(to_finsupp_iso R).symm, by simp⟩ }, -- { refine ⟨λ r, comap_domain _ r (set.inj_on_of_injective (λ a b ab, int.of_nat.inj ab) _), _⟩, -- exact λ r f, comap_domain_smul _ _ _ } -- end -- -- but it would make sense to bundle the maps better, for a smoother user experience. -- I (DT) did not have the strength to embark on this (possibly short!) journey, after getting to -- this stage of the Laurent process! -- This would likely involve adding a comap_domain analogue of -- add_monoid_algebra.map_domain_alg_hom and an R-linear version of -- polynomial.to_finsupp_iso. -- Add degree, int_degree, int_trailing_degree, leading_coeff, trailing_coeff,....

def laurent_polynomial (R : Type u_1) [semiring R] :
Type u_1

The semiring of Laurent polynomials with coefficients in the semiring R. We denote it by R[T;T⁻¹]. The ring homomorphism C : R →+* R[T;T⁻¹] includes R as the constant polynomials.

noncomputable def polynomial.to_laurent {R : Type u_1} [semiring R] :

The ring homomorphism, taking a polynomial with coefficients in R to a Laurent polynomial with coefficients in R.


This is not a simp lemma, as it is usually preferable to use the lemmas about C and X instead.

noncomputable def polynomial.to_laurent_alg {R : Type u_1} [comm_semiring R] :

The R-algebra map, taking a polynomial with coefficients in R to a Laurent polynomial with coefficients in R.


The functions C and T. #

noncomputable def laurent_polynomial.C {R : Type u_1} [semiring R] :

The ring homomorphism C, including R into the ring of Laurent polynomials over R as the constant Laurent polynomials.

theorem laurent_polynomial.algebra_map_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (r : R) :

When we have [comm_semiring R], the function C is the same as algebra_map R R[T;T⁻¹]. (But note that C is defined when R is not necessarily commutative, in which case algebra_map is not available.)

noncomputable def laurent_polynomial.T {R : Type u_1} [semiring R] (n : ) :

The function n ↦ T ^ n, implemented as a sequence ℤ → R[T;T⁻¹].

Using directly T ^ n does not work, since we want the exponents to be of Type and there is no -power defined on R[T;T⁻¹]. Using that T is a unit introduces extra coercions. For these reasons, the definition of T is as a sequence.

Instances for laurent_polynomial.T
theorem laurent_polynomial.T_zero {R : Type u_1} [semiring R] :
theorem laurent_polynomial.T_pow {R : Type u_1} [semiring R] (m : ) (n : ) :

The simp version of mul_assoc, in the presence of T's.

theorem polynomial.to_laurent_one {R : Type u_1} [semiring R] :
@[protected, instance]
noncomputable def laurent_polynomial.invertible_T {R : Type u_1} [semiring R] (n : ) :
theorem laurent_polynomial.induction_on {R : Type u_1} [semiring R] {M : laurent_polynomial R → Prop} (p : laurent_polynomial R) (h_C : ∀ (a : R), M (laurent_polynomial.C a)) (h_add : ∀ {p q : laurent_polynomial R}, M pM qM (p + q)) (h_C_mul_T : ∀ (n : ) (a : R), M (laurent_polynomial.C a * laurent_polynomial.T n)M (laurent_polynomial.C a * laurent_polynomial.T (n + 1))) (h_C_mul_T_Z : ∀ (n : ) (a : R), M (laurent_polynomial.C a * laurent_polynomial.T (-n))M (laurent_polynomial.C a * laurent_polynomial.T (-n - 1))) :
M p
theorem laurent_polynomial.induction_on' {R : Type u_1} [semiring R] {M : laurent_polynomial R → Prop} (p : laurent_polynomial R) (h_add : ∀ (p q : laurent_polynomial R), M pM qM (p + q)) (h_C_mul_T : ∀ (n : ) (a : R), M (laurent_polynomial.C a * laurent_polynomial.T n)) :
M p

To prove something about Laurent polynomials, it suffices to show that

  • the condition is closed under taking sums, and
  • it holds for monomials.
noncomputable def laurent_polynomial.trunc {R : Type u_1} [semiring R] :

trunc : R[T;T⁻¹] →+ R[X] maps a Laurent polynomial f to the polynomial whose terms of nonnegative degree coincide with the ones of f. The terms of negative degree of f "vanish". trunc is a left-inverse to polynomial.to_laurent.

theorem laurent_polynomial.induction_on_mul_T {R : Type u_1} [semiring R] {Q : laurent_polynomial R → Prop} (f : laurent_polynomial R) (Qf : ∀ {f : polynomial R} {n : }, Q (polynomial.to_laurent f * laurent_polynomial.T (-n))) :
Q f

This is a version of exists_T_pow stated as an induction principle.

theorem laurent_polynomial.reduce_to_polynomial_of_mul_T {R : Type u_1} [semiring R] (f : laurent_polynomial R) {Q : laurent_polynomial R → Prop} (Qf : ∀ (f : polynomial R), Q (polynomial.to_laurent f)) (QT : ∀ (f : laurent_polynomial R), Q (f * laurent_polynomial.T 1)Q f) :
Q f

Suppose that Q is a statement about Laurent polynomials such that

  • Q is true on ordinary polynomials;
  • Q (f * T) implies Q f; it follow that Q is true on all Laurent polynomials.

The support of a polynomial f is a finset in . The lemma to_laurent_support f shows that the support of f.to_laurent is the same finset, but viewed in under the natural inclusion ℕ ↪ ℤ.

The degree of a Laurent polynomial takes values in with_bot. If f : R[T;T⁻¹] is a Laurent polynomial, then is the maximum of its support of f, or , if f = 0.

theorem laurent_polynomial.degree_zero {R : Type u_1} [semiring R] :
theorem laurent_polynomial.degree_eq_bot_iff {R : Type u_1} [semiring R] {f : laurent_polynomial R} : = f = 0
theorem laurent_polynomial.degree_C_mul_T {R : Type u_1} [semiring R] (n : ) (a : R) (a0 : a 0) :
theorem laurent_polynomial.degree_T {R : Type u_1} [semiring R] [nontrivial R] (n : ) :
theorem laurent_polynomial.degree_C {R : Type u_1} [semiring R] {a : R} (a0 : a 0) :
theorem laurent_polynomial.degree_C_ite {R : Type u_1} [semiring R] (a : R) :
theorem laurent_polynomial.degree_C_le {R : Type u_1} [semiring R] (a : R) :
@[protected, instance]