Module

ResidueInverseLimit.lean

Nyll.ValuedFieldTheory.LocalField.Padic.ResidueInverseLimit

13 declarations indexed from sourceView source ↗

Module documentation

The topological inverse limit of prime-power residue rings

The actual p-adic integers, with their metric topology, are the ring of compatible residues. Reduction gives the forward map. Its inverse is constructed by the universal property of the p-adic completion, and is continuous because reduction is a continuous bijection from a compact space to a Hausdorff space. No limit comparison is assumed.

Imports3

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.PadicReductionContinuous
Mathlib.NumberTheory.Padics.ProperSpace
Mathlib.Topology.Homeomorph.Lemmas

Imported by2

def

compatibleResidues

L28 ↗

LocalFieldTheory.PadicResidues.compatibleResidues

Documentation

The subring of all compatible prime-power residues, including level zero.

Source context 3 commands

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

noncomputable section
namespace LocalFieldTheory.PadicResidues
variable (p : ℕ)

Lean source · full declaration

def compatibleResidues : Subring (∀ n : ℕ, ZMod (p ^ n)) where
  carrier := {a | ∀ m n (h : m ≤ n), ZMod.castHom (pow_dvd_pow p h) _ (a n) = a m}
  zero_mem' := fun m n h => (ZMod.castHom (pow_dvd_pow p h) _).map_zero
  one_mem' := fun m n h => (ZMod.castHom (pow_dvd_pow p h) _).map_one
  add_mem' := by
    intro a b ha hb m n h
    exact ((ZMod.castHom (pow_dvd_pow p h) _).map_add (a n) (b n)).trans
      (congrArg₂ (· + ·) (ha m n h) (hb m n h))
  mul_mem' := by
    intro a b ha hb m n h
    exact ((ZMod.castHom (pow_dvd_pow p h) _).map_mul (a n) (b n)).trans
      (congrArg₂ (· * ·) (ha m n h) (hb m n h))
  neg_mem' := by
    intro a ha m n h
    exact ((ZMod.castHom (pow_dvd_pow p h) (ZMod (p ^ m))).map_neg (a n)).trans
      (congrArg (fun z : ZMod (p ^ m) => -z) (ha m n h))

theorem

compatibleResidues_of_adjacent

L46 ↗

LocalFieldTheory.PadicResidues.compatibleResidues_of_adjacent

Documentation

Compatibility of adjacent residues implies compatibility at all levels.

Source context 3 commands

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

noncomputable section
namespace LocalFieldTheory.PadicResidues
variable (p : ℕ)

Lean source · statement

theorem compatibleResidues_of_adjacent (a : ∀ n : ℕ, ZMod (p ^ n))
    (ha : ∀ n, ZMod.castHom (pow_dvd_pow p (Nat.le_succ n)) _ (a (n + 1)) = a n) :
    a ∈ compatibleResidues p

def

residueProjection

L64 ↗

LocalFieldTheory.PadicResidues.residueProjection

Documentation

Projection to an actual finite residue ring.

Source context 3 commands

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

noncomputable section
namespace LocalFieldTheory.PadicResidues
variable (p : ℕ)

Lean source · full declaration

def residueProjection (n : ℕ) : compatibleResidues p →+* ZMod (p ^ n) where
  toFun a := a.val n
  map_one' := rfl
  map_mul' _ _ := rfl
  map_zero' := rfl
  map_add' _ _ := rfl

theorem

residueProjection_compatible

L71 ↗

LocalFieldTheory.PadicResidues.residueProjection_compatible

Source context 3 commands

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

noncomputable section
namespace LocalFieldTheory.PadicResidues
variable (p : ℕ)

Lean source · statement

theorem residueProjection_compatible (m n : ℕ) (h : m ≤ n) :
    (ZMod.castHom (pow_dvd_pow p h) _).comp (residueProjection p n) =
      residueProjection p m

def

residueFamily

L81 ↗

LocalFieldTheory.PadicResidues.residueFamily

Documentation

Simultaneous reduction of a p-adic integer.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.PadicResidues
variable (p : ℕ)
variable [Fact p.Prime]

Lean source · full declaration

def residueFamily : ℤ_[p] →+* compatibleResidues p where
  toFun z := ⟨fun n => PadicInt.toZModPow n z, fun m n h =>
    congrArg (fun f : ℤ_[p] →+* ZMod (p ^ m) => f z)
      (PadicInt.zmod_cast_comp_toZModPow m n h)⟩
  map_one' := Subtype.ext (funext fun n => (PadicInt.toZModPow n).map_one)
  map_mul' x y := Subtype.ext (funext fun n => (PadicInt.toZModPow n).map_mul x y)
  map_zero' := Subtype.ext (funext fun n => (PadicInt.toZModPow n).map_zero)
  map_add' x y := Subtype.ext (funext fun n => (PadicInt.toZModPow n).map_add x y)

