map out of algebra.adjoin

Stream: Is there code for X?

[Chris Hughes]

Do we have the obvious map out of algebra.adjoin R {x} given an element y of an R-algebra that is a root of the minpoly of x?

[Johan Commelin]

Isn't that adjoin.lift or something like that?

[Johan Commelin]

You were probably in the hotel room in Orsay when it was written (-;

[Johan Commelin]

Oooh! Never mind. That's adjoin_root.

[Johan Commelin]

There is

variables (F) [field F]

/-- If `p` is the minimal polynomial of `a` over `F` then `F[a] ≃ₐ[F] F[x]/(p)` -/
def alg_equiv.adjoin_singleton_equiv_adjoin_root_minpoly
  {R : Type*} [comm_ring R] [algebra F R] (x : R) :
  algebra.adjoin F ({x} : set R) ≃ₐ[F] adjoin_root (minpoly F x) :=

[Chris Hughes]

Now I need the fact that subalgebra of an algebraic field extension are fields. i.e. If K and L are fields, and L is an algebraic extension of K, then any subalgebra K L is a field.

[Chris Hughes]

But technically I suppose that alg_equiv.adjoin_singleton_equiv_adjoin_root_minpoly should assume F is just a comm_ring I guess.

[Anne Baanen]

Chris Hughes said:

Now I need the fact that subalgebra of an algebraic field extension are fields. i.e. If K and L are fields, and L is an algebraic extension of K, then any subalgebra K L is a field.

That should be docs#subalgebra.to_intermediate_field (perhaps combined with docs#intermediate_field.to_subfield) docs#subalgebra.is_field_of_algebraic

[Anne Baanen]

Chris Hughes said:

Do we have the obvious map out of algebra.adjoin R {x} given an element y of an R-algebra that is a root of the minpoly of x?

More generally there is docs#power_basis.lift