ClassFieldTheory.kummerAlgebra_exists_algEquiv_pi_simpleFields
A Kummer algebra with invertible exponent is a finite product of simple finite separable field extensions. In each factor, the image of the canonical root generates the field and has n-th power a.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheory
universe uLean source · statement
theorem kummerAlgebra_exists_algEquiv_pi_simpleFields
(K : Type u) [Field K] (n : ℕ+) (a : Kˣ)
(hn : IsUnit ((n : ℕ) : K)) :
∃ (I : Type u) (_ : Finite I) (E : I → Type u)
(_ : ∀ i, Field (E i)) (_ : ∀ i, Algebra K (E i))
(e : KummerAlgebra K n a ≃ₐ[K] ∀ i, E i),
∀ i, Module.Finite K (E i) ∧ Algebra.IsSeparable K (E i) ∧
∃ β : E i,
β = (e (AdjoinRoot.root
(Polynomial.X ^ (n : ℕ) - Polynomial.C (a : K)))) i ∧
β ^ (n : ℕ) = algebraMap K (E i) (a : K) ∧
IntermediateField.adjoin K {β} = ⊤