Units of Laurent polynomials

A constant Laurent polynomial C r is a unit exactly when its coefficient r is a unit. The map C is Mathlib's AddMonoidAlgebra.singleZeroRingHom, which is a local ring homomorphism. This is the Laurent counterpart of Mathlib's Polynomial.isUnit_C.

Over a commutative ring without zero divisors, every unit of R[T;T⁻¹] is a unit monomial C r * T n. This is the Laurent counterpart of Mathlib's Polynomial.isUnit_iff, where only the constants survive. Over ℤ it says that the units of ℤ[T;T⁻¹] are exactly ±Tⁿ, which is the form taken by a unimodular determinant over the Laurent ring.

Main results

• LaurentPolynomial.isUnit_C: C r is a unit if and only if r is.
• LaurentPolynomial.isUnit_iff: over a commutative ring without zero divisors, the units of R[T;T⁻¹] are the monomials C r * T n with r a unit.
• LaurentPolynomial.isUnit_iff_exists_eq_T_or_neg_T: the units of ℤ[T;T⁻¹] are the ±Tⁿ.
• TauCeti.shiftClassGroupLaurentPolynomialEquiv: for R[T;T⁻¹] graded with T of degree w, the shift class group TauCeti.ShiftClassGroup of homogeneous unit degrees is ZMod |w|.

@[simp]

theorem LaurentPolynomial.isUnit_C {R : Type u_1} [Semiring R] {r : R} : IsUnit (C r) ↔ IsUnit r

A constant Laurent polynomial is a unit exactly when its coefficient is.

theorem LaurentPolynomial.isUnit_iff {R : Type u_1} [CommRing R] [NoZeroDivisors R] {f : LaurentPolynomial R} : IsUnit f ↔ ∃ (r : R), IsUnit r ∧ ∃ (n : ℤ), C r * T n = f

Units of a Laurent polynomial ring. Over a commutative ring without zero divisors, a Laurent polynomial is a unit exactly when it is a unit monomial C r * T n.

theorem LaurentPolynomial.isUnit_iff_exists_eq_T_or_neg_T {f : LaurentPolynomial ℤ} : IsUnit f ↔ ∃ (n : ℤ), f = T n ∨ f = -T n

Units of ℤ[T;T⁻¹]. An integral Laurent polynomial is a unit exactly when it is Tⁿ or -Tⁿ for some n : ℤ.

noncomputable def TauCeti.shiftClassGroupLaurentPolynomialEquiv (R : Type u_1) [CommSemiring R] [Nontrivial R] (w : ℤ) : ShiftClassGroup (AddMonoidAlgebra.gradeBy R ⇑((zmultiplesHom ℤ) w)) ≃+ ZMod w.natAbs

For the Laurent ring R[T;T⁻¹] over a nontrivial commutative semiring, graded with T of degree w, the degrees of the homogeneous units are the multiples of w (by homogeneousUnitDegrees_gradeBy), so the shift class group is ZMod |w|. This is the graded ring of 𝔾_m acting on itself by s • x = s ^ w * x.

@[simp]

theorem TauCeti.shiftClassGroupLaurentPolynomialEquiv_mk (R : Type u_1) [CommSemiring R] [Nontrivial R] (w d : ℤ) : (shiftClassGroupLaurentPolynomialEquiv R w) ↑d = ↑d

The identification of the shift classes of R[T;T⁻¹] with ZMod |w| sends the class of a shift d to d mod |w|.