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 LaurentPolynomial R. We also define

Implementation notes #

We define Laurent polynomials as AddMonoidAlgebra 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, LaurentPolynomial plays well with polynomials, but there is a little roughness in establishing the API, since the Finsupp implementation of R[X] 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: -- -- def trunc : R[T;T⁻¹] →[R] R[X] := -- begin -- refine (_ : R[ℕ] →[R] R[X]).comp _, -- { exact ⟨(toFinsuppIso R).symm, by simp⟩ }, -- { refine ⟨λ r, comapDomain _ r (Set.injOn_of_injective (λ a b ab, Int.ofNat.inj ab) _), _⟩, -- exact λ r f, comapDomain_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 comapDomain analogue of -- AddMonoidAlgebra.mapDomainAlgHom and an R-linear version of -- Polynomial.toFinsuppIso. -- Add degree, int_degree, int_trailing_degree, leading_coeff, trailing_coeff,....

@[inline, reducible]
abbrev LaurentPolynomial (R : Type u_2) [Semiring R] :
Type u_2

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.

Instances For
    theorem LaurentPolynomial.ext {R : Type u_1} [Semiring R] {p : LaurentPolynomial R} {q : LaurentPolynomial R} (h : ∀ (a : ), p a = q a) :
    p = q

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

    Instances For
      theorem Polynomial.toLaurent_apply {R : Type u_1} [Semiring R] (p : Polynomial R) :
      Polynomial.toLaurent p = AddMonoidAlgebra.mapDomain Nat.cast p.toFinsupp

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

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

      Instances For
        theorem Polynomial.coe_toLaurentAlg {R : Type u_1} [CommSemiring R] :
        Polynomial.toLaurentAlg = Polynomial.toLaurent
        theorem Polynomial.toLaurentAlg_apply {R : Type u_1} [CommSemiring R] (f : Polynomial R) :
        Polynomial.toLaurentAlg f = Polynomial.toLaurent f
        theorem LaurentPolynomial.single_zero_one_eq_one {R : Type u_1} [Semiring R] :
        (fun₀ | 0 => 1) = 1

        The functions C and T. #

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

        Instances For
          theorem LaurentPolynomial.algebraMap_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :
          ↑(algebraMap R (LaurentPolynomial A)) r = LaurentPolynomial.C (↑(algebraMap R A) r)
          theorem LaurentPolynomial.C_eq_algebraMap {R : Type u_2} [CommSemiring R] (r : R) :
          LaurentPolynomial.C r = ↑(algebraMap R (LaurentPolynomial R)) r

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

          theorem LaurentPolynomial.single_eq_C {R : Type u_1} [Semiring R] (r : R) :
          (fun₀ | 0 => r) = LaurentPolynomial.C r
          theorem LaurentPolynomial.C_apply {R : Type u_1} [Semiring R] (t : R) (n : ) :
          ↑(LaurentPolynomial.C t) n = if n = 0 then t else 0

          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
            theorem LaurentPolynomial.T_apply {R : Type u_1} [Semiring R] (m : ) (n : ) :
            ↑(LaurentPolynomial.T n) m = if n = m then 1 else 0
            theorem LaurentPolynomial.T_pow {R : Type u_1} [Semiring R] (m : ) (n : ) :

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

            theorem LaurentPolynomial.single_eq_C_mul_T {R : Type u_1} [Semiring R] (r : R) (n : ) :
            (fun₀ | n => r) = LaurentPolynomial.C r * LaurentPolynomial.T n
            theorem Polynomial.toLaurent_C_mul_T {R : Type u_1} [Semiring R] (n : ) (r : R) :
            Polynomial.toLaurent (↑(Polynomial.monomial n) r) = LaurentPolynomial.C r * LaurentPolynomial.T n
            theorem Polynomial.toLaurent_C {R : Type u_1} [Semiring R] (r : R) :
            Polynomial.toLaurent (Polynomial.C r) = LaurentPolynomial.C r
            theorem Polynomial.toLaurent_comp_C {R : Type u_1} [Semiring R] :
            Polynomial.toLaurent Polynomial.C = LaurentPolynomial.C
            theorem Polynomial.toLaurent_X {R : Type u_1} [Semiring R] :
            Polynomial.toLaurent Polynomial.X = LaurentPolynomial.T 1
            theorem Polynomial.toLaurent_one {R : Type u_1} [Semiring R] :
            Polynomial.toLaurent 1 = 1
            theorem Polynomial.toLaurent_C_mul_eq {R : Type u_1} [Semiring R] (r : R) (f : Polynomial R) :
            Polynomial.toLaurent (Polynomial.C r * f) = LaurentPolynomial.C r * Polynomial.toLaurent f
            theorem Polynomial.toLaurent_X_pow {R : Type u_1} [Semiring R] (n : ) :
            Polynomial.toLaurent (Polynomial.X ^ n) = LaurentPolynomial.T n
            theorem Polynomial.toLaurent_C_mul_X_pow {R : Type u_1} [Semiring R] (n : ) (r : R) :
            Polynomial.toLaurent (Polynomial.C r * Polynomial.X ^ n) = LaurentPolynomial.C r * LaurentPolynomial.T n
            theorem LaurentPolynomial.induction_on {R : Type u_1} [Semiring R] {M : LaurentPolynomial RProp} (p : LaurentPolynomial R) (h_C : (a : R) → M (LaurentPolynomial.C a)) (h_add : {p q : LaurentPolynomial R} → M pM qM (p + q)) (h_C_mul_T : (n : ) → (a : R) → M (LaurentPolynomial.C a * LaurentPolynomial.T n)M (LaurentPolynomial.C a * LaurentPolynomial.T (n + 1))) (h_C_mul_T_Z : (n : ) → (a : R) → M (LaurentPolynomial.C a * LaurentPolynomial.T (-n))M (LaurentPolynomial.C a * LaurentPolynomial.T (-n - 1))) :
            M p
            theorem LaurentPolynomial.induction_on' {R : Type u_1} [Semiring R] {M : LaurentPolynomial RProp} (p : LaurentPolynomial R) (h_add : (p q : LaurentPolynomial R) → M pM qM (p + q)) (h_C_mul_T : (n : ) → (a : R) → M (LaurentPolynomial.C a * LaurentPolynomial.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.

            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.toLaurent.

            Instances For
              theorem LaurentPolynomial.trunc_C_mul_T {R : Type u_1} [Semiring R] (n : ) (r : R) :
              LaurentPolynomial.trunc (LaurentPolynomial.C r * LaurentPolynomial.T n) = if 0 n then ↑(Polynomial.monomial (Int.toNat n)) r else 0
              theorem LaurentPolynomial.leftInverse_trunc_toLaurent {R : Type u_1} [Semiring R] :
              Function.LeftInverse LaurentPolynomial.trunc Polynomial.toLaurent
              theorem Polynomial.trunc_toLaurent {R : Type u_1} [Semiring R] (f : Polynomial R) :
              LaurentPolynomial.trunc (Polynomial.toLaurent f) = f
              theorem Polynomial.toLaurent_injective {R : Type u_1} [Semiring R] :
              Function.Injective Polynomial.toLaurent
              theorem Polynomial.toLaurent_inj {R : Type u_1} [Semiring R] (f : Polynomial R) (g : Polynomial R) :
              Polynomial.toLaurent f = Polynomial.toLaurent g f = g
              theorem Polynomial.toLaurent_ne_zero {R : Type u_1} [Semiring R] {f : Polynomial R} :
              f 0 Polynomial.toLaurent f 0
              theorem LaurentPolynomial.exists_T_pow {R : Type u_1} [Semiring R] (f : LaurentPolynomial R) :
              n f', Polynomial.toLaurent f' = f * LaurentPolynomial.T n
              theorem LaurentPolynomial.induction_on_mul_T {R : Type u_1} [Semiring R] {Q : LaurentPolynomial RProp} (f : LaurentPolynomial R) (Qf : {f : Polynomial R} → {n : } → Q (Polynomial.toLaurent f * LaurentPolynomial.T (-n))) :
              Q f

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

              theorem LaurentPolynomial.reduce_to_polynomial_of_mul_T {R : Type u_1} [Semiring R] (f : LaurentPolynomial R) {Q : LaurentPolynomial RProp} (Qf : (f : Polynomial R) → Q (Polynomial.toLaurent f)) (QT : (f : LaurentPolynomial R) → Q (f * LaurentPolynomial.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.
              theorem LaurentPolynomial.support_C_mul_T {R : Type u_1} [Semiring R] (a : R) (n : ) :
              (LaurentPolynomial.C a * LaurentPolynomial.T n).support {n}
              theorem LaurentPolynomial.support_C_mul_T_of_ne_zero {R : Type u_1} [Semiring R] {a : R} (a0 : a 0) (n : ) :
              (LaurentPolynomial.C a * LaurentPolynomial.T n).support = {n}
              theorem LaurentPolynomial.toLaurent_support {R : Type u_1} [Semiring R] (f : Polynomial R) :
              (Polynomial.toLaurent f).support = Nat.castEmbedding ( f)

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

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

              Instances For
                theorem LaurentPolynomial.degree_C_mul_T {R : Type u_1} [Semiring R] (n : ) (a : R) (a0 : a 0) :
       (LaurentPolynomial.C a * LaurentPolynomial.T n) = n
                theorem LaurentPolynomial.degree_C_mul_T_ite {R : Type u_1} [Semiring R] (n : ) (a : R) :
       (LaurentPolynomial.C a * LaurentPolynomial.T n) = if a = 0 then else n
                theorem LaurentPolynomial.degree_C {R : Type u_1} [Semiring R] {a : R} (a0 : a 0) :
       (LaurentPolynomial.C a) = 0
                theorem LaurentPolynomial.degree_C_ite {R : Type u_1} [Semiring R] (a : R) :
       (LaurentPolynomial.C a) = if a = 0 then else 0
                theorem LaurentPolynomial.degree_C_mul_T_le {R : Type u_1} [Semiring R] (n : ) (a : R) :
       (LaurentPolynomial.C a * LaurentPolynomial.T n) n
                theorem LaurentPolynomial.degree_C_le {R : Type u_1} [Semiring R] (a : R) :
       (LaurentPolynomial.C a) 0
                theorem LaurentPolynomial.algebraMap_eq_toLaurent {R : Type u_1} [CommSemiring R] (f : Polynomial R) :
                ↑(algebraMap (Polynomial R) (LaurentPolynomial R)) f = Polynomial.toLaurent f

                The map which substitutes T ↦ T⁻¹ into a Laurent polynomial.

                Instances For
                  theorem LaurentPolynomial.invert_T {R : Type u_2} [CommSemiring R] (n : ) :
                  LaurentPolynomial.invert (LaurentPolynomial.T n) = LaurentPolynomial.T (-n)
                  theorem LaurentPolynomial.invert_apply {R : Type u_2} [CommSemiring R] (f : LaurentPolynomial R) (n : ) :
                  ↑(LaurentPolynomial.invert f) n = f (-n)
                  theorem LaurentPolynomial.invert_comp_C {R : Type u_2} [CommSemiring R] :
                  LaurentPolynomial.invert LaurentPolynomial.C = LaurentPolynomial.C
                  theorem LaurentPolynomial.invert_C {R : Type u_2} [CommSemiring R] (t : R) :
                  LaurentPolynomial.invert (LaurentPolynomial.C t) = LaurentPolynomial.C t
                  theorem LaurentPolynomial.involutive_invert {R : Type u_2} [CommSemiring R] :
                  Function.Involutive LaurentPolynomial.invert
                  theorem LaurentPolynomial.invert_symm {R : Type u_2} [CommSemiring R] :
                  AlgEquiv.symm LaurentPolynomial.invert = LaurentPolynomial.invert
                  theorem LaurentPolynomial.toLaurent_reverse {R : Type u_2} [CommSemiring R] (p : Polynomial R) :
                  Polynomial.toLaurent (Polynomial.reverse p) = LaurentPolynomial.invert (Polynomial.toLaurent p) * LaurentPolynomial.T ↑(Polynomial.natDegree p)