Module

CompletedChangedStandardCompositum.lean

Nyll.ClassFieldTheory.LubinTate.Padic.CompletedChangedStandardCompositum

24 declarations indexed from sourceView source ↗

Module documentation

The finite standard/changed compositum in the completed p-adic level

The completed level contains two finite abelian extensions of ℚ_[p]:

the image of the ordinary standard multiplicative Lubin--Tate level;
the fixed field of the inverse-unit completed Frobenius lift, identified

with the changed-uniformizer level.

Their compositum is therefore a genuine finite abelian extension. The inverse of the Frobenius lift preserves this compositum, fixes the changed factor, and acts on the standard factor by the direct unit parameter. This is the finite automorphism which the changed-uniformizer norm calculation will identify with the actual local Artin symbol.

Imports3

Imported by2

def

padicCompletedStandardLevelField

L38 ↗

LubinTate.padicCompletedStandardLevelField

Documentation

The copy of the ordinary standard multiplicative level inside the completed level.

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 padicCompletedStandardLevelField
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    IntermediateField ℚ_[p] (padicCompletedLevelField p n)

def

padicStandardLevelEquivCompletedStandardLevelField

L45 ↗

LubinTate.padicStandardLevelEquivCompletedStandardLevelField

Documentation

The ordinary standard level is equivalent to its image in the completed level.

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 padicStandardLevelEquivCompletedStandardLevelField
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    standardLubinTateLevelField
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ≃ₐ[ℚ_[p]]
        padicCompletedStandardLevelField p n

instance

padicCompletedStandardLevelField_finiteDimensional

L53 ↗

LubinTate.padicCompletedStandardLevelField_finiteDimensional

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

instance
    padicCompletedStandardLevelField_finiteDimensional
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    FiniteDimensional ℚ_[p]
      (padicCompletedStandardLevelField p n)

instance

padicCompletedStandardLevelField_isAbelianGalois

L65 ↗

LubinTate.padicCompletedStandardLevelField_isAbelianGalois

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

instance
    padicCompletedStandardLevelField_isAbelianGalois
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    IsAbelianGalois ℚ_[p]
      (padicCompletedStandardLevelField p n)

instance

padicCompletedChangedUniformizerFixedField_finiteDimensional

L77 ↗

LubinTate.padicCompletedChangedUniformizerFixedField_finiteDimensional

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

instance
    padicCompletedChangedUniformizerFixedField_finiteDimensional
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    FiniteDimensional ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n)

instance

padicCompletedChangedUniformizerFixedField_isAbelianGalois

L92 ↗

LubinTate.padicCompletedChangedUniformizerFixedField_isAbelianGalois

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

instance
    padicCompletedChangedUniformizerFixedField_isAbelianGalois
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    IsAbelianGalois ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n)

def

padicCompletedStandardChangedCompositum

L103 ↗

LubinTate.padicCompletedStandardChangedCompositum

Documentation

The finite compositum of the standard level and the actual changed-uniformizer fixed field inside the completed level.

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 padicCompletedStandardChangedCompositum
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    IntermediateField ℚ_[p] (padicCompletedLevelField p n)

instance

padicCompletedStandardChangedCompositum_finiteDimensional

L110 ↗

LubinTate.padicCompletedStandardChangedCompositum_finiteDimensional

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

instance
    padicCompletedStandardChangedCompositum_finiteDimensional
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    FiniteDimensional ℚ_[p]
      (padicCompletedStandardChangedCompositum p u n)

instance

padicCompletedStandardChangedCompositum_isAbelianGalois

L120 ↗

LubinTate.padicCompletedStandardChangedCompositum_isAbelianGalois

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

instance
    padicCompletedStandardChangedCompositum_isAbelianGalois
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    IsAbelianGalois ℚ_[p]
      (padicCompletedStandardChangedCompositum p u n)

instance

padicCompletedStandardChangedCompositum_changedFieldAlgebra

L130 ↗

LubinTate.padicCompletedStandardChangedCompositum_changedFieldAlgebra

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

