Theory Kneser_Cauchy_Davenport_preliminaries
section‹Preliminaries›
theory Kneser_Cauchy_Davenport_preliminaries
imports
Complex_Main
"Pluennecke_Ruzsa_Inequality.Pluennecke_Ruzsa_Inequality"
"HOL-Number_Theory.Prime_Powers"
begin
context subgroup_of_group
begin
interpretation left: left_translations_of_group ..
interpretation right: right_translations_of_group ..
interpretation transformation_group "left.translation ` H" G ..
lemma Right_Coset_eq_iff:
assumes "x ∈ G" and "y ∈ G"
shows "H |⋅ x = (H |⋅ y) ⟷ H |⋅ x ∩ (H |⋅ y) ≠ {}"
using assms Right_Coset_is_orbit
by (metis Int_absorb orbit.disjoint orbit.natural.map_closed orbit.non_vacuous)
end
context additive_abelian_group
begin
subsection‹Elementary lemmas on sumsets ›
lemma sumset_translate_eq_right:
assumes "A ⊆ G" and "B ⊆ G" and "x ∈ G"
shows "(sumset A {x} = sumset B {x}) ⟷ A = B" using assms
by (smt (verit, best) Diff_Int_distrib2 Diff_eq_empty_iff
Int_Un_eq(1) Int_absorb2 Un_Diff_cancel2 Un_commute insert_disjoint(2)
subset_refl sumset_is_empty_iff sumsetdiff_sing)
lemma sumset_translate_eq_left:
assumes "A ⊆ G" and "B ⊆ G" and "x ∈ G"
shows " (sumset {x} A = sumset {x} B) ⟷ A = B" using assms
by (simp add: sumset_commute sumset_translate_eq_right)
lemma differenceset_translate_eq_right:
assumes "A ⊆ G" and "B ⊆ G" and "x ∈ G"
shows "(differenceset A {x} = differenceset B {x}) ⟷ A = B" using assms
by (metis Int_absorb2 differenceset_commute minus_minusset minusset_subset_carrier
sumset_translate_eq_left)
lemma differenceset_translate_eq_left:
assumes "A ⊆ G" and "B ⊆ G" and "x ∈ G"
shows "(differenceset {x} A = differenceset {x} B) ⟷ A = B" using assms
by (metis differenceset_commute differenceset_translate_eq_right)
lemma sumset_inter_union_subset:
"sumset (A ∩ B) (A ∪ B) ⊆ sumset A B"
by (metis Int_Diff_Un Int_Un_eq(2) Un_subset_iff sumset_commute sumset_subset_Un(2)
sumset_subset_Un2)
lemma differenceset_group_eq:
"G = differenceset G G"
using equalityE minusset_eq minusset_triv subset_antisym sumset_D(1) sumset_subset_carrier
sumset_mono image_mono Int_absorb by metis
lemma card_sumset_singleton_subset_eq:
assumes "a ∈ G" and "A ⊆ G"
shows "card (sumset {a} A) = card A"
using assms card_sumset_singleton_eq card.infinite card_sumset_0_iff' le_iff_inf sumset_commute
by metis
lemma card_differenceset_singleton_mem_eq:
assumes "a ∈ G" and "A ⊆ G"
shows "card A = card (differenceset A {a})"
using assms by (metis card_minusset' card_sumset_singleton_subset_eq differenceset_commute
minusset_subset_carrier)
lemma card_singleton_differenceset_eq:
assumes "a ∈ G" and "A ⊆ G"
shows "card A = card (differenceset {a} A)"
using assms by (metis card_minusset' card_sumset_singleton_subset_eq minusset_subset_carrier)
lemma sumset_eq_Union_left:
assumes "A ⊆ G"
shows "sumset A B = (⋃ a ∈ A. sumset {a} B)"
proof
show "sumset A B ⊆ (⋃ a ∈ A. sumset {a} B)"
using assms sumset.cases Int_absorb2 Int_iff UN_iff singletonI sumset.sumsetI
by (smt (verit, del_insts) subsetI)
next
show "(⋃ a ∈ A. sumset {a} B) ⊆ sumset A B"
using sumset by auto
qed
lemma sumset_eq_Union_right:
assumes "B ⊆ G"
shows "sumset A B = (⋃ b ∈ B. sumset A {b})"
using assms sumset_commute sumset_eq_Union_left by (metis (no_types, lifting) Sup.SUP_cong)
lemma sumset_singletons_eq:
assumes "a ∈ G" and "b ∈ G"
shows "sumset {a} {b} = {a ⊕ b}"
using assms sumset.simps subset_antisym by auto
lemma sumset_eq_subset_differenceset:
assumes "K ⊆ G" and "K ≠ {}" and "A ⊆ G" and "sumset A K = sumset B K"
shows "A ⊆ differenceset (sumset B K) K"
proof
fix a assume ha: "a ∈ A"
obtain k where hk: "k ∈ K" using assms(2) by blast
then have "a ⊕ k ∈ sumset B K" using assms sumset.sumsetI ha by blast
then have "a ⊕ (k ⊖ k) ∈ differenceset (sumset B K) K" using hk assms ha minusset.minussetI
subset_iff sumset.sumsetI by (smt (verit) associative composition_closed inverse_closed)
then show "a ∈ differenceset (sumset B K) K" using hk ha subsetD assms right_unit
by (metis invertible invertible_right_inverse)
qed
end
locale subgroup_of_additive_abelian_group =
subgroup_of_abelian_group H G "(⊕)" 𝟬 + additive_abelian_group G "(⊕)" 𝟬
for H G and addition (infixl ‹⊕› 65) and zero (‹𝟬›)
begin
notation Left_Coset (infixl ‹⋅|› 70)
lemma Left_Coset_eq_sumset:
assumes "x ∈ G"
shows "sumset {x} H = x ⋅| H"
using assms Left_Coset_memI sumset.simps by fastforce
lemma sumset_subgroup_eq_iff:
assumes "a ∈ G" and "b ∈ G"
shows "sumset {a} H = sumset {b} H ⟷
(sumset {a} H) ∩ (sumset {b} H) ≠ {}"
using Right_Coset_eq_iff assms Left_Coset_eq_sumset Left_equals_Right_coset by presburger
lemma card_divide_sumset:
assumes "A ⊆ G"
shows "card H dvd card (sumset A H)"
proof(cases "finite H ∧ finite A")
case hfin: True
then have hfinsum: "⋀ X. X ∈ ((λ a. sumset {a} H) ` A) ⟹ finite X"
using finite_sumset by force
moreover have "pairwise disjnt ((λ a. sumset {a} H) ` A)"
using pairwise_imageI disjnt_def sumset_subgroup_eq_iff subset_eq assms by (smt (verit, best))
moreover have "card H dvd sum card ((λ a. sumset {a} H) ` A)"
proof(intro dvd_sum)
fix X assume "X ∈ (λ a. sumset {a} H) ` A"
then show "card H dvd card X" using dvd_refl
using Left_equals_Right_coset Right_Coset_cardinality assms Left_Coset_eq_sumset by auto
qed
ultimately show ?thesis using assms sumset_eq_Union_left card_Union_disjoint by metis
next
case False
then show ?thesis using assms card_sumset_0_iff by (metis card_eq_0_iff dvd_0_right sub subsetI)
qed
lemma sumset_subgroup_eq_Class_Union:
assumes "A ⊆ G"
shows "sumset A H = (⋃ (Class ` A))"
proof
show "sumset A H ⊆ ⋃ (Class ` A)"
proof
fix x assume "x ∈ sumset A H"
then obtain a b where ha: "a ∈ A" and "b ∈ H" and "x = a ⊕ b"
using sumset.cases by blast
then have "x ∈ Class a" using Left_Coset_Class_unit Left_Coset_eq_sumset assms by blast
thus "x ∈ ⋃ (Class ` A)" using ha by blast
qed
next
show "⋃ (Class ` A) ⊆ sumset A H"
proof(intro Union_least)
fix X assume "X ∈ Class ` A"
then obtain a where "a ∈ A" and "X = Class a" by blast
moreover hence "{a} ⊆ A" by auto
ultimately show "X ⊆ sumset A H" using Left_Coset_Class_unit
Left_Coset_eq_sumset assms sumset_mono subset_refl in_mono by metis
qed
qed
lemma Class_image_sumset_subgroup_eq:
assumes "A ⊆ G"
shows "Class ` (sumset A H) = Class ` A"
proof
show "Class ` sumset A H ⊆ Class ` A"
proof
fix x assume "x ∈ Class ` sumset A H"
then obtain c where hc: "c ∈ sumset A H" and "x = Class c" by blast
moreover obtain a b where ha: "a ∈ A" and "b ∈ H" and "c = a ⊕ b" using hc sumset.cases
by blast
ultimately show "x ∈ Class ` A" using ha Class_eq CongruenceI assms composition_closed
sumset.cases Partition_def commutative image_eqI left_unit sub unit_closed
by (smt (verit, ccfv_threshold) Block_self Class_cong Normal_def)
qed
next
show "Class ` A ⊆ Class ` sumset A H" using assms right_unit subsetD subsetI sumset.sumsetI
unit_closed by (smt (verit, del_insts) image_subset_iff sub_unit_closed)
qed
lemma Class_cover_imp_subset_or_disj:
assumes "A = (⋃ (Class ` C))" and "x ∈ G" and "C ⊆ G"
shows "Class x ⊆ A ∨ Class x ∩ A = {}"
proof(intro disjCI)
assume "Class x ∩ A ≠ {}"
then obtain c where "c ∈ C" and "Class x ∩ Class c ≠ {}" using assms by blast
then show "Class x ⊆ A" using assms not_disjoint_implies_equal Sup_upper imageI subset_iff
by blast
qed
end
context additive_abelian_group
begin
subsection‹Stabilizer and basic properties›
text‹We define the stabilizer or group of periods of a nonempty subset of an abelian group.›
definition stabilizer::"'a set ⇒ 'a set " where
"stabilizer S ≡ {x ∈ G. sumset {x} (S ∩ G) = S ∩ G}"
lemma stabilizer_is_subgroup: fixes S :: "'a set"
shows "subgroup (stabilizer S) G (⊕) (𝟬)"
proof (intro subgroupI)
show "stabilizer S ⊆ G" using stabilizer_def by auto
next
show "𝟬 ∈ stabilizer S" using stabilizer_def by (simp add: Int_absorb1 Int_commute)
next
fix a b assume haS: "a ∈ stabilizer S" and hbS: "b ∈ stabilizer S"
then have haG: "a ∈ G" and hbG: "b ∈ G" using stabilizer_def by auto
have "sumset {a ⊕ b} (S ∩ G) = sumset {a} (sumset {b} (S ∩ G))"
proof
show "sumset {a ⊕ b} (S ∩ G) ⊆ sumset {a} (sumset {b} (S ∩ G))" using haG hbG
empty_subsetI insert_subset subsetI sumset.simps sumset_assoc sumset_mono
by metis
show "sumset {a} (sumset {b} (S ∩ G)) ⊆ sumset {a ⊕ b} (S ∩ G)"
using empty_iff insert_iff sumset.simps sumset_assoc by (smt (verit, best) subsetI)
qed
then show "a ⊕ b ∈ stabilizer S" using haS hbS stabilizer_def by auto
next
fix g assume "g ∈ stabilizer S"
thus "invertible g" using stabilizer_def by auto
next
fix g assume hgS: "g ∈ stabilizer S"
then have hinvsum : "inverse g ⊕ g = 𝟬" using stabilizer_def by simp
have "sumset {inverse g} (sumset {g} (S ∩ G)) = (S ∩ G)"
proof
show "sumset {inverse g} (sumset {g} (S ∩ G)) ⊆ (S ∩ G)" using
empty_iff insert_iff sumset.simps sumset_assoc subsetI left_unit hinvsum
by (smt (verit, ccfv_threshold))
show "(S ∩ G) ⊆ sumset {inverse g} (sumset {g} (S ∩ G))"
proof
fix s assume hs: "s ∈ (S ∩ G)"
then have "inverse g ⊕ g ⊕ s ∈ sumset {inverse g} (sumset {g} (S ∩ G))" using
hgS stabilizer_def additive_abelian_group.sumset.sumsetI
additive_abelian_group_axioms associative in_mono inverse_closed mem_Collect_eq singletonI
by (smt (z3) IntD2)
thus "s ∈ sumset {inverse g} (sumset {g} (S ∩ G))" using hinvsum hs
by simp
qed
qed
thus "inverse g ∈ stabilizer S" using hgS stabilizer_def by auto
qed
interpretation subgroup_of_additive_abelian_group "stabilizer A" "G" "(⊕)" "𝟬"
using stabilizer_is_subgroup subgroup_of_abelian_group_def
by (metis abelian_group_axioms additive_abelian_group_axioms group_axioms
subgroup_of_additive_abelian_group_def subgroup_of_group_def)
lemma zero_mem_stabilizer: "𝟬 ∈ stabilizer A" ..
lemma stabilizer_is_nonempty:
shows "stabilizer S ≠ {}"
using sub_unit_closed by blast
lemma Left_Coset_eq_sumset_stabilizer:
assumes "x ∈ G"
shows "sumset {x} (stabilizer B) = x ⋅| (stabilizer B)"
by (simp add: Left_Coset_eq_sumset assms)
lemma stabilizer_subset_difference_singleton:
assumes "S ⊆ G" and "s ∈ S"
shows "stabilizer S ⊆ differenceset S {s}"
proof
fix x assume hx: "x ∈ stabilizer S"
then obtain t where ht: "t ∈ S" and "x ⊕ s = t" using assms stabilizer_def by blast
then have "x = t ⊖ s" using hx stabilizer_def assms associative
by (metis (no_types, lifting) in_mono inverse_closed invertible invertible_right_inverse sub
sub.right_unit)
thus "x ∈ differenceset S {s}" using ht assms
by (simp add: minusset.minussetI subsetD sumset.sumsetI)
qed
lemma stabilizer_subset_singleton_difference:
assumes "S ⊆ G" and "s ∈ S"
shows "stabilizer S ⊆ differenceset {s} S"
proof-
have "stabilizer S ⊆ minusset (stabilizer S)" using assms Int_absorb2 minusset_eq
subgroup.image_of_inverse submonoid.sub subset_eq
by (smt (verit) stabilizer_is_subgroup stabilizer_subset_difference_singleton
sumset_subset_carrier)
moreover have "minusset (stabilizer S) ⊆ minusset (differenceset S {s})"
proof
fix x assume hx1: "x ∈ minusset (stabilizer S)"
then have hx: "inverse x ∈ stabilizer S"
by (metis invertible invertible_inverse_inverse minusset.cases)
then obtain t where ht: "t ∈ S" and "inverse x ⊕ s = t" using assms stabilizer_def by blast
then have hx2: "inverse x = t ⊖ s" using hx stabilizer_def assms
by (smt (verit, ccfv_threshold) commutative in_mono inverse_closed invertible
invertible_left_inverse2 sub)
thus "x ∈ minusset (differenceset S {s})" using ht assms
by (smt (verit, best) hx1 additive_abelian_group.sumset.sumsetI additive_abelian_group_axioms
inverse_closed invertible invertible_inverse_inverse minusset.cases minusset.minussetI
singletonI subset_iff)
qed
ultimately show ?thesis using differenceset_commute assms by blast
qed
lemma stabilizer_subset_nempty:
assumes "S ≠ {}" and "S ⊆ G"
shows "stabilizer S ⊆ differenceset S S"
proof
fix x assume hx: "x ∈ stabilizer S"
then obtain s where hs: "s ∈ S ∩ G" using assms by blast
then have "x ⊕ s ∈ S ∩ G" using stabilizer_def assms hx mem_Collect_eq singletonI
sumset.sumsetI sumset_Int_carrier by blast
then obtain t where ht: "t ∈ S" and "x ⊕ s = t" by blast
then have "x = t ⊖ s" using hx stabilizer_def assms(2) hs ht associative
by (metis IntD2 inverse_closed invertible invertible_right_inverse sub sub.right_unit)
thus "x ∈ differenceset S S" using ht hs using assms(2) by blast
qed
lemma stabilizer_coset_subset:
assumes "A ⊆ G" and "x ∈ A"
shows "sumset {x} (stabilizer A) ⊆ A"
proof
fix y assume "y ∈ sumset {x} (stabilizer A)"
moreover hence "stabilizer A ⊆ differenceset A {x}" using assms
stabilizer_subset_difference_singleton by auto
moreover have "sumset {x} (differenceset A {x}) ⊆ A"
proof
fix z assume "z ∈ sumset {x} (differenceset A {x})"
then obtain a where "a ∈ A" and "z = x ⊕ (a ⊖ x)"
using additive_abelian_group.sumset.cases additive_abelian_group_axioms singletonD
minusset.cases assms subsetD by (smt (verit, ccfv_SIG))
thus "z ∈ A" using assms
by (metis additive_abelian_group.inverse_closed additive_abelian_group_axioms
commutative in_mono invertible invertible_right_inverse2)
qed
ultimately show "y ∈ A" by (meson in_mono subset_singleton_iff sumset_mono)
qed
lemma stabilizer_subset_stabilizer_dvd:
assumes "stabilizer A ⊆ stabilizer B"
shows "card (stabilizer A) dvd card (stabilizer B)"
proof(cases "finite (stabilizer B)")
case hB: True
interpret H: subgroup_of_group "stabilizer A" "stabilizer B" "(⊕)" "𝟬"
proof(unfold_locales)
show "stabilizer A ⊆ stabilizer B" using assms by blast
next
show "⋀a b. a ∈ stabilizer A ⟹ b ∈ stabilizer A ⟹ a ⊕ b ∈ stabilizer A"
using stabilizer_is_subgroup group_axioms by simp
next
show "𝟬 ∈ stabilizer A" using sub_unit_closed by blast
qed
show ?thesis using H.lagrange hB by auto
next
case False
then show ?thesis by simp
qed
lemma stabilizer_coset_Un:
assumes "A ⊆ G"
shows "(⋃ x ∈ A. sumset {x} (stabilizer A)) = A"
proof
show "(⋃x∈A. sumset {x} (stabilizer A)) ⊆ A"
using stabilizer_coset_subset assms by blast
next
show "A ⊆ (⋃x∈A. sumset {x} (stabilizer A))"
proof
fix x assume hx: "x ∈ A"
then have "x ∈ sumset {x} (stabilizer A)" using sub_unit_closed assms
by (metis in_mono right_unit singletonI sumset.sumsetI unit_closed)
thus "x ∈ (⋃x∈A. sumset {x} (stabilizer A))" using hx by blast
qed
qed
lemma stabilizer_empty: "stabilizer {} = G"
using sumset_empty Int_empty_left stabilizer_def subset_antisym
by (smt (verit, best) mem_Collect_eq subsetI sumset_Int_carrier_eq(1) sumset_commute)
lemma stabilizer_finite:
assumes "S ⊆ G" and "S ≠ {}" and "finite S"
shows "finite (stabilizer S)"
using stabilizer_subset_nempty assms
by (meson finite_minusset finite_sumset rev_finite_subset)
lemma stabilizer_subset_group:
shows "stabilizer S ⊆ G" using stabilizer_def by blast
lemma sumset_stabilizer_eq_iff:
assumes "a ∈ G" and "b ∈ G"
shows "sumset {a} (stabilizer A) = sumset {b} (stabilizer A) ⟷
(sumset {a} (stabilizer A)) ∩ (sumset {b} (stabilizer A)) ≠ {}"
by (simp add: assms sumset_subgroup_eq_iff)
lemma sumset_stabilizer_eq_Class_Union:
assumes "A ⊆ G"
shows "sumset A (stabilizer B) = (⋃ (Class B ` A))"
by (simp add: assms sumset_subgroup_eq_Class_Union)
lemma card_stabilizer_divide_sumset:
assumes "A ⊆ G"
shows "card (stabilizer B) dvd card (sumset A (stabilizer B))"
by (simp add: assms card_divide_sumset)
lemma Class_image_sumset_stabilizer_eq:
assumes "A ⊆ G"
shows "Class B ` (sumset A (stabilizer B)) = Class B ` A"
by (simp add: Class_image_sumset_subgroup_eq assms)
lemma Class_cover_imp_subset_or_disj:
assumes "A = (⋃ (Class B ` C))" and "x ∈ G" and "C ⊆ G"
shows "Class B x ⊆ A ∨ Class B x ∩ A = {}"
by (simp add: Class_cover_imp_subset_or_disj assms)
lemma stabilizer_sumset_disjoint:
fixes S1 S2 :: "'a set"
assumes "stabilizer S1 ∩ stabilizer S2 = {𝟬}" and "S1 ⊆ G" and "S2 ⊆ G"
and "finite S1" and "finite S2" and "S1 ≠ {}" and "S2 ≠ {}"
shows "card (sumset (stabilizer S1) (stabilizer S2)) =
card (stabilizer S1) * card (stabilizer S2)"
proof-
have inj_on : "inj_on (λ (a, b). a ⊕ b) (stabilizer S1 × stabilizer S2)"
proof(intro inj_onI)
fix x y assume "x ∈ stabilizer S1 × stabilizer S2" and "y ∈ stabilizer S1 × stabilizer S2" and
"(case x of (a, b) ⇒ a ⊕ b) = (case y of (a, b) ⇒ a ⊕ b)"
then obtain a b c d where hx: "x = (a, b)" and hy: "y = (c, d)" and ha: "a ∈ stabilizer S1" and
hb: "b ∈ stabilizer S2" and hc: "c ∈ stabilizer S1" and hd: "d ∈ stabilizer S2" and
habcd: "a ⊕ b = c ⊕ d" by auto
then have haG: "a ∈ G" using stabilizer_def by blast
have hbG: "b ∈ G" using hb stabilizer_def by blast
have hcG: "c ∈ G" using hc stabilizer_def by blast
have hdG: "d ∈ G" using hd stabilizer_def by blast
then have "a ⊖ c = d ⊖ b" using habcd haG hbG hcG hdG
by (metis (full_types) associative commutative composition_closed inverse_equality invertible
invertible_def invertible_left_inverse2)
moreover have "a ⊖ c ∈ stabilizer S1" using ha hc stabilizer_is_subgroup
subgroup.axioms(1) submonoid.sub_composition_closed
by (metis group.invertible group_axioms hcG subgroup.subgroup_inverse_iff)
moreover have "d ⊖ b ∈ stabilizer S2" using hd hb stabilizer_is_subgroup
subgroup.axioms(1) submonoid.sub_composition_closed
by (metis group.invertible group_axioms hbG subgroup.subgroup_inverse_iff)
ultimately have "a ⊖ c = 𝟬" and "d ⊖ b = 𝟬" using assms(1) by auto
thus "x = y" using hx hy haG hbG hcG hdG
by (metis inverse_closed invertible invertible_right_cancel invertible_right_inverse)
qed
moreover have himage : "(λ (a, b). a ⊕ b) ` (stabilizer S1 × stabilizer S2) =
sumset (stabilizer S1) (stabilizer S2)"
proof
show "(λ(a, b). a ⊕ b) ` (stabilizer S1 × stabilizer S2) ⊆ sumset (stabilizer S1) (stabilizer S2)"
using stabilizer_subset_group by force
next
show "sumset (stabilizer S1) (stabilizer S2) ⊆ (λ(a, b). a ⊕ b) ` (stabilizer S1 × stabilizer S2)"
proof
fix x assume "x ∈ sumset (stabilizer S1) (stabilizer S2)"
then obtain s1 s2 where hs1: "s1 ∈ stabilizer S1" and hs2: "s2 ∈ stabilizer S2" and
"x = s1 ⊕ s2" by (meson sumset.cases)
thus "x ∈ (λ(a, b). a ⊕ b) ` (stabilizer S1 × stabilizer S2)" using hs1 hs2 by auto
qed
qed
ultimately show ?thesis using card_image card_cartesian_product by fastforce
qed
lemma stabilizer_sub_sumset_left:
"stabilizer A ⊆ stabilizer (sumset A B)"
proof
fix x assume hx: "x ∈ stabilizer A"
then have "sumset {x} (sumset A B) = sumset A B" using stabilizer_def sumset_assoc
mem_Collect_eq by (smt (verit, del_insts) sumset_Int_carrier_eq(1) sumset_commute)
thus "x ∈ stabilizer (sumset A B)" using hx stabilizer_def
by (metis (mono_tags, lifting) mem_Collect_eq sumset_Int_carrier)
qed
lemma stabilizer_sub_sumset_right:
"stabilizer B ⊆ stabilizer (sumset A B)"
using stabilizer_sub_sumset_left sumset_commute by fastforce
lemma not_mem_stabilizer_obtain:
assumes "A ≠ {}" and "x ∉ stabilizer A" and "x ∈ G" and "A ⊆ G" and "finite A"
obtains a where "a ∈ A" and "x ⊕ a ∉ A"
proof-
have "sumset {x} A ≠ A" using assms stabilizer_def
by (metis (mono_tags, lifting) inf.orderE mem_Collect_eq)
moreover have "card (sumset {x} A) = card A" using assms
by (metis card_sumset_singleton_eq inf.orderE sumset_commute)
ultimately obtain y where "y ∈ sumset {x} A" and "y ∉ A" using assms
by (meson card_subset_eq subsetI)
then obtain a where "a ∈ A" and "x ⊕ a ∉ A" using assms
by (metis singletonD sumset.cases)
thus ?thesis using that by blast
qed
lemma sumset_eq_sub_stabilizer:
assumes "A ⊆ G" and "B ⊆ G" and "finite B"
shows "sumset A B = B ⟹ A ⊆ stabilizer B"
proof
fix x assume hsum: "sumset A B = B" and hx: "x ∈ A"
have "sumset {x} B = B"
proof-
have "sumset {x} B ⊆ B" using hsum hx
by (metis empty_subsetI equalityE insert_subset sumset_mono)
moreover have "card (sumset {x} B) = card B" using assms
by (metis IntD1 Int_absorb1 card_sumset_singleton_eq hx inf_commute sumset_commute)
ultimately show ?thesis using card_subset_eq assms(3) by auto
qed
thus "x ∈ stabilizer B" using hx assms(1) stabilizer_def
by (metis (mono_tags, lifting) assms(2) inf.orderE mem_Collect_eq subsetD)
qed
lemma sumset_stabilizer_eq:
shows "sumset (stabilizer A) (stabilizer A) = stabilizer A"
proof
show "sumset (stabilizer A) (stabilizer A) ⊆ stabilizer A"
using stabilizer_is_subgroup subgroup.axioms(1) subsetI
by (metis (mono_tags, lifting) additive_abelian_group.sumset.simps additive_abelian_group_axioms
submonoid.sub_composition_closed)
next
show "stabilizer A ⊆ sumset (stabilizer A) (stabilizer A)"
using Left_Coset_eq_sumset stabilizer_is_nonempty
stabilizer_subset_group sub_unit_closed additive_abelian_group_axioms right_unit
subset_iff sumsetI by (smt (verit, best))
qed
lemma differenceset_stabilizer_eq:
shows "differenceset (stabilizer A) (stabilizer A) = stabilizer A"
proof
show "differenceset (stabilizer A) (stabilizer A) ⊆ stabilizer A"
proof
fix x assume "x ∈ differenceset (stabilizer A) (stabilizer A)"
then obtain a b where "a ∈ stabilizer A" and "b ∈ stabilizer A" and "x = a ⊖ b"
by (metis minusset.cases sumset.cases)
thus "x ∈ stabilizer A" using stabilizer_is_subgroup subgroup.axioms(1)
by (smt (verit, ccfv_threshold) in_mono invertible stabilizer_subset_group
subgroup_inverse_iff sub_composition_closed)
qed
next
show "stabilizer A ⊆ differenceset (stabilizer A) (stabilizer A)"
proof
fix x assume hx: "x ∈ stabilizer A"
then have "x ⊖ 𝟬 ∈ differenceset (stabilizer A) (stabilizer A)" by blast
then show "x ∈ differenceset (stabilizer A) (stabilizer A)" using hx by simp
qed
qed
lemma stabilizer2_sub_stabilizer:
shows "stabilizer(stabilizer A) ⊆ stabilizer A"
proof(cases "A ≠ {}")
case True
then have "stabilizer(stabilizer A) ⊆ differenceset (stabilizer A) (stabilizer A)"
by (simp add: stabilizer_is_nonempty stabilizer_subset_group stabilizer_subset_nempty)
thus ?thesis using differenceset_stabilizer_eq by blast
next
case False
then show ?thesis by (simp add: stabilizer_empty stabilizer_subset_group)
qed
lemma stabilizer_left_sumset_invariant:
assumes "a ∈ G" and "A ⊆ G"
shows "stabilizer (sumset {a} A) = stabilizer A"
proof
show "stabilizer (sumset {a} A) ⊆ stabilizer A"
proof
fix x assume hx: "x ∈ stabilizer (sumset {a} A)"
then have hxG: "x ∈ G" using stabilizer_def by blast
have "sumset {x} (sumset {a} A) = sumset {a} A" using stabilizer_def hx
by (metis (mono_tags, lifting) mem_Collect_eq sumset_Int_carrier)
then have "sumset {x} A = A" using assms
by (metis (full_types) sumset_assoc sumset_commute sumset_subset_carrier
sumset_translate_eq_right)
thus "x ∈ stabilizer A" using hxG stabilizer_def
by (metis (mono_tags, lifting) mem_Collect_eq sumset_Int_carrier)
qed
next
show "stabilizer A ⊆ stabilizer (sumset {a} A)" using stabilizer_def
using stabilizer_sub_sumset_right by meson
qed
lemma stabilizer_right_sumset_invariant:
assumes "a ∈ G" and "A ⊆ G"
shows "stabilizer (sumset A {a}) = stabilizer A"
using sumset_commute stabilizer_left_sumset_invariant assms by simp
lemma stabilizer_right_differenceset_invariant:
assumes "b ∈ G" and "A ⊆ G"
shows "stabilizer (differenceset A {b}) = stabilizer A"
using assms minusset_eq stabilizer_right_sumset_invariant by auto
lemma stabilizer_unchanged:
assumes "a ∈ G" and "b ∈ G"
shows "stabilizer (sumset A B) = stabilizer (sumset A (sumset (differenceset B {b}) {a}))"
proof-
have "sumset A (sumset (differenceset B {b}) {a}) = sumset (differenceset (sumset A B) {b}) {a}"
by (simp add: sumset_assoc)
thus ?thesis using stabilizer_right_sumset_invariant
stabilizer_right_differenceset_invariant assms sumset_subset_carrier by simp
qed
lemma subset_stabilizer_of_subset_sumset:
assumes "A ⊆ sumset {x} (stabilizer B)" and "x ∈ G" and "A ≠ {}" and "A ⊆ G"
shows "stabilizer A ⊆ stabilizer B"
proof-
obtain a where ha: "a ∈ A" using assms by blast
moreover then obtain b where hb: "b ∈ stabilizer B" and haxb: "a = x ⊕ b" using sumset.cases assms by blast
ultimately have "stabilizer A ⊆ differenceset A {a}" using assms sumset_subset_carrier
stabilizer_subset_difference_singleton by (meson subset_trans)
also have "... = sumset {inverse a} A" using sumset_commute ha assms(4) inverse_closed
subsetD minusset_eq by auto
also have "... ⊆ sumset {inverse x ⊕ inverse b} (sumset {x} (stabilizer B))"
using assms sumset_mono haxb inverse_closed hb stabilizer_subset_group subsetD
commutative inverse_composition_commute by (metis invertible subset_singleton_iff)
also have "... = sumset {inverse b} (stabilizer B)" using sumset_singletons_eq commutative
assms sumset_assoc hb stabilizer_subset_group inverse_closed invertible
by (metis composition_closed invertible_right_inverse2 sub)
also have "... = stabilizer B" using hb Left_Coset_eq_sumset sub_unit_closed sub subset_iff
additive_abelian_group_axioms calculation disjoint_iff_not_equal factor_unit inverse_closed
sumset_subgroup_eq_iff by (smt (verit, del_insts))
finally show ?thesis .
qed
lemma sumset_stabilizer_eq_self:
assumes "A ⊆ G"
shows "sumset (stabilizer A) A = A"
using assms sumset_eq_Union_left[OF "stabilizer_subset_group"]
Int_absorb2 stabilizer_coset_Un sumset_commute sumset_eq_Union_left by presburger
lemma stabilizer_neq_subset_sumset:
assumes "A ⊆ sumset {x} (stabilizer B)" and "x ∈ A" and "¬ sumset {x} (stabilizer B) ⊆ C" and
"A ⊆ C" and "C ⊆ G"
shows "stabilizer A ≠ stabilizer B"
proof
assume heq: "stabilizer A = stabilizer B"
obtain a where "a ∈ sumset {x} (stabilizer B)" and
"a ∉ C" using assms by blast
moreover then obtain b where "b ∈ stabilizer B" and "a = x ⊕ b" using sumset.cases by blast
ultimately have "b ⊕ x ∉ A" using commutative stabilizer_subset_group assms in_mono by metis
thus False using assms heq stabilizer_coset_subset subset_trans by metis
qed
lemma subset_stabilizer_Un:
shows "stabilizer A ∩ stabilizer B ⊆ stabilizer (A ∪ B)"
proof
fix x assume hx: "x ∈ stabilizer A ∩ stabilizer B"
then have "sumset {x} (A ∩ G) = A ∩ G" using stabilizer_def by blast
moreover have "sumset {x} (B ∩ G) = (B ∩ G)" using stabilizer_def hx by blast
ultimately have "sumset {x} ((A ∪ B) ∩ G) = (A ∪ B) ∩ G" using sumset_subset_Un2
boolean_algebra.conj_disj_distrib2 by auto
then show "x ∈ stabilizer (A ∪ B)" using hx stabilizer_subset_group stabilizer_def by blast
qed
lemma mem_stabilizer_Un_and_left_imp_right:
assumes "finite B" and "x ∈ stabilizer (A ∪ B)" and "x ∈ stabilizer A" and "disjnt A B"
shows "x ∈ stabilizer B"
proof-
have "(A ∩ G) ∪ sumset {x} (B ∩ G) = (A ∩ G) ∪ (B ∩ G)"
using assms(2) sumset_subset_Un2[of "{x}" "A ∩ G" "B ∩ G"] stabilizer_def[of "A ∪ B"]
Int_Un_distrib2[of "A" "B" "G"] assms(3) stabilizer_def
by (metis (mono_tags, lifting) mem_Collect_eq)
then have "B ∩ G ⊆ sumset {x} (B ∩ G)" using assms(4) disjnt_def Int_Un_distrib2 Int_commute
sumset_subset_Un1 by (smt (verit, del_insts) Int_assoc Un_Int_eq(2) inf.orderI insert_is_Un
sumset_empty(2))
then show "x ∈ stabilizer B" using stabilizer_def[of "B"] assms(1) assms(3) card_subset_eq
card_sumset_singleton_subset_eq finite.emptyI finite.insertI finite_Int finite_sumset
inf.cobounded2 stabilizer_subset_group subsetD by (smt (verit) mem_Collect_eq)
qed
lemma mem_stabilizer_Un_and_right_imp_left:
assumes "finite A" and "x ∈ stabilizer (A ∪ B)" and "x ∈ stabilizer B" and "disjnt A B"
shows "x ∈ stabilizer A"
using mem_stabilizer_Un_and_left_imp_right Un_commute assms disjnt_sym by metis
lemma Union_stabilizer_Class_eq:
assumes "A ⊆ G"
shows "A = (⋃ (Class A ` A))" using assms sumset_commute sumset_subgroup_eq_Class_Union
sumset_stabilizer_eq_self by presburger
lemma card_stabilizer_sumset_divide_sumset:
"card (stabilizer (sumset A B)) dvd card (sumset A B)" using card_divide_sumset
sumset_commute sumset_stabilizer_eq_self sumset_subset_carrier by metis
lemma card_stabilizer_le:
assumes "A ⊆ G" and "finite A" and "A ≠ {}"
shows "card (stabilizer A) ≤ card A" using assms
by (metis card_le_sumset finite.cases insertCI insert_subset stabilizer_finite
stabilizer_subset_group sumset_commute sumset_stabilizer_eq_self)
lemma sumset_Inter_subset_sumset:
assumes "a ∈ G" and "b ∈ G"
shows "sumset (A ∩ sumset {a} (stabilizer C)) (B ∩ sumset {b} (stabilizer C)) ⊆
sumset {a ⊕ b} (stabilizer C)" (is "sumset ?A ?B ⊆ _")
proof
fix x assume "x ∈ sumset ?A ?B"
then obtain d1 d2 where "d1 ∈ sumset {a} (stabilizer C)" and
"d2 ∈ sumset {b} (stabilizer C)" and "x = d1 ⊕ d2" by (meson IntD2 sumset.cases)
then obtain c1 c2 where hc1: "c1 ∈ stabilizer C" and hc2: "c2 ∈ stabilizer C" and
"x = (a ⊕ c1) ⊕ (b ⊕ c2)" using sumset.simps by auto
then have "x = (a ⊕ b) ⊕ (c1 ⊕ c2)" using hc1 hc2 assms associative commutative
stabilizer_subset_group by simp
thus "x ∈ sumset {a ⊕ b} (stabilizer C)" using stabilizer_is_subgroup hc1 hc2
stabilizer_subset_group sumset.simps sumset_stabilizer_eq assms by blast
qed
subsection‹Convergent›
definition convergent :: "'a set ⇒ 'a set ⇒ 'a set ⇒ bool" where
"convergent C A B ≡ C ⊆ sumset A B ∧ C ≠ {} ∧
card C + card (stabilizer C) ≥ card (A ∩ B) + card (sumset (A ∪ B) (stabilizer C))"
definition convergent_set :: "'a set ⇒ 'a set ⇒ 'a set set" where
"convergent_set A B = Collect (λ C. convergent C A B)"
lemma convergent_set_sub_powerset:
"convergent_set A B ⊆ Pow (sumset A B)" using convergent_set_def convergent_def by blast
lemma finite_convergent_set:
assumes "finite A" and "finite B"
shows "finite (convergent_set A B)"
using convergent_set_sub_powerset finite_Pow_iff finite_sumset assms finite_subset by metis
subsection‹Technical lemmas from DeVos's proof of Kneser's Theorem›
text‹The following lemmas correspond to intermediate arguments in the proof of Kneser's Theorem
by DeVos that we will be following \cite{DeVos_Kneser}. ›
lemma stabilizer_sumset_psubset_stabilizer:
assumes "a ∈ G" and "b ∈ G" and "A ∩ sumset {a} (stabilizer C) ≠ {}" and
"B ∩ sumset {b} (stabilizer C) ≠ {}" and hnotsub: "¬ sumset {a ⊕ b} (stabilizer C) ⊆ sumset A B"
shows "stabilizer (sumset (A ∩ sumset {a} (stabilizer C)) (B ∩ sumset {b} (stabilizer C))) ⊂
stabilizer C" (is "?H ⊂ _")
proof
have "sumset (A ∩ sumset {a} (stabilizer C)) (B ∩ sumset {b} (stabilizer C)) ≠ {}"
using assms by (simp add: inf_assoc)
then show "?H ⊆ stabilizer C"
by (meson assms(1) assms(2) composition_closed subset_stabilizer_of_subset_sumset sumset_Inter_subset_sumset sumset_subset_carrier)
next
obtain c1 c2 where "a ⊕ c1 ∈ A" and "b ⊕ c2 ∈ B" and hc1: "c1 ∈ stabilizer C" and hc2: "c2 ∈ stabilizer C"
using assms(1, 2, 3, 4) Left_Coset_eq_sumset_stabilizer by fastforce
then have hac1mem: "(a ⊕ c1) ∈ A ∩ sumset {a} (stabilizer C)" and hac1G: "a ⊕ c1 ∈ G" and
hbc2mem: "(b ⊕ c2) ∈ B ∩ sumset {b} (stabilizer C)" and hbc2G: "b ⊕ c2 ∈ G"
by (auto simp add: assms(1, 2) sumset.sumsetI)
have "(a ⊕ c1) ⊕ (b ⊕ c2) ∈ sumset {a ⊕ b} (stabilizer C)" using assms hc1 hc2
by (smt (verit) associative commutative composition_closed insertI1 sub sub_composition_closed sumset.sumsetI)
then have "sumset {a ⊕ b} (stabilizer C) ∩ sumset {(a ⊕ c1) ⊕ (b ⊕ c2)} (stabilizer C) ≠ {}"
using zero_mem_stabilizer by (smt (verit, ccfv_threshold) composition_closed
disjoint_iff_not_equal hac1G hbc2G insertCI right_unit sumset.sumsetI unit_closed)
then have hsumeq: "sumset {a ⊕ b} (stabilizer C) = sumset {(a ⊕ c1) ⊕ (b ⊕ c2)} (stabilizer C)"
using sumset_stabilizer_eq_iff assms hac1G hbc2G composition_closed by presburger
have "(sumset (A ∩ sumset {a} (stabilizer C)) (B ∩ sumset {b} (stabilizer C))) ⊆ sumset {a ⊕ b} (stabilizer C)"
by (simp add: assms(1, 2) sumset_Inter_subset_sumset)
have hsummem: "(a ⊕ c1) ⊕ (b ⊕ c2) ∈ sumset (A ∩ sumset {a} (stabilizer C)) (B ∩ sumset {b} (stabilizer C))"
using hac1mem hbc2mem hac1G hbc2G sumset.sumsetI by blast
show "?H ≠ stabilizer C"
using stabilizer_neq_subset_sumset[OF _ hsummem] hnotsub hsumeq sumset_Inter_subset_sumset assms
sumset_subset_carrier composition_closed sumset_mono sumset.sumsetI zero_mem_stabilizer
inf.cobounded1 right_unit unit_closed by metis
qed
lemma stabilizer_eq_stabilizer_union:
assumes "a ∈ G" and "b ∈ G" and"A ∩ sumset {a} (stabilizer C) ≠ {}" and
"B ∩ sumset {b} (stabilizer C) ≠ {}" and hnotsub: "¬ sumset {a ⊕ b} (stabilizer C) ⊆ sumset A B" and
"C ⊆ sumset A B" and "finite C" and
"C ∩ sumset (A ∩ sumset {a} (stabilizer C)) (B ∩ sumset {b} (stabilizer C)) = {}" and "C ≠ {}" and
"finite A" and "finite B"
shows "stabilizer (sumset (A ∩ sumset {a} (stabilizer C)) (B ∩ sumset {b} (stabilizer C))) =
stabilizer (C ∪ sumset (A ∩ sumset {a} (stabilizer C)) (B ∩ sumset {b} (stabilizer C)))" (is "stabilizer ?H = stabilizer ?K")
proof
show "stabilizer ?H ⊆ stabilizer ?K" using subset_stabilizer_Un Int_absorb1
stabilizer_sumset_psubset_stabilizer psubset_imp_subset assms by metis
next
have hCG : "C ⊆ G" using assms(6) sumset_subset_carrier by force
show "stabilizer ?K ⊆ stabilizer ?H"
proof
fix x assume hxC1: "x ∈ stabilizer ?K"
moreover have "x ∈ stabilizer C"
proof-
have hC_Un: "C = (⋃ (Class C ` C))" using Union_stabilizer_Class_eq hCG by simp
have hCsumx: "sumset {x} C = (⋃ y ∈ Class C ` C. sumset {x} y)"
proof
show "sumset {x} C ⊆ ⋃ (sumset {x} ` Class C ` C)"
proof
fix y assume hy: "y ∈ sumset {x} C"
then obtain c where hc: "c ∈ C" and hyxc: "y = x ⊕ c" using sumset.cases by blast
then obtain K where hK: "K ∈ Class C ` C" and "c ∈ K" using hC_Un by blast
then have "y ∈ sumset {x} K" using hyxc hc by (metis sumset.cases
sumset.sumsetI hCG hy singletonD subset_iff)
then show "y ∈ ⋃ (sumset {x} ` Class C ` C)" using hK by auto
qed
next
show "⋃ (sumset {x} ` Class C ` C) ⊆ sumset {x} C"
proof(intro Union_least)
fix X assume "X ∈ sumset {x} ` Class C ` C"
then obtain K where "K ∈ Class C ` C" and "X = sumset {x} K" by blast
then show "X ⊆ sumset {x} C" using sumset_mono[of "{x}" "{x}" "K" "C"]
hC_Un subset_refl by blast
qed
qed
have "x ∉ stabilizer C ⟹ False"
proof-
assume hxC: "x ∉ stabilizer C"
then have hxG: "x ∈ G" using hxC1 stabilizer_subset_group by blast
then have hxCne: "sumset {x} C ≠ C" using stabilizer_def[of "C"] hCG Int_absorb2
hxC by (metis (mono_tags, lifting) mem_Collect_eq)
moreover have hxsplit: "sumset {x} C ∪ sumset {x} ?H = C ∪ ?H"
using hxC1 stabilizer_def[of "?K"] sumset_subset_carrier assms(6) sumset_subset_Un2 by force
have "sumset {x} C ∩ ?H ≠ {}"
proof
assume "sumset {x} C ∩ ?H = {}"
then have "sumset {x} C ⊂ C" using hxsplit hxCne by blast
thus "False" using hCG assms(6) assms(7) hxC1 stabilizer_subset_group psubset_card_mono
by (metis card_sumset_singleton_eq sumset_Int_carrier sumset_commute
sumset_stabilizer_eq_self hxG less_irrefl_nat)
qed
then obtain c where hc: "c ∈ C" and
hxcne: "sumset {x} (Class C c) ∩ ?H ≠ {}" using hCsumx by blast
then have hxc: "sumset {x} (Class C c) = Class C (x ⊕ c)"
using hxG assms(6) Left_Coset_Class_unit Left_Coset_eq_sumset_stabilizer sumset_assoc
sumset_singletons_eq composition_closed sumset.cases sumset_stabilizer_eq_self hCG by (smt (verit))
have hClassCempty: "Class C (x ⊕ c) ∩ C = {}"
proof-
have "¬ Class C (x ⊕ c) ⊆ C" using hxc hxcne assms(8) by blast
then show ?thesis using Class_cover_imp_subset_or_disj[OF hC_Un _ hCG]
by (meson composition_closed hCG hc hxG subsetD)
qed
have "Class C (x ⊕ c) ⊆ sumset {x} C" using hCsumx hc hxc by blast
then have "Class C (x ⊕ c) ⊆ ?H" using hClassCempty hxsplit by auto
moreover have "card (Class C (x ⊕ c)) = card (stabilizer C)" using hxG hc hCG
composition_closed Right_Coset_Class_unit Right_Coset_cardinality sumset_Int_carrier
Class_cover_imp_subset_or_disj assms by auto
ultimately have "card (stabilizer C) ≤ card ?H" using card_mono finite_sumset assms(10, 11) finite_Int by metis
moreover have "card ?H < card (sumset {a ⊕ b} (stabilizer C))"
proof (intro psubset_card_mono psubsetI sumset_Inter_subset_sumset assms(1) assms(2))
show "finite (sumset {a ⊕ b} (stabilizer C))"
using stabilizer_finite assms finite_sumset by (simp add: hCG)
next
show "?H ≠ sumset {a ⊕ b} (stabilizer C)"
using hnotsub sumset_mono by (metis Int_lower1)
qed
ultimately show "False"
using assms(1, 2) stabilizer_subset_group by (simp add: card_sumset_singleton_subset_eq)
qed
then show ?thesis by auto
qed
moreover have "finite ?H" using finite_sumset assms(10, 11) finite_Int by simp
ultimately show "x ∈ stabilizer ?H" using mem_stabilizer_Un_and_right_imp_left[of "?H" "x" "C"]
disjnt_def assms Un_commute by (metis disjoint_iff_not_equal)
qed
qed
lemma sumset_inter_ineq:
assumes "B ∩ sumset {a} (stabilizer C) = {}" and "stabilizer (sumset (A ∩ sumset {a} (stabilizer C)) (B ∩ sumset {b} (stabilizer C))) ⊂ stabilizer C" and
"a ∈ A" and "a ∈ G" and "finite A" and "finite B" and "A ≠ {}" and "B ≠ {}" and "finite (stabilizer C)"
shows "int (card (sumset (A ∪ B) (stabilizer C))) - card (sumset (A ∪ B) (stabilizer (sumset (A ∩ sumset {a} (stabilizer C)) (B ∩ sumset {b} (stabilizer C))))) ≥
int (card (stabilizer C)) - card (sumset (A ∩ sumset {a} (stabilizer C)) (stabilizer (sumset (A ∩ sumset {a} (stabilizer C)) (B ∩ sumset {b} (stabilizer C)))))"
(is "int (card (sumset (A ∪ B) (stabilizer C))) - card (sumset (A ∪ B) ?H1) ≥
int (card (stabilizer C)) - card (sumset ?A1 ?H1)")
proof-
have hfinsumH1:"finite (sumset (A ∪ B) ?H1)"
using finite_sumset assms by (meson finite_Un psubsetE rev_finite_subset)
have hsubsumH1: "sumset (A ∪ B) ?H1 ⊆ sumset (A ∪ B) (stabilizer C)"
using sumset.cases assms by (meson psubsetE subset_refl sumset_mono)
have hsumH1card_le: "card (sumset (A ∪ B) ?H1) ≤ card (sumset (A ∪ B) (stabilizer C))"
using card_mono finite_sumset stabilizer_finite assms
by (metis equalityE finite_UnI psubset_imp_subset sumset_mono)
have hsub: "sumset ?A1 ?H1 ⊆ sumset {a} (stabilizer C)"
proof
fix x assume "x ∈ sumset ?A1 ?H1"
then obtain h1 f where "h1 ∈ ?A1" and hf: "f ∈ ?H1" and
hx: "x = h1 ⊕ f" by (meson sumset.cases)
then obtain c where hc: "c ∈ stabilizer C" and hac: "h1 = a ⊕ c"
by (metis Int_iff empty_iff insert_iff sumset.cases)
then have hcf: "c ⊕ f ∈ stabilizer C" using hf assms(2) stabilizer_is_subgroup
subgroup_def monoid_axioms Group_Theory.group.axioms(1)
Group_Theory.monoid_def subset_iff psubset_imp_subset
by (smt (verit) stabilizer_subset_group sumset.sumsetI sumset_stabilizer_eq)
have hcG: "c ∈ G" using hc stabilizer_subset_group by auto
have hfG: "f ∈ G" using hf stabilizer_subset_group by auto
show "x ∈ sumset {a} (stabilizer C)" using hx hac assms stabilizer_subset_group hcf
using Left_Coset_eq_sumset_stabilizer Left_Coset_memI associative hcG hfG by presburger
qed
moreover have "finite (sumset ?A1 ?H1)" using finite_sumset assms stabilizer_finite finite_subset
by (metis finite.simps hsub)
ultimately have "card (sumset {a} (stabilizer C)) - card (sumset ?A1 ?H1) =
card (sumset {a} (stabilizer C) - sumset ?A1 ?H1)"
using card_Diff_subset by metis
moreover have "card (sumset ?A1 ?H1) ≤ card (sumset {a} (stabilizer C))"
using card_mono hsub finite_sumset assms by (metis finite.simps)
ultimately have "int (card (sumset {a} (stabilizer C))) - card (sumset ?A1 ?H1) =
card (sumset {a} (stabilizer C) - sumset ?A1 ?H1)" by linarith
also have "... ≤ card ((sumset (A ∪ B) (stabilizer C)) - (sumset (A ∪ B) ?H1))"
proof-
have "sumset {a} (stabilizer C) - sumset ?A1 ?H1 ⊆ sumset (A ∪ B) (stabilizer C) - sumset (A ∪ B) ?H1"
proof
fix x assume hx: "x ∈ sumset {a} (stabilizer C) - sumset ?A1 ?H1"
then obtain c where hxac: "x = a ⊕ c" and hc: "c ∈ stabilizer C" and hcG: "c ∈ G"
using sumset.cases by blast
then have "x ∈ sumset (A ∪ B) (stabilizer C)" using assms sumset.cases by blast
moreover have "x ∉ sumset (A ∪ B) ?H1"
proof
assume "x ∈ sumset (A ∪ B) ?H1"
then obtain y h1 where hy: "y ∈ A ∪ B" and hyG: "y ∈ G" and hh1G: "h1 ∈ G"
and hh1: "h1 ∈ ?H1" and hxy: "x = y ⊕ h1" by (meson sumset.cases)
then have "y = a ⊕ (c ⊕ inverse h1)" using hxac hxy assms associative commutative composition_closed
inverse_closed invertible invertible_left_inverse2 by (metis hcG)
moreover have "h1 ∈ stabilizer C" using hh1 assms by auto
moreover hence "c ⊕ inverse h1 ∈ stabilizer C" using hc stabilizer_is_subgroup subgroup_def
group_axioms invertible subgroup.subgroup_inverse_iff submonoid.sub_composition_closed hh1G by metis
ultimately have "y ∈ sumset {a} (stabilizer C)"
using assms hcG hh1G by blast
moreover hence "y ∈ A" using assms(1) hy by auto
ultimately have "x ∈ sumset ?A1 ?H1" using hxy hh1
by (simp add: hyG hh1G sumset.sumsetI)
thus "False" using hx by auto
qed
ultimately show "x ∈ sumset (A ∪ B) (stabilizer C) - sumset (A ∪ B) ?H1"
by simp
qed
thus ?thesis using card_mono finite_Diff finite_sumset assms
by (metis finite_UnI nat_int_comparison(3))
qed
also have "... = int (card (sumset (A ∪ B) (stabilizer C))) -
card (sumset (A ∪ B) ?H1)"
using card_Diff_subset[OF hfinsumH1 hsubsumH1] hsumH1card_le by linarith
finally show "int (card (sumset (A ∪ B) (stabilizer C))) - card (sumset (A ∪ B) ?H1) ≥
int (card (stabilizer C)) - card (sumset ?A1 ?H1)"
using assms by (metis card_sumset_singleton_subset_eq stabilizer_subset_group)
qed
lemma exists_convergent_min_stabilizer:
assumes hind: "∀m<n. ∀C D. C ⊆ G ⟶ D ⊆ G ⟶ finite C ⟶ finite D ⟶ C ≠ {} ⟶
D ≠ {} ⟶ card (sumset C D) + card C = m ⟶
card (sumset C (stabilizer (sumset C D))) + card (sumset D (stabilizer (sumset C D))) -
card ((stabilizer (sumset C D)))
≤ card (sumset C D)" and hAG: "A ⊆ G" and hBG: "B ⊆ G" and hA: "finite A" and
hB: "finite B" and hAne: "A ≠ {}" and "A ∩ B ≠ {}" and
hcardsum: "card (sumset A B) + card A = n" and hintercardA: "card (A ∩ B) < card A"
obtains X where "convergent X A B" and "⋀ Y. Y ∈ convergent_set A B ⟹
card (stabilizer Y) ≥ card (stabilizer X)"
proof-
let ?C0 = "sumset (A ∩ B) (A ∪ B)"
have hC0ne: "?C0 ≠ {}" using assms by fast
moreover have "finite ?C0" using sumset_inter_union_subset finite_sumset assms by auto
ultimately have "finite (stabilizer ?C0)" using stabilizer_finite
using sumset_subset_carrier by presburger
then have hcard_sumset_le: "card (A ∩ B) ≤ card (sumset (A ∩ B) (stabilizer ?C0))"
using card_le_sumset sumset_commute sub_unit_closed assms
by (metis Int_Un_eq(3) Un_subset_iff finite_Int unit_closed)
have "card ?C0 ≤ card (sumset A B)"
using card_mono sumset_inter_union_subset finite_sumset assms
by (simp add: card_mono finite_sumset hA hB sumset_inter_union_subset)
then have "card ?C0 + card (A ∩ B) < card (sumset A B) + card A"
using hintercardA by auto
then obtain m where "m < n" and "card ?C0 + card (A ∩ B) = m" using hcardsum by auto
then have "card (sumset (A ∩ B) (stabilizer ?C0)) +
card (sumset (A ∪ B) (stabilizer ?C0)) - card (stabilizer ?C0) ≤ card ?C0"
using assms finite_Un finite_Int
by (metis Int_Un_eq(4) Un_empty Un_subset_iff)
then have "card ?C0 + card (stabilizer ?C0) ≥
card (A ∩ B) + card (sumset (A ∪ B) (stabilizer ?C0))" using hcard_sumset_le
by auto
then have "?C0 ∈ convergent_set A B" using convergent_set_def convergent_def
sumset_inter_union_subset hC0ne by auto
then have hconvergent_ne: "convergent_set A B ≠ {}" by auto
define KS where "KS ≡ (λ X. card (stabilizer X)) ` convergent_set A B"
define K where "K ≡ Min KS"
define C where "C ≡ @C. C ∈ convergent_set A B ∧ K = card (stabilizer C)"
obtain KS: "finite KS" "KS ≠ {}"
using hconvergent_ne finite_convergent_set assms KS_def by auto
then have "K ∈ KS" using K_def Min_in by blast
then have "∃ X. X ∈ convergent_set A B ∧ K = card (stabilizer X)"
using KS_def by auto
then obtain "C ∈ convergent_set A B" and Keq: "K = card (stabilizer C)"
by (metis (mono_tags, lifting) C_def someI_ex)
then have hC: "C ⊆ sumset A B" and hCne: "C ≠ {}" and
hCcard: "card C + card (stabilizer C) ≥
card (A ∩ B) + card (sumset (A ∪ B) (stabilizer C))"
using convergent_set_def convergent_def by auto
have hCmin: "⋀ Y. Y ∈ convergent_set A B ⟹
card (stabilizer Y) ≥ card (stabilizer C)"
using K_def KS_def Keq Min_le KS(1) by auto
show ?thesis using hCmin hC hCcard hCne local.convergent_def that by presburger
qed
end
context normal_subgroup
begin
subsection‹ A function that picks coset representatives randomly›
definition φ :: "'a set ⇒ 'a" where
"φ = (λ x. if x ∈ G // K then (SOME a. a ∈ G ∧ x = a ⋅| K) else undefined)"
definition quot_comp_alt :: "'a ⇒ 'a ⇒ 'a" where "quot_comp_alt a b = φ ((a ⋅ b) ⋅| K)"
lemma phi_eq_coset:
assumes "φ x = a" and "a ∈ G" and "x ∈ G // K"
shows "x = a ⋅| K"
proof-
have "(SOME a. a ∈ G ∧ x = a ⋅| K) = a" using φ_def assms by simp
then show ?thesis using some_eq_ex representant_exists Left_Coset_Class_unit assms
by (metis (mono_tags, lifting))
qed
lemma phi_coset_mem:
assumes "a ∈ G"
shows "φ (a ⋅| K) ∈ a ⋅| K"
proof-
obtain x where hx: "x = φ (a ⋅| K)" by auto
then have "x = (SOME x. x ∈ G ∧ a ⋅| K = x ⋅| K)" using φ_def assms
Class_in_Partition Left_Coset_Class_unit by presburger
then show ?thesis using φ_def Class_self Left_Coset_Class_unit hx assms
by (smt (verit, ccfv_SIG) tfl_some)
qed
lemma phi_coset_eq:
assumes "a ∈ G" and "φ x = a" and "x ∈ G // K"
shows "φ (a ⋅| K) = a" using phi_eq_coset assms by metis
lemma phi_inverse_right:
assumes "g ∈ G"
shows "quot_comp_alt g (φ (inverse g ⋅| K)) = φ K"
proof-
have "g ⋅ (φ (inverse g ⋅| K)) ∈ (g ⋅ (inverse g) ⋅| K)"
using phi_coset_mem assms by (smt (z3) Left_Coset_memE factor_unit invertible invertible_right_inverse
invertible_inverse_closed invertible_inverse_inverse sub invertible_left_inverse2)
then have "g ⋅ (φ (inverse g ⋅| K)) ⋅| K = K"
using Block_self Left_Coset_Class_unit Normal_def quotient.unit_closed sub
by (metis assms composition_closed invertible invertible_inverse_closed invertible_right_inverse)
then show ?thesis using quot_comp_alt_def by auto
qed
lemma phi_inverse_left:
assumes "g ∈ G"
shows "quot_comp_alt (φ (inverse g ⋅| K)) g = φ K"
proof-
have "(φ (inverse g ⋅| K)) ⋅ g ∈ ((inverse g) ⋅ g) ⋅| K" using phi_coset_mem assms
by (metis Left_Coset_memE factor_unit invertible invertible_inverse_closed invertible_left_inverse normal)
then have "(φ (inverse g ⋅| K)) ⋅ g ⋅| K = K" using Block_self Left_Coset_Class_unit Normal_def
quotient.unit_closed sub by (smt (verit, best) assms composition_closed invertible invertible_inverse_closed
invertible_left_inverse)
then show ?thesis using quot_comp_alt_def by auto
qed
lemma phi_mem_coset_eq:
assumes "a ∈ G // K" and "b ∈ G"
shows "φ a ∈ b ⋅| K ⟹ a = (b ⋅| K)"
proof-
assume "φ a ∈ b ⋅| K"
then have "a ∩ (b ⋅| K) ≠ {}"
by (metis Class_closed Class_is_Left_Coset Int_iff assms empty_iff phi_coset_mem phi_eq_coset)
then show "a = b ⋅| K" by (metis Class_in_Partition Class_is_Left_Coset assms disjoint)
qed
lemma forall_unique_repr:
"∀ x ∈ G // K. ∃! k ∈ φ ` (G // K). x = k ⋅| K"
proof
fix x assume hx: "x ∈ G // K"
then have "φ x ⋅| K = x"
by (metis Class_is_Left_Coset block_closed phi_coset_mem phi_eq_coset representant_exists)
then have hex: "∃ k ∈ φ ` (G // K). x = k ⋅| K" using hx by blast
moreover have "⋀ a b. a ∈ φ ` (G // K) ⟹ x = a ⋅| K ⟹ b ∈ φ ` (G // K) ⟹ x = b ⋅| K ⟹
a = b"
proof-
fix a b assume "a ∈ φ ` (G // K)" and hxa: "x = a ⋅| K" and "b ∈ φ ` (G // K)" and
hxb: "x = b ⋅| K"
then obtain z w where "a = φ (z ⋅| K)" and "b = φ (w ⋅| K)" and "z ∈ G" and "w ∈ G"
using representant_exists Left_Coset_Class_unit by force
then show "a = b" using hxa hxb
by (metis Class_in_Partition Class_is_Left_Coset block_closed phi_coset_mem phi_eq_coset)
qed
ultimately show "∃! k ∈ φ ` (G // K). x = k ⋅| K" by blast
qed
lemma phi_inj_on:
shows "inj_on φ (G // K)"
proof(intro inj_onI)
fix x y assume "x ∈ G // K" and hy: "y ∈ G // K" and hxy: "φ x = φ y"
then obtain a b where "x = a ⋅| K" and "y = b ⋅| K" and "a ∈ G" and "b ∈ G"
using representant_exists Left_Coset_Class_unit by metis
then show "x = y" using hxy hy by (metis phi_coset_mem phi_mem_coset_eq)
qed
lemma phi_coset_eq_self:
assumes "a ∈ G // K"
shows "φ a ⋅| K = a"
by (metis Class_closed Class_is_Left_Coset assms phi_coset_mem phi_eq_coset representant_exists)
lemma phi_coset_comp_eq:
assumes "a ∈ G // K" and "b ∈ G // K"
shows "φ a ⋅ φ b ⋅| K = a [⋅] b" using assms phi_coset_eq_self
by (metis Class_is_Left_Coset block_closed factor_composition phi_coset_mem representant_exists)
lemma phi_comp_eq:
assumes "a ∈ G // K" and "b ∈ G // K"
shows "φ (a [⋅] b) = quot_comp_alt (φ a) (φ b)"
using phi_coset_comp_eq quot_comp_alt_def assms by auto
lemma phi_image_subset:
"φ ` (G // K) ⊆ G"
proof(intro image_subsetI, simp add: φ_def)
fix x assume "x ∈ G // K"
then show "(SOME a. a ∈ G ∧ x = a ⋅| K) ∈ G"
using Left_Coset_Class_unit representant_exists someI_ex by (metis (mono_tags, lifting))
qed
lemma phi_image_group:
"Group_Theory.group (φ ` (G // K)) quot_comp_alt (φ K)"
proof-
have hmonoid: "Group_Theory.monoid (φ ` (G // K)) quot_comp_alt (φ K)"
proof
show "⋀a b. a ∈ φ ` (G // K) ⟹ b ∈ φ ` (G // K) ⟹
quot_comp_alt a b ∈ φ ` (G // K)" using quot_comp_alt_def imageI phi_image_subset
by (metis Class_in_Partition Left_Coset_Class_unit composition_closed subset_iff)
next
show "(φ K) ∈ φ ` (G // K)" using φ_def Left_Coset_Class_unit imageI Normal_def by blast
next
show "⋀a b c. a ∈ φ ` Partition ⟹ b ∈ φ ` Partition ⟹ c ∈ φ ` Partition ⟹
quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)"
proof-
fix a b c assume ha: "a ∈ φ ` (G // K)" and hb: "b ∈ φ ` (G // K)" and hc: "c ∈ φ ` (G // K)"
have habc: "a ⋅ b ⋅ c ∈ G" using ha hb hc composition_closed phi_image_subset by (meson subsetD)
have hab: "quot_comp_alt a b ∈ (a ⋅ b) ⋅| K" using phi_image_subset quot_comp_alt_def ha hb
by (metis composition_closed phi_coset_mem subsetD)
then have "quot_comp_alt (quot_comp_alt a b) c ∈ (a ⋅ b ⋅ c) ⋅| K" using quot_comp_alt_def phi_image_subset ha hb hc
by (smt (z3) Block_self Class_closed Class_in_Partition Left_Coset_Class_unit composition_closed
natural.commutes_with_composition phi_coset_mem subset_iff)
moreover have hbc: "quot_comp_alt b c ∈ (b ⋅ c) ⋅| K" using hb hc phi_image_subset quot_comp_alt_def
by (metis composition_closed phi_coset_mem subset_iff)
moreover hence "quot_comp_alt a (quot_comp_alt b c) ∈ (a ⋅ b ⋅ c) ⋅| K" using quot_comp_alt_def phi_image_subset ha hb hc
by (smt (verit, del_insts) Block_self Class_closed Class_in_Partition Left_Coset_Class_unit
associative composition_closed natural.commutes_with_composition phi_coset_mem subset_iff)
moreover have "a ⋅ (quot_comp_alt b c) ⋅| K ∈ G // K" using ha hb hc phi_image_subset
by (metis Class_closed Class_in_Partition Class_is_Left_Coset hbc composition_closed in_mono subset_eq)
moreover have "(quot_comp_alt a b) ⋅ c ⋅| K ∈ G // K" using ha hb hc phi_image_subset
by (metis Class_closed Class_in_Partition Left_Coset_Class_unit hab composition_closed in_mono)
ultimately show "quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)"
using phi_mem_coset_eq[OF _ habc] quot_comp_alt_def by metis
qed
next
show "⋀a. a ∈ φ ` Partition ⟹ quot_comp_alt (φ K) a = a" using quot_comp_alt_def φ_def
phi_image_subset image_iff phi_coset_eq subsetD by (smt (z3) Normal_def Partition_def
natural.image.sub_unit_closed phi_comp_eq quotient.left_unit)
next
show "⋀a. a ∈ φ ` Partition ⟹ quot_comp_alt a (φ K) = a" using quot_comp_alt_def φ_def
phi_image_subset image_iff phi_coset_eq subsetD by (smt (verit) Normal_def
factor_composition factor_unit normal_subgroup.phi_coset_eq_self normal_subgroup_axioms
quotient.unit_closed right_unit unit_closed)
qed
moreover show "Group_Theory.group (φ ` (G // K)) quot_comp_alt (φ K)"
proof(simp add: group_def group_axioms_def hmonoid)
show "∀u. u ∈ φ ` Partition ⟶ monoid.invertible (φ ` Partition) quot_comp_alt (φ K) u"
proof(intro allI impI)
fix g assume hg: "g ∈ φ ` (G // K)"
then have "quot_comp_alt g (φ ((inverse g) ⋅| K)) = (φ K)"
and "quot_comp_alt (φ ((inverse g) ⋅| K)) g = (φ K)"
using phi_image_subset phi_inverse_right phi_inverse_left by auto
moreover have "φ ((inverse g) ⋅| K) ∈ φ ` (G // K)" using imageI hg phi_image_subset
by (metis (no_types, opaque_lifting) Class_in_Partition Left_Coset_Class_unit in_mono
invertible invertible_inverse_closed)
ultimately show "monoid.invertible (φ ` Partition) quot_comp_alt (φ K) g"
using monoid.invertibleI[OF hmonoid] hg by presburger
qed
qed
qed
lemma phi_map: "Set_Theory.map φ Partition (φ ` Partition)"
by (auto simp add: Set_Theory.map_def φ_def)
lemma phi_image_isomorphic:
"group_isomorphism φ (G // K) ([⋅]) (Class 𝟭) (φ ` (G // K)) quot_comp_alt (φ K)"
proof -
have "bijective_map φ Partition (φ ` Partition)"
using bijective_map_def bijective_def bij_betw_def phi_inj_on phi_map by blast
moreover have "Group_Theory.monoid (φ ` Partition) quot_comp_alt (φ K)"
using phi_image_group group_def by metis
moreover have "φ (Class 𝟭) = φ K" using Left_Coset_Class_unit Normal_def by auto
ultimately show ?thesis
by (auto simp add: group_isomorphism_def group_homomorphism_def monoid_homomorphism_def
phi_image_group quotient.monoid_axioms quotient.group_axioms monoid_homomorphism_axioms_def
phi_comp_eq phi_map)
qed
end
context subgroup_of_additive_abelian_group
begin
lemma Union_Coset_card_eq:
assumes hSG: "S ⊆ G" and hSU: "(⋃ (Class ` S)) = S"
shows "card S = card H * card (Class ` S)"
proof(cases "finite H")
case hH: True
have hfin: "⋀A. A ∈ Class ` S ⟹ finite A" using hSG Right_Coset_Class_unit
Right_Coset_cardinality hH card_eq_0_iff empty_iff sub_unit_closed subsetD
by (smt (verit, del_insts) imageE)
have "card S = card H * card (Class ` S)" when hS: "finite S"
proof-
have hdisj: "pairwise (λs t. disjnt s t) (Class ` S)"
proof (intro pairwiseI)
fix x y assume "x ∈ Class ` S" and "y ∈ Class ` S" and hxy: "x ≠ y"
then obtain a b where "x = Class a" and "y = Class b" and
"a ∈ S" and "b ∈ S" by blast
then show "disjnt x y" using disjnt_def hxy
by (smt (verit, ccfv_threshold) not_disjoint_implies_equal hSG subsetD)
qed
then have "card (⋃ (Class ` S)) = sum card (Class ` S)" using card_Union_disjoint hfin by blast
moreover have "finite (Class ` S)" using hS by blast
ultimately have "card (⋃ (Class ` S)) = (∑ a ∈ Class ` S. card a)"
using sum_card_image hdisj by blast
moreover have "⋀ a. a ∈ Class ` S ⟹ card a = card H"
using hSG Right_Coset_Class_unit Right_Coset_cardinality by auto
ultimately show "card S = card H * card (Class ` S)"
using hSU by simp
qed
moreover have "card S = card H * card (Class ` S)" when hS: "¬ finite S"
using finite_Union hfin hS hSU by (metis card_eq_0_iff mult_0_right)
ultimately show ?thesis by blast
next
case hH: False
have "card S = card H * card (Class ` S)" when "S = {}"
by (simp add: that)
then have hinf: "⋀ A. A ∈ Class ` S ⟹ infinite A" using hSG Right_Coset_Class_unit
Right_Coset_cardinality hH card_eq_0_iff empty_iff sub_unit_closed subsetD
by (smt (verit) Class_self imageE)
moreover have "card S = card H * card (Class ` S)" when "S ≠ {}" using hSU by (metis Class_closed2
Normal_def card.infinite card_sumset_0_iff hH hSG mult_is_0 sumset_subgroup_eq_Class_Union unit_closed)
ultimately show ?thesis by fastforce
qed
end
context subgroup_of_abelian_group
begin
interpretation GH: additive_abelian_group "G // H" "([⋅])" "Class 𝟭"
proof
fix x y assume "x ∈ G // H" and "y ∈ G // H"
then show "x [⋅] y = y [⋅] x" using Class_commutes_with_composition commutative representant_exists
by metis
qed
interpretation GH_repr: additive_abelian_group "φ ` (G // H)" "quot_comp_alt" "φ H"
proof(simp add: additive_abelian_group_def abelian_group_def phi_image_group
commutative_monoid_def commutative_monoid_axioms_def, intro conjI allI impI)
show "Group_Theory.monoid (φ ` Partition) quot_comp_alt (φ H)"
using phi_image_group group_def by metis
next
show "⋀ x y. x ∈ φ ` Partition ⟹ y ∈ φ ` Partition ⟹ quot_comp_alt x y = quot_comp_alt y x"
by (auto) (metis GH.commutative phi_comp_eq)
qed
lemma phi_image_sumset_eq:
assumes "A ⊆ G // H" and "B ⊆ G // H"
shows "φ ` (GH.sumset A B) = GH_repr.sumset (φ ` A) (φ ` B)"
proof(intro subset_antisym image_subsetI subsetI)
fix x assume "x ∈ GH.sumset A B"
then obtain c d where "x = quotient_composition c d" and hc: "c ∈ A" and hd: "d ∈ B"
using GH.sumset.cases by blast
then have "φ x = quot_comp_alt (φ c) (φ d)"
using phi_comp_eq assms subsetD by blast
then show "φ x ∈ GH_repr.sumset (φ ` A) (φ ` B)"
using hc hd assms subsetD GH_repr.sumsetI imageI by auto
next
fix x assume "x ∈ GH_repr.sumset (φ ` A) (φ ` B)"
then obtain a b where "x = quot_comp_alt a b" and ha: "a ∈ φ ` A" and hb: "b ∈ φ ` B"
using GH_repr.sumset.cases by metis
moreover obtain c d where "a = φ c" and "b = φ d" and "c ∈ A" and "d ∈ B"
using ha hb by blast
ultimately show "x ∈ φ ` GH.sumset A B" using phi_comp_eq assms imageI GH.sumsetI
by (smt (verit, del_insts) subsetD)
qed
lemma phi_image_stabilizer_eq:
assumes "A ⊆ G // H"
shows "φ ` (GH.stabilizer A) = GH_repr.stabilizer (φ ` A)"
proof(intro subset_antisym image_subsetI subsetI)
fix x assume "x ∈ GH.stabilizer A"
then have "GH.sumset {x} A = A" and hx: "x ∈ G // H" using GH.stabilizer_def assms by auto
then have "GH_repr.sumset (φ ` {x}) (φ ` A) = φ ` A" using assms phi_image_sumset_eq
by (metis empty_subsetI insert_subset)
then show "φ x ∈ GH_repr.stabilizer (φ ` A)" using GH_repr.stabilizer_def assms
by (smt (z3) GH_repr.sumset_Int_carrier hx image_empty image_eqI image_insert mem_Collect_eq)
next
fix x assume "x ∈ GH_repr.stabilizer (φ ` A)"
then have hstab: "GH_repr.sumset {x} (φ ` A) = (φ ` A)" and hx: "x ∈ φ ` (G // H)"
using GH_repr.stabilizer_def assms phi_image_subset by auto
then obtain B where hB: "B ∈ G // H" and hBx: "φ B = x" by blast
then have "GH_repr.sumset (φ ` {B}) (φ ` A) = φ ` A" using hstab by auto
then have "GH.sumset {B} A = A" using phi_image_sumset_eq phi_inj_on assms hB
GH.sumset_subset_carrier by (smt (z3) GH.sumset_singletons_eq inj_on_image_eq_iff
quotient.right_unit quotient.unit_closed)
then show "x ∈ φ ` (GH.stabilizer A)" using assms hBx GH.stabilizer_def
by (smt (z3) GH.sumset_Int_carrier hB image_iff mem_Collect_eq)
qed
end
subsection‹Useful group-theoretic results›
lemma residue_group: "abelian_group {0..(m :: nat)-1} (λ x y. ((x + y) mod m)) (0 :: int)"
proof(cases "m > 1")
case hm: True
then have hmonoid: "Group_Theory.monoid {0..m-1} (λ x y. ((x + y) mod m)) (0 :: int)"
by (unfold_locales, auto simp add: of_nat_diff, presburger)
moreover have "monoid.invertible {0..int (m - 1)} (λx y. (x + y) mod int m) 0 u" if "u ∈ {0..int (m - 1)}" for u
proof(cases "u = 0")
case True
then show ?thesis using monoid.invertible_def[OF hmonoid that] monoid.unit_invertible[OF hmonoid] by simp
next
case hx: False
then have "((m - u) + u) mod m = 0" and "(u + (m - u)) mod m = 0" and "m - u ∈ {0..int(m-1)}"
using atLeastAtMost_iff hx that by auto
then show ?thesis using monoid.invertible_def[OF hmonoid that] by metis
qed
moreover have "commutative_monoid {0..m-1} (λ x y. ((x + y) mod m)) (0 :: int)"
using hmonoid commutative_monoid_def commutative_monoid_axioms_def by (smt (verit))
ultimately show ?thesis by (simp add: abelian_group_def group_def group_axioms_def
hmonoid)
next
case hm: False
moreover have hmonoid: "Group_Theory.monoid {0} (λ x y. ((x + y) mod m)) (0 :: int)"
by (unfold_locales, auto)
moreover have "monoid.invertible {0} (λx y. (x + y) mod int m) 0 0" using monoid.invertible_def[OF hmonoid]
monoid.unit_invertible[OF hmonoid] hm by simp
ultimately show ?thesis by (unfold_locales, auto)
qed
lemma (in subgroup_of_group) prime_order_simple:
assumes "prime (card G)"
shows "H = {𝟭} ∨ H = G"
proof-
have "card H dvd card G" using lagrange assms card.infinite dvdI not_prime_0 by fastforce
then have "card H = 1 ∨ card H = card G" using assms prime_nat_iff by blast
then show ?thesis using card_1_singletonE sub_unit_closed card.infinite card_subset_eq sub
assms not_prime_0 subsetI insertE empty_iff by metis
qed
lemma residue_group_simple:
assumes "prime p" and "subgroup H {0..(p :: nat)-1} (λ x y. ((x + y) mod p)) (0 :: int)"
shows "H = {0} ∨ H = {0..int(p-1)}"
proof-
have hprime: "prime (card {0..int(p-1)})" using card_atLeastAtMost_int assms int_ops by auto
moreover have hsub:"subgroup_of_group H {0..(p :: nat)-1} (λ x y. ((x + y) mod p)) (0 :: int)"
using subgroup_of_group_def assms abelian_group_def residue_group by fast
ultimately show ?thesis using assms subgroup_of_group.prime_order_simple[OF hsub hprime] by blast
qed
end