feat(Algebra/Polynomial/Laurent): Lifting maps to ring of Laurent polynomials (#19573)

This PR defines `LaurentPolynomial.eval₂` and provides basic API for it. This was mentioned unter "future work" in the comments.



Co-authored-by: Justus Springer <50165510+justus-springer@users.noreply.github.com>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

Author: justus-springer

Mathlib/Algebra/Polynomial/Laurent.lean

@@ -6,7 +6,7 @@ Authors: Damiano Testa
 import Mathlib.Algebra.Polynomial.AlgebraMap
 import Mathlib.Algebra.Polynomial.Reverse
 import Mathlib.Algebra.Polynomial.Inductions
-import Mathlib.RingTheory.Localization.Defs
+import Mathlib.RingTheory.Localization.Away.Basic
 
 /-!  # Laurent polynomials
 
@@ -49,8 +49,6 @@ 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] :=
@@ -484,7 +482,7 @@ end Semiring
 
 section CommSemiring
 
-variable [CommSemiring R]
+variable [CommSemiring R] {S : Type*} [CommSemiring S] (f : R →+* S) (x : Sˣ)
 
 instance algebraPolynomial (R : Type*) [CommSemiring R] : Algebra R[X] R[T;T⁻¹] where
   algebraMap := Polynomial.toLaurent
@@ -498,7 +496,7 @@ theorem algebraMap_X_pow (n : ℕ) : algebraMap R[X] R[T;T⁻¹] (X ^ n) = T n :
 theorem algebraMap_eq_toLaurent (f : R[X]) : algebraMap R[X] R[T;T⁻¹] f = toLaurent f :=
   rfl
 
-theorem isLocalization : IsLocalization (Submonoid.powers (X : R[X])) R[T;T⁻¹] :=
+instance isLocalization : IsLocalization.Away (X : R[X]) R[T;T⁻¹] :=
   { map_units' := fun ⟨t, ht⟩ => by
       obtain ⟨n, rfl⟩ := ht
       rw [algebraMap_eq_toLaurent, toLaurent_X_pow]
@@ -514,6 +512,79 @@ theorem isLocalization : IsLocalization (Submonoid.powers (X : R[X])) R[T;T⁻¹
       rintro rfl
       exact ⟨1, rfl⟩ }
 
+theorem mk'_mul_T (p : R[X]) (n : ℕ) :
+  IsLocalization.mk' R[T;T⁻¹] p (⟨X^n, n, rfl⟩ : Submonoid.powers (X : R[X])) * T n =
+    toLaurent p := by
+  rw [←toLaurent_X_pow, ←algebraMap_eq_toLaurent, IsLocalization.mk'_spec, algebraMap_eq_toLaurent]
+
+@[simp]
+theorem mk'_eq (p : R[X]) (n : ℕ) : IsLocalization.mk' R[T;T⁻¹] p
+  (⟨X^n, n, rfl⟩ : Submonoid.powers (X : R[X])) = toLaurent p * T (-n) := by
+  rw [←IsUnit.mul_left_inj (isUnit_T n), mul_T_assoc, neg_add_cancel, T_zero, mul_one]
+  exact mk'_mul_T p n
+
+theorem mk'_one_X_pow (n : ℕ) : IsLocalization.mk' R[T;T⁻¹] 1
+  (⟨X^n, n, rfl⟩ : Submonoid.powers (X : R[X])) = T (-n) := by
+  rw [mk'_eq 1 n, toLaurent_one, one_mul]
+
+@[simp]
+theorem mk'_one_X : IsLocalization.mk' R[T;T⁻¹] 1
+  (⟨X, 1, pow_one X⟩ : Submonoid.powers (X : R[X])) = T (-1) := by
+  convert mk'_one_X_pow 1
+  exact (pow_one X).symm
+
+/-- Given a ring homomorphism `f : R →+* S` and a unit `x` in `S`, the induced homomorphism
+`R[T;T⁻¹] →+* S` sending `T` to `x` and `T⁻¹` to `x⁻¹`. -/
+def eval₂ : R[T;T⁻¹] →+* S :=
+  IsLocalization.lift (M := Submonoid.powers (X : R[X])) (g := Polynomial.eval₂RingHom f x) (by
+    rintro ⟨y, n, rfl⟩
+    simpa only [coe_eval₂RingHom, eval₂_X_pow] using IsUnit.pow n x.isUnit
+  )
+
+@[simp]
+theorem eval₂_toLaurent (p : R[X]) : eval₂ f x (toLaurent p) = Polynomial.eval₂ f x p := by
+  unfold eval₂
+  rw [←algebraMap_eq_toLaurent, IsLocalization.lift_eq]
+  rfl
+
+theorem eval₂_T_n (n : ℕ) : eval₂ f x (T n) = x ^ n := by
+  rw [←Polynomial.toLaurent_X_pow, eval₂_toLaurent, eval₂_X_pow]
+
+theorem eval₂_T_neg_n (n : ℕ) : eval₂ f x (T (-n)) = x⁻¹ ^ n := by
+  rw [←mk'_one_X_pow]
+  unfold eval₂
+  rw [IsLocalization.lift_mk'_spec, map_one, coe_eval₂RingHom, eval₂_X_pow, ←mul_pow,
+    Units.mul_inv, one_pow]
+
+@[simp]
+theorem eval₂_T (n : ℤ) : eval₂ f x (T n) = (x ^ n).val := by
+  by_cases hn : 0 ≤ n
+  · lift n to ℕ using hn
+    apply eval₂_T_n
+  · obtain ⟨m, rfl⟩ := Int.exists_eq_neg_ofNat (Int.le_of_not_le hn)
+    rw [eval₂_T_neg_n, zpow_neg]
+    rfl
+
+@[simp]
+theorem eval₂_C (r : R) : eval₂ f x (C r) = f r := by
+  rw [← toLaurent_C, eval₂_toLaurent, Polynomial.eval₂_C]
+
+theorem eval₂_C_mul_T_n (r : R) (n : ℕ) : eval₂ f x (C r * T n) = f r * x ^ n := by
+  rw [←Polynomial.toLaurent_C_mul_T, eval₂_toLaurent, eval₂_monomial]
+
+theorem eval₂_C_mul_T_neg_n (r : R) (n : ℕ) : eval₂ f x (C r * T (-n)) =
+  f r * x⁻¹ ^ n := by rw [map_mul, eval₂_T_neg_n, eval₂_C]
+
+@[simp]
+theorem eval₂_C_mul_T (r : R) (n : ℤ) : eval₂ f x (C r * T n) = f r * (x ^ n).val := by
+  by_cases hn : 0 ≤ n
+  · lift n to ℕ using hn
+    rw [map_mul, eval₂_C, eval₂_T_n]
+    rfl
+  · obtain ⟨m, rfl⟩ := Int.exists_eq_neg_ofNat (Int.le_of_not_le hn)
+    rw [map_mul, eval₂_C, eval₂_T_neg_n, zpow_neg]
+    rfl
+
 end CommSemiring
 
 section Inversion