Conjugating square roots by algebra homomorphisms #
If y and z are square roots of the same scalar r : K and K(y) is quadratic, any
K-algebra homomorphism from the algebra containing z into the normal field containing y
can be adjusted to carry z to y.
theorem
TauCeti.exists_algHom_apply_eq_of_sq_eq
{K : Type u_1}
{L : Type u_2}
{M : Type u_3}
[Field K]
[Field L]
[Semiring M]
[Algebra K L]
[Algebra K M]
{r : K}
{y : L}
{z : M}
[Normal K L]
(hy : y ^ 2 = (algebraMap K L) r)
(hydegree : Module.finrank K ↥K⟮y⟯ = 2)
(hz : z ^ 2 = (algebraMap K M) r)
(hφ : Nonempty (M →ₐ[K] L))
:
If y and z are square roots of the same scalar and K(y) is quadratic, any
K-algebra homomorphism from the algebra containing z into the normal field containing y can
be adjusted by an automorphism of the target to carry z to y.