Module

PrimeCyclicEigenunit.lean

Nyll.GaloisCohomology.Kummer.Concrete.PrimeCyclicEigenunit

1 declaration indexed from sourceView source ↗

Module documentation

Primitive eigenunits in prime-degree Galois extensions

A nonidentity automorphism of a prime-degree Galois extension has an eigenunit with primitive eigenvalue when the base field contains the corresponding roots of unity. The unit is produced by the cyclic Kummer radical generator theorem.

Imports4

Nyll.GaloisCohomology.Kummer.Concrete.CyclicExtension
Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Imported by4

theorem

exists_primitive_eigenunit_of_prime_degree

L30 ↗

KummerTheory.exists_primitive_eigenunit_of_prime_degree

Documentation

A nonidentity automorphism of a prime-degree Galois extension admits an eigenunit with a primitive eigenvalue, constructed from roots of unity in the base field.

Source context 3 commands

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

namespace KummerTheory
open IntermediateField
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem exists_primitive_eigenunit_of_prime_degree
    [FiniteDimensional K L] [IsGalois K L]
    {p : ℕ} (hp : p.Prime) (hdeg : Module.finrank K L = p)
    (hμ : (primitiveRoots p K).Nonempty)
    (σ : Gal(L/K)) (hσ : σ ≠ 1) :
    ∃ α : Lˣ, ∃ ζ : Lˣ,
      IsPrimitiveRoot ζ p ∧ Units.map σ.toMonoidHom α = ζ * α

Module documentation

Primitive eigenunits in prime-degree Galois extensions

Declarations

exists_primitive_eigenunit_of_prime_degree