Laurent polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
C : R →+* R[T;T⁻¹]the inclusion of constant polynomials, analogous to the one forR[X];T : ℤ → R[T;T⁻¹]the sequence of powers of the variableT.
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 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:
-- 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,....
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.
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.
The R-algebra map, taking a polynomial with coefficients in R to a Laurent polynomial
with coefficients in R.
The functions C and T. #
The ring homomorphism C, including R into the ring of Laurent polynomials over R as
the constant Laurent polynomials.
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.)
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
Instances for laurent_polynomial.T
The simp version of mul_assoc, in the presence of T's.
Equations
- laurent_polynomial.invertible_T n = {inv_of := laurent_polynomial.T (-n), inv_of_mul_self := _, mul_inv_of_self := _}
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.to_laurent.
Equations
- laurent_polynomial.trunc = (polynomial.to_finsupp_iso R).symm.to_add_monoid_hom.comp (finsupp.comap_domain.add_monoid_hom laurent_polynomial.trunc._proof_1)
This is a version of exists_T_pow stated as an induction principle.
Suppose that Q is a statement about Laurent polynomials such that
Qis true on ordinary polynomials;Q (f * T)impliesQ f; it follow thatQis 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 f.degree is the maximum of its support of f,
or ⊥, if f = 0.
Equations
- laurent_polynomial.algebra_polynomial R = {to_has_smul := smul_zero_class.to_has_smul smul_with_zero.to_smul_zero_class, to_ring_hom := {to_fun := polynomial.to_laurent.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}