Module

Correspondence.lean

Nyll.GaloisCohomology.Kummer.Concrete.Correspondence

11 declarations indexed from sourceView source ↗

Module documentation

Kummer subgroup-extension correspondence

For a fixed separable closure Omega/K, a positive integer n, and enough n-th roots of unity in K, admissible subgroups of Kˣ correspond to abelian Galois intermediate extensions whose Galois groups have exponent dividing n.

Imports2

Imported by2

structure

KummerExtension

L30 ↗

KummerTheory.KummerExtension

Documentation

An extension-side object in the Kummer correspondence.

The structure stores only an intermediate field, its Galois and abelian properties, and the exponent bound. Radical generation and both round-trip equalities are derived theorems.

Source context 3 commands

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

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

Lean source · full declaration

structure KummerExtension (K Omega : Type*) [Field K] [Field Omega]
    [Algebra K Omega] (n : ℕ+) where
  /-- The intermediate field of `Omega/K` represented by this extension-side object. -/
  toIntermediateField : IntermediateField K Omega
  /-- The represented intermediate field is Galois over `K`. -/
  toIsGalois : IsGalois K toIntermediateField
  /-- The Galois group of the represented intermediate field is commutative. -/
  toIsMulCommutative : IsMulCommutative Gal(toIntermediateField/K)
  /-- Every Galois automorphism has order dividing `n`. -/
  exponent : ∀ sigma : Gal(toIntermediateField/K), sigma ^ (n : ℕ) = 1

instance

(anonymous instance)

L46 ↗

Documentation

A Kummer extension supplies a Galois structure on its intermediate field.

Source context 5 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
namespace KummerExtension
variable {n : ℕ+}

Lean source · statement

instance (E : KummerExtension K Omega n) :
    IsGalois K E.toIntermediateField

instance

(anonymous instance)

L50 ↗

Documentation

The Galois group of a Kummer extension is commutative.

Source context 5 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
namespace KummerExtension
variable {n : ℕ+}

Lean source · statement

instance (E : KummerExtension K Omega n) :
    IsMulCommutative Gal(E.toIntermediateField/K)

theorem

ext

L56 ↗

KummerTheory.KummerExtension.ext

Documentation

Extension-side objects are equal when their intermediate fields are equal; the remaining fields are propositions.

Source context 5 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
namespace KummerExtension
variable {n : ℕ+}

Lean source · statement

theorem ext {E F : KummerExtension K Omega n}
    (h : E.toIntermediateField = F.toIntermediateField) : E = F

def

toKummerSubgroup

L64 ↗

KummerTheory.KummerExtension.toKummerSubgroup

Documentation

The base-field radical subgroup attached to an extension-side object.

Source context 5 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
namespace KummerExtension
variable {n : ℕ+}

Lean source · statement

def toKummerSubgroup (E : KummerExtension K Omega n) : KummerSubgroup K n

theorem

toKummerSubgroup_carrier

L76 ↗

KummerTheory.KummerExtension.toKummerSubgroup_carrier

Documentation

The subgroup recovered from a Kummer extension has the extension's defining radical as carrier.

Source context 5 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
namespace KummerExtension
variable {n : ℕ+}

Lean source · statement

theorem toKummerSubgroup_carrier (E : KummerExtension K Omega n) :
    (E.toKummerSubgroup).1 =
      finiteKummerRadicalSubgroup
        (K := K) (L := E.toIntermediateField) n

def

kummerExtensionOfSubgroup

L88 ↗

KummerTheory.kummerExtensionOfSubgroup

Documentation

Construct the radical extension attached to an admissible Kummer subgroup.

Source context 4 commands

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

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

Lean source · full declaration

def kummerExtensionOfSubgroup
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n) : KummerExtension K Omega n where
  toIntermediateField :=
    kummerRadicalExtension (K := K) (Omega := Omega) n Delta.1
  toIsGalois := kummerRadicalExtension_isGalois n Delta.1
  toIsMulCommutative :=
    kummerRadicalExtension_isMulCommutative n hmu Delta.1
  exponent := kummerRadicalExtension_galois_pow_eq_one n hmu Delta.1

theorem

kummerExtensionOfSubgroup_toIntermediateField

L100 ↗

KummerTheory.kummerExtensionOfSubgroup_toIntermediateField

Documentation

The extension built from a Kummer subgroup has the expected intermediate field.

Source context 4 commands

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

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

Lean source · statement

theorem kummerExtensionOfSubgroup_toIntermediateField
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n) :
    (kummerExtensionOfSubgroup
      (K := K) (Omega := Omega) n hmu Delta).toIntermediateField =
      kummerRadicalExtension (K := K) (Omega := Omega) n Delta.1

def

kummerSubgroupEquivKummerExtension

L110 ↗

KummerTheory.kummerSubgroupEquivKummerExtension

Documentation

Admissible Kummer subgroups are equivalent to abelian Galois intermediate extensions whose Galois groups have exponent dividing n.

Source context 4 commands

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

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

Lean source · full declaration

def kummerSubgroupEquivKummerExtension
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    KummerSubgroup K n ≃ KummerExtension K Omega n where
  toFun := kummerExtensionOfSubgroup n hmu
  invFun := KummerExtension.toKummerSubgroup
  left_inv Delta := by
    apply Subtype.ext
    exact finiteKummerRadicalSubgroup_kummerRadicalExtension_eq
      (K := K) (Omega := Omega) n hn hmu Delta
  right_inv E := by
    apply KummerExtension.ext
    exact kummerRadicalExtension_finiteKummerRadicalSubgroup_eq
      E.toIntermediateField n hmu E.exponent

theorem

kummerSubgroupEquivKummerExtension_apply_toIntermediateField

L127 ↗

KummerTheory.kummerSubgroupEquivKummerExtension_apply_toIntermediateField

Documentation

The Kummer correspondence sends a subgroup to the intermediate field it generates.

Source context 4 commands

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

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

Lean source · statement

theorem kummerSubgroupEquivKummerExtension_apply_toIntermediateField
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n) :
    ((kummerSubgroupEquivKummerExtension
      (K := K) (Omega := Omega) n hn hmu) Delta).toIntermediateField =
      kummerRadicalExtension (K := K) (Omega := Omega) n Delta.1

theorem

kummerSubgroupEquivKummerExtension_symm_apply_carrier

L138 ↗

KummerTheory.kummerSubgroupEquivKummerExtension_symm_apply_carrier

Documentation

The inverse Kummer correspondence recovers the radical subgroup carrier.

Source context 4 commands

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

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

Lean source · statement

theorem kummerSubgroupEquivKummerExtension_symm_apply_carrier
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (E : KummerExtension K Omega n) :
    ((kummerSubgroupEquivKummerExtension
      (K := K) (Omega := Omega) n hn hmu).symm E).1 =
      finiteKummerRadicalSubgroup
        (K := K) (L := E.toIntermediateField) n

Module documentation

Kummer subgroup-extension correspondence

Declarations