Module

PrimePowerRootObstruction.lean

Nyll.GaloisCohomology.Kummer.Concrete.PrimePowerRootObstruction

1 declaration indexed from sourceView source ↗

Module documentation

A prime-power root obstruction in the Kummer quotient

A primitive r-th root cannot be an r^s-th power if the field has no primitive r^(s+1)-th root. The quotient here is the ordinary power-class group used by absoluteKummerContinuousNthRootsCharacterEquiv.

Imports4

Mathlib.Algebra.Group.Hom.Basic
Mathlib.GroupTheory.OrderOfElement
Mathlib.GroupTheory.QuotientGroup.Defs
Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Imported by2

theorem

primitiveRoot_primePowerClass_ne_one

L27 ↗

KummerTheory.primitiveRoot_primePowerClass_ne_one

Documentation

At the last available prime-power root level, a primitive root of prime order has nonidentity power class. The missing next root level is supplied by maximality of s in the roots-downstairs argument.

Source context 2 commands

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

namespace KummerTheory
variable {K : Type*} [Field K]

Lean source · statement

theorem primitiveRoot_primePowerClass_ne_one
    {r : ℕ} (hr : r.Prime) (s : ℕ) {ζ : Kˣ}
    (hζ : IsPrimitiveRoot ζ r)
    (hnext : ¬ (primitiveRoots (r ^ (s + 1)) K).Nonempty) :
    (ζ : Kˣ ⧸ (powMonoidHom (r ^ s) : Kˣ →* Kˣ).range) ≠ 1

Module documentation

A prime-power root obstruction in the Kummer quotient

Declarations

primitiveRoot_primePowerClass_ne_one