Theory Fin_Field_Product
theory Fin_Field_Product
imports
Distinguished_Quotients
pAdic_Product
begin
section ‹
Finite fields of prime order as quotients of the ring of integers of p-adic fields
›
subsection ‹The type›
subsubsection ‹
The prime ideal as the distinguished ideal of the ring of adelic integers
›
instantiation adelic_int ::
(nontrivial_factorial_idom) comm_ring_1_with_distinguished_ideal
begin
definition distinguished_subset_adelic_int :: "'a adelic_int set"
where distinguished_subset_adelic_int_def[simp]:
"distinguished_subset_adelic_int ≡ 𝒫⇩∀⇩p"
instance
proof (standard, safe)
show "(𝒩 ::'a adelic_int set) = {} ⟹ False"
using global_p_depth_adelic_int.global_depth_set_0 by auto
next
fix g h :: "'a adelic_int"
assume "g ∈ 𝒩" and "h ∈ 𝒩"
thus "g - h ∈ 𝒩"
using global_p_depth_adelic_int.global_depth_set_minus by auto
next
fix r x :: "'a adelic_int"
assume "x ∈ 𝒩"
thus "r * x ∈ 𝒩"
using global_p_depth_adelic_int.global_depth_set_ideal nonpos_global_depth_set_adelic_int
by fastforce
next
define n where "n ≡ (1::'a adelic_int)"
moreover assume "n ∈ 𝒩"
ultimately show False using global_p_depth_adelic_int.pos_global_depth_set_1 by force
qed
end
lemma distinguished_subset_adelic_int_inverse:
"inverse x = 0" if "x ∈ 𝒫⇩∀⇩p"
for x :: "'a::nontrivial_factorial_unique_euclidean_bezout adelic_int"
using that global_p_depth_adelic_int.global_depth_setD adelic_int_inverse_eq0_iff by fastforce
subsubsection ‹The finite field product type as a quotient›
text ‹Create type wrapper @{type coset_by_dist_sbgrp} over @{type adelic_int}.›
typedef (overloaded) 'a adelic_int_quot =
"UNIV :: 'a::nontrivial_factorial_idom adelic_int coset_by_dist_sbgrp set"
..
abbreviation
"adelic_int_quot ≡ λx. Abs_adelic_int_quot (distinguished_quotient_coset x)"
abbreviation "p_adic_prod_int_quot ≡ λx. adelic_int_quot (Abs_adelic_int x)"
lemma adelic_int_quot_cases [case_names adelic_int_quot]:
obtains y where "x = adelic_int_quot y"
proof (cases x)
case (Abs_adelic_int_quot y) with that show thesis by (cases y) blast
qed
lemma Abs_adelic_int_quot_cases [case_names adelic_int_quot_Abs_adelic_int]:
obtains z where "x = p_adic_prod_int_quot z" "z ∈ 𝒪⇩∀⇩p"
proof (cases x rule: adelic_int_quot_cases)
case (adelic_int_quot y) with that show thesis by (cases y) blast
qed
lemmas two_adelic_int_quot_cases = adelic_int_quot_cases[case_product adelic_int_quot_cases]
and three_adelic_int_quot_cases =
adelic_int_quot_cases[case_product adelic_int_quot_cases[case_product adelic_int_quot_cases]]
lemma abs_adelic_int_eq_iff:
"adelic_int_quot x = adelic_int_quot y ⟷
y - x ∈ 𝒫⇩∀⇩p"
using Abs_adelic_int_quot_inject distinguished_quotient_coset_eq_iff by force
lemma p_adic_prod_int_quot_eq_iff:
"p_adic_prod_int_quot x = p_adic_prod_int_quot y ⟷
y - x ∈ 𝒫⇩∀⇩p"
if "x ∈ 𝒪⇩∀⇩p" and "y ∈ 𝒪⇩∀⇩p"
using that abs_adelic_int_eq_iff[of "Abs_adelic_int x" "Abs_adelic_int y"] Abs_adelic_int_inject
minus_adelic_int_abs_eq[of y x] nonneg_global_depth_set_adelic_int_eq_projection[of 1]
global_p_depth_p_adic_prod.global_depth_set_minus[of y 0 x]
global_p_depth_p_adic_prod.global_depth_set_antimono[of 0 1]
by fastforce
subsubsection ‹Algebraic instantiations›
instantiation adelic_int_quot :: (nontrivial_factorial_idom) comm_ring_1
begin
definition "0 = Abs_adelic_int_quot 0"
lemma zero_adelic_int_quot_rep_eq: "Rep_adelic_int_quot 0 = 0"
using Abs_adelic_int_quot_inverse by (simp add: zero_adelic_int_quot_def)
lemma zero_adelic_int_quot: "0 = adelic_int_quot 0"
using zero_adelic_int_quot_def zero_coset_by_dist_sbgrp.abs_eq by simp
definition "1 ≡ Abs_adelic_int_quot 1"
lemma one_adelic_int_quot_rep_eq: "Rep_adelic_int_quot 1 = 1"
using Abs_adelic_int_quot_inverse by (simp add: one_adelic_int_quot_def)
lemma one_adelic_int_quot: "1 = adelic_int_quot 1"
using one_adelic_int_quot_def one_coset_by_dist_sbgrp.abs_eq by simp
definition "x + y = Abs_adelic_int_quot (Rep_adelic_int_quot x + Rep_adelic_int_quot y)"
lemma plus_adelic_int_quot_rep_eq:
"Rep_adelic_int_quot (a + b) = Rep_adelic_int_quot a + Rep_adelic_int_quot b"
using Rep_adelic_int_quot Abs_adelic_int_quot_inverse
unfolding plus_adelic_int_quot_def
by blast
lemma plus_adelic_int_quot_abs_eq:
"Abs_adelic_int_quot x + Abs_adelic_int_quot y = Abs_adelic_int_quot (x + y)"
using Abs_adelic_int_quot_inverse[of x] Abs_adelic_int_quot_inverse[of y]
unfolding plus_adelic_int_quot_def
by simp
lemma plus_adelic_int_quot: "adelic_int_quot x + adelic_int_quot y = adelic_int_quot (x + y)"
using plus_adelic_int_quot_abs_eq plus_coset_by_dist_sbgrp.abs_eq by fastforce
definition "-x = Abs_adelic_int_quot (- Rep_adelic_int_quot x)"
lemma uminus_adelic_int_quot_rep_eq: "Rep_adelic_int_quot (- x) = - Rep_adelic_int_quot x"
using Rep_adelic_int_quot Abs_adelic_int_quot_inverse
unfolding uminus_adelic_int_quot_def
by blast
lemma uminus_adelic_int_quot_abs_eq: "- Abs_adelic_int_quot x = Abs_adelic_int_quot (- x)"
using Abs_adelic_int_quot_inverse[of x] unfolding uminus_adelic_int_quot_def by simp
lemma uminus_adelic_int_quot: "- adelic_int_quot x = adelic_int_quot (-x)"
using uminus_adelic_int_quot_abs_eq uminus_coset_by_dist_sbgrp.abs_eq by fastforce
definition minus_adelic_int_quot ::
"'a adelic_int_quot ⇒ 'a adelic_int_quot ⇒ 'a adelic_int_quot"
where "minus_adelic_int_quot ≡ (λx y. x + - y)"
lemma minus_adelic_int_quot_rep_eq:
"Rep_adelic_int_quot (x - y) = Rep_adelic_int_quot x - Rep_adelic_int_quot y"
using plus_adelic_int_quot_rep_eq uminus_adelic_int_quot_rep_eq
by (simp add: minus_adelic_int_quot_def)
lemma minus_adelic_int_quot_abs_eq:
"Abs_adelic_int_quot x - Abs_adelic_int_quot y = Abs_adelic_int_quot (x - y)"
by (simp add:
minus_adelic_int_quot_def uminus_adelic_int_quot_abs_eq
plus_adelic_int_quot_abs_eq
)
lemma minus_adelic_int_quot: "adelic_int_quot x - adelic_int_quot y = adelic_int_quot (x - y)"
using minus_adelic_int_quot_abs_eq minus_coset_by_dist_sbgrp.abs_eq by fastforce
definition "x * y = Abs_adelic_int_quot (Rep_adelic_int_quot x * Rep_adelic_int_quot y)"
lemma times_adelic_int_quot_rep_eq:
"Rep_adelic_int_quot (x * y) = Rep_adelic_int_quot x * Rep_adelic_int_quot y"
using Rep_adelic_int_quot Abs_adelic_int_quot_inverse
unfolding times_adelic_int_quot_def
by blast
lemma times_adelic_int_quot_abs_eq:
"Abs_adelic_int_quot x * Abs_adelic_int_quot y = Abs_adelic_int_quot (x * y)"
using Abs_adelic_int_quot_inverse[of x] Abs_adelic_int_quot_inverse[of y]
unfolding times_adelic_int_quot_def
by simp
lemma times_adelic_int_quot: "adelic_int_quot x * adelic_int_quot y = adelic_int_quot (x * y)"
using times_adelic_int_quot_abs_eq times_coset_by_dist_sbgrp.abs_eq by auto
instance
proof
fix a b c :: "'a adelic_int_quot"
show "a + b + c = a + (b + c)"
by (cases a, cases b, cases c) (simp add: plus_adelic_int_quot_abs_eq add.assoc)
show "a + b = b + a" by (cases a, cases b) (simp add: plus_adelic_int_quot_abs_eq add.commute)
show "0 + a = a"
using plus_adelic_int_quot_abs_eq[of 0] by (cases a, simp add: zero_adelic_int_quot_def)
show "1 * a = a"
using times_adelic_int_quot_abs_eq[of 1] by (cases a) (simp add: one_adelic_int_quot_def)
show "- a + a = 0"
by (cases a)
(simp add:
uminus_adelic_int_quot_abs_eq plus_adelic_int_quot_abs_eq zero_adelic_int_quot_def
)
show "a - b = a + - b" by (simp add: minus_adelic_int_quot_def)
show "a * b * c = a * (b * c)"
by (cases a, cases b, cases c)
(simp add: times_adelic_int_quot_abs_eq mult.assoc)
show "a * b = b * a" by (cases a, cases b) (simp add: times_adelic_int_quot_abs_eq mult.commute)
show "(a + b) * c = a * c + b * c"
by (cases a, cases b, cases c)
(simp add: plus_adelic_int_quot_abs_eq times_adelic_int_quot_abs_eq distrib_right)
show "(0::'a adelic_int_quot) ≠ 1"
using Abs_adelic_int_quot_inject[of "0::'a adelic_int coset_by_dist_sbgrp" 1]
by (simp add: zero_adelic_int_quot_def one_adelic_int_quot_def)
qed
end
instantiation adelic_int_quot ::
(nontrivial_factorial_unique_euclidean_bezout) "{divide_trivial, inverse}"
begin
lift_definition inverse_adelic_int_coset ::
"'a adelic_int coset_by_dist_sbgrp ⇒ 'a adelic_int coset_by_dist_sbgrp"
is inverse
unfolding distinguished_subset_adelic_int_def
proof
fix x y :: "'a adelic_int"
assume xy: "- y + x ∈ 𝒫⇩∀⇩p"
show "- inverse y + inverse x ∈ 𝒫⇩∀⇩p"
proof (intro adelic_int_global_depth_setI)
fix p :: "'a prime"
assume xy': "- inverse y + inverse x ¬≃⇩p 0"
have "((inverse x - inverse y)°⇧p) > 0"
proof (intro adelic_int_diff_cancel_lead_coeff)
from xy' show "x ¬≃⇩p y"
using p_equality_adelic_int.conv_0 adelic_int_inverse_pcong by fastforce
with xy show "((x - y)°⇧p) > 0"
using p_equality_adelic_int.conv_0 global_p_depth_adelic_int.global_depth_setD
by fastforce
moreover from this xy' show "x ¬≃⇩p 0" and "y ¬≃⇩p 0"
using adelic_int_inverse_equiv0_iff global_p_depth_adelic_int.depth_diff_equiv0_left[of p x]
global_p_depth_adelic_int.depth_diff_equiv0_right[of p y]
p_equality_adelic_int.minus_0[of p "inverse x" "inverse y"]
by (force, force)
ultimately show "(x°⇧p) = 0" and "(y°⇧p) = 0"
using xy' adelic_int_depth adelic_int_inverse_equiv0_iff
global_p_depth_adelic_int.depth_pre_nonarch_diff_left[of p x y]
global_p_depth_adelic_int.depth_pre_nonarch_diff_right[of p y x]
p_equality_adelic_int.minus_0[of p "inverse x" "inverse y"]
by (force, force)
qed
thus "((- inverse y + inverse x)°⇧p) ≥ 1" by force
qed
qed simp
definition inverse_adelic_int_quot :: "'a adelic_int_quot ⇒ 'a adelic_int_quot"
where
"inverse_adelic_int_quot x ≡
Abs_adelic_int_quot (inverse_adelic_int_coset (Rep_adelic_int_quot x))"
lemma inverse_adelic_int_quot: "inverse (adelic_int_quot x) = adelic_int_quot (inverse x)"
unfolding inverse_adelic_int_quot_def
by (simp add: Abs_adelic_int_quot_inverse inverse_adelic_int_coset.abs_eq)
lemma inverse_adelic_int_quot_0[simp]: "inverse (0 :: 'a adelic_int_quot) = 0"
by (metis zero_adelic_int_quot inverse_adelic_int_quot adelic_int_inverse0)
lemma inverse_adelic_int_quot_1[simp]: "inverse (1 :: 'a adelic_int_quot) = 1"
by (metis one_adelic_int_quot inverse_adelic_int_quot adelic_int_inverse1)
definition divide_adelic_int_quot ::
"'a adelic_int_quot ⇒ 'a adelic_int_quot ⇒ 'a adelic_int_quot"
where divide_adelic_int_quot_def[simp]: "divide_adelic_int_quot x y ≡ x * inverse y"
instance by standard simp_all
end
lemma divide_adelic_int_quot: "adelic_int_quot x / adelic_int_quot y = adelic_int_quot (x / y)"
for x y :: "'a::nontrivial_factorial_unique_euclidean_bezout adelic_int"
using times_adelic_int_quot inverse_adelic_int_quot
unfolding divide_adelic_int_quot_def divide_adelic_int_def
by metis
subsection ‹Equivalence relative to a prime›
subsubsection ‹Equivalence›
overloading
p_equal_adelic_int_coset ≡
"p_equal :: 'a::nontrivial_factorial_idom prime ⇒
'a adelic_int coset_by_dist_sbgrp ⇒
'a adelic_int coset_by_dist_sbgrp ⇒ bool"
p_equal_adelic_int_quot ≡
"p_equal :: 'a::nontrivial_factorial_idom prime ⇒
'a adelic_int_quot ⇒ 'a adelic_int_quot ⇒ bool"
p_restrict_adelic_int_coset ≡
"p_restrict :: 'a adelic_int coset_by_dist_sbgrp ⇒
('a prime ⇒ bool) ⇒ 'a adelic_int coset_by_dist_sbgrp"
p_restrict_adelic_int_quot ≡
"p_restrict :: 'a adelic_int_quot ⇒
('a prime ⇒ bool) ⇒ 'a adelic_int_quot"
begin
lift_definition p_equal_adelic_int_coset ::
"'a::nontrivial_factorial_idom prime ⇒
'a adelic_int coset_by_dist_sbgrp ⇒
'a adelic_int coset_by_dist_sbgrp ⇒ bool"
is "λp x y. x ≃⇩p y ∨ ((x - y)°⇧p) ≥ 1"
unfolding distinguished_subset_adelic_int_def
proof-
fix p :: "'a prime" and w x y z :: "'a adelic_int"
assume "-w + y ∈ 𝒫⇩∀⇩p" and "-x + z ∈ 𝒫⇩∀⇩p"
moreover have
"⋀w x y z :: 'a adelic_int.
y - w ∈ 𝒫⇩∀⇩p ⟹
z - x ∈ 𝒫⇩∀⇩p ⟹
w ≃⇩p x ∨ ((w - x)°⇧p) ≥ 1 ⟹
((y - z)°⇧p) ≥ 1 ∨ y ≃⇩p z"
proof clarify
fix w x y z :: "'a adelic_int"
assume wy : "y - w ∈ 𝒫⇩∀⇩p"
and xz : "z - x ∈ 𝒫⇩∀⇩p"
and equiv : "w ≃⇩p x ∨ ((w - x)°⇧p) ≥ 1"
and nequiv: "y ¬≃⇩p z"
have 1: "y - z = w - x + ((y - w) - (z - x))" by simp
from wy xz have 2: "(y - w) - (z - x) ∈ 𝒫⇩∀⇩p"
using global_p_depth_adelic_int.global_depth_set_minus by auto
show "((y - z)°⇧p) ≥ 1"
proof (
cases "w ≃⇩p x" "(y - w) ≃⇩p (z - x)"
rule: case_split[case_product case_split],
metis nequiv 1 p_equality_adelic_int.conv_0 p_equality_adelic_int.add_0,
metis 1 2 p_equality_adelic_int.conv_0 global_p_depth_adelic_int.depth_add_equiv0_left
global_p_depth_adelic_int.global_depth_setD global_depth_set_adelic_int_def,
metis equiv 1 p_equality_adelic_int.conv_0
global_p_depth_adelic_int.depth_add_equiv0_right
)
case False_False
hence wx: "w - x ¬≃⇩p 0"
and wyxz: "(y - w) - (z - x) ¬≃⇩p 0"
using p_equality_adelic_int.conv_0
by (fast, fast)
with nequiv equiv False_False(1) show ?thesis
using 1 2 global_p_depth_adelic_int.depth_nonarch p_equality_adelic_int.conv_0
global_p_depth_adelic_int.global_depth_setD[of p "(y - w) - (z - x)" 1]
by fastforce
qed
qed
ultimately show
"w ≃⇩p x ∨ ((w - x)°⇧p) ≥ 1 ⟷
y ≃⇩p z ∨ ((y - z)°⇧p) ≥ 1"
by (metis uminus_add_conv_diff symp_lcosetrel distinguished_subset_adelic_int_def)
qed
definition p_equal_adelic_int_quot ::
"'a::nontrivial_factorial_idom prime ⇒
'a adelic_int_quot ⇒ 'a adelic_int_quot ⇒ bool"
where
"p_equal_adelic_int_quot p x y ≡
(Rep_adelic_int_quot x) ≃⇩p (Rep_adelic_int_quot y)"
lift_definition p_restrict_adelic_int_coset ::
"'a::nontrivial_factorial_idom adelic_int coset_by_dist_sbgrp ⇒
('a prime ⇒ bool) ⇒ 'a adelic_int coset_by_dist_sbgrp"
is "λx P. x prestrict P"
by (
simp add: global_p_depth_adelic_int.global_depth_set_p_restrict
flip: global_p_depth_adelic_int.p_restrict_minus
)
definition p_restrict_adelic_int_quot ::
"'a::nontrivial_factorial_idom adelic_int_quot ⇒
('a prime ⇒ bool) ⇒ 'a adelic_int_quot"
where
"p_restrict_adelic_int_quot x P ≡
Abs_adelic_int_quot ((Rep_adelic_int_quot x) prestrict P)"
end
context
fixes p :: "'a::nontrivial_factorial_idom prime"
begin
lemma p_equal_adelic_int_coset_abs_eq0:
"distinguished_quotient_coset x ≃⇩p 0 ⟷
x ≃⇩p 0 ∨ (x°⇧p) ≥ 1"
for x :: "'a adelic_int"
unfolding p_equal_adelic_int_coset.abs_eq zero_coset_by_dist_sbgrp.abs_eq by simp
lemma p_equal_adelic_int_coset_abs_eq1:
"distinguished_quotient_coset x ≃⇩p 1 ⟷
x ≃⇩p 1 ∨ ((x - 1)°⇧p) ≥ 1"
for x :: "'a adelic_int"
unfolding p_equal_adelic_int_coset.abs_eq one_coset_by_dist_sbgrp.abs_eq by simp
lemma p_equal_adelic_int_quot_abs_eq:
"(adelic_int_quot x) ≃⇩p (adelic_int_quot y) ⟷
x ≃⇩p y ∨ ((x - y)°⇧p) ≥ 1"
for x y :: "'a adelic_int"
using Abs_adelic_int_quot_inverse[of "distinguished_quotient_coset x"]
Abs_adelic_int_quot_inverse[of "distinguished_quotient_coset y"]
p_equal_adelic_int_coset.abs_eq
unfolding p_equal_adelic_int_quot_def
by auto
lemma p_equal_adelic_int_quot_abs_eq0:
"adelic_int_quot x ≃⇩p 0 ⟷
x ≃⇩p 0 ∨ (x°⇧p) ≥ 1"
for x :: "'a adelic_int"
using p_equal_adelic_int_quot_abs_eq unfolding zero_adelic_int_quot by fastforce
lemma p_equal_adelic_int_quot_abs_eq1:
"adelic_int_quot x ≃⇩p 1 ⟷
x ≃⇩p 1 ∨ ((x - 1)°⇧p) ≥ 1"
for x :: "'a adelic_int"
using p_equal_adelic_int_quot_abs_eq unfolding one_adelic_int_quot by fastforce
end
lemma p_restrict_adelic_int_quot_abs_eq:
"(adelic_int_quot x) prestrict P = adelic_int_quot (x prestrict P)"
for P :: "'a::nontrivial_factorial_idom prime ⇒ bool" and x :: "'a adelic_int"
unfolding p_restrict_adelic_int_quot_def
by (simp add: Abs_adelic_int_quot_inverse p_restrict_adelic_int_coset.abs_eq)
global_interpretation p_equality_adelic_int_quot:
p_equality_no_zero_divisors_1
"p_equal :: 'a::nontrivial_euclidean_ring_cancel prime ⇒
'a adelic_int_quot ⇒ 'a adelic_int_quot ⇒ bool"
proof
fix p :: "'a prime"
define E :: "'a adelic_int_quot ⇒ 'a adelic_int_quot ⇒ bool"
where "E ≡ p_equal p"
have "reflp E"
unfolding E_def
proof (intro reflpI)
fix x :: "'a adelic_int_quot" show "x ≃⇩p x"
by (cases x rule: adelic_int_quot_cases, simp add: p_equal_adelic_int_quot_abs_eq)
qed
moreover have "symp E"
unfolding E_def
proof (intro sympI)
fix x y :: "'a adelic_int_quot"
show "x ≃⇩p y ⟹ y ≃⇩p x"
by (
cases x y rule: two_adelic_int_quot_cases, simp add: p_equal_adelic_int_quot_abs_eq,
metis p_equality_adelic_int.sym global_p_depth_adelic_int.depth_diff
)
qed
moreover have "transp E"
unfolding E_def
proof (intro transpI)
fix x y z :: "'a adelic_int_quot"
assume xy: "x ≃⇩p y" and yz: "y ≃⇩p z"
show "x ≃⇩p z"
proof (cases x y z rule: three_adelic_int_quot_cases)
case (adelic_int_quot_adelic_int_quot_adelic_int_quot a b c)
have "a ≃⇩p c ∨ ((a - c)°⇧p) ≥ 1"
proof (rule iffD1, rule disj_commute, intro disjCI)
assume ac: "a ¬≃⇩p c"
with xy yz adelic_int_quot_adelic_int_quot_adelic_int_quot consider
(ab) "a ≃⇩p b" "1 ≤ ((b - c)°⇧p)" |
(bc) "b ≃⇩p c" "1 ≤ ((a - b)°⇧p)" |
(neither) "1 ≤ ((a - b)°⇧p)" "1 ≤ ((b - c)°⇧p)"
using p_equal_adelic_int_quot_abs_eq p_equality_adelic_int.trans by meson
thus "1 ≤ ((a - c)°⇧p)"
proof cases
case ab thus ?thesis using adelic_int_diff_depth_gt0_equiv_trans[of 0 p a b c] by simp
next
case bc thus ?thesis
using adelic_int_diff_depth_gt0_equiv_trans[of 0 p c b a] p_equality_adelic_int.sym
global_p_depth_adelic_int.depth_diff[of p b a]
global_p_depth_adelic_int.depth_diff[of p a c]
by force
next
case neither with ac show ?thesis
using adelic_int_diff_depth_gt0_trans[of 0 p a b c] by simp
qed
qed
with adelic_int_quot_adelic_int_quot_adelic_int_quot(1,3) show ?thesis
using p_equal_adelic_int_quot_abs_eq by auto
qed
qed
ultimately show "equivp E" by (auto intro: equivpI)
fix x y :: "'a adelic_int_quot"
show "(x ≃⇩p y) = (x - y ≃⇩p 0)"
by (
cases x y rule: two_adelic_int_quot_cases,
simp add: minus_adelic_int_quot p_equal_adelic_int_quot_abs_eq
p_equal_adelic_int_quot_abs_eq0,
metis p_equality_adelic_int.conv_0
)
show "y ≃⇩p 0 ⟹ x * y ≃⇩p 0"
proof (cases x y rule: two_adelic_int_quot_cases)
case (adelic_int_quot_adelic_int_quot a b)
assume "y ≃⇩p 0"
with adelic_int_quot_adelic_int_quot(2)
have "b ≃⇩p 0 ∨ 1 ≤ (b°⇧p)"
using p_equal_adelic_int_quot_abs_eq0
by fast
hence "a * b ≃⇩p 0 ∨ 1 ≤ ((a * b)°⇧p)"
using adelic_int_depth[of p a] global_p_depth_adelic_int.depth_mult_additive
p_equality_adelic_int.mult_0_right
by fastforce
with adelic_int_quot_adelic_int_quot show ?thesis
using times_adelic_int_quot p_equal_adelic_int_quot_abs_eq0 by metis
qed
have "(1::'a adelic_int_quot) ¬≃⇩p 0"
unfolding p_equal_adelic_int_quot_def
by (
simp only: zero_adelic_int_quot_rep_eq one_adelic_int_quot_rep_eq, transfer,
simp, rule p_equality_adelic_int.one_p_nequal_zero
)
thus "∃x::'a adelic_int_quot. x ¬≃⇩p 0" by blast
show
"x ¬≃⇩p 0 ⟹ y ¬≃⇩p 0 ⟹
x * y ¬≃⇩p 0"
proof (cases x y rule: two_adelic_int_quot_cases)
case (adelic_int_quot_adelic_int_quot a b)
assume x: "x ¬≃⇩p 0" and y: "y ¬≃⇩p 0"
with adelic_int_quot_adelic_int_quot
have a: "a ¬≃⇩p 0" "(a°⇧p) < 1"
and b: "b ¬≃⇩p 0" "(b°⇧p) < 1"
using p_equal_adelic_int_quot_abs_eq0
by (fast, fastforce, fast, fastforce)
from a(1) b(1) have "a * b ¬≃⇩p 0"
using p_equality_adelic_int.no_zero_divisors by blast
moreover from this a(2) b(2) have "((a * b)°⇧p) < 1"
using adelic_int_depth global_p_depth_adelic_int.depth_mult_additive by fastforce
ultimately have "adelic_int_quot (a * b) ¬≃⇩p 0"
using p_equal_adelic_int_quot_abs_eq0 by fastforce
with adelic_int_quot_adelic_int_quot times_adelic_int_quot show "x * y ¬≃⇩p 0"
by metis
qed
qed
overloading
globally_p_equal_adelic_int_quot ≡
"globally_p_equal ::
'a::nontrivial_euclidean_ring_cancel adelic_int_quot ⇒
'a adelic_int_quot ⇒ bool"
begin
definition globally_p_equal_adelic_int_quot ::
"'a::nontrivial_euclidean_ring_cancel adelic_int_quot ⇒
'a adelic_int_quot ⇒ bool"
where globally_p_equal_adelic_int_quot_def[simp]:
"globally_p_equal_adelic_int_quot = p_equality_adelic_int_quot.globally_p_equal"
end
subsubsection ‹Embedding of constants›
global_interpretation global_p_equal_adelic_int_quot:
global_p_equal_w_consts
"p_equal :: 'a::nontrivial_euclidean_ring_cancel prime ⇒
'a adelic_int_quot ⇒ 'a adelic_int_quot ⇒ bool"
"p_restrict ::
'a adelic_int_quot ⇒ ('a prime ⇒ bool) ⇒
'a adelic_int_quot"
"λf. adelic_int_quot (adelic_int_consts f)"
proof (unfold_locales, fold globally_p_equal_adelic_int_quot_def)
fix p :: "'a prime"
and x y :: "'a adelic_int_quot"
show "x ≃⇩∀⇩p y ⟹ x = y"
proof (cases x y rule: two_adelic_int_quot_cases)
case (adelic_int_quot_adelic_int_quot a b)
moreover assume xy: "x ≃⇩∀⇩p y"
ultimately have
"∀p::'a prime.
- a + b ¬≃⇩p 0 ⟶ ((- a + b)°⇧p) ≥ 1"
using p_equality_adelic_int.conv_0[of _ b a] p_equal_adelic_int_quot_abs_eq[of _ a b]
p_equality_adelic_int.sym[of _ a b]
global_p_depth_adelic_int.depth_diff[of _ a b]
by fastforce
with adelic_int_quot_adelic_int_quot show "x = y"
using distinguished_quotient_coset_eqI[of a b] global_p_depth_adelic_int.global_depth_setI
by fastforce
qed
fix P :: "'a prime ⇒ bool"
show "P p ⟹ x prestrict P ≃⇩p x"
by (
cases x rule: adelic_int_quot_cases,
simp add: p_restrict_adelic_int_quot_abs_eq p_equal_adelic_int_quot_abs_eq
global_p_depth_adelic_int.p_restrict_equiv
)
show "¬ P p ⟹ x prestrict P ≃⇩p 0"
by (
cases x rule: adelic_int_quot_cases,
simp add: p_restrict_adelic_int_quot_abs_eq p_equal_adelic_int_quot_abs_eq0,
metis global_p_depth_adelic_int.p_restrict_equiv0
)
fix f g :: "'a prime ⇒ 'a"
show
"adelic_int_quot (adelic_int_consts (f - g)) =
adelic_int_quot (adelic_int_consts f) - adelic_int_quot (adelic_int_consts g)"
using global_p_depth_adelic_int.consts_diff minus_adelic_int_quot by metis
show
"adelic_int_quot (adelic_int_consts (f * g)) =
adelic_int_quot (adelic_int_consts f) * adelic_int_quot (adelic_int_consts g)"
using global_p_depth_adelic_int.consts_mult times_adelic_int_quot by metis
qed (metis global_p_depth_adelic_int.consts_1 one_adelic_int_quot)
abbreviation "adelic_int_quot_consts ≡ global_p_equal_adelic_int_quot.consts"
abbreviation "adelic_int_quot_const ≡ global_p_equal_adelic_int_quot.const"
lemma p_equal_adelic_int_quot_consts_iff:
"(adelic_int_quot_consts f) ≃⇩p (adelic_int_quot_consts g) ⟷
(f p) pmod p = (g p) pmod p"
(is "?L ⟷ ?R")
proof-
have "((λp. fls_const (f p)) - (λp. fls_const (g p))) p = fls_const (f p - g p)"
by (simp add: fls_minus_const)
have "?L ⟷ f p = g p ∨ 1 ≤ int (pmultiplicity p ((f - g) p))"
using p_equal_adelic_int_quot_abs_eq global_p_depth_adelic_int.consts_diff
global_p_depth_adelic_int.p_equal_func_of_consts
global_p_depth_adelic_int.p_depth_func_of_consts
by metis
also have "… ⟷ ?R"
using Rep_prime_not_unit multiplicity_gt_zero_iff[of "f p - g p"]
mod_eq_dvd_iff[of "f p" "Rep_prime p" "g p"]
by force
finally show ?thesis by blast
qed
lemma p_equal0_adelic_int_quot_consts_iff:
"(adelic_int_quot_consts f) ≃⇩p 0 ⟷ (f p) pmod p = 0"
(is "?L ⟷ ?R")
proof-
have "?L ⟷ f p pmod p = 0 pmod p"
by (
metis global_p_equal_adelic_int_quot.consts_0 p_equal_adelic_int_quot_consts_iff
zero_fun_apply
)
thus ?thesis by auto
qed
lemma adelic_int_quot_consts_eq_iff:
"adelic_int_quot_consts f = adelic_int_quot_consts g ⟷
(∀p. (f p) pmod p = (g p) pmod p)"
using global_p_equal_adelic_int_quot.global_eq_iff p_equal_adelic_int_quot_consts_iff[of _ f g]
by auto
lemma adelic_int_quot_consts_eq0_iff:
"(adelic_int_quot_consts f) = 0 ⟷
(∀p. (f p) pmod p = 0)"
using global_p_equal_adelic_int_quot.global_eq_iff p_equal0_adelic_int_quot_consts_iff[of _ f]
by auto
lemmas
p_equal_adelic_int_quot_const_iff =
p_equal_adelic_int_quot_consts_iff[of _ "λp. _" "λp. _"]
and p_equal0_adelic_int_quot_const_iff = p_equal0_adelic_int_quot_consts_iff[of _ "λp. _"]
and adelic_int_quot_const_eq_iff = adelic_int_quot_consts_eq_iff[of "λp. _" "λp. _"]
and adelic_int_quot_const_eq0_iff = adelic_int_quot_consts_eq0_iff[of "λp. _"]
lemma adelic_int_quot_UNIV_eq_consts_range:
"(UNIV::'a::nontrivial_euclidean_ring_cancel adelic_int_quot set) =
range (adelic_int_quot_consts)"
proof (standard, standard)
fix x :: "'a adelic_int_quot"
show "x ∈ range adelic_int_quot_consts"
proof (cases x rule: Abs_adelic_int_quot_cases)
case (adelic_int_quot_Abs_adelic_int a)
have "p_adic_prod_int_quot a ∈ range adelic_int_quot_consts"
proof (cases a)
case (abs_p_adic_prod X)
with adelic_int_quot_Abs_adelic_int(2)
have dX: "∀p::'a prime. (X°⇧p) ≥ 0"
using global_p_depth_p_adic_prod.nonpos_global_depth_setD
p_depth_p_adic_prod.abs_eq[of _ X]
by fastforce
define f :: "'a prime ⇒ 'a" where "f ≡ λp. (X p pmod p) $$ 0"
have "adelic_int_consts f - Abs_adelic_int a ∈ 𝒫⇩∀⇩p"
unfolding global_depth_set_adelic_int_def
proof (intro global_p_depth_adelic_int.global_depth_setI)
fix p :: "'a prime"
assume "(adelic_int_consts f - Abs_adelic_int a) ¬≃⇩p 0"
with adelic_int_quot_Abs_adelic_int(2) abs_p_adic_prod
have nequiv: "(fls_const (f p)) ¬≃⇩p (X p pmod p)"
using p_equality_adelic_int.conv_0
global_p_depth_p_adic_prod.global_depth_set_consts p_equal_adelic_int_abs_eq
p_equal_p_adic_prod.abs_eq global_depth_set_p_adic_prod_def p_equal_fls_pseq_def
fls_pmod_equiv p_equality_fls.trans_left
by metis
have "∀k<0. (X p pmod p) $$ k = 0"
proof clarify
fix k :: int assume "k < 0"
moreover have "(X p°⇧p) ≥ 0" using dX by auto
ultimately show "(X p pmod p) $$ k = 0" using fls_pmod_subdegree[of _ p] by simp
qed
moreover have "fls_const (f p) ≠ X p pmod p" using nequiv by auto
ultimately have "fls_subdegree (fls_const (f p) - X p pmod p) > 0"
by (auto intro: fls_subdegree_greaterI simp add: f_def)
moreover from adelic_int_quot_Abs_adelic_int(2) abs_p_adic_prod have
"((adelic_int_consts f - Abs_adelic_int a)°⇧p) =
((fls_const (f p) - X p pmod p)°⇧p)"
using global_p_depth_p_adic_prod.global_depth_set_consts minus_apply[of _ X p]
p_depth_adelic_int_diff_abs_eq[of _ a p] p_depth_p_adic_prod_diff_abs_eq[of p _ X]
p_depth_fls_pseq_def global_depth_set_p_adic_prod_def p_depth_fls.depth_equiv
p_equality_fls.minus_left fls_pmod_equiv
by metis
ultimately show "((adelic_int_consts f - Abs_adelic_int a)°⇧p) ≥ 1"
using nequiv p_equality_fls.conv_0 p_depth_fls_ge_p_equal_subdegree' by fastforce
qed
hence
"p_adic_prod_int_quot a =
p_adic_prod_int_quot (abs_p_adic_prod (λp. fls_const (f p)))"
using Abs_adelic_int_quot_inject distinguished_quotient_coset_eqI by force
thus "adelic_int_quot (Abs_adelic_int a) ∈ range adelic_int_quot_consts" by blast
qed
with adelic_int_quot_Abs_adelic_int(1) show ?thesis by blast
qed
qed simp
lemma adelic_int_quot_constsE:
fixes x :: "'a::nontrivial_euclidean_ring_cancel adelic_int_quot"
obtains f where "x = adelic_int_quot_consts f"
using adelic_int_quot_UNIV_eq_consts_range by blast
lemma adelic_int_quot_reduced_constsE:
fixes x :: "'a::nontrivial_euclidean_ring_cancel adelic_int_quot"
obtains f
where "x = adelic_int_quot_consts f"
and "∀p::'a prime. (f p) pdiv p = 0"
proof-
obtain g where g: "x = adelic_int_quot_consts g"
using adelic_int_quot_constsE by blast
define f :: "'a prime ⇒ 'a" where "f ≡ λp. g p pmod p"
hence "∀p::'a prime. (f p) pdiv p = 0"
using div_mult_mod_eq by fastforce
moreover from g f_def have "x = adelic_int_quot_consts f"
using adelic_int_quot_consts_eq_iff by force
ultimately show thesis using that by presburger
qed
lemma adelic_int_quot_prestrict_zero_depth_abs_eq:
"adelic_int_quot (x prestrict (λp::'a prime. (x°⇧p) = 0)) =
adelic_int_quot x"
for x :: "'a::nontrivial_euclidean_ring_cancel adelic_int"
proof (intro global_p_equal_adelic_int_quot.global_imp_eq, standard)
fix p :: "'a prime"
define P :: "'a prime ⇒ bool" where "P ≡ λp. (x°⇧p) = 0"
hence
"x prestrict P ¬≃⇩p x ⟹
((x prestrict P - x)°⇧p) ≥ 1"
using adelic_int_prestrict_zero_depth by fast
thus "(adelic_int_quot (x prestrict P)) ≃⇩p (adelic_int_quot x)"
using p_equal_adelic_int_quot_abs_eq by blast
qed
subsubsection ‹Division and inverses›
global_interpretation p_equal_div_inv_adelic_int_quot:
global_p_equal_div_inv
"p_equal :: 'a::nontrivial_factorial_unique_euclidean_bezout prime ⇒
'a adelic_int_quot ⇒ 'a adelic_int_quot ⇒ bool"
"p_restrict ::
'a adelic_int_quot ⇒ ('a prime ⇒ bool) ⇒
'a adelic_int_quot"
proof
define A :: "'a adelic_int coset_by_dist_sbgrp ⇒ 'a adelic_int_quot"
where "A ≡ Abs_adelic_int_quot"
fix p :: "'a prime" and x y :: "'a adelic_int_quot"
show "inverse (inverse x) = x"
proof (cases x rule: adelic_int_quot_cases)
case (adelic_int_quot a)
moreover define P :: "'a prime ⇒ bool"
where "P ≡ λp. (a°⇧p) = 0"
moreover from this have "adelic_int_quot (a prestrict P) = adelic_int_quot a"
using global_p_equal_adelic_int_quot.global_imp_eq p_equal_adelic_int_quot_abs_eq
adelic_int_prestrict_zero_depth
by fast
ultimately show "inverse (inverse x) = x"
using inverse_adelic_int_quot adelic_int_inverse_inverse by metis
qed
show "(inverse x ≃⇩p 0) = (x ≃⇩p 0)"
by (
cases x rule: adelic_int_quot_cases,
simp add: A_def inverse_adelic_int_quot p_equal_adelic_int_quot_abs_eq0
adelic_int_inverse_depth adelic_int_inverse_equiv0_iff'
)
show "x ¬≃⇩p 0 ⟹ x / x ≃⇩p 1"
proof (cases x rule: adelic_int_quot_cases)
case (adelic_int_quot a)
moreover assume "x ¬≃⇩p 0"
ultimately have "a ¬≃⇩p 0" and "a°⇧p = 0"
using p_equal_adelic_int_quot_abs_eq0 adelic_int_depth[of p a] by (blast, fastforce)
hence "a / a ≃⇩p 1"
using adelic_int_divide_self[of a] global_p_depth_adelic_int.p_restrict_equiv[of _ p]
by presburger
with adelic_int_quot show "x / x ≃⇩p 1"
using p_equal_adelic_int_quot_abs_eq1 divide_adelic_int_quot by metis
qed
show "inverse (x * y) = inverse x * inverse y"
by (
cases x y rule: two_adelic_int_quot_cases,
simp add: A_def inverse_adelic_int_quot times_adelic_int_quot adelic_int_inverse_mult
)
qed simp
subsection ‹Special case of integer›
context
fixes p :: "int prime"
begin
lemma inj_on_const_prestrict_single_int_prime:
"inj_on (λk. adelic_int_quot_const k prestrict ((=) p)) {0..Rep_prime p - 1}"
proof (standard, unfold atLeastAtMost_iff, clarify)
define pp :: int and C :: "int ⇒ int adelic_int_quot"
where "pp ≡ Rep_prime p"
and "C ≡ λk. adelic_int_quot_const k prestrict ((=) p)"
fix j k :: int
show
"⟦ j ≥ 0; j ≤ pp - 1; k ≥ 0; k ≤ pp - 1; C j = C k ⟧
⟹ j = k"
proof (induct j k rule: linorder_wlog)
fix j k :: int
assume j : "j ≥ 0" "j ≤ pp - 1"
and k : "k ≥ 0" "k ≤ pp - 1"
and jk: "j ≤ k" "C j = C k"
from pp_def j(1) k(2) jk(1) have "((k - j)°⇧p) = 0"
using p_depth_const[of p "k - j"] zdvd_imp_le[of pp "k - j"] not_dvd_imp_multiplicity_0
by (cases "j = k") auto
hence "¬ ((k - j)°⇧p) ≥ 1" by presburger
with C_def jk(2) show "j = k"
using global_p_equal_adelic_int_quot.p_equal_iff_p_restrict_eq adelic_int_p_depth_const
global_p_depth_adelic_int.const_diff global_p_depth_adelic_int.const_p_equal[of p]
p_equal_adelic_int_quot_abs_eq[of p "adelic_int_const k" "adelic_int_const j"]
by metis
qed simp
qed
lemma range_prestrict_single_int_prime:
"range (λx. x prestrict ((=) p)) =
(λk. adelic_int_quot_const k prestrict ((=) p)) ` {0..Rep_prime p - 1}"
proof safe
define pp :: int and C :: "int ⇒ int adelic_int_quot"
where "pp ≡ Rep_prime p"
and "C ≡ λk. adelic_int_quot_const k prestrict ((=) p)"
fix x :: "int adelic_int_quot"
obtain f where f: "x = adelic_int_quot_consts f" "(f p) pdiv p = 0"
using adelic_int_quot_reduced_constsE by blast
from f(2) pp_def have "f p ∈ {0..pp - 1}"
using div_mult_mod_eq[of "f p" "Rep_prime p"] prime_gt_0_int Rep_prime pos_mod_sign[of pp "f p"]
pos_mod_bound[of pp "f p"]
by auto
with f(1) show "x prestrict ((=) p) ∈ C ` {0..pp - 1}"
using p_equal_adelic_int_quot_consts_iff
unfolding C_def
by (fastforce intro: global_p_equal_adelic_int_quot.p_restrict_eq_p_restrictI)
qed simp
lemma finite_range_prestrict_single_int_prime:
"finite (range (λx::int adelic_int_quot. x prestrict ((=) p)))"
using range_prestrict_single_int_prime finite_image_iff inj_on_const_prestrict_single_int_prime
by simp
lemma card_range_prestrict_single_int_prime:
"card (range (λx::int adelic_int_quot. x prestrict ((=) p))) = nat (Rep_prime p)"
using bij_betw_imageI[of _ _ "range (λx. x prestrict ((=) p))"] bij_betw_same_card
inj_on_const_prestrict_single_int_prime range_prestrict_single_int_prime[symmetric]
by fastforce
end
end