Abstract
We develop a framework for reasoning computationally about \(p\)-adic fields via formal Laurent series with integer coefficients.
We define a ring-class quotient type consisting of equivalence classes of prime-indexed sequences of formal Laurent series, in which every \(p\)-adic field is contained as a subring.
Via a further quotient of the ring of \(p\)-adic integers (that is, the elements of depth at least \(0\)) by the prime ideal (that is, the subring of elements of depth at least \(1\)), we define a ring-class type in which every prime-order finite field is contained as a subring.
Finally, some topological properties are developed using depth as a proxy for a metric, Hensel's Lemma is proved, and the compactness of local rings of integers is established.
License
Topics
Session Computational_pAdics
- Distinguished_Quotients
- Polynomial_Extras
- Parametric_Equiv_Depth
- FLS_Prime_Equiv_Depth
- pAdic_Product
- Fin_Field_Product
- More_pAdic_Product