ClassFieldTheory.kummerAlgebra_exists_pi_copies_simpleFactor
A Kummer algebra of exponent n is a product of exactly n / d copies of one finite separable field factor of degree d. The norm is the product of the coordinate field norms under this algebra equivalence.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory
universe uLean source · statement
theorem kummerAlgebra_exists_pi_copies_simpleFactor
(K : Type u) [Field K] (n : ℕ+) (a : Kˣ)
(hn : IsUnit ((n : ℕ) : K))
(hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
∃ (F : Type u) (_ : Field F) (_ : Algebra K F)
(_ : Module.Finite K F) (_ : Algebra.IsSeparable K F) (d : ℕ),
0 < d ∧ Module.finrank K F = d ∧
((n : ℕ) / d) * d = (n : ℕ) ∧
∃ e : KummerAlgebra K n a ≃ₐ[K] (Fin ((n : ℕ) / d) → F),
∀ z : KummerAlgebra K n a,
Algebra.norm K z = ∏ j : Fin ((n : ℕ) / d), Algebra.norm K (e z j)