Theory Padic_Field_Topology_Bridge
section ‹Topology, metric space, completeness for $p$-adic fields›
text ‹This additional theory links the topology of a $p$-adic field to the standard notion
of abstract topology from the Analysis library. It also proves completeness for $p$-adic fields.
Supplied by LCP and Claude.›
theory Padic_Field_Topology_Bridge
imports Padic_Field_Topology "HOL-Analysis.Abstract_Metric_Spaces"
begin
context padic_fields
begin
subsection ‹The $p$-adic topology is a topology›
definition padic_topology :: "padic_number topology" where
"padic_topology = topology is_open"
lemma istopology_padic: "istopology is_open"
unfolding istopology_def
proof (intro conjI allI impI)
fix S T
assume "is_open S" "is_open T"
show "is_open (S ∩ T)"
proof (rule is_openI)
show "S ∩ T ⊆ carrier Q⇩p"
using ‹is_open S› is_open_imp_in_Qp by blast
fix c assume "c ∈ S ∩ T"
then obtain n m where "B⇘n⇙[c] ⊆ S" "B⇘m⇙[c] ⊆ T"
using ‹is_open S› ‹is_open T› is_open_def by force
then have "B⇘max n m⇙[c] ⊆ S ∩ T"
by (smt (verit, ccfv_SIG) IntE Int_mono ‹c ∈ S ∩ T› ‹is_open S› order.trans inf.orderE
is_ball_def is_open_imp_in_Qp' nested_balls)
then show "∃k. B⇘k⇙[c] ⊆ S ∩ T" by blast
qed
qed (fastforce simp: is_open_def)
text ‹Agreement on the notions of open set.›
lemma openin_padic_topology: "openin padic_topology = is_open"
unfolding padic_topology_def
using istopology_padic topology_inverse' by blast
subsection ‹Bridging lemmas — connect old and new frameworks›
lemma topspace_padic: "topspace padic_topology = carrier Q⇩p"
proof
show "topspace padic_topology ⊆ carrier Q⇩p"
by (metis is_open_def openin_padic_topology openin_topspace)
show "carrier Q⇩p ⊆ topspace padic_topology"
by (simp add: c_ball_in_Qp is_openI openin_padic_topology openin_subset)
qed
lemma openin_ball:
assumes "c ∈ carrier Q⇩p"
shows "openin padic_topology (B⇘n⇙[c])"
using openin_padic_topology ball_is_open is_ball_def assms
by auto
lemma interior_eq:
assumes "U ⊆ carrier Q⇩p"
shows "interior U = Abstract_Topology.interior_of padic_topology U"
by (metis assms interiorI interior_of_unique interior_open interior_subset openin_padic_topology)
subsection ‹Main topological results in the standard framework›
text ‹Balls are open.›
lemma ball_openin_padic: "is_ball B ⟹ openin padic_topology B"
using openin_padic_topology ball_is_open by simp
text ‹Hensel's lemma consequence: compactness of $\mathbb{Z}_p$.›
text ‹Open decomposition into maximal balls.›
lemma open_max_ball_decomposition:
assumes "openin padic_topology U" "U ≠ topspace padic_topology"
shows "U = ⋃(max_balls U)"
proof -
have "⋃(max_balls U) ⊆ carrier Q⇩p"
using is_ball_imp_in_Qp is_max_ball_of_def max_balls_def by auto
moreover have "interior U = {x ∈ carrier Q⇩p. ∃B∈max_balls U. x ∈ B}"
using max_balls_interior assms is_open_def openin_padic_topology topspace_padic by auto
then have "U = {x ∈ carrier Q⇩p. ∃B∈max_balls U. x ∈ B}"
using assms(1) local.open_interior openin_padic_topology by force
ultimately show ?thesis by auto
qed
end
subsection ‹The $p$-adic metric on $\mathbb{Q}_p$›
context padic_fields
begin
text ‹The $p$-adic absolute value / distance function.
Convention: $|x|_p = p^{-\mathrm{val}(x)}$, with $|0|_p = 0$.›
definition padic_norm :: "padic_number ⇒ real" where
"padic_norm x ≡ (if x = 𝟬 then 0 else p powr (- real_of_int (ord x)))"
definition padic_dist :: "padic_number ⇒ padic_number ⇒ real" where
"padic_dist x y ≡ if x ∈ carrier Q⇩p ∧ y ∈ carrier Q⇩p then padic_norm (x ⊖ y) else 0"
subsection ‹$\mathbb{Q}_p$ is a Metric\_space›
lemma padic_dist_nonneg: "0 ≤ padic_dist x y"
by (simp add: padic_dist_def padic_norm_def)
lemma padic_dist_commute_aux:
assumes "x ∈ carrier Q⇩p" and "y ∈ carrier Q⇩p"
shows"real_of_int p powr - real_of_int (ord (x ⊖ y)) = real_of_int p powr - real_of_int (ord (y ⊖ x))"
using assms
by (metis Qp.not_eq_diff_nonzero Qp.not_nonzero_memI Qp.plus_diff_simp
Qp.r_right_minus_eq diff_ord_nonzero)
lemma padic_dist_commute:
shows "padic_dist x y = padic_dist y x"
using padic_dist_commute_aux Qp.r_right_minus_eq padic_dist_def padic_norm_def by presburger
lemma padic_dist_zero:
assumes "x ∈ carrier Q⇩p" "y ∈ carrier Q⇩p"
shows "padic_dist x y = 0 ⟷ x = y"
unfolding padic_dist_def padic_norm_def
using Qp.int_inc_zero Qp.nonzero_memE(2) assms p_nonzero by auto
lemma p_gt_1: "1 < (p :: int)"
using prime prime_gt_1_int by auto
lemma p_ge_1_real: "(1 :: real) ≤ real_of_int p"
using p_gt_1 by linarith
lemma p_gt_1_real: "(1 :: real) < real_of_int p"
using p_gt_1 by linarith
lemma diff_sum:
assumes "x ∈ carrier Q⇩p" "y ∈ carrier Q⇩p" "z ∈ carrier Q⇩p"
shows "x ⊖ z = (x ⊖ y) ⊕ (y ⊖ z)"
by (metis Qp.minus_a_inv Qp_diff_diff a_minus_def assms)
lemma padic_norm_ultrametric:
assumes "a ∈ carrier Q⇩p" "b ∈ carrier Q⇩p"
shows "padic_norm (a ⊕ b) ≤ max (padic_norm a) (padic_norm b)"
proof (cases "a ⊕ b = 𝟬")
case True
then have "padic_norm (a ⊕ b) = 0" unfolding padic_norm_def by simp
then show ?thesis using padic_norm_def powr_non_neg
by (simp add: le_max_iff_disj)
next
case ab_nz: False
then have ab_nonzero: "a ⊕ b ∈ nonzero Q⇩p"
using assms Qp.nonzero_memI Qp.add.m_closed by auto
have val_ineq: "min (val a) (val b) ≤ val (a ⊕ b)"
using val_ultrametric assms by auto
show ?thesis
proof (cases "a = 𝟬 ∨ b = 𝟬")
case True
then show ?thesis unfolding padic_norm_def
using assms by fastforce
next
case False
then have ord_ineq: "min (ord a) (ord b) ≤ ord (a ⊕ b)"
using Qp.nonzero_memI ab_nonzero assms ord_ultrametric by presburger
then have "p powr (- real_of_int (ord (a ⊕ b))) ≤
max (p powr (- real_of_int (ord a))) (p powr (- real_of_int (ord b)))"
using le_max_iff_disj ord_ineq p_gt_1_real by fastforce
then show ?thesis
using padic_norm_def False ab_nz by auto
qed
qed
lemma padic_dist_ultrametric:
assumes "x ∈ carrier Q⇩p" "y ∈ carrier Q⇩p" "z ∈ carrier Q⇩p"
shows "padic_dist x z ≤ max (padic_dist x y) (padic_dist y z)"
proof (cases "x = z")
case True
then have "padic_dist x z = 0" using assms padic_dist_zero by auto
then show ?thesis using padic_dist_nonneg[of x y] padic_dist_nonneg[of y z] by simp
next
case xz: False
have "padic_norm (x ⊖ z) ≤ max (padic_norm (x ⊖ y)) (padic_norm (y ⊖ z))"
by (metis Qp.minus_closed assms diff_sum padic_norm_ultrametric)
then show ?thesis
using assms unfolding padic_dist_def by auto
qed
text ‹The ultrametric inequality implies the triangle inequality.›
lemma padic_dist_triangle:
assumes "x ∈ carrier Q⇩p" "y ∈ carrier Q⇩p" "z ∈ carrier Q⇩p"
shows "padic_dist x z ≤ padic_dist x y + padic_dist y z"
using padic_dist_ultrametric[OF assms] padic_dist_nonneg
by (metis add_increasing add_increasing2 max_def)
interpretation padic: Metric_space "carrier Q⇩p" padic_dist
proof
fix x y
show "0 ≤ padic_dist x y"
by (simp add: padic_dist_nonneg)
show "padic_dist x y = padic_dist y x"
using padic_dist_commute by auto
assume "x ∈ carrier Q⇩p" and "y ∈ carrier Q⇩p"
then show "(padic_dist x y = 0) = (x = y)"
using padic_dist_zero by auto
fix z assume "z ∈ carrier Q⇩p"
then show "padic_dist x z ≤ padic_dist x y + padic_dist y z"
by (simp add: ‹x ∈ carrier Q⇩p› ‹y ∈ carrier Q⇩p› padic_dist_triangle)
qed
text ‹Key correspondence:
@{term ‹c_ball n c›} $= \{x \in \mathrm{carrier}\; \mathbb{Q}_p \mid \mathrm{val}(x - c) \ge n\}$
$= \{x \in \mathrm{carrier}\; \mathbb{Q}_p \mid \mathrm{padic\_dist}\; c\; x \le p^{-n}\}$
$=$ @{term ‹padic.mcball c (p powr (-n))›}.›
lemma padic_dist_as_norm:
assumes "x ∈ carrier Q⇩p" "y ∈ carrier Q⇩p"
shows "padic_dist x y = padic_norm (x ⊖ y)"
unfolding padic_dist_def using assms by auto
lemma c_ball_eq_mcball:
assumes "c ∈ carrier Q⇩p"
shows "c_ball n c = padic.mcball c (real_of_int p powr (- real_of_int n))"
proof (rule Set.set_eqI)
fix x
show "x ∈ c_ball n c ⟷ x ∈ padic.mcball c (real_of_int p powr (- real_of_int n))"
proof
assume xin: "x ∈ c_ball n c"
then have x_car: "x ∈ carrier Q⇩p" and val_ge: "eint n ≤ val (x ⊖ c)"
using c_ball_def by auto
show "x ∈ padic.mcball c (real_of_int p powr (- real_of_int n))"
unfolding padic.in_mcball
proof (intro conjI)
show "c ∈ carrier Q⇩p" using assms by auto
show "x ∈ carrier Q⇩p" using x_car by auto
show "padic_dist c x ≤ real_of_int p powr (- real_of_int n)"
proof (cases "x = c")
case True
then show ?thesis using assms padic_dist_zero powr_non_neg by auto
next
case False
then have xc_nz: "x ⊖ c ∈ nonzero Q⇩p"
using x_car assms Qp.not_eq_diff_nonzero by auto
have "val (x ⊖ c) = eint (ord (x ⊖ c))" using val_ord xc_nz by auto
then have ord_ge: "n ≤ ord (x ⊖ c)" using val_ge by simp
have "padic_dist c x = padic_norm (x ⊖ c)"
by (metis assms padic_dist_as_norm padic_dist_commute x_car)
also have "… = p powr (- real_of_int (ord (x ⊖ c)))"
using padic_norm_def Qp.nonzero_memE(2)[OF xc_nz] by auto
also have "… ≤ p powr (- real_of_int n)"
using powr_mono p_ge_1_real ord_ge by auto
finally show ?thesis .
qed
qed
next
assume xin: "x ∈ padic.mcball c (real_of_int p powr (- real_of_int n))"
then have x_car: "x ∈ carrier Q⇩p" and dist_le: "padic_dist c x ≤ p powr (- real_of_int n)"
using padic.in_mcball by auto
show "x ∈ c_ball n c"
proof (cases "x = c")
case True then show ?thesis
using assms c_ball_center_in is_ball_def by blast
next
case False
then have xc_nz: "x ⊖ c ∈ nonzero Q⇩p"
using x_car assms Qp.not_eq_diff_nonzero by auto
have "padic_dist c x = padic_norm (x ⊖ c)"
by (metis assms padic.commute padic_dist_as_norm x_car)
also have "… = p powr (- real_of_int (ord (x ⊖ c)))"
using padic_norm_def Qp.nonzero_memE(2)[OF xc_nz] by auto
finally have "p powr (- real_of_int (ord (x ⊖ c))) ≤ p powr (- real_of_int n)"
using dist_le by linarith
then have "- real_of_int (ord (x ⊖ c)) ≤ - real_of_int n"
using powr_le_cancel_iff[OF p_gt_1_real] by auto
then have "eint n ≤ val (x ⊖ c)"
using val_ord xc_nz by auto
then show ?thesis using c_ballI x_car by auto
qed
qed
qed
text ‹Open balls in the metric sense correspond to @{term c_ball} with shifted index.›
lemma mball_eq_c_ball:
assumes "c ∈ carrier Q⇩p"
shows "padic.mball c (real_of_int p powr (- real_of_int n)) = c_ball (n + 1) c"
proof (rule Set.set_eqI)
fix x
show "x ∈ padic.mball c (real_of_int p powr (- real_of_int n)) ⟷ x ∈ c_ball (n + 1) c"
proof
assume xin: "x ∈ padic.mball c (real_of_int p powr (- real_of_int n))"
then have x_car: "x ∈ carrier Q⇩p" and dist_lt: "padic_dist c x < p powr (- real_of_int n)"
using padic.in_mball by auto
show "x ∈ c_ball (n + 1) c"
proof (cases "x = c")
case True
then show ?thesis
using assms c_ball_center_in is_ball_def by blast
next
case False
then have xc_nz: "x ⊖ c ∈ nonzero Q⇩p"
using x_car assms Qp.not_eq_diff_nonzero by auto
have "padic_dist c x = padic_norm (x ⊖ c)"
by (metis assms padic.commute padic_dist_as_norm x_car)
then have "p powr (- real_of_int (ord (x ⊖ c))) < p powr (- real_of_int n)"
using dist_lt padic_norm_def Qp.nonzero_memE(2)[OF xc_nz] by auto
then have "- real_of_int (ord (x ⊖ c)) < - real_of_int n"
using powr_less_cancel_iff[OF p_gt_1_real] by auto
then show ?thesis using val_ord xc_nz c_ballI x_car by auto
qed
next
assume xin: "x ∈ c_ball (n + 1) c"
then have x_car: "x ∈ carrier Q⇩p" and val_ge: "eint (n + 1) ≤ val (x ⊖ c)"
using c_ball_def by auto
show "x ∈ padic.mball c (real_of_int p powr (- real_of_int n))"
unfolding padic.in_mball
proof (intro conjI)
show "c ∈ carrier Q⇩p" "x ∈ carrier Q⇩p" using assms x_car by auto
show "padic_dist c x < real_of_int p powr (- real_of_int n)"
proof (cases "x = c")
case True
then show ?thesis
using assms padic_dist_zero p_gt_1_real by auto
next
case False
then have xc_nz: "x ⊖ c ∈ nonzero Q⇩p"
using x_car assms Qp.not_eq_diff_nonzero by auto
have "val (x ⊖ c) = eint (ord (x ⊖ c))" using val_ord xc_nz by auto
then have "- real_of_int (ord (x ⊖ c)) < - real_of_int n" using val_ge by simp
then have "p powr (- real_of_int (ord (x ⊖ c))) < p powr (- real_of_int n)"
using p_gt_1_real by (simp add: powr_less_cancel_iff)
moreover have "padic_dist c x = p powr (- real_of_int (ord (x ⊖ c)))"
proof -
have "padic_dist c x = padic_norm (x ⊖ c)"
by (metis assms padic.commute padic_dist_as_norm x_car)
also have "… = p powr (- real_of_int (ord (x ⊖ c)))"
using padic_norm_def Qp.nonzero_memE(2)[OF xc_nz] by auto
finally show ?thesis .
qed
ultimately show ?thesis by linarith
qed
qed
qed
qed
subsection ‹The metric topology equals @{term is_open}›
lemma padic_topology_eq_mtopology:
"openin padic.mtopology U ⟷ is_open U"
proof
assume "openin padic.mtopology U"
then have U_sub: "U ⊆ carrier Q⇩p" and
U_ball: "⋀x. x ∈ U ⟹ ∃r>0. padic.mball x r ⊆ U"
using padic.openin_mtopology by auto
show "is_open U"
proof (rule is_openI[OF U_sub])
fix c assume c_in: "c ∈ U"
obtain r where r_pos: "r > 0" and r_sub: "padic.mball c r ⊆ U"
using U_ball c_in by auto
obtain n where n_large: "p powr (- real_of_int n) < r"
by (meson ex_less_of_int less_log_iff minus_less_iff p_gt_1_real r_pos)
have "c_ball (n + 1) c = padic.mball c (p powr (- real_of_int n))"
using mball_eq_c_ball U_sub by (simp add: c_in in_mono)
then show "∃k. c_ball k c ⊆ U"
using r_sub padic.mball_subset_concentric n_large by fastforce
qed
next
assume U_open: "is_open U"
show "openin padic.mtopology U"
unfolding padic.openin_mtopology
proof (intro conjI allI impI)
show "U ⊆ carrier Q⇩p" using U_open is_open_imp_in_Qp by blast
next
fix x assume x_in: "x ∈ U"
then have x_car: "x ∈ carrier Q⇩p" using U_open is_open_imp_in_Qp by blast
obtain n where n_sub: "c_ball n x ⊆ U"
using U_open x_in is_open_def by auto
have ball_eq: "padic.mball x (p powr (- real_of_int (n - 1))) = c_ball n x"
using mball_eq_c_ball[OF x_car, of "n - 1"] by auto
have r_pos: "0 < p powr (- real_of_int (n - 1))"
using p_gt_1_real by simp
show "∃r>0. padic.mball x r ⊆ U"
using ball_eq n_sub r_pos by blast
qed
qed
lemma padic_mtopology_eq: "padic.mtopology = padic_topology"
using padic_topology_eq_mtopology openin_padic_topology
by (intro topology.openin_inject[THEN iffD1] ext iffI; simp)
lemma mcball_is_open:
assumes "c ∈ carrier Q⇩p" "0 < r"
shows "openin padic.mtopology (padic.mcball c r)"
unfolding padic.openin_mtopology
proof (intro conjI strip)
show "padic.mcball c r ⊆ carrier Q⇩p"
using padic.mcball_subset_mspace by auto
next
fix y assume y_in: "y ∈ padic.mcball c r"
then have y_car: "y ∈ carrier Q⇩p" and dy: "padic_dist c y ≤ r"
using padic.in_mcball by auto
show "∃ε>0. padic.mball y ε ⊆ padic.mcball c r"
proof (intro exI conjI subsetI)
show "0 < r" using assms by auto
next
fix z assume z_in: "z ∈ padic.mball y r"
then have z_car: "z ∈ carrier Q⇩p" and dyz: "padic_dist y z < r"
using padic.in_mball by auto
have "padic_dist c z ≤ max (padic_dist c y) (padic_dist y z)"
using padic_dist_ultrametric[OF assms(1) y_car z_car] by auto
also have "… ≤ r" using dy dyz by simp
finally show "z ∈ padic.mcball c r"
by (simp add: assms z_car)
qed
qed
text ‹Equivalently, balls are clopen.›
lemma c_ball_open:
assumes "c ∈ carrier Q⇩p"
shows "openin padic.mtopology (c_ball n c)"
using assms openin_ball padic_mtopology_eq by force
lemma c_ball_closed:
assumes "c ∈ carrier Q⇩p"
shows "closedin padic.mtopology (c_ball n c)"
using assms c_ball_eq_mcball by force
lemma c_ball_clopen:
assumes "c ∈ carrier Q⇩p"
shows "openin padic.mtopology (c_ball n c) ∧ closedin padic.mtopology (c_ball n c)"
by (simp add: assms c_ball_closed c_ball_open)
text ‹Total disconnectedness.›
lemma padic_mtop_totally_disconnected:
assumes "connectedin padic.mtopology S"
shows "∃a. S ⊆ {a}"
proof (rule ccontr)
assume neg: "¬(∃a. S ⊆ {a})"
have S_sub: "S ⊆ carrier Q⇩p"
using assms connectedin_subset_topspace padic.topspace_mtopology by blast
obtain x y where xy: "x ∈ S" "y ∈ S" "x ≠ y"
by (metis insertI1 neg subsetI)
have x_car: "x ∈ carrier Q⇩p" and y_car: "y ∈ carrier Q⇩p"
using S_sub xy by auto
have xy_nz: "x ⊖ y ∈ nonzero Q⇩p"
using xy x_car y_car Qp.not_eq_diff_nonzero by auto
define n where "n = ord (x ⊖ y) + 1"
have x_in_ball: "x ∈ c_ball n x"
using c_ball_center_in is_ball_def x_car by blast
have y_not_in_ball: "y ∉ c_ball n x"
proof
assume "y ∈ c_ball n x"
then have val_ge: "eint n ≤ val (y ⊖ x)" using c_ballE by auto
have yx_nz: "y ⊖ x ∈ nonzero Q⇩p"
using xy x_car y_car Qp.not_eq_diff_nonzero by auto
have "val (y ⊖ x) = eint (ord (y ⊖ x))" using val_ord[OF yx_nz] by auto
then have n_le: "n ≤ ord (y ⊖ x)" using val_ge by simp
have "y ⊖ x = ⊖ (x ⊖ y)"
using x_car y_car using Qp.minus_a_inv by blast
then have "ord (y ⊖ x) = ord (x ⊖ y)"
using ord_minus xy_nz by presburger
then show False using n_le n_def by linarith
qed
have "S ⊆ c_ball n x ∨ disjnt S (c_ball n x)"
using connectedin_clopen_cases[OF assms] c_ball_closed
using openin_ball padic_mtopology_eq x_car by auto
then show False
by (meson disjnt_iff in_mono x_in_ball xy y_not_in_ball)
qed
text ‹Nested balls — reproved from the ultrametric inequality.›
lemma ultrametric_nested:
assumes "padic.mcball x r ∩ padic.mcball y s ≠ {}"
shows "padic.mcball x r ⊆ padic.mcball y s ∨ padic.mcball y s ⊆ padic.mcball x r"
proof -
obtain z where z_xr: "z ∈ padic.mcball x r" and z_ys: "z ∈ padic.mcball y s"
using assms by blast
then have x_car: "x ∈ carrier Q⇩p" and y_car: "y ∈ carrier Q⇩p" and z_car: "z ∈ carrier Q⇩p"
and dxz: "padic_dist x z ≤ r" and dyz: "padic_dist y z ≤ s"
using padic.in_mcball by auto
have dzx: "padic_dist z x ≤ r" using dxz padic_dist_commute by simp
have dzy: "padic_dist z y ≤ s" using dyz padic_dist_commute by simp
show ?thesis
proof (cases "r ≤ s")
case True
show ?thesis
proof (intro disjI1 subsetI)
fix w assume w_in: "w ∈ padic.mcball x r"
then have w_car: "w ∈ carrier Q⇩p" and dxw: "padic_dist x w ≤ r"
using padic.in_mcball by auto
have "padic_dist z w ≤ max (padic_dist z x) (padic_dist x w)"
using padic_dist_ultrametric[OF z_car x_car w_car] by auto
also have "… ≤ r" using dzx dxw by simp
finally have dzw: "padic_dist z w ≤ r" .
have "padic_dist y w ≤ max (padic_dist y z) (padic_dist z w)"
using padic_dist_ultrametric[OF y_car z_car w_car] by auto
also have "… ≤ s" using dyz dzw True by simp
finally show "w ∈ padic.mcball y s"
using padic.in_mcball y_car w_car by auto
qed
next
case False
then have sr: "s ≤ r" by simp
show ?thesis
proof (intro disjI2 subsetI)
fix w assume w_in: "w ∈ padic.mcball y s"
then have w_car: "w ∈ carrier Q⇩p" and dyw: "padic_dist y w ≤ s"
using padic.in_mcball by auto
have "padic_dist z w ≤ max (padic_dist z y) (padic_dist y w)"
using padic_dist_ultrametric[OF z_car y_car w_car] by auto
also have "… ≤ s" using dzy dyw by simp
finally have dzw: "padic_dist z w ≤ s" .
have "padic_dist x w ≤ max (padic_dist x z) (padic_dist z w)"
using padic_dist_ultrametric[OF x_car z_car w_car] by auto
also have "… ≤ r" using dxz dzw sr by simp
finally show "w ∈ padic.mcball x r"
using padic.in_mcball x_car w_car by auto
qed
qed
qed
subsection ‹Closedness and disconnectedness›
text ‹Balls are also closed (clopen).›
lemma closedin_ball:
assumes "c ∈ carrier Q⇩p"
shows "closedin padic_topology (B⇘n⇙[c])"
using c_ball_clopen[OF assms] padic_mtopology_eq by simp
lemma ball_closedin_padic:
"is_ball B ⟹ closedin padic_topology B"
using closedin_ball is_ball_def by auto
text ‹The $p$-adic topology is totally disconnected.›
lemma padic_totally_disconnected:
assumes "connectedin padic_topology S"
shows "∃a. S ⊆ {a}"
using padic_mtop_totally_disconnected assms padic_mtopology_eq by simp
subsection ‹Completeness›
text ‹$\mathbb{Q}_p$ is complete: every Cauchy sequence converges.
This uses @{term ‹Metric_space.mcomplete›}.›
theorem padic_complete: "padic.mcomplete"
unfolding padic.mcomplete_def
proof (intro allI impI)
fix σ assume cauchy: "padic.MCauchy σ"
text ‹Step 1: Reduce to bounded sequences.
Every Cauchy sequence in $\mathbb{Q}_p$ is eventually in some ball @{term ‹c_ball 0 c›}.
By rescaling (multiplying by a power of $p$), we can reduce to a
sequence in $\mathbb{Z}_p$ (i.e., with non-negative valuation).›
have σ_range: "range σ ⊆ carrier Q⇩p"
using cauchy padic.MCauchy_def by auto
obtain c N where c_car: "c ∈ carrier Q⇩p"
and eventually_in_ball: "∀m ≥ N. σ m ∈ c_ball 0 c"
proof -
obtain N where hN: "∀n n'. N ≤ n ⟶ N ≤ n' ⟶ padic_dist (σ n) (σ n') < 1"
using cauchy[unfolded padic.MCauchy_def] by (meson zero_less_one)
have σN_car: "σ N ∈ carrier Q⇩p"
using σ_range by auto
have "∀m ≥ N. σ m ∈ c_ball 0 (σ N)"
proof (intro allI impI)
fix m assume "N ≤ m"
then have "padic_dist (σ N) (σ m) < 1" using hN by auto
then have "padic_dist (σ N) (σ m) ≤ real_of_int p powr (- real_of_int 0)"
using p_ge_1_real by simp
then have "σ m ∈ padic.mcball (σ N) (real_of_int p powr (- real_of_int 0))"
using padic.in_mcball σN_car σ_range by auto
then show "σ m ∈ c_ball 0 (σ N)"
using c_ball_eq_mcball[OF σN_car] by simp
qed
then show thesis using that σN_car by blast
qed
text ‹Step 2: Translate metric Cauchy to val-based Cauchy.
Show that @{term padic.MCauchy} (in @{term padic_dist}) implies that
for all $n$, eventually $\mathrm{val}(\sigma_m - \sigma_k) \ge n$.›
have val_cauchy: "∃K. ∀m k. m ≥ K ⟶ k ≥ K ⟶ eint n ≤ val (σ m ⊖ σ k)" for n
proof -
have "real_of_int p powr (- real_of_int n) > 0"
using p_gt_1 by (simp add: powr_gt_zero)
then obtain K where hK: "∀m k. K ≤ m ⟶ K ≤ k ⟶ padic_dist (σ m) (σ k) < real_of_int p powr (- real_of_int n)"
using cauchy[unfolded padic.MCauchy_def] by (meson less_le_not_le)
show "∃K. ∀m k. m ≥ K ⟶ k ≥ K ⟶ eint n ≤ val (σ m ⊖ σ k)"
proof (intro exI allI impI)
fix m k assume "K ≤ m" "K ≤ k"
then have dist_bound: "padic_dist (σ m) (σ k) < real_of_int p powr (- real_of_int n)"
using hK by auto
have σm_car: "σ m ∈ carrier Q⇩p" and σk_car: "σ k ∈ carrier Q⇩p"
using σ_range by auto
have diff_car: "σ m ⊖ σ k ∈ carrier Q⇩p"
using Qp.minus_closed σm_car σk_car by auto
show "eint n ≤ val (σ m ⊖ σ k)"
proof (cases "σ m ⊖ σ k = 𝟬")
case True
then show ?thesis using val_zero by simp
next
case False
then have diff_nz: "σ m ⊖ σ k ∈ nonzero Q⇩p"
using Qp.nonzero_memI diff_car by auto
have norm_eq: "padic_norm (σ m ⊖ σ k) = real_of_int p powr (- real_of_int (ord (σ m ⊖ σ k)))"
using padic_norm_def False by auto
have "padic_norm (σ m ⊖ σ k) < real_of_int p powr (- real_of_int n)"
using dist_bound padic_dist_as_norm σm_car σk_car by auto
then have "- real_of_int (ord (σ m ⊖ σ k)) < - real_of_int n"
using local.norm_eq p_gt_1_real by force
then have "n ≤ ord (σ m ⊖ σ k)" by linarith
then show ?thesis
using val_ord diff_nz eint_ord_code(1) by auto
qed
qed
qed
text ‹Step 3: Reduce to $\mathbb{Z}_p$.
After shifting/rescaling, express the (tail of the) sequence as
$\iota \circ s$ for some $s : \mathbb{N} \to \mathrm{carrier}\; \mathbb{Z}_p$,
then show $s$ is @{term is_Zp_cauchy}.›
define s where "s m = to_Zp (σ m ⊖ c)" for m
have s_Zp: "s m ∈ carrier Z⇩p" for m
proof -
have "σ m ⊖ c ∈ carrier Q⇩p" using Qp.minus_closed c_car σ_range by auto
then show ?thesis unfolding s_def using to_Zp_closed by auto
qed
have diff_in_val_ring: "σ m ⊖ c ∈ 𝒪⇩p" if "N ≤ m" for m
proof -
have "σ m ∈ c_ball 0 c" using that eventually_in_ball by auto
then show ?thesis
by (simp add: Qp_val_ringI c_ballE c_car zero_eint_def)
qed
have s_eq: "σ m = ι (s m) ⊕ c" if "N ≤ m" for m
proof -
have in_val: "σ m ⊖ c ∈ 𝒪⇩p" using diff_in_val_ring that by auto
have "ι (s m) = ι (to_Zp (σ m ⊖ c))" unfolding s_def by simp
also have "… = σ m ⊖ c" using to_Zp_inc[OF in_val] by simp
finally have inc_eq: "ι (s m) = σ m ⊖ c" .
have "σ m ∈ carrier Q⇩p" using σ_range by auto
then show "σ m = ι (s m) ⊕ c"
by (metis inc_eq c_car Qp.add.inv_solve_right Qp.minus_closed a_minus_def)
qed
have s_closed: "s ∈ carrier Z⇩p⇗ω⇖"
using s_Zp closed_seqs_memI by auto
have s_val_cauchy: "∃M. ∀m k. M < m ∧ M < k ⟶ eint n < val_Zp_dist (s m) (s k)" for n
proof -
obtain K where hK: "∀m k. m ≥ K ⟶ k ≥ K ⟶ eint (n + 1) ≤ val (σ m ⊖ σ k)"
using val_cauchy by (meson le_cases)
define K' where "K' = max N K"
show "∃M. ∀m k. M < m ∧ M < k ⟶ eint n < val_Zp_dist (s m) (s k)"
proof (intro exI strip)
fix m k assume mk: "K' < m ∧ K' < k"
then have hm: "m ≥ N" "m ≥ K" and hk: "k ≥ N" "k ≥ K"
unfolding K'_def by auto
have sm_car: "s m ∈ carrier Z⇩p" and sk_car: "s k ∈ carrier Z⇩p"
using s_Zp by auto
have diff_Zp: "s m ⊖⇘Z⇩p⇙ s k ∈ carrier Z⇩p"
using Zp.minus_closed sm_car sk_car by auto
have "val_Zp_dist (s m) (s k) = val_Zp (s m ⊖⇘Z⇩p⇙ s k)"
using val_Zp_dist_def by auto
also have "… = val (ι (s m ⊖⇘Z⇩p⇙ s k))"
using val_of_inc[OF diff_Zp] by simp
also have "… = val (ι (s m) ⊖ ι (s k))"
using inc_of_diff[OF sm_car sk_car] by simp
also have "… = val ((σ m ⊖ c) ⊖ (σ k ⊖ c))"
using diff_in_val_ring hk(1) hm(1) s_def to_Zp_inc by presburger
also have "… = val (σ m ⊖ σ k)"
by (metis Qp_diff_diff c_ballE(1) c_car eventually_in_ball hk(1) hm(1))
finally have val_eq: "val_Zp_dist (s m) (s k) = val (σ m ⊖ σ k)" .
have "eint (n + 1) ≤ val (σ m ⊖ σ k)"
using hK hm(2) hk(2) by auto
then show "eint n < val_Zp_dist (s m) (s k)"
using val_eq Suc_ile_eq by auto
qed
qed
have s_cauchy: "is_Zp_cauchy s"
using s_closed s_val_cauchy is_Zp_cauchy_def by auto
text ‹Step 4: Apply $\mathbb{Z}_p$ completeness.
Use @{thm [source] is_Zp_cauchy_imp_has_limit} to get the limit in $\mathbb{Z}_p$,
then map it back to $\mathbb{Q}_p$.›
define a where "a = res_lim s"
have a_Zp: "a ∈ carrier Z⇩p"
using s_cauchy res_lim_in_Zp a_def by auto
have Zp_conv: "Zp_converges_to s a"
using is_Zp_cauchy_imp_has_limit s_cauchy a_def by auto
text ‹Step 5: Translate $\mathbb{Z}_p$ convergence back to $\mathbb{Q}_p$ metric convergence.
Show @{term ‹Zp_converges_to s a›} implies
@{term ‹limitin padic.mtopology σ L sequentially›}.
Key bridge: @{thm [source] val_of_inc}, @{thm [source] inc_of_diff}, and the characterization
@{thm [source] padic.limitin_metric_dist_null}.›
define L where "L = ι a ⊕ c"
have L_car: "L ∈ carrier Q⇩p"
unfolding L_def using Qp.a_closed[OF inc_closed[OF a_Zp] c_car] by simp
have inc_a_car: "ι a ∈ carrier Q⇩p" using inc_closed a_Zp by auto
have "limitin padic.mtopology σ L sequentially"
unfolding padic.limitin_metric_dist_null
proof (intro conjI)
show "L ∈ carrier Q⇩p" by (rule L_car)
next
show "∀⇩F m in sequentially. σ m ∈ carrier Q⇩p"
using σ_range by (simp add: eventually_sequentially, intro exI[of _ 0]) auto
next
show "((λm. padic_dist (σ m) L) ⤏ 0) sequentially"
proof (rule metric_LIMSEQ_I)
fix r :: real assume "r > 0"
define n where "n = ⌈- log (real_of_int p) r⌉ + 1"
have n_bound: "real_of_int n > - log (real_of_int p) r"
unfolding n_def using le_of_int_ceiling[of "- log (real_of_int p) r"]
by linarith
have p_powr_bound: "real_of_int p powr (- real_of_int n) < r"
using ‹0 < r› n_bound p_gt_1_real powr_less_iff by auto
have "∃k. ∀m>k. eint n < val_Zp (s m ⊖⇘Z⇩p⇙ a)"
using Zp_conv[unfolded Zp_converges_to_def] by blast
then obtain K where hK: "∀m>K. eint n < val_Zp (s m ⊖⇘Z⇩p⇙ a)"
by auto
define M where "M = max (nat (K + 1)) N"
show "∃no. ∀m≥no. dist ((λm. padic_dist (σ m) L) m) 0 < r"
proof (intro exI allI impI)
fix m assume hm: "M ≤ m"
have m_ge_N: "m ≥ N" and m_gt_K: "m > K"
using hm unfolding M_def by linarith+
have σm_car: "σ m ∈ carrier Q⇩p" using σ_range by auto
have sm_car: "s m ∈ carrier Z⇩p" using s_Zp by auto
have diff_car: "s m ⊖⇘Z⇩p⇙ a ∈ carrier Z⇩p"
using Zp.minus_closed[OF sm_car a_Zp] by auto
have inc_sm: "ι (s m) = σ m ⊖ c"
using s_eq m_ge_N σm_car c_car
by (metis diff_in_val_ring s_def to_Zp_inc)
have "ι (s m ⊖⇘Z⇩p⇙ a) = ι (s m) ⊖ ι a"
using inc_of_diff[OF sm_car a_Zp] by simp
also have "… = (σ m ⊖ c) ⊖ ι a"
using inc_sm by simp
also have "… = σ m ⊖ (c ⊕ ι a)"
using Qp.right_inv_add[OF c_car inc_a_car σm_car] by simp
also have "… = σ m ⊖ (ι a ⊕ c)"
using Qp.a_comm[OF c_car inc_a_car] by simp
also have "… = σ m ⊖ L" unfolding L_def by simp
finally have key_eq: "ι (s m ⊖⇘Z⇩p⇙ a) = σ m ⊖ L" .
have val_bound: "eint n < val_Zp (s m ⊖⇘Z⇩p⇙ a)"
using hK m_gt_K by auto
have val_inc: "val_Zp (s m ⊖⇘Z⇩p⇙ a) = val (ι (s m ⊖⇘Z⇩p⇙ a))"
using val_of_inc[OF diff_car] by simp
have val_diff: "eint n < val (σ m ⊖ L)"
using val_bound val_inc key_eq by simp
have diff_car2: "σ m ⊖ L ∈ carrier Q⇩p"
using Qp.minus_closed[OF σm_car L_car] by simp
have dist_eq: "padic_dist (σ m) L = padic_norm (σ m ⊖ L)"
using padic_dist_as_norm[OF σm_car L_car] by simp
show "dist ((λm. padic_dist (σ m) L) m) 0 < r"
proof (cases "σ m ⊖ L = 𝟬")
case True
then have "padic_dist (σ m) L = 0"
using dist_eq padic_norm_def by simp
then show ?thesis using ‹r > 0› by (simp add: dist_real_def)
next
case False
have nz: "σ m ⊖ L ∈ nonzero Q⇩p"
using Qp.nonzero_memI[OF diff_car2 False] by simp
have val_eq: "val (σ m ⊖ L) = eint (ord (σ m ⊖ L))"
using val_ord[OF nz] by simp
have ord_bound: "n < ord (σ m ⊖ L)"
using val_diff val_eq by simp
have neg_ord_bound: "- real_of_int (ord (σ m ⊖ L)) < - real_of_int n"
using ord_bound by linarith
have norm_eq: "padic_norm (σ m ⊖ L) = real_of_int p powr (- real_of_int (ord (σ m ⊖ L)))"
using padic_norm_def False by simp
have "padic_norm (σ m ⊖ L) < real_of_int p powr (- real_of_int n)"
using norm_eq powr_less_mono[OF neg_ord_bound p_gt_1_real] by simp
then have "padic_dist (σ m) L < r"
using dist_eq p_powr_bound by linarith
then show ?thesis
using padic_dist_nonneg[of "σ m" L] by (simp add: dist_real_def)
qed
qed
qed
qed
then show "∃x. limitin padic.mtopology σ x sequentially"
by blast
qed
end
end