ModuleProfiniteUnits.lean
Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.ProfiniteUnits
4 declarations indexed from sourceView source ↗ Module documentation
Profinite valuation-ring units
The topology of a nonarchimedean local field is Hausdorff and totally disconnected because valuation balls are clopen. This file records those structures as named results, without registering additional global instances, and packages the valuation-ring unit group as a profinite group.
Declarations
LocalFieldTheory.localFieldT2Space
DocumentationA nonarchimedean local field is Hausdorff for its valuative topology.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
namespace LocalFieldTheory
open scoped ValuativeRel
LocalFieldTheory.localFieldTotallySeparatedSpace
DocumentationDistinct points of a nonarchimedean local field are separated by a clopen valuation ball.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
namespace LocalFieldTheory
open scoped ValuativeRel
LocalFieldTheory.localFieldTotallyDisconnectedSpace
DocumentationA nonarchimedean local field is totally disconnected for its valuative topology.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
namespace LocalFieldTheory
open scoped ValuativeRel
LocalFieldTheory.localUnits_profinite
DocumentationThe unit group of the valuation ring of a nonarchimedean local field, as a profinite group.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
namespace LocalFieldTheory
open scoped ValuativeRel