NYLL
Module

FiniteAbelianFamilyUnramifiedCompositum.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FiniteAbelianFamilyUnramifiedCompositum
2 declarations indexed from sourceView source ↗

Module documentation

An unramified factor large enough for finite Artin rigidity

For a finite abelian local extension E, adjoining the unramified extension of degree divisible by |Gal(E/K)| produces a Galois group annihilated by that degree. Restriction to the unramified factor sends the normalized Artin value of a valuation-one unit to a generator. These are the two field-level inputs to cyclic-quotient rigidity.

Imports6
Imported by2

Declarations

theorem

finiteAbelianUnramifiedCompositum_pow_eq_one

L33 ↗
LocalClassFieldTheory.finiteAbelianUnramifiedCompositum_pow_eq_one
Documentation

The Galois group of the compositum is annihilated by the unramified degree when that degree is divisible by the size of the first Galois group.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open RamificationTheory LocalFieldTheory
open scoped ValuativeRel
Lean source · statement
theorem finiteAbelianUnramifiedCompositum_pow_eq_one
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (E : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K E] [IsAbelianGalois K E]
    (d : ℕ) (hd : 0 < d)
    (hcard : Nat.card (E ≃ₐ[K] E) ∣ d) :
    ∀ σ : Gal(↑(E ⊔ localFiniteUnramifiedField K d hd) / K),
      σ ^ d = 1
theorem

finiteAbelianArtin_unramifiedRestriction_zpowers_eq_top

L67 ↗
LocalClassFieldTheory.finiteAbelianArtin_unramifiedRestriction_zpowers_eq_top
Documentation

Restriction of the canonical local Artin value of a valuation-one unit generates the Galois group of the standard unramified extension.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open RamificationTheory LocalFieldTheory
open scoped ValuativeRel
Lean source · statement
theorem finiteAbelianArtin_unramifiedRestriction_zpowers_eq_top
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d)
    (F : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K F] [IsAbelianGalois K F]
    (hUF : localFiniteUnramifiedField K d hd ≤ F)
    (u : Kˣ)
    (hu : LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K
      (Additive.ofMul u) = 1) :
    Subgroup.zpowers
      (intermediateFieldRestrictNormalHom
        (localFiniteUnramifiedField K d hd) F hUF
        (abelianLocalArtinMap K F u)) = ⊤

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.