Module

ExtensionRoundTrip.lean

Nyll.GaloisCohomology.Kummer.Concrete.ExtensionRoundTrip

4 declarations indexed from sourceView source ↗

Module documentation

extension-side round trip

For an abelian Galois intermediate extension E/K of exponent dividing n, adjoining in the ambient algebraic closure all n-th roots belonging to the actual radical subgroup of E recovers E itself.

Imports2

Imported by3

theorem

kummerRootSet_finiteKummerRadicalSubgroup_le

L29 ↗

KummerTheory.kummerRootSet_finiteKummerRadicalSubgroup_le

Documentation

Every ambient root belonging to the actual radical subgroup of E already lies in E. Its ratio with a root chosen in E is an n-th root of unity, hence belongs to K.

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 · statement

theorem kummerRootSet_finiteKummerRadicalSubgroup_le
    (E : IntermediateField K Omega) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    kummerRootSet (K := K) (Omega := Omega) n
        (finiteKummerRadicalSubgroup (K := K) (L := E) n) ⊆ E

theorem

kummerRadicalExtension_finiteKummerRadicalSubgroup_le

L68 ↗

KummerTheory.kummerRadicalExtension_finiteKummerRadicalSubgroup_le

Documentation

The radical extension constructed from the actual radical subgroup of E is contained in E.

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 · statement

theorem kummerRadicalExtension_finiteKummerRadicalSubgroup_le
    (E : IntermediateField K Omega) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    kummerRadicalExtension (K := K) (Omega := Omega) n
        (finiteKummerRadicalSubgroup (K := K) (L := E) n) ≤ E

theorem

le_kummerRadicalExtension_finiteKummerRadicalSubgroup

L78 ↗

KummerTheory.le_kummerRadicalExtension_finiteKummerRadicalSubgroup

Documentation

The internal generation theorem for E/K, transported through E.val, gives the reverse inclusion into the ambient radical extension.

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 · statement

theorem le_kummerRadicalExtension_finiteKummerRadicalSubgroup
    (E : IntermediateField K Omega)
    [IsGalois K E] [IsMulCommutative Gal(E/K)]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1) :
    E ≤ kummerRadicalExtension (K := K) (Omega := Omega) n
      (finiteKummerRadicalSubgroup (K := K) (L := E) n)

theorem

kummerRadicalExtension_finiteKummerRadicalSubgroup_eq

L119 ↗

KummerTheory.kummerRadicalExtension_finiteKummerRadicalSubgroup_eq

Documentation

the Kummer correspondence, extension-side round trip. For an abelian Galois intermediate extension of exponent dividing n, taking its actual radical subgroup and adjoining all corresponding roots in the ambient closure recovers the original intermediate field.

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 · statement

theorem kummerRadicalExtension_finiteKummerRadicalSubgroup_eq
    (E : IntermediateField K Omega)
    [IsGalois K E] [IsMulCommutative Gal(E/K)]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1) :
    kummerRadicalExtension (K := K) (Omega := Omega) n
        (finiteKummerRadicalSubgroup (K := K) (L := E) n) = E

Module documentation

extension-side round trip

Declarations

kummerRootSet_finiteKummerRadicalSubgroup_le

kummerRadicalExtension_finiteKummerRadicalSubgroup_le

le_kummerRadicalExtension_finiteKummerRadicalSubgroup

kummerRadicalExtension_finiteKummerRadicalSubgroup_eq