Theory More_pAdic_Product
theory More_pAdic_Product
imports Fin_Field_Product
begin
section ‹Compactness of local ring of integers›
subsection ‹Preliminaries›
lemma infinite_vimageE:
fixes f :: "'a ⇒ 'b"
assumes "infinite (UNIV :: 'a set)" and "range f ⊆ B" and "finite B"
obtains b where "b ∈ B" and "infinite (f -` {b})"
proof-
from assms(2) have "f -` B = UNIV" using subsetD rangeI by blast
with assms(1,3) have "¬ (∀b∈B. finite (f -` {b}))"
using finite_UN[of B "λb. f -` {b}"] vimage_eq_UN[of f B] by argo
from this obtain b where "b ∈ B" and "infinite (f -` {b})" by blast
with that show ?thesis by fast
qed
primrec subset_subseq ::
"(nat ⇒ 'a) ⇒ 'a set ⇒ nat ⇒ nat"
where
"subset_subseq f A 0 = (LEAST k. f k ∈ A)" |
"subset_subseq f A (Suc n) = (LEAST k. k > subset_subseq f A n ∧ f k ∈ A)"
lemma
assumes "infinite (f -` A)"
shows subset_subseq_strict_mono: "strict_mono (subset_subseq f A)"
and subset_subseq_range : "f (subset_subseq f A n) ∈ A"
proof-
from assms have "f -` A ≠ {}" by auto
hence "∃k. f k ∈ A" by blast
hence ex_first:
"∃!k. f k ∈ A ∧ (∀j. f j ∈ A ⟶ k ≤ j)"
using ex_ex1_least_nat_le by simp
define P where "P ≡ λN k. k > N ∧ f k ∈ A"
have "⋀N. (f -` A) ∩ {N<..} ≠ {}"
proof
fix N assume "(f -` A) ∩ {N<..} = {}"
hence "(f -` A) ⊆ {..N}" by fastforce
with assms show False using finite_subset by fast
qed
with P_def have "⋀N. ∃k. P N k" by fast
hence ex_next:
"⋀N. ∃!k. P N k ∧ (∀j. P N j ⟶ k ≤ j)"
using ex_ex1_least_nat_le by force
from P_def show "f (subset_subseq f A n) ∈ A"
using Least1I[OF ex_first] Least1I[OF ex_next] by (cases n) auto
from P_def have step: "⋀n. subset_subseq f A (Suc n) > subset_subseq f A n"
using Least1I[OF ex_next] by auto
show "strict_mono (subset_subseq f A)"
proof
fix m n show "m < n ⟹ subset_subseq f A m < subset_subseq f A n"
proof (induct n)
case (Suc n) thus ?case using step[of n] by (cases "n = m") simp_all
qed simp
qed
qed
subsection ‹Sequential compactness›
subsubsection ‹Creating a Cauchy subsequence›
abbreviation
"p_adic_prod_int_convergent_subseq_seq_step p X g n ≡
λk. p_adic_prod_int_quot (p_adic_prod_shift_p_depth p (- int n) ((X (g k) - X (g 0))))"
primrec p_adic_prod_int_convergent_subseq_seq ::
"'a::nontrivial_factorial_unique_euclidean_bezout prime ⇒
(nat ⇒ 'a p_adic_prod) ⇒ nat ⇒ (nat ⇒ nat)"
where "p_adic_prod_int_convergent_subseq_seq p X 0 = id" |
"p_adic_prod_int_convergent_subseq_seq p X (Suc n) =
p_adic_prod_int_convergent_subseq_seq p X n ∘
subset_subseq
(
p_adic_prod_int_convergent_subseq_seq_step p X (
p_adic_prod_int_convergent_subseq_seq p X n
) n
)
{SOME z.
infinite (
p_adic_prod_int_convergent_subseq_seq_step p X (
p_adic_prod_int_convergent_subseq_seq p X n
) n
-` {z}
)
}"
abbreviation
"p_adic_prod_int_convergent_subseq p X n ≡
p_adic_prod_int_convergent_subseq_seq p X n n"
lemma restricted_X_infinite_quot_vimage:
"∃z. infinite ((λk. p_adic_prod_int_quot (X k)) -` {z})"
if fin_p_quot : "finite (range (λx::'a adelic_int_quot. x prestrict ((=) p)))"
and range_X : "range X ⊆ 𝒪⇩∀⇩p"
and restricted_X: "∀n. X n = (X n) prestrict ((=) p)"
for p :: "'a::nontrivial_factorial_idom prime" and X :: "nat ⇒ 'a p_adic_prod"
proof-
define resp where "resp ≡ λx::'a adelic_int_quot. x prestrict ((=) p)"
define X_quot where "X_quot ≡ λk. p_adic_prod_int_quot (X k)"
have "range X_quot ⊆ range resp"
proof safe
fix k
from range_X restricted_X X_quot_def resp_def have
"X_quot k = resp (adelic_int_quot (Abs_adelic_int (X k)))"
using p_restrict_adelic_int_abs_eq p_restrict_adelic_int_quot_abs_eq rangeI subsetD by metis
thus "X_quot k ∈ range resp" by simp
qed
with fin_p_quot resp_def obtain b where "b ∈ range resp" and "infinite (X_quot -` {b})"
using infinite_vimageE by blast
with X_quot_def show ?thesis by fast
qed
context
fixes p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime"
and X :: "nat ⇒ 'a p_adic_prod"
and ss :: "nat ⇒ (nat ⇒ nat)"
and ss_step :: "nat ⇒ (nat ⇒ 'a adelic_int_quot)"
and nth_im :: "nat ⇒ 'a adelic_int_quot"
and subss :: "nat ⇒ (nat ⇒ nat)"
defines
"ss ≡ p_adic_prod_int_convergent_subseq_seq p X"
and
"ss_step ≡ λn. p_adic_prod_int_convergent_subseq_seq_step p X (ss n) n"
and "nth_im ≡ λn. (SOME z. infinite (ss_step n -` {z}))"
and "subss ≡ λn. subset_subseq (ss_step n) {nth_im n}"
assumes fin_p_quot : "finite (range (λx::'a adelic_int_quot. x prestrict ((=) p)))"
and range_X : "range X ⊆ 𝒪⇩∀⇩p"
and restricted_X: "∀n. X n = (X n) prestrict ((=) p)"
begin
lemma p_adic_prod_int_convergent_subseq_seq_step_infinite_quot_vimage:
"∃z. infinite (ss_step n -` {z})" (is ?A)
and p_adic_prod_int_convergent_subseq_seq_step_depth:
"∀k. (X (ss n k)) ¬≃⇩p (X (ss n 0)) ⟶
((X (ss n k) - X (ss n 0))°⇧p) ≥ int n"
(is ?B)
proof-
have "?A ∧ ?B"
proof (induct n)
case 0
from range_X have "range (λk. X k - X 0) ⊆ 𝒪⇩∀⇩p"
using global_p_depth_p_adic_prod.global_depth_set_minus by fastforce
moreover from restricted_X have
"∀k. X k - X 0 = (X k - X 0) prestrict (=) p"
using global_p_depth_p_adic_prod.p_restrict_minus by metis
ultimately
have A: "∃z. infinite ((λk. p_adic_prod_int_quot (X k - X 0)) -` {z})"
using fin_p_quot restricted_X_infinite_quot_vimage
by blast
from ss_def range_X have B:
"∀k. (X (ss 0 k)) ¬≃⇩p (X (ss 0 0)) ⟶
int 0 ≤ ((X (ss 0 k) - X (ss 0 0))°⇧p)"
using global_p_depth_p_adic_prod.global_depth_set_minus
p_equality_p_adic_prod.conv_0 global_p_depth_p_adic_prod.global_depth_setD
by fastforce
with ss_step_def ss_def show
"(∃z. infinite (ss_step 0 -` {z})) ∧
(∀k. (X (ss 0 k)) ¬≃⇩p (X (ss 0 0)) ⟶
int 0 ≤ ((X (ss 0 k) - X (ss 0 0))°⇧p))"
using A B by simp
next
case (Suc n)
hence inf : "∃z. infinite (ss_step n -` {z})"
and depth:
"⋀k. (X (ss n k)) ¬≃⇩p (X (ss n 0)) ⟹
int n ≤ ((X (ss n k) - X (ss n 0))°⇧p)"
by auto
from nth_im_def have inf_nth_vimage: "infinite (ss_step n -` {nth_im n})"
using someI_ex[OF inf] by blast
from subss_def have ss_step_kth: "∀k. ss_step n (subss n k) = nth_im n"
using subset_subseq_range[OF inf_nth_vimage] by blast
have
"⋀k.
p_adic_prod_shift_p_depth p (- int n) ((X (ss n k) - X (ss n 0)) prestrict ((=) p))
∈ 𝒪⇩∀⇩p"
using p_adic_prod_depth_embeds.shift_p_depth_p_restrict_global_depth_set_memI
depth p_equality_p_adic_prod.conv_0
by fastforce
with restricted_X have depth_set:
"⋀k.
p_adic_prod_shift_p_depth p (- int n) (X (ss n k) - X (ss n 0))
∈ 𝒪⇩∀⇩p"
using global_p_depth_p_adic_prod.p_restrict_minus by metis
have B:
"∀k. (X (ss (Suc n) k)) ¬≃⇩p (X (ss (Suc n) 0)) ⟶
((X (ss (Suc n) k) - X (ss (Suc n) 0))°⇧p) ≥ int (Suc n)"
proof clarify
fix k assume k: "(X (ss (Suc n) k)) ¬≃⇩p (X (ss (Suc n) 0))"
from ss_def ss_step_def subss_def nth_im_def
have X_Suc_n_k: "X (ss (Suc n) k) = X (ss n (subss n k))"
and X_Suc_n_0: "X (ss (Suc n) 0) = X (ss n (subss n 0))"
by auto
from ss_step_def have
"p_adic_prod_shift_p_depth p (- int n) (X (ss (Suc n) 0) - X (ss (Suc n) k))
∈ 𝒫⇩∀⇩p"
using depth_set X_Suc_n_k X_Suc_n_0 ss_step_kth p_adic_prod_int_quot_eq_iff
p_adic_prod_depth_embeds.shift_p_depth_minus
by fastforce
with k show "((X (ss (Suc n) k) - X (ss (Suc n) 0))°⇧p) ≥ int (Suc n)"
using p_adic_prod_depth_embeds.shift_p_depth_mem_global_depth_set
p_equality_p_adic_prod.sym[of p] global_p_depth_p_adic_prod.depth_diff[of p]
p_equality_p_adic_prod.conv_0[of p "X (ss (Suc n) 0)"]
by fastforce
qed
from ss_step_def ss_def have ss_step_Suc_n:
"ss_step (Suc n) = (λk.
p_adic_prod_int_quot (
p_adic_prod_shift_p_depth p (- int (Suc n)) ((X (ss (Suc n) k) - X (ss (Suc n) 0)))
)
)"
by presburger
moreover have
"∃z. infinite (
(λk.
p_adic_prod_int_quot (
p_adic_prod_shift_p_depth p (-int (Suc n)) ((X (ss (Suc n) k) - X (ss (Suc n) 0)))
)
) -` {z}
)"
proof (intro restricted_X_infinite_quot_vimage, rule fin_p_quot, safe)
fix k
have
"p_adic_prod_shift_p_depth p (- int (Suc n)) (
(X (ss (Suc n) k) - X (ss (Suc n) 0)) prestrict ((=) p)
) ∈ 𝒪⇩∀⇩p"
using B p_adic_prod_depth_embeds.shift_p_depth_p_restrict_global_depth_set_memI
p_equality_p_adic_prod.conv_0
by fastforce
with restricted_X show
"p_adic_prod_shift_p_depth p (- int (Suc n)) (X (ss (Suc n) k) - X (ss (Suc n) 0))
∈ 𝒪⇩∀⇩p"
using global_p_depth_p_adic_prod.p_restrict_minus by metis
from restricted_X show
"p_adic_prod_shift_p_depth p (- int (Suc n)) (X (ss (Suc n) k) - X (ss (Suc n) 0)) =
p_adic_prod_shift_p_depth p (- int (Suc n)) (
X (ss (Suc n) k) - X (ss (Suc n) 0)
) prestrict (=) p"
using p_adic_prod_depth_embeds.shift_p_depth_p_restrict
global_p_depth_p_adic_prod.p_restrict_minus
by metis
qed
ultimately have A: "∃z. infinite (ss_step (Suc n) -` {z})" by presburger
show
"(∃z. infinite (ss_step (Suc n) -` {z})) ∧
(∀k. (X (ss (Suc n) k)) ¬≃⇩p (X (ss (Suc n) 0)) ⟶
int (Suc n) ≤ ((X (ss (Suc n) k) - X (ss (Suc n) 0))°⇧p))"
using A B by blast
qed
thus ?A and ?B by auto
qed
lemma p_adic_prod_int_convergent_subset_subseq_strict_mono:
"strict_mono (subset_subseq (ss_step n) {nth_im n})"
using ss_step_def nth_im_def p_adic_prod_int_convergent_subseq_seq_step_infinite_quot_vimage
subset_subseq_strict_mono someI_ex
by fast
lemma p_adic_prod_int_convergent_subseq_strict_mono': "strict_mono (ss n)"
proof (induct n)
case (Suc n) from ss_def ss_step_def nth_im_def show "strict_mono (ss (Suc n))"
using ss_def ss_step_def nth_im_def strict_monoD[OF Suc]
strict_monoD[OF p_adic_prod_int_convergent_subset_subseq_strict_mono]
by (force intro: strict_mono_onI)
qed (simp add: ss_def strict_mono_id flip: id_def)
lemma p_adic_prod_int_convergent_subseq_strict_mono:
"strict_mono (p_adic_prod_int_convergent_subseq p X)"
proof (rule iffD2, rule strict_mono_Suc_iff, clarify)
fix n :: nat
have "Suc n ≤ subset_subseq (ss_step n) {nth_im n} (Suc n)"
using strict_mono_imp_increasing p_adic_prod_int_convergent_subset_subseq_strict_mono by fast
hence "n < subset_subseq (ss_step n) {nth_im n} (Suc n)" by linarith
with ss_def ss_step_def nth_im_def
show "p_adic_prod_int_convergent_subseq p X n < p_adic_prod_int_convergent_subseq p X (Suc n)"
using ss_def strict_monoD p_adic_prod_int_convergent_subseq_strict_mono'
by auto
qed
lemma p_adic_prod_int_convergent_subseq_Cauchy:
"p_adic_prod_p_cauchy p (X ∘ p_adic_prod_int_convergent_subseq p X)"
proof (rule iffD2, rule global_p_depth_p_adic_prod.p_consec_cauchy, clarify)
fix n
define C where "C ≡ X ∘ p_adic_prod_int_convergent_subseq p X"
have
"global_p_depth_p_adic_prod.p_consec_cauchy_condition p C n (nat (n + 1))"
unfolding global_p_depth_p_adic_prod.p_consec_cauchy_condition_def
proof clarify
fix k :: nat
assume k: "k ≥ nat (n + 1)" "(C (Suc k)) ¬≃⇩p (C k)"
define D0 D1 D2
where "D0 ≡ C (Suc k) - C k"
and "D1 ≡ X (ss k (subss k (Suc k))) - X (ss k 0)"
and "D2 ≡ X (ss k k) - X (ss k 0)"
with C_def ss_def ss_step_def subss_def nth_im_def have D0_eq: "D0 = D1 - D2"
by (force simp add: algebra_simps)
from k(2) D0_def have D0_nequiv0: "D0 ¬≃⇩p 0"
using p_equality_p_adic_prod.conv_0 by fast
consider (D1) "D1 ≃⇩p 0" | (D2) "D2 ≃⇩p 0" |
(neither) "D1 ¬≃⇩p 0" "D2 ¬≃⇩p 0"
by blast
thus "(D0°⇧p) > n"
proof cases
case D1
moreover from this have "D2 ¬≃⇩p 0"
using D0_eq D0_nequiv0 p_equality_p_adic_prod.minus by fastforce
ultimately show ?thesis
using k(1) D2_def D0_eq global_p_depth_p_adic_prod.depth_diff_equiv0_left
p_equality_p_adic_prod.conv_0 p_adic_prod_int_convergent_subseq_seq_step_depth
by fastforce
next
case D2
moreover from this have "D1 ¬≃⇩p 0"
using D0_eq D0_nequiv0 p_equality_p_adic_prod.minus by fastforce
ultimately show ?thesis
using k(1) D1_def D0_eq global_p_depth_p_adic_prod.depth_diff_equiv0_right
p_equality_p_adic_prod.conv_0 p_adic_prod_int_convergent_subseq_seq_step_depth
by fastforce
next
case neither
moreover from this D1_def D2_def
have "k ≤ min (D1°⇧p) (D2°⇧p)"
using p_equality_p_adic_prod.conv_0 p_adic_prod_int_convergent_subseq_seq_step_depth
by fastforce
ultimately show ?thesis
using k(1) D0_eq D0_nequiv0 global_p_depth_p_adic_prod.depth_nonarch_diff by fastforce
qed
qed
thus "∃K. global_p_depth_p_adic_prod.p_consec_cauchy_condition p C n K" by blast
qed
lemma p_adic_prod_int_convergent_subseq_limseq:
"x ∈ (λz. z prestrict ((=) p)) ` 𝒪⇩∀⇩p"
if "p_adic_prod_p_open_nbhds_limseq (X ∘ g) x"
proof (intro image_eqI global_p_depth_p_adic_prod.global_imp_eq, standard)
fix q :: "'a prime"
show "x ≃⇩q x prestrict ((=) p)"
proof (cases "q = p")
case False
moreover from that have "p_adic_prod_p_limseq q (X ∘ g) x"
using global_p_depth_p_adic_prod.globally_limseq_imp_locally_limseq by fast
moreover from restricted_X have "∀n. (X ∘ g) n = (X ∘ g) n prestrict (=) p"
by force
ultimately show "x ≃⇩q (x prestrict ((=) p))"
using global_p_depth_p_adic_prod.p_restrict_equiv0
global_p_depth_p_adic_prod.p_limseq_p_constant
global_p_depth_p_adic_prod.p_limseq_unique p_equality_p_adic_prod.trans_left[of q x 0]
by (metis (full_types))
qed (simp add: global_p_depth_p_adic_prod.p_restrict_equiv[symmetric])
from that range_X show "x ∈ 𝒪⇩∀⇩p"
using eventually_sequentially
global_p_depth_p_adic_prod.global_depth_set_p_open_nbhds_LIMSEQ_closed
by force
qed
end
subsubsection ‹Proving sequential compactness›
context
fixes p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime"
assumes fin_p_quot: "finite (range (λx::'a adelic_int_quot. x prestrict ((=) p)))"
begin
lemma p_adic_prod_local_int_ring_seq_compact':
"∃g::nat⇒nat. strict_mono g ∧ p_adic_prod_p_cauchy p (X ∘ g)"
if range_X:
"range X ⊆ (λx. x prestrict ((=) p)) ` (𝒪⇩∀⇩p)"
for X :: "nat ⇒ 'a p_adic_prod"
proof-
define g where "g ≡ p_adic_prod_int_convergent_subseq p X"
from range_X have "range X ⊆ 𝒪⇩∀⇩p"
using global_p_depth_p_adic_prod.global_depth_set_closed_under_p_restrict_image by force
moreover from range_X have "∀n. X n = X n prestrict ((=) p)"
using subsetD
global_p_depth_p_adic_prod.p_restrict_image_restrict[of
"X _" "(=) p" "𝒪⇩∀⇩p"
]
by force
ultimately have "strict_mono g" and "p_adic_prod_p_cauchy p (X ∘ g)"
using g_def fin_p_quot p_adic_prod_int_convergent_subseq_Cauchy[of p X]
p_adic_prod_int_convergent_subseq_strict_mono
by (blast, presburger)
thus ?thesis by blast
qed
lemma p_adic_prod_local_int_ring_seq_compact:
"∃x∈(λx. x prestrict ((=) p)) ` (𝒪⇩∀⇩p).
∃g::nat⇒nat.
strict_mono g ∧ p_adic_prod_p_open_nbhds_limseq (X ∘ g) x"
if range_X:
"range X ⊆ (λx. x prestrict ((=) p)) ` (𝒪⇩∀⇩p)"
for X :: "nat ⇒ 'a p_adic_prod"
proof-
from range_X have 1: "range X ⊆ 𝒪⇩∀⇩p"
using global_p_depth_p_adic_prod.global_depth_set_closed_under_p_restrict_image by force
moreover from range_X have 2: "∀n. X n = X n prestrict ((=) p)"
using subsetD
global_p_depth_p_adic_prod.p_restrict_image_restrict[of
"X _" "(=) p" "𝒪⇩∀⇩p"
]
by force
from range_X obtain g where g: "strict_mono g" "p_adic_prod_p_cauchy p (X ∘ g)"
using p_adic_prod_local_int_ring_seq_compact' by blast
from g(2) obtain x
where "p_adic_prod_p_open_nbhds_limseq (λn. (X ∘ g) n prestrict (=) p) x "
using p_complete_p_adic_prod.p_cauchyE
by blast
moreover have "(λn. (X ∘ g) n prestrict (=) p) = X ∘ g" using 2 by auto
ultimately have "p_adic_prod_p_open_nbhds_limseq (X ∘ g) x" by auto
moreover from this fin_p_quot
have "x ∈ (λx. x prestrict ((=) p)) ` (𝒪⇩∀⇩p)"
using 1 2 p_adic_prod_int_convergent_subseq_limseq
by blast
ultimately show ?thesis using g(1) by blast
qed
lemma adelic_int_local_int_ring_seq_abs:
"range X ⊆ (λx. x prestrict ((=) p)) ` (𝒪⇩∀⇩p)"
if range_X: "range X ⊆ 𝒪⇩∀⇩p"
and range_abs_X:
"range (λk. Abs_adelic_int (X k)) ⊆ range (λx. x prestrict ((=) p))"
for X :: "nat ⇒ 'a p_adic_prod"
proof (standard, clarify, rule image_eqI)
fix n
from range_X show *: "X n ∈ 𝒪⇩∀⇩p" by fast
from range_abs_X obtain y where "Abs_adelic_int (X n) = y prestrict ((=) p)" by blast
from this obtain x
where "x ∈ 𝒪⇩∀⇩p"
and "Abs_adelic_int (X n) = Abs_adelic_int (x prestrict ((=) p))"
using Abs_adelic_int_cases p_restrict_adelic_int_abs_eq
by metis
thus "X n = X n prestrict ((=) p)"
using * global_p_depth_p_adic_prod.global_depth_set_p_restrict Abs_adelic_int_inject
global_p_depth_p_adic_prod.p_restrict_restrict'
by force
qed
lemma adelic_int_local_int_ring_seq_compact':
"∃g::nat⇒nat. strict_mono g ∧ adelic_int_p_cauchy p (X ∘ g)"
if range_X:
"range X ⊆ (λx. x prestrict ((=) p)) ` (𝒪⇩∀⇩p)"
for X :: "nat ⇒ 'a adelic_int"
proof (cases X rule : adelic_int_seq_cases)
case (Abs_adelic_int F)
with range_X
have "range F ⊆ (λx. x prestrict ((=) p)) ` (𝒪⇩∀⇩p)"
using adelic_int_local_int_ring_seq_abs
by fast
with fin_p_quot obtain g where g: "strict_mono g" "p_adic_prod_p_cauchy p (F ∘ g)"
using p_adic_prod_local_int_ring_seq_compact' by blast
moreover from Abs_adelic_int(1)
have "(λn. Abs_adelic_int ((F ∘ g) n)) = X ∘ g"
by fastforce
moreover from Abs_adelic_int(2)
have "range (F ∘ g) ⊆ 𝒪⇩∀⇩p"
by auto
ultimately have "adelic_int_p_cauchy p (X ∘ g)" using adelic_int_p_cauchy_abs_eq by metis
with g(1) show ?thesis by blast
qed
lemma adelic_int_local_int_ring_seq_compact:
"∃x∈range (λx. x prestrict ((=) p)).
∃g::nat⇒nat.
strict_mono g ∧ adelic_int_p_open_nbhds_limseq (X ∘ g) x"
if range_X:
"range X ⊆ range (λx. x prestrict ((=) p))"
for X :: "nat ⇒ 'a adelic_int"
proof (cases X rule : adelic_int_seq_cases)
case (Abs_adelic_int F)
with range_X
have "range F ⊆ (λx. x prestrict ((=) p)) ` (𝒪⇩∀⇩p)"
using adelic_int_local_int_ring_seq_abs
by fast
with fin_p_quot obtain y g
where y : "y ∈ (λx. x prestrict (=) p) ` 𝒪⇩∀⇩p"
and g : "strict_mono g"
and g_y: "p_adic_prod_p_open_nbhds_limseq (F ∘ g) y"
using p_adic_prod_local_int_ring_seq_compact by blast
from y have "y ∈ 𝒪⇩∀⇩p"
using global_p_depth_p_adic_prod.global_depth_set_closed_under_p_restrict_image by auto
moreover from Abs_adelic_int(2)
have "range (F ∘ g) ⊆ 𝒪⇩∀⇩p"
by force
ultimately have
"adelic_int_p_open_nbhds_limseq
(λk. Abs_adelic_int ((F ∘ g) k)) (Abs_adelic_int y)"
using g_y adelic_int_p_open_nbhds_limseq_abs_eq
by blast
moreover from Abs_adelic_int(1)
have "(λk. Abs_adelic_int ((F ∘ g) k)) = X ∘ g"
by fastforce
ultimately have lim: "adelic_int_p_open_nbhds_limseq (X ∘ g) (Abs_adelic_int y)" by force
from y obtain z where z: "z ∈ 𝒪⇩∀⇩p" "y = z prestrict (=) p" by fast
hence "Abs_adelic_int y = Abs_adelic_int z prestrict (=) p"
using p_restrict_adelic_int_abs_eq by fastforce
with g show ?thesis using lim by blast
qed
end
lemma int_adic_prod_local_int_ring_seq_compact:
"∃x∈(λx. x prestrict ((=) p)) ` (𝒪⇩∀⇩p).
∃g::nat⇒nat.
strict_mono g ∧ p_adic_prod_p_open_nbhds_limseq (X ∘ g) x"
if "range X ⊆ (λx. x prestrict ((=) p)) ` (𝒪⇩∀⇩p)"
for p :: "int prime"
and X :: "nat ⇒ int p_adic_prod"
using that p_adic_prod_local_int_ring_seq_compact finite_range_prestrict_single_int_prime
by blast
lemma int_adelic_int_local_int_ring_seq_compact:
"∃x∈range (λx. x prestrict ((=) p)).
∃g::nat⇒nat.
strict_mono g ∧ adelic_int_p_open_nbhds_limseq (X ∘ g) x"
if "range X ⊆ range (λx. x prestrict ((=) p))"
for p :: "int prime"
and X :: "nat ⇒ int adelic_int"
using that adelic_int_local_int_ring_seq_compact finite_range_prestrict_single_int_prime
by blast
subsection ‹Finite-open-cover compactness›
function exclusion_sequence ::
"'a set ⇒ ('a ⇒ 'a set) ⇒
'a ⇒ nat ⇒ 'a"
where "exclusion_sequence A f a 0 = a" |
"exclusion_sequence A f a (Suc n) =
(SOME x. x ∈ A ∧ x ∉ (⋃k≤n. f (exclusion_sequence A f a k)))"
by pat_completeness auto
termination by (relation "measure(λ(A,f,a,n). n)") auto
lemma
assumes "¬ A ⊆ (⋃k≤n. f (exclusion_sequence A f a k))"
shows exclusion_sequence_mem: "exclusion_sequence A f a (Suc n) ∈ A"
and exclusion_sequence_excludes:
"exclusion_sequence A f a (Suc n) ∉ (⋃k≤n. f (exclusion_sequence A f a k))"
proof-
from assms have *:
"∃x. x ∈ A ∧ x ∉ (⋃k≤n. f (exclusion_sequence A f a k))"
by blast
show "exclusion_sequence A f a (Suc n) ∈ A"
and
"exclusion_sequence A f a (Suc n) ∉ (⋃k≤n. f (exclusion_sequence A f a k))"
using someI_ex[OF *] by auto
qed
context
fixes p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime"
assumes fin_p_quot: "finite (range (λx::'a adelic_int_quot. x prestrict ((=) p)))"
begin
lemma p_adic_prod_local_int_ring_finite_cover:
"∃C. finite C ∧
C ⊆ (λx. x prestrict ((=) p)) ` 𝒪⇩∀⇩p ∧
(λx. x prestrict ((=) p)) ` 𝒪⇩∀⇩p ⊆
(⋃c∈C. p_adic_prod_p_open_nbhd p n c)"
for C :: "'a set"
proof-
define p_ring :: "'a p_adic_prod set"
where "p_ring ≡ (λx. x prestrict ((=) p)) ` 𝒪⇩∀⇩p"
have
"¬ (∀C⊆p_ring.
p_ring ⊆ (⋃c∈C. p_adic_prod_p_open_nbhd p n c) ⟶
infinite C
)"
proof (safe)
assume n:
"∀C⊆p_ring.
p_ring ⊆ ⋃ (p_adic_prod_p_open_nbhd p n ` C) ⟶ infinite C"
define X where
"X ≡
λk. exclusion_sequence p_ring (p_adic_prod_p_open_nbhd p n) (0::'a p_adic_prod) k"
have partial_dn_cover:
"∀k. X ` {..k} ⊆ p_ring ⟶
¬ p_ring ⊆ (⋃j≤k. p_adic_prod_p_open_nbhd p n (X j))"
proof clarify
fix k
assume "X ` {..k} ⊆ p_ring"
and "p_ring ⊆ (⋃j≤k. p_adic_prod_p_open_nbhd p n (X j))"
with n have "infinite (X ` {..k})" by auto
thus False by blast
qed
moreover have partial_range_X: "∀k. X ` {..k} ⊆ p_ring"
proof
fix k show "X ` {..k} ⊆ p_ring"
proof (induct k)
case 0 from X_def p_ring_def show ?case
using global_p_depth_p_adic_prod.global_depth_set_0
global_p_depth_p_adic_prod.p_restrict_zero
by fastforce
next
case (Suc k)
hence "¬ p_ring ⊆ (⋃j≤k. p_adic_prod_p_open_nbhd p n (X j))"
using partial_dn_cover by blast
with X_def have "X (Suc k) ∈ p_ring" using exclusion_sequence_mem by force
moreover have "{..Suc k} = insert (Suc k) {..k}" by auto
ultimately show ?case using Suc by auto
qed
qed
ultimately
have dn_cover:
"∀k. ¬ p_ring ⊆ (⋃j≤k. p_adic_prod_p_open_nbhd p n (X j))"
and range_X: "range X ⊆ p_ring"
by (fastforce, fast)
from p_ring_def fin_p_quot obtain g
where g: "strict_mono g" "p_adic_prod_p_cauchy p (X ∘ g)"
using range_X p_adic_prod_local_int_ring_seq_compact'
by metis
from this obtain K where K: "p_adic_prod_p_cauchy_condition p (X ∘ g) n K" by fast
have "X (g (Suc K)) ∉ p_adic_prod_p_open_nbhd p n (X (g K))"
proof
assume "X (g (Suc K)) ∈ p_adic_prod_p_open_nbhd p n (X (g K))"
moreover from g(1) have g_K: "g K < g (Suc K)" using strict_monoD by blast
ultimately have
"X (g (Suc K)) ∈ (⋃j≤g (Suc K) - 1. p_adic_prod_p_open_nbhd p n (X j))"
by force
with X_def show False
using g_K dn_cover
exclusion_sequence_excludes[of p_ring "p_adic_prod_p_open_nbhd p n" 0 "g (Suc K) - 1"]
by simp
qed
hence "(X (g (Suc K))) ¬≃⇩p (X (g K))"
and "((X (g (Suc K)) - X (g K))°⇧p) < n"
using global_p_depth_p_adic_prod.p_open_nbhd_eq_circle
by (blast, fastforce)
with K show False
using global_p_depth_p_adic_prod.p_cauchy_conditionD[of p "X ∘ g" n K "Suc K" K] by auto
qed
thus ?thesis using p_ring_def by fast
qed
lemma p_adic_prod_local_int_ring_lebesgue_number:
"∃d. ∀x∈(λx. x prestrict ((=) p)) ` 𝒪⇩∀⇩p.
∃A∈𝒜. p_adic_prod_p_open_nbhd p d x ⊆ A"
if cover:
"(λx. x prestrict ((=) p)) ` 𝒪⇩∀⇩p ⊆ ⋃ 𝒜"
and by_opens:
"∀A∈𝒜. generate_topology (p_adic_prod_local_p_open_nbhds p) A"
proof-
define p_ring :: "'a p_adic_prod set"
where "p_ring ≡ (λx. x prestrict ((=) p)) ` 𝒪⇩∀⇩p"
have
"¬ (∀d. ∃x∈p_ring. ∀A∈𝒜.
¬ p_adic_prod_p_open_nbhd p d x ⊆ A)"
proof
assume *:
"∀d. ∃x∈p_ring. ∀A∈𝒜.
¬ p_adic_prod_p_open_nbhd p d x ⊆ A"
define X where
"X ≡ λn. SOME x.
x ∈ p_ring ∧
(∀A∈𝒜. ¬ p_adic_prod_p_open_nbhd p (int n) x ⊆ A)"
have range_X: "range X ⊆ p_ring"
proof safe
fix n
from * have ex_x:
"∃x. x ∈ p_ring ∧
(∀A∈𝒜. ¬ p_adic_prod_p_open_nbhd p (int n) x ⊆ A)"
by force
from X_def show "X n ∈ p_ring" using someI_ex[OF ex_x] by fast
qed
with fin_p_quot obtain a g
where g: "strict_mono g"
and a: "p_adic_prod_p_open_nbhds_limseq (X ∘ g) a"
using p_adic_prod_local_int_ring_seq_compact
unfolding X_def p_ring_def
by blast
from range_X p_ring_def have "range X ⊆ 𝒪⇩∀⇩p"
using global_p_depth_p_adic_prod.global_depth_set_closed_under_p_restrict_image by force
moreover from range_X p_ring_def have "∀n. X n = X n prestrict ((=) p)"
using subsetD
global_p_depth_p_adic_prod.p_restrict_image_restrict[of
"X _" "(=) p" "𝒪⇩∀⇩p"
]
by force
ultimately have "a ∈ p_ring"
using p_ring_def fin_p_quot a p_adic_prod_int_convergent_subseq_limseq by blast
with cover p_ring_def obtain A where A: "A ∈ 𝒜" "a ∈ A" by blast
with by_opens obtain n where n: "p_adic_prod_p_open_nbhd p n a ⊆ A"
using global_p_depth_p_adic_prod.p_open_nbhds_open_subopen by blast
from a have "p_adic_prod_p_limseq p (X ∘ g) a"
using global_p_depth_p_adic_prod.globally_limseq_imp_locally_limseq by fast
from this obtain K where K: "p_adic_prod_p_limseq_condition p (X ∘ g) a n K" by presburger
define k where "k ≡ max (nat n) K"
from * have ex_x:
"∃x. x ∈ p_ring ∧
(∀A∈𝒜. ¬ p_adic_prod_p_open_nbhd p (int (g k)) x ⊆ A)"
by force
from X_def A(1)
have X_g_m: "¬ p_adic_prod_p_open_nbhd p (int (g k)) (X (g k)) ⊆ A"
using someI_ex[OF ex_x]
by fast
moreover from g k_def have n_g_k: "n ≤ int (g k)"
using strict_mono_imp_increasing[of g k] by linarith
ultimately have "X (g k) ¬≃⇩p a"
using n X_g_m global_p_depth_p_adic_prod.p_open_nbhd_eq_circle
global_p_depth_p_adic_prod.p_open_nbhd_circle_multicentre
global_p_depth_p_adic_prod.p_open_nbhd_antimono
by blast
with K k_def have "X (g k) ∈ p_adic_prod_p_open_nbhd p n a"
using global_p_depth_p_adic_prod.p_limseq_conditionD[of p _ a n K k]
global_p_depth_p_adic_prod.p_open_nbhd_eq_circle
by force
with n show False
using n_g_k X_g_m global_p_depth_p_adic_prod.p_open_nbhd_circle_multicentre
global_p_depth_p_adic_prod.p_open_nbhd_antimono
by fast
qed
thus ?thesis using p_ring_def by force
qed
lemma p_adic_prod_local_int_ring_compact:
"∃ℬ⊆𝒜. finite ℬ ∧
(λx. x prestrict ((=) p)) ` 𝒪⇩∀⇩p ⊆ ⋃ ℬ"
if cover:
"(λx. x prestrict ((=) p)) ` 𝒪⇩∀⇩p ⊆ ⋃ 𝒜"
and by_opens:
"∀A∈𝒜. generate_topology (p_adic_prod_local_p_open_nbhds p) A"
proof-
define p_ring :: "'a p_adic_prod set"
where "p_ring ≡ (λx. x prestrict ((=) p)) ` 𝒪⇩∀⇩p"
with cover by_opens obtain d where d:
"∀x∈p_ring. ∃A∈𝒜. p_adic_prod_p_open_nbhd p d x ⊆ A"
using p_adic_prod_local_int_ring_lebesgue_number by presburger
from p_ring_def obtain C where C:
"finite C" "C ⊆ p_ring"
"p_ring ⊆ (⋃c∈C. p_adic_prod_p_open_nbhd p d c)"
using p_adic_prod_local_int_ring_finite_cover by metis
define f where
"f ≡ λc. SOME A. A ∈ 𝒜 ∧ p_adic_prod_p_open_nbhd p d c ⊆ A"
define ℬ where "ℬ ≡ f ` C"
have "ℬ ⊆ 𝒜"
unfolding ℬ_def
proof safe
fix c assume "c ∈ C"
with d C(2)
have ex_A: "∃A. A ∈ 𝒜 ∧ p_adic_prod_p_open_nbhd p d c ⊆ A"
by blast
from f_def show "f c ∈ 𝒜" using someI_ex[OF ex_A] by blast
qed
moreover from ℬ_def C(1) have "finite ℬ" by simp
moreover have "p_ring ⊆ ⋃ ℬ"
proof
fix x assume "x ∈ p_ring"
with C(3) obtain c where c: "c ∈ C" "x ∈ p_adic_prod_p_open_nbhd p d c" by auto
from d C(2) c(1)
have ex_A: "∃A. A ∈ 𝒜 ∧ p_adic_prod_p_open_nbhd p d c ⊆ A"
by blast
from f_def have "p_adic_prod_p_open_nbhd p d c ⊆ f c" using someI_ex[OF ex_A] by auto
with ℬ_def c show "x ∈ ⋃ ℬ" by auto
qed
ultimately show ?thesis using p_ring_def by blast
qed
lemma p_adic_prod_local_scaled_int_ring_compact:
"∃ℬ⊆𝒜. finite ℬ ∧
(λx. x prestrict ((=) p)) ` (𝒫⇩∀⇩p⇧n)
⊆ ⋃ ℬ"
if cover:
"(λx. x prestrict ((=) p)) ` (𝒫⇩∀⇩p⇧n)
⊆ ⋃ 𝒜"
and by_opens:
"∀A∈𝒜. generate_topology (p_adic_prod_local_p_open_nbhds p) A"
for 𝒜 :: "'a p_adic_prod set set"
proof-
define p_ring p_depth_ring :: "'a p_adic_prod set"
where "p_ring ≡ (λx. x prestrict ((=) p)) ` 𝒪⇩∀⇩p"
and
"p_depth_ring ≡
(λx. x prestrict ((=) p)) ` (𝒫⇩∀⇩p⇧n)"
from p_ring_def p_depth_ring_def
have drop: "p_adic_prod_shift_p_depth p n ` p_ring = p_depth_ring"
and lift: "p_adic_prod_shift_p_depth p (-n) ` p_depth_ring = p_ring"
by (simp_all add: p_adic_prod_depth_embeds.shift_p_depth_p_restrict_global_depth_set_image)
define 𝒜' where "𝒜' ≡ (`) (p_adic_prod_shift_p_depth p (-n)) ` 𝒜"
from cover p_depth_ring_def 𝒜'_def have "p_ring ⊆ ⋃ 𝒜'" using lift by blast
moreover from by_opens have by_opens':
"∀A'∈𝒜'. generate_topology (p_adic_prod_local_p_open_nbhds p) A'"
using p_adic_prod_depth_embeds.shift_p_depth_p_open_set unfolding 𝒜'_def by fast
ultimately obtain ℬ'
where ℬ': "ℬ' ⊆ 𝒜'" "finite ℬ'" "p_ring ⊆ ⋃ ℬ'"
using fin_p_quot p_ring_def p_adic_prod_local_int_ring_compact
by force
define ℬ where "ℬ ≡ (`) (p_adic_prod_shift_p_depth p n) ` ℬ'"
have "ℬ ⊆ 𝒜"
unfolding ℬ_def
proof clarify
fix B' assume "B' ∈ ℬ'"
with ℬ'(1) 𝒜'_def obtain A
where "A ∈ 𝒜" and "B' = p_adic_prod_shift_p_depth p (-n) ` A"
by blast
thus "p_adic_prod_shift_p_depth p n ` B' ∈ 𝒜"
using p_adic_prod_depth_embeds.shift_shift_p_depth_image[of p n "-n"] by simp
qed
moreover from ℬ_def ℬ'(2) have "finite ℬ" by blast
moreover from ℬ_def ℬ'(3) have "p_depth_ring ⊆ ⋃ ℬ" using drop by blast
ultimately show ?thesis using p_depth_ring_def by blast
qed
lemma adelic_int_local_int_ring_compact:
"∃ℬ⊆𝒜. finite ℬ ∧
range (λx. x prestrict ((=) p)) ⊆ ⋃ ℬ"
if fin_p_quot: "finite (range (λx::'a adelic_int_quot. x prestrict ((=) p)))"
and cover: "range (λx. x prestrict ((=) p)) ⊆ ⋃ 𝒜"
and by_opens:
"∀A∈𝒜. generate_topology (adelic_int_local_p_open_nbhds p) A"
for 𝒜 :: "'a adelic_int set set"
proof-
define f f' :: "'a p_adic_prod ⇒ 'a p_adic_prod"
where "f ≡ λx. x prestrict ((=) p)"
and "f' ≡ λx. x prestrict ((≠) p)"
define f_f' where "f_f' ≡ λA. f ` Rep_adelic_int ` A + range f'"
define p_ring :: "'a p_adic_prod set" where "p_ring ≡ f ` 𝒪⇩∀⇩p"
define 𝒜' where "𝒜' ≡ f_f' ` 𝒜"
from cover f_def f'_def f_f'_def p_ring_def 𝒜'_def have "p_ring ⊆ ⋃ 𝒜'"
using adelic_int_local_depth_ring_lift_cover[of 0] by fast
moreover from by_opens f_def f'_def f_f'_def 𝒜'_def have
"∀A'∈𝒜'. generate_topology (p_adic_prod_local_p_open_nbhds p) A'"
using adelic_int_lift_local_p_open by fast
ultimately obtain ℬ'
where ℬ': "ℬ' ⊆ 𝒜'" "finite ℬ'" "p_ring ⊆ ⋃ ℬ'"
using fin_p_quot f_def p_ring_def p_adic_prod_local_int_ring_compact
by force
define g where "g ≡ λB'. SOME B. B ∈ 𝒜 ∧ B' = f_f' B"
define ℬ where "ℬ ≡ g ` ℬ'"
from ℬ_def ℬ'(2) have "finite ℬ" by fast
moreover have subcover: "ℬ ⊆ 𝒜"
unfolding ℬ_def
proof clarify
fix B' assume "B' ∈ ℬ'"
with 𝒜'_def ℬ'(1) have ex_B: "∃B. B ∈ 𝒜 ∧ B' = f_f' B" by blast
from g_def show "g B' ∈ 𝒜" using someI_ex[OF ex_B] by fastforce
qed
moreover have "range (λx. x prestrict ((=) p)) ⊆ ⋃ ℬ"
proof clarify
fix x show "x prestrict (=) p ∈ ⋃ ℬ"
proof (cases x)
case (Abs_adelic_int a)
from p_ring_def Abs_adelic_int(2) ℬ'(3) have "f a ∈ ⋃ ℬ'" by auto
from this obtain B' where B': "B' ∈ ℬ'" "f a ∈ B'" by fast
from 𝒜'_def ℬ'(1) B'(1) have ex_B: "∃B. B ∈ 𝒜 ∧ B' = f_f' B" by auto
from B'(1) ℬ_def have g_B': "g B' ∈ ℬ" by auto
from g_def B'(2) have "f a ∈ f_f' (g B')" using someI_ex[OF ex_B] by simp
with f_f'_def obtain b c where b: "b ∈ g B'" and bc: "f a = f (Rep_adelic_int b) + f' c"
using set_plus_elim by blast
have "f' c = 0"
proof (intro global_p_depth_p_adic_prod.global_imp_eq, standard)
fix q :: "'a prime" show "f' c ≃⇩q 0"
proof (cases "p = q")
case True with f'_def show ?thesis
using global_p_depth_p_adic_prod.p_restrict_equiv0 by fast
next
case False
moreover from f_def bc have "f' c = f (a - Rep_adelic_int b)"
by (simp add: global_p_depth_p_adic_prod.p_restrict_minus)
ultimately show ?thesis
using f_def global_p_depth_p_adic_prod.p_restrict_equiv0 by auto
qed
qed
with f_def Abs_adelic_int bc have
"x prestrict (=) p = b prestrict ((=) p)"
using p_restrict_adelic_int_abs_eq p_restrict_adelic_int_abs_eq
Rep_adelic_int[of b] Rep_adelic_int_inverse[of b]
by fastforce
moreover from by_opens b(1) have "b prestrict ((=) p) ∈ g B'"
using subcover g_B' global_p_depth_adelic_int.p_restrict_p_open_set_mem_iff by blast
ultimately show ?thesis using g_B' by auto
qed
qed
ultimately show ?thesis by blast
qed
lemma adelic_int_local_scaled_int_ring_compact:
"∃ℬ⊆𝒜. finite ℬ ∧
(λx. x prestrict ((=) p)) ` (𝒫⇩∀⇩p⇧n)
⊆ ⋃ ℬ"
if fin_p_quot: "finite (range (λx::'a adelic_int_quot. x prestrict ((=) p)))"
and cover:
"(λx. x prestrict ((=) p)) ` (𝒫⇩∀⇩p⇧n)
⊆ ⋃ 𝒜"
and by_opens:
"∀A∈𝒜. generate_topology (adelic_int_local_p_open_nbhds p) A"
for 𝒜 :: "'a adelic_int set set"
proof-
show ?thesis
proof (cases "n ≤ 0")
case True
hence
"(λx::'a adelic_int. x prestrict ((=) p)) ` (𝒫⇩∀⇩p⇧n) =
range (λx. x prestrict ((=) p))"
using nonpos_global_depth_set_adelic_int by auto
with fin_p_quot cover by_opens show ?thesis
using adelic_int_local_int_ring_compact by fastforce
next
case False
define f f' :: "'a p_adic_prod ⇒ 'a p_adic_prod"
where "f ≡ λx. x prestrict ((=) p)"
and "f' ≡ λx. x prestrict ((≠) p)"
define f_f' where "f_f' ≡ λA. f ` Rep_adelic_int ` A + range f'"
define p_ring p_depth_ring :: "'a p_adic_prod set"
where "p_ring ≡ f ` 𝒪⇩∀⇩p"
and "p_depth_ring ≡ f ` (𝒫⇩∀⇩p⇧n)"
define 𝒜' where "𝒜' ≡ f_f' ` 𝒜"
from False cover f_def f'_def f_f'_def p_depth_ring_def 𝒜'_def
have "p_depth_ring ⊆ ⋃ 𝒜'"
using adelic_int_local_depth_ring_lift_cover[of n p 𝒜]
by auto
moreover from by_opens f_def f'_def f_f'_def 𝒜'_def have
"∀A'∈𝒜'. generate_topology (p_adic_prod_local_p_open_nbhds p) A'"
using adelic_int_lift_local_p_open by fast
ultimately obtain ℬ' where ℬ':
"ℬ' ⊆ 𝒜'" "finite ℬ'" "p_depth_ring ⊆ ⋃ ℬ'"
using fin_p_quot f_def p_depth_ring_def p_adic_prod_local_scaled_int_ring_compact[of n]
by force
define g where "g ≡ λB'. SOME B. B ∈ 𝒜 ∧ B' = f_f' B"
define ℬ where "ℬ ≡ g ` ℬ'"
from ℬ_def ℬ'(2) have "finite ℬ" by fast
moreover have subcover: "ℬ ⊆ 𝒜"
unfolding ℬ_def
proof clarify
fix B' assume "B' ∈ ℬ'"
with 𝒜'_def ℬ'(1) have ex_B: "∃B. B ∈ 𝒜 ∧ B' = f_f' B" by blast
from g_def show "g B' ∈ 𝒜" using someI_ex[OF ex_B] by fastforce
qed
moreover have
"(λx. x prestrict ((=) p)) ` (𝒫⇩∀⇩p⇧n) ⊆
⋃ ℬ"
proof clarify
fix x :: "'a adelic_int" assume x: "x ∈ 𝒫⇩∀⇩p⇧n"
show "x prestrict (=) p ∈ ⋃ ℬ"
proof (cases x)
case (Abs_adelic_int a)
hence "a = Rep_adelic_int x" using Abs_adelic_int_inverse by fastforce
with False x have "a ∈ 𝒫⇩∀⇩p⇧n"
using lift_nonneg_global_depth_set_adelic_int[of n] by auto
with p_depth_ring_def ℬ'(3) have "f a ∈ ⋃ ℬ'"
using nonneg_global_depth_set_adelic_int_eq_projection[of n] by fast
from this obtain B' where B': "B' ∈ ℬ'" "f a ∈ B'" by fast
from 𝒜'_def ℬ'(1) B'(1) have ex_B: "∃B. B ∈ 𝒜 ∧ B' = f_f' B"
by auto
from B'(1) ℬ_def have g_B': "g B' ∈ ℬ" by auto
from g_def B'(2) have "f a ∈ f_f' (g B')" using someI_ex[OF ex_B] by simp
with f_f'_def obtain b c where b: "b ∈ g B'" and bc: "f a = f (Rep_adelic_int b) + f' c"
using set_plus_elim by blast
have "f' c = 0"
proof (intro global_p_depth_p_adic_prod.global_imp_eq, standard)
fix q :: "'a prime" show "f' c ≃⇩q 0"
proof (cases "p = q")
case True with f'_def show ?thesis
using global_p_depth_p_adic_prod.p_restrict_equiv0 by fast
next
case False
moreover from f_def bc have "f' c = f (a - Rep_adelic_int b)"
by (simp add: global_p_depth_p_adic_prod.p_restrict_minus)
ultimately show ?thesis
using f_def global_p_depth_p_adic_prod.p_restrict_equiv0 by auto
qed
qed
with f_def Abs_adelic_int bc have
"x prestrict (=) p = b prestrict ((=) p)"
using p_restrict_adelic_int_abs_eq p_restrict_adelic_int_abs_eq
Rep_adelic_int[of b] Rep_adelic_int_inverse[of b]
by fastforce
moreover from by_opens b(1) have "b prestrict ((=) p) ∈ g B'"
using subcover g_B' global_p_depth_adelic_int.p_restrict_p_open_set_mem_iff by blast
ultimately show ?thesis using g_B' by auto
qed
qed
ultimately show ?thesis by blast
qed
qed
end
lemma int_adic_prod_local_int_ring_compact:
"∃ℬ⊆𝒜. finite ℬ ∧
(λx. x prestrict ((=) p)) ` 𝒪⇩∀⇩p ⊆ ⋃ ℬ"
if "(λx. x prestrict ((=) p)) ` 𝒪⇩∀⇩p ⊆ ⋃ 𝒜"
and "∀A∈𝒜. generate_topology (p_adic_prod_local_p_open_nbhds p) A"
for p :: "int prime"
and 𝒜 :: "int p_adic_prod set set"
using that p_adic_prod_local_int_ring_compact[of p 𝒜] finite_range_prestrict_single_int_prime
by presburger
lemma int_adic_prod_local_scaled_int_ring_compact:
"∃ℬ⊆𝒜. finite ℬ ∧
(λx. x prestrict ((=) p)) ` (𝒫⇩∀⇩p⇧n)
⊆ ⋃ ℬ"
if
"(λx. x prestrict ((=) p)) ` (𝒫⇩∀⇩p⇧n)
⊆ ⋃ 𝒜"
and "∀A∈𝒜. generate_topology (p_adic_prod_local_p_open_nbhds p) A"
for p :: "int prime"
and 𝒜 :: "int p_adic_prod set set"
using that p_adic_prod_local_scaled_int_ring_compact[of p n 𝒜]
finite_range_prestrict_single_int_prime
by presburger
lemma int_adelic_int_local_int_ring_compact:
"∃ℬ⊆𝒜. finite ℬ ∧
range (λx. x prestrict ((=) p)) ⊆ ⋃ ℬ"
if "range (λx. x prestrict ((=) p)) ⊆ ⋃ 𝒜"
and "∀A∈𝒜. generate_topology (adelic_int_local_p_open_nbhds p) A"
for p :: "int prime"
and 𝒜 :: "int adelic_int set set"
using that adelic_int_local_int_ring_compact[of p 𝒜] finite_range_prestrict_single_int_prime
by presburger
lemma int_adelic_int_local_scaled_int_ring_compact:
"∃ℬ⊆𝒜. finite ℬ ∧
(λx. x prestrict ((=) p)) ` (𝒫⇩∀⇩p⇧n)
⊆ ⋃ ℬ"
if
"(λx. x prestrict ((=) p)) ` (𝒫⇩∀⇩p⇧n)
⊆ ⋃ 𝒜"
and "∀A∈𝒜. generate_topology (adelic_int_local_p_open_nbhds p) A"
for p :: "int prime"
and 𝒜 :: "int adelic_int set set"
using that adelic_int_local_scaled_int_ring_compact[of p n 𝒜]
finite_range_prestrict_single_int_prime
by presburger
end