algebra K L implies algebra (polynomial K) (polynomial L)

Stream: new members

[Sebastian Monnet]

According to polynomial.algebra_of_algebra, if we have a field extension $L/K$, then we also have that polynomial L is an algebra over polynomial K. I'm trying to get the algebra map from polynomial K to polynomial L, and I can't understand why the following doesn't work.

import field_theory.adjoin
import algebra.big_operators.basic
import data.polynomial.algebra_map

def alg_map (K L : Type*) [field K] [field L] [algebra K L] : polynomial(K) →+* polynomial(L) := algebra_map (polynomial K) (polynomial L)

Can anyone help?

[Kevin Buzzard]

So the reason what you wrote doesn't work is that we don't have the instance that if L is a K-algebra then $L[X]$ is a $K[X]$-algebra. In fact it might be best not to have that instance, because one could imagine wanting to give $L[X]$ a different algebra structure, and making it an instance would make this quite annoying to do (the point of an instance is that it's the "one fixed canonical" term of the class; this is why stuff like ring_hom is not a class, because it's completely fine to have two ring homomorphisms between two rings $A$ and $B$ in a proof).

[Kevin Buzzard]

Here's how to do it:

import field_theory.adjoin
import algebra.big_operators.basic
import data.polynomial.algebra_map

noncomputable def alg_map (K L : Type*) [field K] [field L] [algebra K L] :
  polynomial(K) →+* polynomial(L) :=
polynomial.map_ring_hom (algebra_map K L)

polynomial.map_ring_hom is the functoriality of polynomial with respect to ring homomorphisms -- it eats a ring hom $K\to L$ and outputs a ring hom $K[X]\to L[X]$.

[Johan Commelin]

So what is docs#polynomial.algebra_of_algebra

[Johan Commelin]

Aha, @Sebastian Monnet that instance gives you the algebra structure K → L[X]

[Kevin Buzzard]

Looks like it's the $K$-algebra structure on $L[X]$ so no contradiction.

[Kevin Buzzard]

polynomial.map_ring_hom should probably just be called polynomial.map. Then what to call polynomial.map?

[Johan Commelin]

Maybe it can cease to exist?

[Johan Commelin]

Otoh, sometimes you just want to apply a function to the coefficients, without it being a ring hom. There are some weird edge cases.

[Johan Commelin]

E.g., if you have f ∈ ℤ[X] and a proof that all coefficients are positive, then you might want to map it through int.to_nat to get a polynomial in ℕ[X].

[Sebastian Monnet]

Ohhhh yes I misread polynomial.algebra_of_algebra to be the thing I was looking for!

[Sebastian Monnet]

Thanks