Extending a RingHom by adjoining new elements

Stream: Is there code for X?

[Weiyi Wang]

How would I write this definition? (Or is something like this already in Mathlib?)

import Mathlib

/-- Extend a ring hom from subring by adjoining a new element and specifying the corresponding value -/
def ringHomExtend {F G : Type*} [Ring F] [Ring G]
    (F' : Subring F) (f : F' →+* G) (x : F) (hx : x ∉ F') (y : G) :
    Subring.closure (F' ∪ {x}) →+* G := sorry

[Aaron Liu]

Does that always work?

[Aaron Liu]

What if the x satisfies equations over F that are not satisfied by y?

[Weiyi Wang]

That's a good question

[Weiyi Wang]

:melting_face: welp, that means I need to rethink the whole idea of the thing I wanted to prove

[Weiyi Wang]

I am aware that I am likely going to run into XY problem if I keep asking following this path, but just out of curiosity, let's say I add additional condition saying x is transcendental, would this work and how to write it?

[Aaron Liu]

If x is transcendental, then Subring.closure (F' ∪ {x}) is isomorphic to F'[X], and you can use the universal property of polynomials

[Kevin Buzzard]

In this generality (no commutativity, no domain assumption) I am not at all sure what "transcendental" even means.

[Kevin Buzzard]

Certainly what Aaron says is false because there's no reason x will commute with F'.

[Aaron Liu]

oh I guess if it's not a commutative ring then polynomials don't have the same universal property

[Weiyi Wang]

That's my bad. The case I am considering is commutative. This is some really early prototype code that by no means captures the correct generality