Module

FiniteUnramifiedField.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.FiniteUnramifiedField

11 declarations indexed from sourceView source ↗

Module documentation

The standard finite unramified local extension

The abstract local class formation already constructs, for every positive d, a canonical finite unramified abelian subextension of the local absolute Galois group. This file takes its actual fixed field in the chosen separable closure and equips that field with the existing spectral local-field structure.

No second Frobenius is introduced. The canonical lift on this field is the existing arithmeticFrobeniusOfUnramifiedValuation.

Imports5

Imported by7

abbrev

localFiniteUnramifiedField

L34 ↗

LocalClassFieldTheory.localFiniteUnramifiedField

Documentation

The actual fixed field of the canonical degree-d unramified factor.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory

Lean source · statement

abbrev localFiniteUnramifiedField
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) :
    IntermediateField K (SeparableClosure K)

instance

localFiniteUnramifiedField_finiteDimensional

L43 ↗

LocalClassFieldTheory.localFiniteUnramifiedField_finiteDimensional

Documentation

The standard unramified fixed field is finite over its base.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory

Lean source · statement

instance localFiniteUnramifiedField_finiteDimensional
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) :
    FiniteDimensional K (localFiniteUnramifiedField K d hd)

instance

localFiniteUnramifiedField_isAbelianGalois

L54 ↗

LocalClassFieldTheory.localFiniteUnramifiedField_isAbelianGalois

Documentation

The standard unramified fixed field is abelian Galois over its base.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory

Lean source · statement

instance localFiniteUnramifiedField_isAbelianGalois
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) :
    IsAbelianGalois K (localFiniteUnramifiedField K d hd)

instance

localFiniteUnramifiedField_nontriviallyNormedField

L63 ↗

LocalClassFieldTheory.localFiniteUnramifiedField_nontriviallyNormedField

Documentation

The canonical spectral norm on the standard unramified fixed field.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory

Lean source · statement

instance localFiniteUnramifiedField_nontriviallyNormedField
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) :
    NontriviallyNormedField (localFiniteUnramifiedField K d hd)

instance

localFiniteUnramifiedField_valuativeRel

L72 ↗

LocalClassFieldTheory.localFiniteUnramifiedField_valuativeRel

Documentation

The valuation relation induced by the canonical spectral norm.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory

Lean source · statement

instance localFiniteUnramifiedField_valuativeRel
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) :
    ValuativeRel (localFiniteUnramifiedField K d hd)

instance

localFiniteUnramifiedField_isNonarchimedeanLocalField

L81 ↗

LocalClassFieldTheory.localFiniteUnramifiedField_isNonarchimedeanLocalField

Documentation

A standard finite unramified fixed field is again a local field.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory

Lean source · statement

instance localFiniteUnramifiedField_isNonarchimedeanLocalField
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) :
    IsNonarchimedeanLocalField (localFiniteUnramifiedField K d hd)

instance

localFiniteUnramifiedField_valuationHasExtension

L90 ↗

LocalClassFieldTheory.localFiniteUnramifiedField_valuationHasExtension

Documentation

The spectral valuation is the extension of the valuation on K.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory

Lean source · statement

instance localFiniteUnramifiedField_valuationHasExtension
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) :
    Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation (localFiniteUnramifiedField K d hd))

theorem

localFiniteUnramifiedField_finrank

L101 ↗

LocalClassFieldTheory.localFiniteUnramifiedField_finrank

Documentation

The fixed field has the degree prescribed by the abstract unramified factor.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory

Lean source · statement

theorem localFiniteUnramifiedField_finrank
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) :
    Module.finrank K (localFiniteUnramifiedField K d hd) = d

theorem

localFiniteUnramifiedField_residue_finrank

L143 ↗

LocalClassFieldTheory.localFiniteUnramifiedField_residue_finrank

Documentation

The literal residue extension of the standard fixed field also has degree d.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory

Lean source · statement

theorem localFiniteUnramifiedField_residue_finrank
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) :
    @Module.finrank 𝓀[K]
      𝓀[localFiniteUnramifiedField K d hd] _ _
        (IsLocalRing.ResidueField.instModule
          (R := 𝒪[K])
          (S := 𝒪[localFiniteUnramifiedField K d hd])) = d

instance

localFiniteUnramifiedField_isUnramifiedValuedExtension

L191 ↗

LocalClassFieldTheory.localFiniteUnramifiedField_isUnramifiedValuedExtension

Documentation

The standard fixed field is unramified for the actual local valuations.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory

Lean source · full declaration

instance localFiniteUnramifiedField_isUnramifiedValuedExtension
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) :
    IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K
      (localFiniteUnramifiedField K d hd) where
  maximalIdeal_ramificationIdx_eq_one := by
    have hfund :=
      maximalIdeal_ramificationIdx_mul_residue_finrank_eq_finrank K
        (localFiniteUnramifiedField K d hd)
    have hmax : (𝓂[K] : Ideal 𝒪[K]) ≠ ⊥ :=
      Ring.ne_bot_of_isMaximal_of_not_isField
        (IsLocalRing.maximalIdeal.isMaximal 𝒪[K])
        (IsDiscreteValuationRing.not_isField 𝒪[K])
    rw [Ideal.ramificationIdx'_eq_ramificationIdx _ _ hmax,
      localFiniteUnramifiedField_residue_finrank K d hd,
      localFiniteUnramifiedField_finrank K d hd] at hfund
    apply Nat.eq_of_mul_eq_mul_right hd
    simpa only [one_mul] using hfund

theorem

localFiniteUnramifiedField_arithmeticFrobenius_order

L213 ↗

LocalClassFieldTheory.localFiniteUnramifiedField_arithmeticFrobenius_order

Documentation

On the standard degree-d fixed field, the existing arithmetic Frobenius has order exactly d.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory

Lean source · statement

theorem localFiniteUnramifiedField_arithmeticFrobenius_order
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) :
    orderOf
        (arithmeticFrobeniusOfUnramifiedValuation K
          (localFiniteUnramifiedField K d hd)) =
      d

Module documentation

The standard finite unramified local extension

Declarations