def

residueLimit

L91 ↗

LocalFieldTheory.PadicResidues.residueLimit

Documentation

The actual p-adic integer represented by a compatible residue family.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.PadicResidues
variable (p : ℕ)
variable [Fact p.Prime]

Lean source · statement

def residueLimit : compatibleResidues p →+* ℤ_[p]

theorem

residueLimit_spec

L95 ↗

LocalFieldTheory.PadicResidues.residueLimit_spec

Documentation

The constructed limit has exactly the prescribed residues.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.PadicResidues
variable (p : ℕ)
variable [Fact p.Prime]

Lean source · statement

theorem residueLimit_spec (a : compatibleResidues p) (n : ℕ) :
    PadicInt.toZModPow n (residueLimit p a) = a.val n

def

residueFamilyRingEquiv

L101 ↗

LocalFieldTheory.PadicResidues.residueFamilyRingEquiv

Documentation

Reduction identifies the p-adic integer ring with compatible residues.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.PadicResidues
variable (p : ℕ)
variable [Fact p.Prime]

Lean source · full declaration

def residueFamilyRingEquiv : ℤ_[p] ≃+* compatibleResidues p where
  __ := residueFamily p
  invFun := residueLimit p
  left_inv z := PadicInt.ext_of_toZModPow.mp fun n => residueLimit_spec p (residueFamily p z) n
  right_inv a := Subtype.ext (funext fun n => residueLimit_spec p a n)

instance

residueTopology

L107 ↗

LocalFieldTheory.PadicResidues.residueTopology

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.PadicResidues
variable (p : ℕ)
variable [Fact p.Prime]

Lean source · statement

instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (p ^ n))

instance

residueDiscreteTopology

L108 ↗

LocalFieldTheory.PadicResidues.residueDiscreteTopology

Source context 5 commands

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

noncomputable section
namespace LocalFieldTheory.PadicResidues
variable (p : ℕ)
variable [Fact p.Prime]
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (p ^ n)) := ⊥

Lean source · statement

instance residueDiscreteTopology (n : ℕ) : DiscreteTopology (ZMod (p ^ n))

theorem

continuous_residueFamily

L113 ↗

LocalFieldTheory.PadicResidues.continuous_residueFamily

Documentation

Reduction to the inverse limit is continuous for its subspace product topology.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory.PadicResidues
variable (p : ℕ)
variable [Fact p.Prime]
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (p ^ n)) := ⊥
local instance residueDiscreteTopology (n : ℕ) : DiscreteTopology (ZMod (p ^ n)) := ⟨rfl⟩
open DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal

Lean source · statement

theorem continuous_residueFamily : Continuous (residueFamily p)

theorem

residueFamily_isHomeomorph

L120 ↗

LocalFieldTheory.PadicResidues.residueFamily_isHomeomorph

Documentation

The metric p-adic topology agrees with the inverse-limit topology.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory.PadicResidues
variable (p : ℕ)
variable [Fact p.Prime]
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (p ^ n)) := ⊥
local instance residueDiscreteTopology (n : ℕ) : DiscreteTopology (ZMod (p ^ n)) := ⟨rfl⟩
open DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal

Lean source · statement

theorem residueFamily_isHomeomorph : IsHomeomorph (residueFamilyRingEquiv p)

theorem

continuous_iff_residues

L125 ↗

LocalFieldTheory.PadicResidues.continuous_iff_residues

Documentation

A map to the p-adic integers is continuous exactly when every residue is continuous.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory.PadicResidues
variable (p : ℕ)
variable [Fact p.Prime]
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (p ^ n)) := ⊥
local instance residueDiscreteTopology (n : ℕ) : DiscreteTopology (ZMod (p ^ n)) := ⟨rfl⟩
open DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal

Lean source · full declaration

theorem continuous_iff_residues {Y : Type*} [TopologicalSpace Y] (f : Y → ℤ_[p]) :
    Continuous f ↔ ∀ n, Continuous (fun y => PadicInt.toZModPow n (f y)) := by
  constructor
  · intro hf n
    exact (continuous_padicIntToZModPow p n).comp hf
  · intro hf
    apply (residueFamily_isHomeomorph p).isEmbedding.continuous_iff.mpr
    exact (continuous_pi hf).subtype_mk _

Module documentation

The topological inverse limit of prime-power residue rings

Declarations