NYLL
Module

NumberFieldAbelianRadicals.lean

Nyll.AnabelianGeometry.KummerTheory.NumberFieldAbelianRadicals
2 declarations indexed from sourceView source ↗

Module documentation

A uniform bound for radicals in abelian extensions of number fields

The number of roots of unity in the original number field annihilates any power class that acquires a radical in an abelian Galois extension containing the relevant roots of unity. The bound is independent of the radical exponent and the extension.

Imports3
Imported by2

Declarations

theorem

primitiveRoot_order_dvd_torsionOrder

L30 ↗
AnabelianGeometry.KummerTheory.primitiveRoot_order_dvd_torsionOrder
Documentation

The order of a primitive root in a number field divides the number of roots of unity of that field.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped NumberField IsMulCommutative
namespace AnabelianGeometry.KummerTheory
variable {K : Type*} [Field K]
Lean source · statement
theorem primitiveRoot_order_dvd_torsionOrder
    (n : ℕ+) (ζ : K) (hζ : IsPrimitiveRoot ζ (n : ℕ)) :
    (n : ℕ) ∣ NumberField.Units.torsionOrder K
theorem

exists_unit_power_torsionOrder_of_abelian

L50 ↗
AnabelianGeometry.KummerTheory.exists_unit_power_torsionOrder_of_abelian
Documentation

The roots-of-unity order of the original number field uniformly kills the power class of every radical in an abelian Galois extension containing all roots of unity of the relevant order.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped NumberField IsMulCommutative
namespace AnabelianGeometry.KummerTheory
variable {K : Type*} [Field K]
Lean source · statement
theorem exists_unit_power_torsionOrder_of_abelian
    [NumberField K] {L : Type*} [Field L] [Algebra K L] [IsGalois K L]
    [IsMulCommutative (L ≃ₐ[K] L)]
    (n : ℕ+) (ζ : L) (hζ : IsPrimitiveRoot ζ (n : ℕ))
    (a : Kˣ) (r : L) (hr : r ≠ 0)
    (ha : r ^ (n : ℕ) = algebraMap K L (a : K)) :
    ∃ c : Kˣ, c ^ (n : ℕ) = a ^ NumberField.Units.torsionOrder K

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.