Eigencharacter descent in a cyclic Kummer extension #
If a prime power of an element in F(eta), with eta ^ e = v, lies in the base field and the
base contains a primitive e-th root of unity, the element has only one Kummer character. The
proof constructs the root-scaling automorphism and compares coefficients in the canonical power
basis. This is the generic descent needed before applying trace-curve Kummer-class independence
at primes dividing both cover exponents.
theorem
BGS.Algebra.kummerPowerBasis_eigenvector_eq_rootMonomial
{F : Type u}
[Field F]
{e : ℕ}
(he : 0 < e)
{v ζ : F}
(hζ : IsPrimitiveRoot ζ e)
(T : AdjoinRoot (Polynomial.X ^ e - Polynomial.C v) →ₐ[F] AdjoinRoot (Polynomial.X ^ e - Polynomial.C v))
(hTroot :
T (AdjoinRoot.root (Polynomial.X ^ e - Polynomial.C v)) = (algebraMap F (AdjoinRoot (Polynomial.X ^ e - Polynomial.C v))) ζ * AdjoinRoot.root (Polynomial.X ^ e - Polynomial.C v))
(k : Fin (Polynomial.X ^ e - Polynomial.C v).natDegree)
(z : AdjoinRoot (Polynomial.X ^ e - Polynomial.C v))
(hz : T z = (algebraMap F (AdjoinRoot (Polynomial.X ^ e - Polynomial.C v))) (ζ ^ ↑k) * z)
:
∃ (c : F),
z = (algebraMap F (AdjoinRoot (Polynomial.X ^ e - Polynomial.C v))) c * AdjoinRoot.root (Polynomial.X ^ e - Polynomial.C v) ^ ↑k
theorem
BGS.Algebra.exists_rootMonomial_of_primePower_mem_base
{F : Type u}
[Field F]
{e q : ℕ}
(he : 0 < e)
{v ζ a : F}
(hζ : IsPrimitiveRoot ζ e)
(hirr : Irreducible (Polynomial.X ^ e - Polynomial.C v))
(hq : Nat.Prime q)
(hqe : q ∣ e)
(z : AdjoinRoot (Polynomial.X ^ e - Polynomial.C v))
(hzq : z ^ q = (algebraMap F (AdjoinRoot (Polynomial.X ^ e - Polynomial.C v))) a)
:
∃ k < e,
e ∣ q * k ∧ ∃ (c : F),
z = (algebraMap F (AdjoinRoot (Polynomial.X ^ e - Polynomial.C v))) c * AdjoinRoot.root (Polynomial.X ^ e - Polynomial.C v) ^ k
If a prime power of an element of a Kummer extension lies in the base field, then the
element occupies one residue character. The exponent k satisfies the exact invariance
condition e ∣ q*k; no coprimality between q and e is assumed.