Module

FiniteGaloisDual.lean

Nyll.GaloisCohomology.Kummer.Concrete.FiniteGaloisDual

2 declarations indexed from sourceView source ↗

Module documentation

Finite Galois-side Kummer duality

For a finite abelian Galois extension of exponent dividing n, the Kummer pairing identifies the Galois group with the character group of the actual radical quotient.

Imports1

Nyll.GaloisCohomology.Kummer.Concrete.FiniteDualSeparation

Imported by1

Nyll.GaloisCohomology.Kummer.Concrete.All

def

finiteKummerGaloisCharacterEquiv

L25 ↗

KummerTheory.finiteKummerGaloisCharacterEquiv

Documentation

The Galois group of a finite abelian Kummer extension is canonically dual to its radical quotient.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

def finiteKummerGaloisCharacterEquiv
    [FiniteDimensional K L] [IsGalois K L] [IsMulCommutative Gal(L/K)]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(L/K), sigma ^ (n : ℕ) = 1) :
    Gal(L/K) ≃*
      ((chosenFiniteKummerRadicalDatum (K := K) (L := L) n).RadicalQuotient →*
        nthRootsSubgroup L (n : ℕ))

theorem

finiteKummerGaloisCharacterEquiv_apply

L41 ↗

KummerTheory.finiteKummerGaloisCharacterEquiv_apply