Module

CompletedChangedStandardFixedField.lean

Nyll.ClassFieldTheory.LubinTate.Padic.CompletedChangedStandardFixedField

4 declarations indexed from sourceView source ↗

Module documentation

Fixed field of the finite changed-uniformizer Artin candidate

Inside the finite standard/changed compositum, the cyclic subgroup generated by the inverse completed Frobenius has fixed field exactly the changed Lubin--Tate factor. Thus the automorphisms over the changed factor are precisely the powers of the finite Artin candidate.

Imports1

Nyll.ClassFieldTheory.LubinTate.Padic.CompletedChangedStandardCompositum

Imported by2

def

padicCompletedChangedFieldInStandardChangedCompositum

L29 ↗

LubinTate.padicCompletedChangedFieldInStandardChangedCompositum

Documentation

The changed fixed field, now regarded as an intermediate field of the finite standard/changed compositum.

Source context 4 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp

Lean source · statement

def padicCompletedChangedFieldInStandardChangedCompositum
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    IntermediateField ℚ_[p]
      (padicCompletedStandardChangedCompositum p u n)

theorem

padicCompletedChangedUniformizerArtinCandidate_fixedField_eq_changed

L42 ↗

LubinTate.padicCompletedChangedUniformizerArtinCandidate_fixedField_eq_changed

Documentation

The fixed field of the cyclic finite Artin candidate is the actual changed-uniformizer factor.

Source context 4 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp

Lean source · statement

theorem
    padicCompletedChangedUniformizerArtinCandidate_fixedField_eq_changed
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    IntermediateField.fixedField
        (Subgroup.zpowers
          (padicCompletedChangedUniformizerArtinCandidate p u n)) =
      padicCompletedChangedFieldInStandardChangedCompositum p u n

theorem

padicCompletedChangedUniformizerArtinCandidate_zpowers_eq_fixingSubgroup

L111 ↗

LubinTate.padicCompletedChangedUniformizerArtinCandidate_zpowers_eq_fixingSubgroup

Documentation

The relative Galois group of the finite standard/changed compositum over the changed factor is cyclic and generated by the finite Artin candidate.

Source context 4 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp

Lean source · statement

theorem
    padicCompletedChangedUniformizerArtinCandidate_zpowers_eq_fixingSubgroup
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Subgroup.zpowers
        (padicCompletedChangedUniformizerArtinCandidate p u n) =
      (padicCompletedChangedFieldInStandardChangedCompositum
        p u n).fixingSubgroup

theorem

padicCompletedChangedUniformizerRelativeArtinCandidate_zpowers_eq_top

L135 ↗

LubinTate.padicCompletedChangedUniformizerRelativeArtinCandidate_zpowers_eq_top

Documentation

Over the changed field itself, the relative finite Artin candidate generates the full relative Galois group.

Source context 4 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp

Lean source · statement

theorem
    padicCompletedChangedUniformizerRelativeArtinCandidate_zpowers_eq_top
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Subgroup.zpowers
        (padicCompletedChangedUniformizerRelativeArtinCandidate p u n) =
      ⊤

Module documentation

Fixed field of the finite changed-uniformizer Artin candidate

Declarations

padicCompletedChangedFieldInStandardChangedCompositum

padicCompletedChangedUniformizerArtinCandidate_fixedField_eq_changed

padicCompletedChangedUniformizerArtinCandidate_zpowers_eq_fixingSubgroup

padicCompletedChangedUniformizerRelativeArtinCandidate_zpowers_eq_top