instance
    padicCompletedStandardChangedCompositum_changedFieldAlgebra
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Algebra (padicCompletedChangedUniformizerFixedField p u n)
      (padicCompletedStandardChangedCompositum p u n)

instance

padicCompletedStandardChangedCompositum_changedFieldScalarTower

L138 ↗

LubinTate.padicCompletedStandardChangedCompositum_changedFieldScalarTower

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

instance padicCompletedStandardChangedCompositum_changedFieldScalarTower
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    IsScalarTower ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n)
      (padicCompletedStandardChangedCompositum p u n)

instance

padicCompletedStandardChangedCompositum_relative_isAbelianGalois

L149 ↗

LubinTate.padicCompletedStandardChangedCompositum_relative_isAbelianGalois

Documentation

The standard/changed compositum is also abelian Galois over its changed-uniformizer factor. Relative automorphisms embed faithfully into the already commutative Galois group over ℚ_p.

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

instance
    padicCompletedStandardChangedCompositum_relative_isAbelianGalois
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    IsAbelianGalois
      (padicCompletedChangedUniformizerFixedField p u n)
      (padicCompletedStandardChangedCompositum p u n)

def

padicStandardLevelToCompletedChangedCompositum

L162 ↗

LubinTate.padicStandardLevelToCompletedChangedCompositum

Documentation

The standard finite level embedded into 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 padicStandardLevelToCompletedChangedCompositum
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    standardLubinTateLevelField
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      →ₐ[ℚ_[p]]
        padicCompletedStandardChangedCompositum p u n

def

padicCompletedChangedFixedFieldToStandardChangedCompositum

L180 ↗

LubinTate.padicCompletedChangedFixedFieldToStandardChangedCompositum

Documentation

The changed fixed field included into 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
    padicCompletedChangedFixedFieldToStandardChangedCompositum
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    padicCompletedChangedUniformizerFixedField p u n
      →ₐ[ℚ_[p]]
        padicCompletedStandardChangedCompositum p u n

theorem

padicCompletedChangedUniformizerFrobenius_symm_map_standard_le

L191 ↗

LubinTate.padicCompletedChangedUniformizerFrobenius_symm_map_standard_le

Documentation

The inverse-unit Frobenius inverse carries the standard completed copy to itself.

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
    padicCompletedChangedUniformizerFrobenius_symm_map_standard_le
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    (padicCompletedStandardLevelField p n).map
        (padicCompletedChangedUniformizerFrobeniusAlgEquiv
          p u n).symm.toAlgHom ≤
      padicCompletedStandardLevelField p n

theorem

padicCompletedChangedUniformizerFrobenius_symm_fixed

L222 ↗

LubinTate.padicCompletedChangedUniformizerFrobenius_symm_fixed

Documentation

Every element of the changed fixed field is fixed by the inverse of its defining Frobenius lift.

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
    padicCompletedChangedUniformizerFrobenius_symm_fixed
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ)
    (x : padicCompletedChangedUniformizerFixedField p u n) :
    (padicCompletedChangedUniformizerFrobeniusAlgEquiv p u n).symm
      (x : padicCompletedLevelField p n) =
        x

theorem

padicCompletedChangedUniformizerFrobenius_symm_map_fixedField_le

L256 ↗

LubinTate.padicCompletedChangedUniformizerFrobenius_symm_map_fixedField_le

Documentation

The inverse defining Frobenius carries the changed fixed field to itself.

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
    padicCompletedChangedUniformizerFrobenius_symm_map_fixedField_le
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    (padicCompletedChangedUniformizerFixedField p u n).map
        (padicCompletedChangedUniformizerFrobeniusAlgEquiv
          p u n).symm.toAlgHom ≤
      padicCompletedChangedUniformizerFixedField p u n

theorem

padicCompletedChangedUniformizerFrobenius_symm_map_compositum_le

L277 ↗

LubinTate.padicCompletedChangedUniformizerFrobenius_symm_map_compositum_le

