English
Laurent polynomials are the localization of R[X] by inverting the element X, i.e., IsLocalization Away (X) from R[X] to R[T;T^{-1}].
Русский
Полиномы Лаурента являются локализацией R[X] по обращению элемента X, то есть IsLocalization Away (X) из R[X] в R[T;T^{-1}].
LaTeX
$$$IsLocalization.Away (X : R[X]) (R[T;T^{-1}]).$$$
Lean4
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]
exact isUnit_T ↑n
surj
f :=
by
induction f using LaurentPolynomial.induction_on_mul_T with
| _ f n
have : X ^ n ∈ Submonoid.powers (X : R[X]) := ⟨n, rfl⟩
refine ⟨(f, ⟨_, this⟩), ?_⟩
simp only [algebraMap_eq_toLaurent, toLaurent_X_pow, mul_T_assoc, neg_add_cancel, T_zero, mul_one]
exists_of_eq := fun {f g} =>
by
rw [algebraMap_eq_toLaurent, algebraMap_eq_toLaurent, Polynomial.toLaurent_inj]
rintro rfl
exact ⟨1, rfl⟩ }
