English
There is a ring homomorphism eval₂: R[T;T⁻¹] → S sending T to x and T⁻¹ to x⁻¹, defined via IsLocalization.lift with respect to the powers of X.
Русский
Существуют кольцевые однородные отображения eval₂: R[T;T⁻¹] → S, отправляющее T в x и T⁻¹ в x⁻¹, определяемое через IsLocalization.lift по степеням X.
LaTeX
$$$\\mathrm{eval_2}: R[T;T^{-1}] \\to S \\quad\\text{such that}\\quad \\mathrm{eval_2}(T)=x,\\; \\mathrm{eval_2}(T^{-1})=x^{-1}.$$$
Lean4
/-- 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 x.isUnit.pow n