Documentation

The inverse defining Frobenius preserves 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

theorem
    padicCompletedChangedUniformizerFrobenius_symm_map_compositum_le
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    (padicCompletedStandardChangedCompositum p u n).map
        (padicCompletedChangedUniformizerFrobeniusAlgEquiv
          p u n).symm.toAlgHom ≤
      padicCompletedStandardChangedCompositum p u n

def

padicCompletedChangedUniformizerArtinCandidateAlgHom

L295 ↗

LubinTate.padicCompletedChangedUniformizerArtinCandidateAlgHom

Documentation

The inverse defining Frobenius restricted to the genuine 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 padicCompletedChangedUniformizerArtinCandidateAlgHom
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    padicCompletedStandardChangedCompositum p u n
      →ₐ[ℚ_[p]]
        padicCompletedStandardChangedCompositum p u n

def

padicCompletedChangedUniformizerArtinCandidate

L312 ↗

LubinTate.padicCompletedChangedUniformizerArtinCandidate

Documentation

The finite Artin candidate is an automorphism.

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 padicCompletedChangedUniformizerArtinCandidate
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    padicCompletedStandardChangedCompositum p u n
      ≃ₐ[ℚ_[p]]
        padicCompletedStandardChangedCompositum p u n

theorem

padicCompletedChangedUniformizerArtinCandidate_standardLevel

L329 ↗

LubinTate.padicCompletedChangedUniformizerArtinCandidate_standardLevel

Documentation

On the standard factor, the finite Artin candidate is the direct unit-parameter automorphism.

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_standardLevel
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ)
    (x :
      standardLubinTateLevelField
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n) :
    padicCompletedChangedUniformizerArtinCandidate p u n
        (padicStandardLevelToCompletedChangedCompositum p u n x) =
      padicStandardLevelToCompletedChangedCompositum p u n
        (standardLubinTateUnitParameterAlgEquiv
          (padicLocalField p)
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n
          (standardLubinTateUnitParameterClass
            (padicLocalField p) n u) x)

theorem

padicCompletedChangedUniformizerArtinCandidate_fixedField

L351 ↗

LubinTate.padicCompletedChangedUniformizerArtinCandidate_fixedField

Documentation

On the changed factor, the finite Artin candidate is the identity.

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
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ)
    (x : padicCompletedChangedUniformizerFixedField p u n) :
    padicCompletedChangedUniformizerArtinCandidate p u n
        (padicCompletedChangedFixedFieldToStandardChangedCompositum
          p u n x) =
      padicCompletedChangedFixedFieldToStandardChangedCompositum
        p u n x

def

padicCompletedChangedUniformizerRelativeArtinCandidate

L367 ↗

LubinTate.padicCompletedChangedUniformizerRelativeArtinCandidate

Documentation

The finite Artin candidate as an automorphism over the changed fixed field that it fixes pointwise.

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 · full declaration

def
    padicCompletedChangedUniformizerRelativeArtinCandidate
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    padicCompletedStandardChangedCompositum p u n
      ≃ₐ[padicCompletedChangedUniformizerFixedField p u n]
        padicCompletedStandardChangedCompositum p u n where
  __ := (padicCompletedChangedUniformizerArtinCandidate p u n).toRingEquiv
  commutes' x :=
    padicCompletedChangedUniformizerArtinCandidate_fixedField
      p u n x

theorem

padicCompletedChangedUniformizerRelativeArtinCandidate_apply

L382 ↗

LubinTate.padicCompletedChangedUniformizerRelativeArtinCandidate_apply

Documentation

Forgetting the changed-field scalar structure recovers the original finite 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 padicCompletedChangedUniformizerRelativeArtinCandidate_apply
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ)
    (x : padicCompletedStandardChangedCompositum p u n) :
    padicCompletedChangedUniformizerRelativeArtinCandidate p u n x =
      padicCompletedChangedUniformizerArtinCandidate p u n x

Module documentation

The finite standard/changed compositum in the completed p-adic level

Declarations