The largest admissible Kummer subgroup is the full unit group. Its restricted radical quotient is canonically the ordinary power-class group.
The largest admissible Kummer subgroup, corresponding to adjoining all n-th roots of elements of Kˣ.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]def maximalKummerSubgroup (n : ℕ+) : KummerSubgroup K nIn the maximal Kummer subgroup, restricted ambient powers are the ordinary n-th-power subgroup of the top subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]theorem restrictedNthPowersSubgroup_maximal_eq (n : ℕ+) :
restrictedNthPowersSubgroup n (maximalKummerSubgroup K n) =
(powMonoidHom (n : ℕ) : (⊤ : Subgroup Kˣ) →* (⊤ : Subgroup Kˣ)).rangeThe radical quotient for the maximal Kummer subgroup is canonically the power-class group Kˣ / Kˣⁿ.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]def maximalRestrictedRadicalQuotientEquiv (n : ℕ+) :
Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range ≃*
RestrictedRadicalQuotient n (maximalKummerSubgroup K n)