Formalizing the p-adic numbers.md (1249B)
1 +++ 2 title = 'Formalizing the p-adic numbers' 3 +++ 4 # Formalizing the p-adic numbers 5 The rational numbers Q are incomplete: the sets `{x ∈ Q | x² < 2}` and `{x ∈ Q | x² > 2}` partition Q, but both are open. 6 7 A sequence is Cauchy if its entries eventually become arbitrarily close. 8 9 Two sequences are equivalent if they eventually become arbitrarily close to each other: `s ∼ t` if for every positive `ε ∈ Q`, there exists and N such that for all `k ≥ N`, `|s_k - t_k| < ε`. 10 11 equivalence relation: binary relation that is reflexive, symmetric, and transitive 12 13 equivalence class: for `≈` as equivalence relation on S, the equivalence class of `a ∈ S` is `⟦a⟧ = {x ∈ S | a ≈ x}.` 14 15 quotient: based on the above equivalence class, is the set `{⟦a⟧ | a ∈ S}` (so set of all equivalence classes) 16 17 The set of real numbers is the set `{s : N → Q | s is Cauchy}`. It is the quotient of set of rational Cauchy sequences, with respect to equivalence. This is the completion of Q. 18 19 ## The p-adic norm 20 An alternate absolute value. 21 22 If `q ≠ 0`, the p-adic norm of rational `q` is `p ^ (-(padic_val_rat p q))`. 23 If `q = 0`, p-adic norm of `q` is 0. 24 25 The p-adic numbers are the Cauchy completion of Q with respect to the p-adic norm.