Defining an explicit ring homomorphism

Stream: new members

[Caroline Nunn]

Hi, apologies if this is too simple of a question for this chat. I am trying to write a simple proof in Lean to get familiar with how everything works, and I am trying to define the ring homomorphism from ℤ[X] to FractionRing ℤ[X] which sends X to X+1/X. Is there an easy way to do this?

[Paul Schwahn]

I don't know the answer unfortunately, but I can expand on the question, because I'd also like to know: Does there exist an analogue of Basis.constr (which yields a homomorphism if you specify the values for a set of generators) for free (unital, associative) algebras instead of just free modules?

[Daniel Weber]

Can you use docs#Polynomial.aeval here?

[Kevin Buzzard]

import Mathlib

-- we're doing maths
suppress_compilation

-- we want polynomial notation like `X` and `ℤ[X]`
open Polynomial

-- let K be the fraction field of ℤ[X]
notation "K" => FractionRing (ℤ[X])

-- let Y be the image of X in K (`algebraMap ℤ[X] K` is the canonical map to the field of fracs)
notation "Y" => algebraMap ℤ[X] K X

-- here's the ℤ-algebra homomorphism
example : ℤ[X] →ₐ[ℤ] K := aeval (Y + 1/Y)

-- Here's the underlying ring homomorphism
example : ℤ[X] →+* K := (aeval (Y + 1/Y)).toRingHom

@Caroline Nunn just to be clear -- the new members channel is happy to accept beginner level questions, that's the point of the channel. Please feel free to ask anything!