galois action is injective on roots

Stream: Is there code for X?

[Andrew Yang]

What is the easiest way to show the following?

import MathLib

example {K L} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    (pb : PowerBasis K L) : Function.Injective (fun i : L ≃ₐ[K] L ↦ i pb.gen) := sorry

To unxy, I would like to show that $\sum_\sigma \frac{f(X)}{X - \sigma\alpha}\frac{\sigma\alpha^r}{f'(\sigma\alpha)} = X ^ r$ by showing that both sides have n common roots. The sorry above is used to show that the roots are distinct.

[Kevin Buzzard]

Here's a rather inelegant but short solution (change MathLib to mathlib first ;-) ):

example {K L} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    (pb : PowerBasis K L) : Function.Injective (fun i : L ≃ₐ[K] L ↦ i pb.gen) := by
  intro φ ψ h
  suffices φ.toAlgHom = ψ by
    ext x
    rw [FunLike.ext_iff] at this
    apply this
  apply PowerBasis.algHom_ext
  exact h

[Junyan Xu]

Yeah, pb : PowerBasis K L says in particular that L is generated over K by pb.gen, so a K-AlgHom out of L is determined by its value at pb.gen, and it being an AlgEquiv or L/K being finite-dimensional/Galois are irrelevant.

[Junyan Xu]

Golfed:

import Mathlib
example {K L} [CommRing K] [Ring L] [Algebra K L]
    (pb : PowerBasis K L) : Function.Injective (fun i : L ≃ₐ[K] L ↦ i pb.gen) :=
  fun _φ _ψ h ↦ AlgEquiv.coe_algHom_injective (pb.algHom_ext h)

[Andrew Yang]

Oh, Indeed. The hard part is Fintype.card (L ≃ₐ[K] L) = Finset.card (minpoly K pb.gen).roots but the existing API got me covered on this.

[Andrew Yang]

thanks!