ClassFieldTheory.kummerAlgebra_exists_uniformFactorDegree
The uniform finite separable factors have common positive degree d, and their number is n / d. This includes degree-one and reducible cases.
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_uniformFactorDegree
(K : Type u) [Field K] (n : ℕ+) (a : Kˣ)
(hn : IsUnit ((n : ℕ) : K))
(hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
∃ (I : Type u) (_ : Finite I) (E : I → Type u)
(_ : ∀ i, Field (E i)) (_ : ∀ i, Algebra K (E i))
(_ : KummerAlgebra K n a ≃ₐ[K] ∀ i, E i) (d : ℕ),
0 < d ∧
(∀ i, Module.Finite K (E i) ∧ Algebra.IsSeparable K (E i) ∧
Module.finrank K (E i) = d) ∧
(∀ i j, Nonempty (E i ≃ₐ[K] E j)) ∧
Nat.card I * d = (n : ℕ) ∧ Nat.card I = (n : ℕ) / d