Module

CompletedUnramifiedFrobeniusFixed.lean

Nyll.ClassFieldTheory.LubinTate.Padic.CompletedUnramifiedFrobeniusFixed

2 declarations indexed from sourceView source ↗

Module documentation

Fixed points of p-adic completed-unramified Frobenius

Witt Frobenius on W(AlgebraicClosure (ZMod p)) has exactly the canonical copy of ℤ_[p] as its fixed ring. Passing to fraction fields shows that the arithmetic Frobenius on the completed maximal-unramified coefficient field has exactly the canonical copy of ℚ_[p] as its fixed field.

The fraction-field argument is integral: after writing a denominator as a power of p times a unit, multiplication by that power of p puts a fixed fraction back in the Witt ring.

Imports2

Mathlib.FieldTheory.Finite.Basic
Nyll.ClassFieldTheory.LubinTate.Padic.CompletedUnramifiedField

Imported by2

theorem

padicCompletedUnramifiedWittRing_frobenius_fixed_iff

L34 ↗

LubinTate.padicCompletedUnramifiedWittRing_frobenius_fixed_iff

Documentation

The fixed ring of Witt Frobenius on the completed-unramified Witt ring is the canonical image of the p-adic integers.

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 padicCompletedUnramifiedWittRing_frobenius_fixed_iff
    (p : ℕ) [Fact p.Prime]
    (x : padicCompletedUnramifiedWittRing p) :
    WittVector.frobenius x = x ↔
      ∃ z : ℤ_[p],
        padicIntToCompletedUnramifiedWittRing p z = x

theorem

padicCompletedUnramifiedFrobenius_fixed_iff

L80 ↗

LubinTate.padicCompletedUnramifiedFrobenius_fixed_iff