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

• C : R →+* R[T;T⁻¹] the inclusion of constant polynomials, analogous to the one for R[X];
• T : ℤ → R[T;T⁻¹] the sequence of powers of the variable T.

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] := -- refine (?_ : R[ℕ] →[R] R[X]).comp ?_ -- · exact ⟨(toFinsuppIso R).symm, by simp⟩ -- · refine ⟨fun r ↦ comapDomain _ r -- (Set.injOn_of_injective (fun _ _ ↦ Int.ofNat.inj) _), ?_⟩ -- exact fun r f ↦ comapDomain_smul .. -- -- 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,....

@[reducible, inline]

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.

Equations

• LaurentPolynomial R = AddMonoidAlgebra R ℤ

def LaurentPolynomial.«term_[T;T⁻¹]» : Lean.TrailingParserDescr

Equations

• LaurentPolynomial.«term_[T;T⁻¹]» = Lean.ParserDescr.trailingNode `LaurentPolynomial.«term_[T;T⁻¹]» 9000 0 (Lean.ParserDescr.symbol "[T;T⁻¹]")

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

def Polynomial.toLaurent {R : Type u_1} [Semiring R] : Polynomial R →+* LaurentPolynomial R

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

Equations

• Polynomial.toLaurent = (AddMonoidAlgebra.mapDomainRingHom R Int.ofNatHom).comp ↑(Polynomial.toFinsuppIso R)

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.

def Polynomial.toLaurentAlg {R : Type u_1} [CommSemiring R] : Polynomial R →ₐ[R] LaurentPolynomial R

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

Equations

• Polynomial.toLaurentAlg = (AddMonoidAlgebra.mapDomainAlgHom R R Int.ofNatHom).comp ↑(Polynomial.toFinsuppIsoAlg R)

@[simp]

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] : Finsupp.single 0 1 = 1

The functions C and T.

def LaurentPolynomial.C {R : Type u_1} [Semiring R] : R →+* LaurentPolynomial R

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

Equations

• LaurentPolynomial.C = AddMonoidAlgebra.singleZeroRingHom

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) : Finsupp.single 0 r = LaurentPolynomial.C r

@[simp]

theorem LaurentPolynomial.C_apply {R : Type u_1} [Semiring R] (t : R) (n : ℤ) : (LaurentPolynomial.C t) n = if n = 0 then t else 0

def LaurentPolynomial.T {R : Type u_1} [Semiring R] (n : ℤ) : LaurentPolynomial R

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.

Equations

• LaurentPolynomial.T n = Finsupp.single n 1

@[simp]

theorem LaurentPolynomial.T_apply {R : Type u_1} [Semiring R] (m n : ℤ) : (LaurentPolynomial.T n) m = if n = m then 1 else 0

@[simp]

theorem LaurentPolynomial.T_zero {R : Type u_1} [Semiring R] : LaurentPolynomial.T 0 = 1

theorem LaurentPolynomial.T_add {R : Type u_1} [Semiring R] (m n : ℤ) : LaurentPolynomial.T (m + n) = LaurentPolynomial.T m * LaurentPolynomial.T n

theorem LaurentPolynomial.T_sub {R : Type u_1} [Semiring R] (m n : ℤ) : LaurentPolynomial.T (m - n) = LaurentPolynomial.T m * LaurentPolynomial.T (-n)

@[simp]

theorem LaurentPolynomial.T_pow {R : Type u_1} [Semiring R] (m : ℤ) (n : ℕ) : LaurentPolynomial.T m ^ n = LaurentPolynomial.T (↑n * m)

@[simp]

theorem LaurentPolynomial.mul_T_assoc {R : Type u_1} [Semiring R] (f : LaurentPolynomial R) (m n : ℤ) : f * LaurentPolynomial.T m * LaurentPolynomial.T n = f * LaurentPolynomial.T (m + n)

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

@[simp]

theorem LaurentPolynomial.single_eq_C_mul_T {R : Type u_1} [Semiring R] (r : R) (n : ℤ) : Finsupp.single n r = LaurentPolynomial.C r * LaurentPolynomial.T n

@[simp]

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

@[simp]

theorem Polynomial.toLaurent_C {R : Type u_1} [Semiring R] (r : R) : Polynomial.toLaurent (Polynomial.C r) = LaurentPolynomial.C r

@[simp]

theorem Polynomial.toLaurent_comp_C {R : Type u_1} [Semiring R] : ⇑Polynomial.toLaurent ∘ ⇑Polynomial.C = ⇑LaurentPolynomial.C

@[simp]

theorem Polynomial.toLaurent_X {R : Type u_1} [Semiring R] : Polynomial.toLaurent Polynomial.X = LaurentPolynomial.T 1

@[simp]

theorem Polynomial.toLaurent_one {R : Type u_1} [Semiring R] : Polynomial.toLaurent 1 = 1

@[simp]

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

@[simp]

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

instance LaurentPolynomial.invertibleT {R : Type u_1} [Semiring R] (n : ℤ) : Invertible (LaurentPolynomial.T n)

Equations

• LaurentPolynomial.invertibleT n = { invOf := LaurentPolynomial.T (-n), invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

@[simp]

theorem LaurentPolynomial.invOf_T {R : Type u_1} [Semiring R] (n : ℤ) : ⅟(LaurentPolynomial.T n) = LaurentPolynomial.T (-n)

theorem LaurentPolynomial.isUnit_T {R : Type u_1} [Semiring R] (n : ℤ) : IsUnit (LaurentPolynomial.T n)

theorem LaurentPolynomial.induction_on {R : Type u_1} [Semiring R] {M : LaurentPolynomial R → Prop} (p : LaurentPolynomial R) (h_C : ∀ (a : R), M (LaurentPolynomial.C a)) (h_add : ∀ {p q : LaurentPolynomial R}, M p → M q → M (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 R → Prop} (p : LaurentPolynomial R) (h_add : ∀ (p q : LaurentPolynomial R), M p → M q → M (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.

theorem LaurentPolynomial.commute_T {R : Type u_1} [Semiring R] (n : ℤ) (f : LaurentPolynomial R) : Commute (LaurentPolynomial.T n) f

@[simp]

theorem LaurentPolynomial.T_mul {R : Type u_1} [Semiring R] (n : ℤ) (f : LaurentPolynomial R) : LaurentPolynomial.T n * f = f * LaurentPolynomial.T n

def LaurentPolynomial.trunc {R : Type u_1} [Semiring R] : LaurentPolynomial R →+ Polynomial 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.toLaurent.

Equations

• LaurentPolynomial.trunc = (Polynomial.toFinsuppIso R).symm.toAddMonoidHom.comp (Finsupp.comapDomain.addMonoidHom ⋯)

@[simp]

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 n.toNat) r else 0

@[simp]

theorem LaurentPolynomial.leftInverse_trunc_toLaurent {R : Type u_1} [Semiring R] : Function.LeftInverse ⇑LaurentPolynomial.trunc ⇑Polynomial.toLaurent

@[simp]

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

@[simp]

theorem Polynomial.toLaurent_inj {R : Type u_1} [Semiring R] (f 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 R), Polynomial.toLaurent f' = f * LaurentPolynomial.T ↑n

theorem LaurentPolynomial.induction_on_mul_T {R : Type u_1} [Semiring R] {Q : LaurentPolynomial R → Prop} (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 R → Prop} (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 = Finset.map Nat.castEmbedding f.support

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 ℕ ↪ ℤ.

def LaurentPolynomial.degree {R : Type u_1} [Semiring R] (f : LaurentPolynomial R) : WithBot ℤ

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

Equations

• f.degree = f.support.max

@[simp]

theorem LaurentPolynomial.degree_zero {R : Type u_1} [Semiring R] : LaurentPolynomial.degree 0 = ⊥

@[simp]

theorem LaurentPolynomial.degree_eq_bot_iff {R : Type u_1} [Semiring R] {f : LaurentPolynomial R} : f.degree = ⊥ ↔ f = 0

@[simp]

theorem LaurentPolynomial.degree_C_mul_T {R : Type u_1} [Semiring R] (n : ℤ) (a : R) (a0 : a ≠ 0) : (LaurentPolynomial.C a * LaurentPolynomial.T n).degree = ↑n

theorem LaurentPolynomial.degree_C_mul_T_ite {R : Type u_1} [Semiring R] [DecidableEq R] (n : ℤ) (a : R) : (LaurentPolynomial.C a * LaurentPolynomial.T n).degree = if a = 0 then ⊥ else ↑n

@[simp]

theorem LaurentPolynomial.degree_T {R : Type u_1} [Semiring R] [Nontrivial R] (n : ℤ) : (LaurentPolynomial.T n).degree = ↑n

theorem LaurentPolynomial.degree_C {R : Type u_1} [Semiring R] {a : R} (a0 : a ≠ 0) : (LaurentPolynomial.C a).degree = 0

theorem LaurentPolynomial.degree_C_ite {R : Type u_1} [Semiring R] [DecidableEq R] (a : R) : (LaurentPolynomial.C a).degree = 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).degree ≤ ↑n

theorem LaurentPolynomial.degree_T_le {R : Type u_1} [Semiring R] (n : ℤ) : (LaurentPolynomial.T n).degree ≤ ↑n

theorem LaurentPolynomial.degree_C_le {R : Type u_1} [Semiring R] (a : R) : (LaurentPolynomial.C a).degree ≤ 0

instance LaurentPolynomial.instModulePolynomial {R : Type u_1} [Semiring R] : Module (Polynomial R) (LaurentPolynomial R)

Equations

• LaurentPolynomial.instModulePolynomial = Module.compHom (LaurentPolynomial R) Polynomial.toLaurent

instance LaurentPolynomial.instIsScalarTowerPolynomial (R : Type u_2) [Semiring R] : IsScalarTower (Polynomial R) (Polynomial R) (LaurentPolynomial R)

Equations

• ⋯ = ⋯

instance LaurentPolynomial.algebraPolynomial (R : Type u_2) [CommSemiring R] : Algebra (Polynomial R) (LaurentPolynomial R)

Equations

• LaurentPolynomial.algebraPolynomial R = Algebra.mk Polynomial.toLaurent ⋯ ⋯

theorem LaurentPolynomial.algebraMap_X_pow {R : Type u_1} [CommSemiring R] (n : ℕ) : (algebraMap (Polynomial R) (LaurentPolynomial R)) (Polynomial.X ^ n) = LaurentPolynomial.T ↑n

@[simp]

theorem LaurentPolynomial.algebraMap_eq_toLaurent {R : Type u_1} [CommSemiring R] (f : Polynomial R) : (algebraMap (Polynomial R) (LaurentPolynomial R)) f = Polynomial.toLaurent f

theorem LaurentPolynomial.isLocalization {R : Type u_1} [CommSemiring R] : IsLocalization (Submonoid.closure {Polynomial.X}) (LaurentPolynomial R)

def LaurentPolynomial.invert {R : Type u_2} [CommSemiring R] : LaurentPolynomial R ≃ₐ[R] LaurentPolynomial R

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

Equations

• LaurentPolynomial.invert = AddMonoidAlgebra.domCongr R R (AddEquiv.neg ℤ)

@[simp]

theorem LaurentPolynomial.invert_T {R : Type u_2} [CommSemiring R] (n : ℤ) : LaurentPolynomial.invert (LaurentPolynomial.T n) = LaurentPolynomial.T (-n)

@[simp]

theorem LaurentPolynomial.invert_apply {R : Type u_2} [CommSemiring R] (f : LaurentPolynomial R) (n : ℤ) : (LaurentPolynomial.invert f) n = f (-n)

@[simp]

theorem LaurentPolynomial.invert_comp_C {R : Type u_2} [CommSemiring R] : ⇑LaurentPolynomial.invert ∘ ⇑LaurentPolynomial.C = ⇑LaurentPolynomial.C

@[simp]

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

@[simp]

theorem LaurentPolynomial.invert_symm {R : Type u_2} [CommSemiring R] : LaurentPolynomial.invert.symm = LaurentPolynomial.invert

theorem LaurentPolynomial.toLaurent_reverse {R : Type u_2} [CommSemiring R] (p : Polynomial R) : Polynomial.toLaurent p.reverse = LaurentPolynomial.invert (Polynomial.toLaurent p) * LaurentPolynomial.T ↑p.natDegree