Module

LocalMaximalKummerExtension.lean

Nyll.GaloisCohomology.Kummer.Concrete.LocalMaximalKummerExtension

2 declarations indexed from sourceView source ↗

Module documentation

Maximal finite Kummer extensions of local fields

For a positive integer n that is nonzero in a nonarchimedean local field, the Kummer extension obtained by adjoining all n-th roots is finite.

Imports3

Imported by3

theorem

finite_maximalRestrictedRadicalQuotient

L31 ↗

KummerTheory.finite_maximalRestrictedRadicalQuotient

Documentation

The maximal restricted radical quotient is finite when the exponent is nonzero in the local field.

Source context 4 commands

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

noncomputable section
universe v
namespace KummerTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem finite_maximalRestrictedRadicalQuotient
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0) :
    Finite (RestrictedRadicalQuotient n (maximalKummerSubgroup K n))

theorem

maximalKummerRadicalExtension_finiteDimensional

L44 ↗

KummerTheory.maximalKummerRadicalExtension_finiteDimensional