NYLL
Module

AbelianRadicalPowerClasses.lean

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

Module documentation

Power classes of radicals in abelian extensions

If an n-th radical lies in an abelian Galois extension containing the n-th roots of unity, its power-class order is the order of a root of unity in the original base field. This follows from the explicit cyclotomic descent calculation for every Galois automorphism; no uniform cyclotomic-image hypothesis is supplied as an assumption.

Imports3
Imported by2

Declarations

theorem

exists_cyclotomic_displacement

L31 ↗
AnabelianGeometry.KummerTheory.exists_cyclotomic_displacement
Documentation

Every automorphism acts on the n-th roots of unity by a positive power. The exponent is obtained from a primitive root, rather than assumed.

Source context 4 commands

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

noncomputable section
open scoped IsMulCommutative
namespace AnabelianGeometry.KummerTheory
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem exists_cyclotomic_displacement
    (n : ℕ+) (ζ : L) (hζ : IsPrimitiveRoot ζ (n : ℕ)) (σ : L ≃ₐ[K] L) :
    ∃ m : ℕ, ∀ ξ : L, ξ ^ (n : ℕ) = 1 → σ ξ = ξ ^ (m + 1)
theorem

exists_primitiveRoot_powerClass_order_of_abelian

L49 ↗
AnabelianGeometry.KummerTheory.exists_primitiveRoot_powerClass_order_of_abelian
Documentation

The order of a radical power class in an abelian Galois extension is realized by a primitive root of unity in the original field.

Source context 4 commands

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

noncomputable section
open scoped IsMulCommutative
namespace AnabelianGeometry.KummerTheory
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem exists_primitiveRoot_powerClass_order_of_abelian
    [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)) :
    ∃ η : K, IsPrimitiveRoot η
      (orderOf ((QuotientGroup.mk' (powMonoidHom (α := Kˣ) (n : ℕ)).range) a))

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