Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PadicModuleStructure

Module documentation

Topological structure of a finite p-adic module

This file packages the PID step in the mixed-characteristic proof of the local-field structure theory, the field-unit structure theorem. Once the torsion submodule is known to be a finite cyclic group of order p^a, and the torsion-free quotient has rank d, the module is topologically the product of that cyclic factor and d copies of Z_p.

def

chosenPadicModuleContinuousAddEquivZModProdFinPi

L42 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.chosenPadicModuleContinuousAddEquivZModProdFinPi

Documentation

A finite topological Z_p-module with cyclic torsion of order p^a and torsion-free quotient of rank d is topologically ZMod (p^a) × Z_p^d.

The algebraic splitting is obtained by projectively lifting the quotient map and applying lequivProdOfRightSplitExact. For continuity, its restriction to the finite torsion factor is automatic, while its restriction to the free factor is a linear map out of a finite Cartesian power of Z_p.

Source context 5 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup

Lean source · statement

def chosenPadicModuleContinuousAddEquivZModProdFinPi
    (p : ℕ) [Fact p.Prime]
    (M : Type u) [TopologicalSpace M] [AddCommGroup M] [Module ℤ_[p] M]
    [ContinuousAdd M] [ContinuousSMul ℤ_[p] M]
    [CompactSpace M] [T2Space M] [Module.Finite ℤ_[p] M]
    (a d : ℕ)
    [Finite (Submodule.torsion ℤ_[p] M)]
    (hcyclic : IsAddCyclic (Submodule.torsion ℤ_[p] M))
    (hcard : Nat.card (Submodule.torsion ℤ_[p] M) = p ^ a)
    (hfinrank : Module.finrank ℤ_[p]
      (M ⧸ Submodule.torsion ℤ_[p] M) = d) :
    (ZMod (p ^ a) × (Fin d → ℤ_[p])) ≃ₜ+ M

Module documentation

Topological structure of a finite p-adic module

Declarations

chosenPadicModuleContinuousAddEquivZModProdFinPi