Module

InfiniteGeneration.lean

Nyll.GaloisCohomology.Kummer.Concrete.InfiniteGeneration

1 declaration indexed from sourceView source ↗

Module documentation

infinite actual-field form

For an arbitrary Galois extension Ω/K, each element of Ω lies in a finite Galois intermediate field. If the full Galois group is abelian and killed by n, restriction gives the same two properties at that finite stage. The finite actual-field case of the Kummer generation theorem then shows that the element belongs to the field generated by the global n-th radicals.

This is the actual-field n-th-power case. It does not claim the general abstract-operator statement of the Kummer generation theorem.

Imports1

Nyll.GaloisCohomology.Kummer.Concrete.FiniteGeneration

Imported by2

theorem

kummerRootSet_adjoin_eq_top

L37 ↗

KummerTheory.kummerRootSet_adjoin_eq_top

Documentation

The Kummer generation theorem for a possibly infinite actual-field Galois extension and the n-th-power operator.

The finite-stage abelian and exponent hypotheses are derived through the surjective restriction map; they are not supplied as extra assumptions.

Source context 4 commands

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

noncomputable section
namespace KummerTheory
open scoped IsMulCommutative
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem kummerRootSet_adjoin_eq_top
    [IsGalois K Ω] [IsMulCommutative Gal(Ω/K)]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ σ : Gal(Ω/K), σ ^ (n : ℕ) = 1) :
    IntermediateField.adjoin K (finiteKummerRootSet (K := K) (L := Ω) n) = ⊤

Module documentation

infinite actual-field form

Declarations

kummerRootSet_adjoin_eq_top