Laurent polynomials coming from polynomials

A Laurent polynomial comes from a polynomial exactly when all its negative coefficients vanish. The same criterion applies to an algebra homomorphism with Laurent-polynomial values: it factors through Polynomial.toLaurent exactly when all negative coefficients of its values vanish, and such a factorization is unique because Polynomial.toLaurent is injective.

Main results

• TauCeti.exists_toLaurent_eq_iff: a Laurent polynomial lies in the image of Polynomial.toLaurent iff its negative coefficients vanish.
• TauCeti.exists_algHom_toLaurent_comp_eq_iff: the same criterion for a Laurent-valued algebra homomorphism to factor through Polynomial.toLaurentAlg.
• LaurentPolynomial.isScalarTower_polynomial: the scalar tower R → R[X] → R[T;T⁻¹] along Polynomial.toLaurent.

@[simp]

theorem TauCeti.exists_toLaurent_eq_iff {A : Type u_2} [Semiring A] {p : LaurentPolynomial A} : (∃ (q : Polynomial A), Polynomial.toLaurent q = p) ↔ ∀ n < 0, p.coeff n = 0

A Laurent polynomial comes from a polynomial exactly when its negative coefficients vanish.

theorem TauCeti.exists_algHom_toLaurent_comp_eq_iff {R : Type u_1} {A : Type u_2} {H : Type u_3} [CommSemiring R] [CommSemiring A] [Semiring H] [Algebra R A] [Algebra R H] {f : H →ₐ[R] LaurentPolynomial A} : (∃ (F : H →ₐ[R] Polynomial A), (AlgHom.restrictScalars R Polynomial.toLaurentAlg).comp F = f) ↔ ∀ (h : H), ∀ n < 0, (f h).coeff n = 0

A Laurent-valued algebra homomorphism extends to polynomial values exactly when all its negative coefficients vanish.

instance LaurentPolynomial.isScalarTower_polynomial (R : Type u_1) [CommSemiring R] : IsScalarTower R (Polynomial R) (LaurentPolynomial R)

The scalar tower R → R[X] → R[T;T⁻¹], along Polynomial.toLaurent.