Detecting Laurent polynomials by evaluations

An infinite family of distinct units in an integral domain detects Laurent polynomials, provided that the coefficient homomorphism is injective. This applies in particular to reconstructing a polynomial from specializations of an invertible variable to successive powers of an indeterminate.

theorem TauCeti.eq_zero_of_infinite_laurent_eval₂_eq_zero {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] (f : R →+* S) (hf : Function.Injective ⇑f) (p : LaurentPolynomial R) (h : {u : Sˣ | (LaurentPolynomial.eval₂ f u) p = 0}.Infinite) : p = 0

A Laurent polynomial vanishing at infinitely many units is zero, as long as the coefficient homomorphism is injective.

theorem TauCeti.eq_of_infinite_laurent_eval₂_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] (f : R →+* S) (hf : Function.Injective ⇑f) (p q : LaurentPolynomial R) (h : {u : Sˣ | (LaurentPolynomial.eval₂ f u) p = (LaurentPolynomial.eval₂ f u) q}.Infinite) : p = q

Laurent polynomials that agree at infinitely many units are equal.

theorem TauCeti.laurent_eval₂_family_injective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] {ι : Type u_3} (f : R →+* S) (hf : Function.Injective ⇑f) (u : ι → Sˣ) (hu : (Set.range u).Infinite) : Function.Injective fun (p : LaurentPolynomial R) (i : ι) => (LaurentPolynomial.eval₂ f (u i)) p

Evaluations along any infinite range of units jointly detect Laurent polynomials. The index type need not be countable, and the family need not be injective.

theorem TauCeti.laurent_eval₂_injective_of_transcendental {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (u : Sˣ) (hu : Transcendental R ↑u) : Function.Injective ⇑(LaurentPolynomial.eval₂ (algebraMap R S) u)

Evaluation at a transcendental unit is injective.