Module

FiniteCharacterEquiv.lean

Nyll.GaloisCohomology.Kummer.Concrete.FiniteCharacterEquiv

7 declarations indexed from sourceView source ↗

Module documentation

finite Kummer character isomorphism

For an actual finite Galois extension L/K, this file constructs

Delta = {a : Kˣ | there is beta : Lˣ with beta ^ n = a}

as a subgroup, chooses one root for each element only after the subgroup has been constructed, and proves the character isomorphism

Delta / (Delta intersect Kˣ^n) ~= Hom(Gal(L/K), mu_n).

There is no multiplicative choice of roots. Surjectivity is produced by Noether's Hilbert theorem 90. This is the finite actual-field character- isomorphism half of The finite Kummer character equivalence; it does not assert the full lattice correspondence between radical subgroups and abelian extensions.

Imports1

Nyll.GaloisCohomology.Kummer.Concrete.RadicalQuotient

Imported by3

def

finiteKummerRadicalSubgroup

L40 ↗

KummerTheory.finiteKummerRadicalSubgroup

Documentation

The radical subgroup A_L^n intersect Kˣ for the actual extension L/K: its elements are precisely the base-field units admitting an n-th root in Lˣ.

Source context 4 commands

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

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

Lean source · full declaration

def finiteKummerRadicalSubgroup (n : ℕ+) : Subgroup Kˣ where
  carrier := {a | ∃ β : Lˣ,
    β ^ (n : ℕ) = Units.map (algebraMap K L).toMonoidHom a}
  one_mem' := ⟨1, by simp⟩
  mul_mem' := by
    rintro a b ⟨α, hα⟩ ⟨β, hβ⟩
    refine ⟨α * β, ?_⟩
    rw [mul_pow, hα, hβ, map_mul]
  inv_mem' := by
    rintro a ⟨α, hα⟩
    refine ⟨α⁻¹, ?_⟩
    rw [inv_pow, hα, map_inv]

theorem

mem_finiteKummerRadicalSubgroup_iff

L55 ↗

KummerTheory.mem_finiteKummerRadicalSubgroup_iff

Documentation

The finite Kummer radical consists exactly of classes annihilated by every defining character.

Source context 4 commands

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

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

Lean source · statement

theorem mem_finiteKummerRadicalSubgroup_iff
    (n : ℕ+) {a : Kˣ} :
    a ∈ finiteKummerRadicalSubgroup (K := K) (L := L) n ↔
      ∃ β : Lˣ, β ^ (n : ℕ) = Units.map (algebraMap K L).toMonoidHom a

def

chosenFiniteKummerRadicalDatum

L63 ↗

KummerTheory.chosenFiniteKummerRadicalDatum

Documentation

An arbitrary root choice on the already constructed radical subgroup. No compatibility between the choices is imposed.

Source context 4 commands

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

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

Lean source · full declaration

def chosenFiniteKummerRadicalDatum (n : ℕ+) : RadicalDatum (K := K) (L := L) n where
  carrier := finiteKummerRadicalSubgroup (K := K) (L := L) n
  root a := Classical.choose a.property
  root_pow_eq a := Classical.choose_spec a.property

def

NthRootsOfUnityInBase

L71 ↗

KummerTheory.NthRootsOfUnityInBase

Documentation

The field-level form of the roots-of-unity hypothesis mu_n subset K, restricted to the roots of unity occurring in L: every n-th root of unity in Lˣ comes from a unit of K.

Source context 4 commands

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

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

Lean source · statement

def NthRootsOfUnityInBase (n : ℕ+) : Prop

theorem

nthRootsOfUnity_fixed

L76 ↗

KummerTheory.nthRootsOfUnity_fixed

Documentation

Under mu_n subset K, every Galois automorphism fixes mu_n(L).

Source context 4 commands

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

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

Lean source · statement

theorem nthRootsOfUnity_fixed
    (n : ℕ+) (hmu : NthRootsOfUnityInBase (K := K) (L := L) n)
    (sigma : Gal(L/K)) (u : Lˣ) (hu : u ^ (n : ℕ) = 1) :
    sigma • u = u

theorem

finiteKummerQuotientCharacter_surjective

L86 ↗

KummerTheory.finiteKummerQuotientCharacter_surjective

Documentation

The root-choice-free Kummer character on the ambient-power quotient is surjective. The preimage of a character is produced by Noether Hilbert 90, not supplied as a hypothesis.

Source context 4 commands

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

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

Lean source · statement

theorem finiteKummerQuotientCharacter_surjective
    [FiniteDimensional K L] [IsGalois K L]
    (n : ℕ+) (hmu : NthRootsOfUnityInBase (K := K) (L := L) n) :
    Function.Surjective
      ((chosenFiniteKummerRadicalDatum (K := K) (L := L) n).quotientKummerCharacterWithoutSection
          (nthRootsOfUnity_fixed (K := K) (L := L) n hmu))

def

finiteKummerCharacterEquiv

L149 ↗

KummerTheory.finiteKummerCharacterEquiv

Documentation

The finite actual-field Kummer character isomorphism on Delta / (Delta intersect Kˣ^n). This is the character-isomorphism half of the finite Kummer character equivalence, not the full subgroup/extension correspondence.

Source context 4 commands

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

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

Lean source · statement

def finiteKummerCharacterEquiv
    [FiniteDimensional K L] [IsGalois K L]
    (n : ℕ+) (hmu : NthRootsOfUnityInBase (K := K) (L := L) n) :
    (chosenFiniteKummerRadicalDatum (K := K) (L := L) n).RadicalQuotient ≃*
      (Gal(L/K) →* nthRootsSubgroup L (n : ℕ))

Module documentation

finite Kummer character isomorphism

Declarations

finiteKummerRadicalSubgroup

mem_finiteKummerRadicalSubgroup_iff

chosenFiniteKummerRadicalDatum

NthRootsOfUnityInBase

nthRootsOfUnity_fixed

finiteKummerQuotientCharacter_surjective

finiteKummerCharacterEquiv