Module

CyclicExtension.lean

Nyll.GaloisCohomology.Kummer.Concrete.CyclicExtension

3 declarations indexed from sourceView source ↗

Module documentation

Cyclic Kummer extensions

A cyclic Galois extension whose Galois group has exponent dividing n is generated by a single element whose n-th power lies in the base field, provided the base field contains a primitive n-th root of unity.

Imports2

Mathlib.SetTheory.Cardinal.Finite
Mathlib.FieldTheory.KummerExtension

Imported by2

theorem

finiteDimensionalOfCyclicGaloisExponent

L24 ↗

KummerTheory.finiteDimensionalOfCyclicGaloisExponent

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 finiteDimensionalOfCyclicGaloisExponent
    [IsGalois K L] [IsCyclic Gal(L/K)]
    (n : ℕ+) (hexponent : ∀ σ : Gal(L/K), σ ^ (n : ℕ) = 1) :
    FiniteDimensional K L

theorem

finrankDvdOfCyclicGaloisExponent

L39 ↗

KummerTheory.finrankDvdOfCyclicGaloisExponent

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 finrankDvdOfCyclicGaloisExponent
    [IsGalois K L] [IsCyclic Gal(L/K)]
    (n : ℕ+) (hexponent : ∀ σ : Gal(L/K), σ ^ (n : ℕ) = 1) :
    Module.finrank K L ∣ (n : ℕ)

theorem

exists_single_radical_generator_of_cyclic_galois_exponent

L58 ↗

KummerTheory.exists_single_radical_generator_of_cyclic_galois_exponent

Documentation

A cyclic Galois extension of exponent dividing n is generated by one nonzero radical when the base field contains a primitive n-th root of unity.

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_single_radical_generator_of_cyclic_galois_exponent
    [IsGalois K L] [IsCyclic Gal(L/K)]
    (n : ℕ+) (hμ : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ σ : Gal(L/K), σ ^ (n : ℕ) = 1) :
    ∃ α : L, α ≠ 0 ∧
      α ^ (n : ℕ) ∈ Set.range (algebraMap K L) ∧ K⟮α⟯ = ⊤

Module documentation

Cyclic Kummer extensions

Declarations

finiteDimensionalOfCyclicGaloisExponent

finrankDvdOfCyclicGaloisExponent

exists_single_radical_generator_of_cyclic_galois_exponent