Hostname: page-component-76fb5796d-9pm4c Total loading time: 0 Render date: 2024-04-26T05:01:21.015Z Has data issue: false hasContentIssue false
  • English
  • Français

A univalent formalization of the p-adic numbers

Published online by Cambridge University Press:  13 February 2015

ÁLVARO PELAYO ,
VLADIMIR VOEVODSKY  and
MICHAEL A. WARREN
ÁLVARO PELAYO
Affiliation:
Department of Mathematics, University of California, San Diego, 9500 Gilman Dr #0112, La Jolla, California 92093-0112, U.S.A. Email: alpelayo@math.ucsd.edu School of Mathematics, Institute for Advanced Study, Einstein Drive, Princeton, New Jersey 08540, U.S.A. Email: vladimir@ias.edu
VLADIMIR VOEVODSKY
Affiliation:
School of Mathematics, Institute for Advanced Study, Einstein Drive, Princeton, New Jersey 08540, U.S.A. Email: vladimir@ias.edu
MICHAEL A. WARREN
Affiliation:
Los Angeles, California, U.S.A. Email: maw@mawarren.net
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

The goal of this paper is to report on a formalization of the p-adic numbers in the setting of the second author's univalent foundations program. This formalization, which has been verified in the Coq proof assistant, provides an approach to the p-adic numbers in constructive algebra and analysis.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 25 , Special Issue 5: From type theory and homotopy theory to Univalent Foundations of Mathematics , June 2015 , pp. 1147 - 1171
Copyright
Copyright © Cambridge University Press 2015 

References

Atiyah, M. (1982) Convexity and commuting Hamiltonians. Bulletin of the London Mathematical Society 14 1–15.Google Scholar
Awodey, S. (2012) Type theory and homotopy. In: Dybjer, P., Lindström, S., Palmgren, E. and Sundholm, B. G. (eds.) Epistemology versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf Logic, Epistemology, and the Unity of Science volume 27, Springer, Dordrecht 183–201.CrossRefGoogle Scholar
Awodey, S., Pelayo, Á. and Warren, M. A. (2013) Voevodsky's univalence axiom in homotopy type theory, Notices of the American Mathematical Society 60 (08) 1164–1167.Google Scholar
Bertot, Y. and Castéran, P. (2004) Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions, Texts Theoretical Computer Science An EATCS Series, Springer-Verlag.Google Scholar
Brekke, L. and Freund, P. G. O. (1993) p-adic numbers in physics. Physics Reports 233 (1) 1–66.Google Scholar
Bridges, D. and Richman, F. (1987) Varieties of Constructive Mathematics, London Mathematical Society Lecture Note Series, Cambridge University Press.CrossRefGoogle Scholar
Delzant, T. (1988) Hamiltoniens périodiques et image convexe de l'application moment. Bulletin de la Société Mathématique de France 116 315–339.Google Scholar
Gouvêa, F. (1993) p-adic Numbers. An Introduction, Universitext, Springer-Verlag.Google Scholar
Guillemin, V. and Sternberg, S. (1982) Convexity properties of the moment mapping. Inventiones Mathematicae 67 491–513.Google Scholar
Hensel, K. (1900) Über eine Theorie der algebraischen Functionen zweier Variablen. Acta Mathematica 23 (1) 339–416.Google Scholar
Koblitz, N. (1984) p-adic Numbers, p-adic Analysis and Zeta-Functions, 2nd ed. Graduate Texts in Mathematics volume 58, Springer-Verlag.Google Scholar
Mines, R., Richman, F. and Ruitenburg, W. (1988) A Course in Constructive Algebra, Springer-Verlag.Google Scholar
Pelayo, Á. and Vũ Ngoc, S. (2009) Semitoric integrable systems on symplectic 4-manifolds, Inventiones Mathematicae 177 571–597.Google Scholar
Pelayo, Á. and Vũ Ngoc, S. (2011) Constructing integrable systems of semitoric type. Acta Mathematica 206 93–125.Google Scholar
Pelayo, Á. and Warren, M. A. (2014) Homotopy type theory and Voevodsky's Univalent Foundations Bulletin of the American Mathematical Society 51 (4), 597–648.Google Scholar
Schikhof, W. H. (1984) Ultrametric Calculus. An Introduction to p-adic Analysis, Cambridge Studies in Advanced Mathematics volume 4, Cambridge University Press.Google Scholar
Serre, J. P. (1965) Classification des variétés analytiques p-adiques compactes. Topology 3 409–412.Google Scholar
Voevodsky, V. (2010) Extended version of NSF proposal at: www.math.ias.edu/~vladimir.Google Scholar
Voevodsky, V. (2011) Coq library at: www.math.ias.edu/~vladimir, Fall 2011 version.Google Scholar
Voevodsky, V. (2014) Experimental library of univalent formalization of mathematics. Mathematical Structures Computer Science, to appear. (Preprint on the arxiv as arXiv:1401.0053.)Google Scholar
Supplementary material: File

Pelayo supplementary materials

Pelayo supplementary materials 1

Download Pelayo supplementary materials(File)
File 247.3 KB