Module

CompletedResidueFrobenius.lean

Nyll.ClassFieldTheory.LubinTate.Padic.CompletedResidueFrobenius

8 declarations indexed from sourceView source ↗

Module documentation

Residue Frobenius on completed p-adic Lubin--Tate levels

The completed multiplicative Lubin--Tate level is totally ramified over its completed-unramified coefficient field. Hence the canonical residue map is an isomorphism. Under this identification, every unit-indexed completed Frobenius lift induces the arithmetic Frobenius x ↦ x ^ p on the residue field.

Imports2

Imported by2

theorem

padicCompletedLevel_residueDegree_eq_one

L34 ↗

LubinTate.padicCompletedLevel_residueDegree_eq_one

Documentation

The completed multiplicative level has residue degree one over the completed-unramified coefficient field.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
open ValuationTheory.DiscreteValuationField.ValuedExtension

Lean source · statement

theorem padicCompletedLevel_residueDegree_eq_one
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    residueDegree
        (padicCompletedUnramifiedCompleteDVF p).toDVF
        (padicCompletedLevelCompleteDVF p n).toDVF = 1

theorem

padicCompletedLevel_residueField_finrank_eq_one

L54 ↗

LubinTate.padicCompletedLevel_residueField_finrank_eq_one

Documentation

The target residue field has linear rank one over the completed-unramified residue field.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
open ValuationTheory.DiscreteValuationField.ValuedExtension

Lean source · statement

theorem padicCompletedLevel_residueField_finrank_eq_one
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Module.finrank
        (padicCompletedUnramifiedCompleteDVF p).residueField
        (padicCompletedLevelCompleteDVF p n).residueField = 1

theorem

padicCompletedLevel_residueMap_surjective

L83 ↗

LubinTate.padicCompletedLevel_residueMap_surjective

Documentation

The canonical residue map from the completed-unramified coefficient field onto the completed level is surjective.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
open ValuationTheory.DiscreteValuationField.ValuedExtension

Lean source · statement

theorem padicCompletedLevel_residueMap_surjective
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Function.Surjective
      (residueMap
        (padicCompletedUnramifiedCompleteDVF p).toDVF
        (padicCompletedLevelCompleteDVF p n).toDVF)

def

padicCompletedLevelResidueFieldEquiv

L102 ↗

LubinTate.padicCompletedLevelResidueFieldEquiv

Documentation

The canonical residue-field equivalence from the completed-unramified coefficient field to a completed multiplicative level.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
open ValuationTheory.DiscreteValuationField.ValuedExtension

Lean source · statement

def padicCompletedLevelResidueFieldEquiv
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicCompletedUnramifiedCompleteDVF p).residueField ≃+*
      (padicCompletedLevelCompleteDVF p n).residueField

theorem

padicCompletedLevelResidueFieldEquiv_apply

L114 ↗

LubinTate.padicCompletedLevelResidueFieldEquiv_apply

Documentation

The completed-level residue equivalence evaluates by the canonical residue map.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
open ValuationTheory.DiscreteValuationField.ValuedExtension

Lean source · statement

theorem padicCompletedLevelResidueFieldEquiv_apply
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedUnramifiedCompleteDVF p).residueField) :
    padicCompletedLevelResidueFieldEquiv p n x =
      residueMap
        (padicCompletedUnramifiedCompleteDVF p).toDVF
        (padicCompletedLevelCompleteDVF p n).toDVF x

theorem

padicCompletedLevelResidueFieldEquiv_apply_residue

L126 ↗

LubinTate.padicCompletedLevelResidueFieldEquiv_apply_residue

Documentation

On integral representatives, the completed-level residue equivalence is the residue of the canonical valuation-ring inclusion.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
open ValuationTheory.DiscreteValuationField.ValuedExtension

Lean source · statement

theorem padicCompletedLevelResidueFieldEquiv_apply_residue
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : (padicCompletedUnramifiedCompleteDVF p).valuationSubring) :
    padicCompletedLevelResidueFieldEquiv p n
        ((padicCompletedUnramifiedCompleteDVF p).residueMap a) =
      (padicCompletedLevelCompleteDVF p n).residueMap
        (integerMap
          (padicCompletedUnramifiedCompleteDVF p).toDVF
          (padicCompletedLevelCompleteDVF p n).toDVF a)

theorem

padicCompletedUnramifiedWitt_residue_frobenius_eq_pow

L141 ↗

LubinTate.padicCompletedUnramifiedWitt_residue_frobenius_eq_pow

Source context 7 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
open ValuationTheory.DiscreteValuationField.ValuedExtension

Lean source · statement

theorem
    padicCompletedUnramifiedWitt_residue_frobenius_eq_pow
    (p : ℕ) [Fact p.Prime]
    (a : padicCompletedUnramifiedWittRing p) :
    IsLocalRing.residue (padicCompletedUnramifiedWittRing p)
        (WittVector.frobenius a) =
      IsLocalRing.residue (padicCompletedUnramifiedWittRing p) a ^ p

theorem

padicCompletedUnitFrobeniusIntegerEquiv_residue_apply_eq_pow

L168 ↗

LubinTate.padicCompletedUnitFrobeniusIntegerEquiv_residue_apply_eq_pow

Documentation

The actual residue action induced by every unit-indexed completed Frobenius lift is the arithmetic Frobenius x ↦ x ^ p.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
open ValuationTheory.DiscreteValuationField.ValuedExtension

Lean source · statement

theorem
    padicCompletedUnitFrobeniusIntegerEquiv_residue_apply_eq_pow
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicLocalField
      p).valuationSubringˣ)
    (x : (padicCompletedLevelCompleteDVF p n).residueField) :
    IsLocalRing.ResidueField.mapEquiv
        (padicCompletedUnitFrobeniusIntegerEquiv p n u) x =
      x ^ p

Module documentation

Residue Frobenius on completed p-adic Lubin--Tate levels

Declarations