Universal property of polynomial ring

Stream: Is there code for X?

[Artie Khovanov]

We have Polynomial.algHom_ext_iff. But do we have the bijection itself? I can't find it. Here's roughly what I'm looking for:

variable {A B : Type*} [CommSemiring A] [Semiring B] [Algebra A B]

@[simps]
noncomputable def AlgHomEquiv : (A[X] →ₐ[A] B) ≃ B where
  toFun f := f X
  invFun y := aeval y
  left_inv f := by ext; simp
  right_inv y := by simp

[Riccardo Brasca]

I don't think so, but in practice using aeval works well

[Artie Khovanov]

Yeah I agree.
However I really wanted the bijection because I wanted to prove other, more complicated, universal properties easily.
In any case this is not much code so nbd.

[Riccardo Brasca]

We have MonoidAlgebra.lift that is basically the general case for monoid algebras

[Riccardo Brasca]

but it is surely more painful to use than just aeval

[Artie Khovanov]

My application:

variable (R : Type*) {S : Type*} [CommRing R] [Ring S] [Algebra R S] (x : S)

structure IsGenerator : Prop where
  adjoin_eq_top : adjoin R {x} = ⊤

variable {R x} (hx : IsGenerator R x)

variable {T : Type*} [Ring T] [Algebra R T]

noncomputable def liftEquiv :
    { y : T // ∀ g : R[X], aeval x g = 0 → aeval y g = 0 } ≃ (S →ₐ[R] T) :=
  ((AlgHomEquiv R T).subtypeEquiv (by simp [SetLike.le_def])).trans <|
  AlgHom.liftOfSurjective _ hx.aeval_surjective

(AlgHom.liftOfSurjective doesn't exist in Mathlib but it's just a striaghtforward generalisation of RingHom.liftOfSurjective)