# Theory Set_Multiplication

(* File: Set_Multiplication.thy Author: Joseph Thommes, TU München *) section ‹Set Multiplication› theory Set_Multiplication imports "HOL-Algebra.Algebra" begin text ‹This theory/section is of auxiliary nature and is mainly used to establish a connection between the set multiplication and the multiplication of subgroups via the ‹IDirProd› (although this particular notion is introduced later). However, as in every section of this entry, there are some lemmas that do not have any further usage in this entry, but are of interest just by themselves.› lemma (in group) set_mult_union: "A <#> (B ∪ C) = (A <#> B) ∪ (A <#> C)" unfolding set_mult_def by auto lemma (in group) set_mult_card_single_el_eq: assumes "J ⊆ carrier G" "x ∈ carrier G" shows "card (l_coset G x J) = card J" unfolding l_coset_def proof - have "card ((⊗) x ` J) = card J" using inj_on_cmult[of x] card_image[of "(⊗) x" J] assms inj_on_subset[of "(⊗) x" "carrier G" J] by blast moreover have "(⋃y∈J. {x ⊗ y}) = (⊗) x ` J" using image_def[of "(⊗) x" J] by blast ultimately show "card (⋃h∈J. {x ⊗ h}) = card J" by presburger qed text ‹We find an upper bound for the cardinality of a set product.› lemma (in group) set_mult_card_le: assumes "finite H" "H ⊆ carrier G" "J ⊆ carrier G" shows "card (H <#> J) ≤ card H * card J" using assms proof (induction "card H" arbitrary: H) case 0 then have "H = {}" by force then show ?case using set_mult_def[of G H J] by simp next case (Suc n) then obtain a where a_def: "a ∈ H" by fastforce then have c_n: "card (H - {a}) = n" using Suc by force then have "card ((H - {a}) <#> J) ≤ card (H - {a}) * card J" using Suc by blast moreover have "card ({a} <#> J) = card J" using Suc(4, 5) a_def set_mult_card_single_el_eq[of J a] l_coset_eq_set_mult[of G a J] by auto moreover have "H <#> J = (H - {a} <#> J) ∪ ({a} <#> J)" using set_mult_def[of G _ J] a_def by auto moreover have "card (H - {a}) * card J + card J = Suc n * card J" using c_n mult_Suc by presburger ultimately show ?case using card_Un_le[of "H - {a} <#> J" "{a} <#> J"] c_n ‹Suc n = card H› by auto qed lemma (in group) set_mult_finite: assumes "finite H" "finite J" "H ⊆ carrier G" "J ⊆ carrier G" shows "finite (H <#> J)" using assms set_mult_def[of G H J] by auto text ‹The next lemma allows us to later to derive that two finite subgroups $J$ and $H$ are complementary if and only if their product has the cardinality $|J| \cdot |H|$.› lemma (in group) set_mult_card_eq_impl_empty_inter: assumes "finite H" "finite J" "H ⊆ carrier G" "J ⊆ carrier G" "card (H <#> J) = card H * card J" shows "⋀a b. ⟦a ∈ H; b ∈ H; a ≠ b⟧ ⟹ ((⊗) a ` J) ∩ ((⊗) b ` J) = {}" using assms proof (induction H rule: finite_induct) case empty then show ?case by fast next case step: (insert x H) from step have x_c: "x ∈ carrier G" by simp from step have H_c: "H ⊆ carrier G" by simp from set_mult_card_single_el_eq[of J x] have card_x: "card ({x} <#> J) = card J" using ‹J ⊆ carrier G› x_c l_coset_eq_set_mult by metis moreover have ins: "(insert x H) <#> J = (H <#> J) ∪ ({x} <#> J)" using set_mult_def[of G _ J] by auto ultimately have "card (H <#> J) ≥ card H * card J" using card_Un_le[of "H <#> J" "{x} <#> J"] ‹card (insert x H <#> J) = card (insert x H) * card J› by (simp add: step.hyps(1) step.hyps(2)) then have card_eq:"card (H <#> J) = card H * card J" using set_mult_card_le[of H J] step H_c by linarith then have ih: "⋀a b. ⟦a ∈ H; b ∈ H; a ≠ b⟧ ⟹ ((⊗) a ` J) ∩ ((⊗) b ` J) = {}" using step H_c by presburger have "card (insert x H) * card J = card H * card J + card J" using ‹x ∉ H› using step by simp then have "({x} <#> J) ∩ (H <#> J) = {}" using card_eq card_x ins card_Un_Int[of "H <#> J" "{x} <#> J"] step set_mult_finite by auto then have "⋀a. a ∈ H ⟹ (⋃y∈J. {a ⊗ y}) ∩ (⋃y∈J. {x ⊗ y}) = {}" using set_mult_def[of G _ J] by blast then have "⋀a b. ⟦a ∈ (insert x H); b ∈ (insert x H); a ≠ b⟧ ⟹ ((⊗) a ` J) ∩ ((⊗) b ` J) = {}" using ‹x ∉ H› ih by blast then show ?case using step by algebra qed lemma (in group) set_mult_card_eq_impl_empty_inter': assumes "finite H" "finite J" "H ⊆ carrier G" "J ⊆ carrier G" "card (H <#> J) = card H * card J" shows "⋀a b. ⟦a ∈ H; b ∈ H; a ≠ b⟧ ⟹ (l_coset G a J) ∩ (l_coset G b J) = {}" unfolding l_coset_def using set_mult_card_eq_impl_empty_inter image_def[of "(⊗) _" J] assms by blast lemma (in comm_group) set_mult_comm: assumes "H ⊆ carrier G" "J ⊆ carrier G" shows "(H <#> J) = (J <#> H)" unfolding set_mult_def proof - have 1: "⋀a b. ⟦a ∈ carrier G; b ∈ carrier G⟧ ⟹ {a ⊗ b} = {b ⊗ a}" using m_comm by simp then have "⋀a b.⟦a ∈ H; b ∈ J⟧ ⟹ {a ⊗ b} = {b ⊗ a}" using assms by auto moreover have "⋀a b.⟦b ∈ H; a ∈ J⟧ ⟹ {a ⊗ b} = {b ⊗ a}" using assms 1 by auto ultimately show "(⋃h∈H. ⋃k∈J. {h ⊗ k}) = (⋃k∈J. ⋃h∈H. {k ⊗ h})" by fast qed lemma (in group) set_mult_one_imp_inc: assumes "𝟭 ∈ A" "A ⊆ carrier G" "B ⊆ carrier G" shows "B ⊆ (B <#> A)" proof fix x assume "x ∈ B" thus "x ∈ (B <#> A)" using assms unfolding set_mult_def by force qed text ‹In all cases, we know that the product of two sets is always contained in the subgroup generated by them.› lemma (in group) set_mult_subset_generate: assumes "A ⊆ carrier G" "B ⊆ carrier G" shows "A <#> B ⊆ generate G (A ∪ B)" proof fix x assume "x ∈ A <#> B" then obtain a b where ab: "a ∈ A" "b ∈ B" "x = a ⊗ b" unfolding set_mult_def by blast then have "a ∈ generate G (A ∪ B)" "b ∈ generate G (A ∪ B)" using generate.incl[of _ "A ∪ B" G] by simp+ thus "x ∈ generate G (A ∪ B)" using ab generate.eng by metis qed text ‹In the case of subgroups, the set product is just the subgroup generated by both of the subgroups.› lemma (in comm_group) set_mult_eq_generate_subgroup: assumes "subgroup H G" "subgroup J G" shows "generate G (H ∪ J) = H <#> J" (is "?L = ?R") proof show "?L ⊆ ?R" proof fix x assume "x ∈ ?L" then show "x ∈ ?R" proof(induction rule: generate.induct) case one have "𝟭 ⊗ 𝟭 = 𝟭" using nat_pow_one[of 2] by simp thus ?case using assms subgroup.one_closed[OF assms(1)] subgroup.one_closed[OF assms(2)] set_mult_def[of G H J] by fastforce next case (incl x) have H1: "𝟭 ∈ H" using assms subgroup.one_closed by auto have J1: "𝟭 ∈ J" using assms subgroup.one_closed by auto have lx: "x ⊗ 𝟭 = x" using r_one[of x] incl subgroup.subset assms by blast have rx: "𝟭 ⊗ x = x" using l_one[of x] incl subgroup.subset assms by blast show ?case proof (cases "x ∈ H") case True then show ?thesis using set_mult_def J1 lx by fastforce next case False then show ?thesis using set_mult_def H1 rx incl by fastforce qed next case (inv h) then have inv_in:"(inv h) ∈ H ∪ J" (is "?iv ∈ H ∪ J") using assms subgroup.m_inv_closed[of _ G h] by (cases "h ∈ H"; blast) have H1: "𝟭 ∈ H" using assms subgroup.one_closed by auto have J1: "𝟭 ∈ J" using assms subgroup.one_closed by auto have lx: "?iv ⊗ 𝟭 = ?iv" using r_one[of "?iv"] subgroup.subset inv_in assms by blast have rx: "𝟭 ⊗ ?iv = ?iv" using l_one[of "?iv"] incl subgroup.subset inv_in assms by blast show ?case proof (cases "?iv ∈ H") case True then show ?thesis using set_mult_def[of G H J] J1 lx by fastforce next case False then show ?thesis using set_mult_def[of G H J] H1 rx inv_in by fastforce qed next case (eng h g) from eng(3) obtain a b where aH: "a ∈ H" and bJ: "b ∈ J" and h_def: "h = a ⊗ b" using set_mult_def[of G H J] by fast have a_carr: "a ∈ carrier G" by (metis subgroup.mem_carrier assms(1) aH) have b_carr: "b ∈ carrier G" by (metis subgroup.mem_carrier assms(2) bJ) from eng(4) obtain c d where cH: "c ∈ H" and dJ: "d ∈ J" and g_def: "g = c ⊗ d" using set_mult_def[of G H J] by fast have c_carr: "c ∈ carrier G" by (metis subgroup.mem_carrier assms(1) cH) have d_carr: "d ∈ carrier G" by (metis subgroup.mem_carrier assms(2) dJ) then have "h ⊗ g = (a ⊗ c) ⊗ (b ⊗ d)" using a_carr b_carr c_carr d_carr g_def h_def m_assoc m_comm by force moreover have "a ⊗ c ∈ H" using assms(1) aH cH subgroup.m_closed by fast moreover have "b ⊗ d ∈ J" using assms(2) bJ dJ subgroup.m_closed by fast ultimately show ?case using set_mult_def by fast qed qed next show "?R ⊆ ?L" using set_mult_subset_generate[of H J] subgroup.subset assms by blast qed end

# Theory Miscellaneous_Groups

(* File: Miscellaneous_Groups.thy Author: Joseph Thommes, TU München *) section ‹Miscellaneous group facts› theory Miscellaneous_Groups imports Set_Multiplication begin text ‹As the name suggests, this section contains several smaller lemmas about groups.› (* Manuel Eberl *) lemma (in subgroup) nat_pow_closed [simp,intro]: "a ∈ H ⟹ pow G a (n::nat) ∈ H" by (induction n) (auto simp: nat_pow_def) (* Manuel Eberl *) lemma nat_pow_modify_carrier: "a [^]⇘_{G⦇carrier := H⦈}⇙ b = a [^]⇘_{G}⇙ (b::nat)" by (simp add: nat_pow_def) lemma (in group) subgroup_card_dvd_group_ord: assumes "subgroup H G" shows "card H dvd order G" using Coset.group.lagrange[of G H] assms group_axioms by (metis dvd_triv_right) lemma (in group) subgroup_card_eq_order: assumes "subgroup H G" shows "card H = order (G⦇carrier := H⦈)" unfolding order_def by simp lemma (in group) finite_subgroup_card_neq_0: assumes "subgroup H G" "finite H" shows "card H ≠ 0" using subgroup_nonempty assms by auto lemma (in group) subgroup_order_dvd_group_order: assumes "subgroup H G" shows "order (G⦇carrier := H⦈) dvd order G" by (metis subgroup_card_dvd_group_ord[of H] assms subgroup_card_eq_order) lemma (in group) sub_subgroup_dvd_card: assumes "subgroup H G" "subgroup J G" "J ⊆ H" shows "card J dvd card H" by (metis subgroup_incl[of J H] subgroup_card_eq_order[of H] group.subgroup_card_dvd_group_ord[of "(G⦇carrier := H⦈)" J] assms subgroup.subgroup_is_group[of H G] group_axioms) lemma (in group) inter_subgroup_dvd_card: assumes "subgroup H G" "subgroup J G" shows "card (H ∩ J) dvd card H" using subgroups_Inter_pair[of H J] assms sub_subgroup_dvd_card[of H "H ∩ J"] by blast lemma (in group) subgroups_card_coprime_inter_card_one: assumes "subgroup H G" "subgroup J G" "coprime (card H) (card J)" shows "card (H ∩ J) = 1" proof - from assms inter_subgroup_dvd_card have "is_unit (card (H ∩ J))" unfolding coprime_def by (meson Int_lower2 sub_subgroup_dvd_card subgroup_Int) then show ?thesis by simp qed lemma (in group) coset_neq_imp_empty_inter: assumes "subgroup H G" "a ∈ carrier G" "b ∈ carrier G" shows "H #> a ≠ H #> b ⟹ (H #> a) ∩ (H #> b) = {}" by (metis Int_emptyI assms repr_independence) lemma (in comm_group) subgroup_is_comm_group: assumes "subgroup H G" shows "comm_group (G⦇carrier := H⦈)" unfolding comm_group_def proof interpret H: subgroup H G by fact interpret H: submonoid H G using H.subgroup_is_submonoid . show "Group.group (G⦇carrier := H⦈)" by blast show "comm_monoid (G⦇carrier := H⦈)" using submonoid_is_comm_monoid H.submonoid_axioms by blast qed lemma (in group) pow_int_mod_ord: assumes [simp]:"a ∈ carrier G" "ord a ≠ 0" shows "a [^] (n::int) = a [^] (n mod ord a)" proof - obtain q r where d: "q = n div ord a" "r = n mod ord a" "n = q * ord a + r" using mod_div_decomp by blast hence "a [^] n = (a [^] int (ord a)) [^] q ⊗ a [^] r" using assms(1) int_pow_mult int_pow_pow by (metis mult_of_nat_commute) also have "… = 𝟭 [^] q ⊗ a [^] r" by (simp add: int_pow_int) also have "… = a [^] r" by simp finally show ?thesis using d(2) by blast qed lemma (in group) pow_nat_mod_ord: assumes [simp]:"a ∈ carrier G" "ord a ≠ 0" shows "a [^] (n::nat) = a [^] (n mod ord a)" proof - obtain q r where d: "q = n div ord a" "r = n mod ord a" "n = q * ord a + r" using mod_div_decomp by blast hence "a [^] n = (a [^] ord a) [^] q ⊗ a [^] r" using assms(1) nat_pow_mult nat_pow_pow by presburger also have "… = 𝟭 [^] q ⊗ a [^] r" by auto also have "… = a [^] r" by simp finally show ?thesis using d(2) by blast qed lemma (in group) ord_min: assumes "m ≥ 1" "x ∈ carrier G" "x [^] m = 𝟭" shows "ord x ≤ m" using assms pow_eq_id by auto (* Manuel Eberl *) lemma (in group) bij_betw_mult_left[intro]: assumes [simp]: "x ∈ carrier G" shows "bij_betw (λy. x ⊗ y) (carrier G) (carrier G)" by (intro bij_betwI[where ?g = "λy. inv x ⊗ y"]) (auto simp: m_assoc [symmetric]) (* Manuel Eberl *) lemma (in subgroup) inv_in_iff: assumes "x ∈ carrier G" "group G" shows "inv x ∈ H ⟷ x ∈ H" proof safe assume "inv x ∈ H" hence "inv (inv x) ∈ H" by blast also have "inv (inv x) = x" by (intro group.inv_inv) (use assms in auto) finally show "x ∈ H" . qed auto (* Manuel Eberl *) lemma (in subgroup) mult_in_cancel_left: assumes "y ∈ carrier G" "x ∈ H" "group G" shows "x ⊗ y ∈ H ⟷ y ∈ H" proof safe assume "x ⊗ y ∈ H" hence "inv x ⊗ (x ⊗ y) ∈ H" using assms by blast also have "inv x ⊗ (x ⊗ y) = y" using assms by (simp add: ‹x ⊗ y ∈ H› group.inv_solve_left') finally show "y ∈ H" . qed (use assms in auto) (* Manuel Eberl *) lemma (in subgroup) mult_in_cancel_right: assumes "x ∈ carrier G" "y ∈ H" "group G" shows "x ⊗ y ∈ H ⟷ x ∈ H" proof safe assume "x ⊗ y ∈ H" hence "(x ⊗ y) ⊗ inv y ∈ H" using assms by blast also have "(x ⊗ y) ⊗ inv y = x" using assms by (simp add: ‹x ⊗ y ∈ H› group.inv_solve_right') finally show "x ∈ H" . qed (use assms in auto) lemma (in group) (* Manuel Eberl *) assumes "x ∈ carrier G" and "x [^] n = 𝟭" and "n > 0" shows ord_le: "ord x ≤ n" and ord_pos: "ord x > 0" proof - have "ord x dvd n" using pow_eq_id[of x n] assms by auto thus "ord x ≤ n" "ord x > 0" using assms by (auto intro: dvd_imp_le) qed lemma (in group) ord_conv_Least: (* Manuel Eberl *) assumes "x ∈ carrier G" "∃n::nat > 0. x [^] n = 𝟭" shows "ord x = (LEAST n::nat. 0 < n ∧ x [^] n = 𝟭)" proof (rule antisym) show "ord x ≤ (LEAST n::nat. 0 < n ∧ x [^] n = 𝟭)" using assms LeastI_ex[OF assms(2)] by (intro ord_le) auto show "ord x ≥ (LEAST n::nat. 0 < n ∧ x [^] n = 𝟭)" using assms by (intro Least_le) (auto intro: pow_ord_eq_1 ord_pos) qed lemma (in group) ord_conv_Gcd: (* Manuel Eberl *) assumes "x ∈ carrier G" shows "ord x = Gcd {n. x [^] n = 𝟭}" by (rule sym, rule Gcd_eqI) (use assms in ‹auto simp: pow_eq_id›) lemma (in group) subgroup_ord_eq: assumes "subgroup H G" "x ∈ H" shows "group.ord (G⦇carrier := H⦈) x = ord x" using nat_pow_consistent ord_def group.ord_def[of "(G⦇carrier := H⦈)" x] subgroup.subgroup_is_group[of H G] assms by simp lemma (in group) ord_FactGroup: assumes "subgroup P G" "group (G Mod P)" shows "order (G Mod P) * card P = order G" using lagrange[of P] FactGroup_def[of G P] assms order_def[of "(G Mod P)"] by fastforce lemma (in group) one_is_same: assumes "subgroup H G" shows "𝟭⇘_{G⦇carrier := H⦈}⇙ = 𝟭" by simp lemma (in group) kernel_FactGroup: assumes "P ⊲ G" shows "kernel G (G Mod P) (λx. P #> x) = P" proof(rule equalityI; rule subsetI) fix x assume "x ∈ kernel G (G Mod P) ((#>) P)" then have "P #> x = 𝟭⇘_{G Mod P}⇙" "x ∈ carrier G" unfolding kernel_def by simp+ with coset_join1[of P x] show "x ∈ P" using assms unfolding normal_def by simp next fix x assume x:"x ∈ P" then have xc: "x ∈ carrier G" using assms subgroup.subset unfolding normal_def by fast from x have "P #> x = P" using assms by (simp add: normal_imp_subgroup subgroup.rcos_const) thus "x ∈ kernel G (G Mod P) ((#>) P)" unfolding kernel_def using xc by simp qed lemma (in group) sub_subgroup_coprime: assumes "subgroup H G" "subgroup J G" "coprime (card H) (card J)" and "subgroup sH G" "subgroup sJ G" "sH ⊆ H" "sJ ⊆ J" shows "coprime (card sH) (card sJ)" using assms by (meson coprime_divisors sub_subgroup_dvd_card) lemma (in group) pow_eq_nat_mod: assumes "a ∈ carrier G" "a [^] n = a [^] m" shows "n mod (ord a) = m mod (ord a)" proof - from assms have "a [^] (n - m) = 𝟭" using pow_eq_div2 by blast hence "ord a dvd n - m" using assms(1) pow_eq_id by blast thus ?thesis by (metis assms mod_eq_dvd_iff_nat nat_le_linear pow_eq_div2 pow_eq_id) qed lemma (in group) pow_eq_int_mod: fixes n m::int assumes "a ∈ carrier G" "a [^] n = a [^] m" shows "n mod (ord a) = m mod (ord a)" proof - from assms have "a [^] (n - m) = 𝟭" using int_pow_closed int_pow_diff r_inv by presburger hence "ord a dvd n - m" using assms(1) int_pow_eq_id by blast thus ?thesis by (meson mod_eq_dvd_iff) qed end

# Theory Generated_Groups_Extend

(* File: Generated_Groups_Extend.thy Author: Joseph Thommes, TU München *) section ‹Generated Groups› theory Generated_Groups_Extend imports Miscellaneous_Groups "HOL-Algebra.Algebra" begin text ‹This section extends the lemmas and facts about ‹generate›. Starting with a basic fact.› lemma (in group) generate_sincl: "A ⊆ generate G A" using generate.incl by fast text ‹The following lemmas reflect some of the idempotence characteristics of ‹generate› and have proved useful at several occasions.› lemma (in group) generate_idem: assumes "A ⊆ carrier G" shows "generate G (generate G A) = generate G A" using assms generateI group.generate_is_subgroup by blast lemma (in group) generate_idem': assumes "A ⊆ carrier G" "B ⊆ carrier G" shows "generate G (generate G A ∪ B) = generate G (A ∪ B)" proof show "generate G (generate G A ∪ B) ⊆ generate G (A ∪ B)" proof - have "generate G A ∪ B ⊆ generate G (A ∪ B)" proof - have "generate G A ⊆ generate G (A ∪ B)" using mono_generate by simp moreover have "B ⊆ generate G (A ∪ B)" by (simp add: generate.incl subset_iff) ultimately show ?thesis by simp qed then have "generate G (generate G A ∪ B) ⊆ generate G (generate G (A ∪ B))" using mono_generate by auto with generate_idem[of "A ∪ B"] show ?thesis using assms by simp qed show "generate G (A ∪ B) ⊆ generate G (generate G A ∪ B)" proof - have "A ⊆ generate G A" using generate.incl by fast thus ?thesis using mono_generate[of "A ∪ B" "generate G A ∪ B"] by blast qed qed lemma (in group) generate_idem'_right: assumes "A ⊆ carrier G" "B ⊆ carrier G" shows "generate G (A ∪ generate G B) = generate G (A ∪ B)" using generate_idem'[OF assms(2) assms(1)] by (simp add: sup_commute) lemma (in group) generate_idem_Un: assumes "A ⊆ carrier G" shows "generate G (⋃x∈A. generate G {x}) = generate G A" proof have "A ⊆ (⋃x∈A. generate G {x})" using generate.incl by force thus "generate G A ⊆ generate G (⋃x∈A. generate G {x})" using mono_generate by presburger have "⋀x. x ∈ A ⟹ generate G {x} ⊆ generate G A" using mono_generate by auto hence "(⋃x∈A. generate G {x}) ⊆ generate G A" by blast thus "generate G (⋃x∈A. generate G {x}) ⊆ generate G A" using generate_idem[OF assms] mono_generate by blast qed lemma (in group) generate_idem_fUn: assumes "f A ⊆ carrier G" shows "generate G (⋃ {generate G {x} |x. x ∈ f A}) = generate G (f A)" proof have "f A ⊆ ⋃ {generate G {x} |x. x ∈ f A}" proof fix x assume x: "x ∈ f A" have "x ∈ generate G {x}" using generate.incl by fast thus "x ∈ ⋃ {generate G {x} |x. x ∈ f A}" using x by blast qed thus "generate G (f A) ⊆ generate G (⋃ {generate G {x} |x. x ∈ f A})" using mono_generate by auto have "⋀x. x ∈ f A ⟹ generate G {x} ⊆ generate G (f A)" using mono_generate by simp hence "(⋃ {generate G {x} |x. x ∈ f A}) ⊆ generate G (f A)" by blast with mono_generate[OF this] show "generate G (⋃ {generate G {x} |x. x ∈ f A}) ⊆ generate G (f A)" using generate_idem[OF assms] by simp qed lemma (in group) generate_idem_fim_Un: assumes "⋃(f ` A) ⊆ carrier G" shows "generate G (⋃S ∈ A. generate G (f S)) = generate G (⋃ {generate G {x} |x. x ∈ ⋃ (f ` A)})" proof have "⋀S. S ∈ A ⟹ generate G (f S) = generate G (⋃ {generate G {x} |x. x ∈ f S})" using generate_idem_fUn[of f] assms by blast then have "generate G (⋃S ∈ A. generate G (f S)) = generate G (⋃S ∈ A. generate G (⋃ {generate G {x} |x. x ∈ f S}))" by simp have "⋃ {generate G {x} |x. x ∈ ⋃ (f ` A)} ⊆ (⋃S∈A. generate G (f S))" proof fix x assume x: "x ∈ ⋃ {generate G {x} |x. x ∈ ⋃ (f ` A)}" then obtain a where a: "x ∈ generate G {a}" "a ∈ ⋃ (f ` A)" by blast then obtain M where M: "a ∈ f M" "M ∈ A" by blast then have "generate G {a} ⊆ generate G (f M)" using generate.incl[OF M(1), of G] mono_generate[of "{a}" "generate G (f M)"] generate_idem assms by auto then have "x ∈ generate G (f M)" using a by blast thus "x ∈ (⋃S∈A. generate G (f S))" using M by blast qed thus "generate G (⋃ {generate G {x} |x. x ∈ ⋃ (f ` A)}) ⊆ generate G (⋃S∈A. generate G (f S))" using mono_generate by simp have a: "generate G (⋃S∈A. generate G (f S)) ⊆ generate G (⋃ (f ` A))" proof - have "⋀S. S ∈ A ⟹ generate G (f S) ⊆ generate G (⋃ (f ` A))" using mono_generate[of _ "⋃ (f ` A)"] by blast then have "(⋃S∈A. generate G (f S)) ⊆ generate G (⋃ (f ` A))" by blast then have "generate G (⋃S∈A. generate G (f S)) ⊆ generate G (generate G (⋃ (f ` A)))" using mono_generate by meson thus "generate G (⋃S∈A. generate G (f S)) ⊆ generate G (⋃ (f ` A))" using generate_idem assms by blast qed have "⋃ {generate G {x} |x. x ∈ ⋃ (f ` A)} = (⋃x∈⋃ (f ` A). generate G {x})" by blast with generate_idem_Un[OF assms] have "generate G (⋃ {generate G {x} |x. x ∈ ⋃ (f ` A)}) = generate G (⋃ (f ` A))" by simp with a show "generate G (⋃S∈A. generate G (f S)) ⊆ generate G (⋃ {generate G {x} |x. x ∈ ⋃ (f ` A)})" by blast qed text ‹The following two rules allow for convenient proving of the equality of two generated sets.› lemma (in group) generate_eqI: assumes "A ⊆ carrier G" "B ⊆ carrier G" "A ⊆ generate G B" "B ⊆ generate G A" shows "generate G A = generate G B" using assms generate_idem by (metis generate_idem' inf_sup_aci(5) sup.absorb2) lemma (in group) generate_one_switched_eqI: assumes "A ⊆ carrier G" "a ∈ A" "B = (A - {a}) ∪ {b}" and "b ∈ generate G A" "a ∈ generate G B" shows "generate G A = generate G B" proof(intro generate_eqI) show "A ⊆ carrier G" by fact show "B ⊆ carrier G" using assms generate_incl by blast show "A ⊆ generate G B" using assms generate_sincl[of B] by blast show "B ⊆ generate G A" using assms generate_sincl[of A] by blast qed lemma (in group) generate_subset_eqI: assumes "A ⊆ carrier G" "B ⊆ A" "A - B ⊆ generate G B" shows "generate G A = generate G B" proof show "generate G B ⊆ generate G A" by (intro mono_generate, fact) show "generate G A ⊆ generate G B" proof(subst generate_idem[of "B", symmetric]) show "generate G A ⊆ generate G (generate G B)" by (intro mono_generate, use assms generate_sincl[of B] in auto) qed (use assms in blast) qed text ‹Some smaller lemmas about ‹generate›.› lemma (in group) generate_subset_change_eqI: assumes "A ⊆ carrier G" "B ⊆ carrier G" "C ⊆ carrier G" "generate G A = generate G B" shows "generate G (A ∪ C) = generate G (B ∪ C)" by (metis assms generate_idem') lemma (in group) generate_subgroup_id: assumes "subgroup H G" shows "generate G H = H" using assms generateI by auto lemma (in group) generate_consistent': assumes "subgroup H G" "A ⊆ H" shows "∀x ∈ A. generate G {x} = generate (G⦇carrier := H⦈) {x}" using generate_consistent assms by auto lemma (in group) generate_singleton_one: assumes "generate G {a} = {𝟭}" shows "a = 𝟭" using generate.incl[of a "{a}" G] assms by auto lemma (in group) generate_inv_eq: assumes "a ∈ carrier G" shows "generate G {a} = generate G {inv a}" by (intro generate_eqI; use assms generate.inv[of a] generate.inv[of "inv a" "{inv a}" G] inv_inv[OF assms] in auto) lemma (in group) generate_eq_imp_subset: assumes "generate G A = generate G B" shows "A ⊆ generate G B" using generate.incl assms by fast text ‹The neutral element does not play a role when generating a subgroup.› lemma (in group) generate_one_irrel: "generate G A = generate G (A ∪ {𝟭})" proof show "generate G A ⊆ generate G (A ∪ {𝟭})" by (intro mono_generate, blast) show "generate G (A ∪ {𝟭}) ⊆ generate G A" proof(rule subsetI) show "x ∈ generate G A" if "x ∈ generate G (A ∪ {𝟭})" for x using that by (induction rule: generate.induct; use generate.one generate.incl generate.inv generate.eng in auto) qed qed lemma (in group) generate_one_irrel': "generate G A = generate G (A - {𝟭})" using generate_one_irrel by (metis Un_Diff_cancel2) text ‹Also, we can express the subgroup generated by a singleton with finite order using just its powers up to its order.› lemma (in group) generate_nat_pow: assumes "ord a ≠ 0" "a ∈ carrier G" shows "generate G {a} = {a [^] k |k. k ∈ {0..ord a - 1}}" using assms generate_pow_nat ord_elems_inf_carrier by auto lemma (in group) generate_nat_pow': assumes "ord a ≠ 0" "a ∈ carrier G" shows "generate G {a} = {a [^] k |k. k ∈ {1..ord a}}" proof - have "{a [^] k |k. k ∈ {1..ord a}} = {a [^] k |k. k ∈ {0..ord a - 1}}" proof - have "a [^] k ∈ {a [^] k |k. k ∈ {0..ord a - 1}}" if "k ∈ {1..ord a}" for k using that pow_nat_mod_ord[OF assms(2, 1), of "ord a"] assms by (cases "k = ord a"; force) moreover have "a [^] k ∈ {a [^] k |k. k ∈ {1..ord a}}" if "k ∈ {0..ord a - 1}" for k proof(cases "k = 0") case True hence "a [^] k = a [^] ord a" using pow_ord_eq_1[OF assms(2)] by auto moreover have "ord a ∈ {1..ord a}" using assms unfolding atLeastAtMost_def atLeast_def atMost_def by auto ultimately show ?thesis by blast next case False then show ?thesis using that by auto qed ultimately show ?thesis by blast qed with generate_nat_pow[OF assms] show ?thesis by simp qed end

# Theory General_Auxiliary

(* File: General_Auxiliary.thy Author: Joseph Thommes, TU München; Manuel Eberl, TU München *) section ‹Auxiliary lemmas› theory General_Auxiliary imports "HOL-Algebra.Algebra" begin lemma inter_imp_subset: "A ∩ B = A ⟹ A ⊆ B" by blast lemma card_inter_eq: assumes "finite A" "card (A ∩ B) = card A" shows "A ⊆ B" proof - have "A ∩ B ⊆ A" by blast with assms have "A ∩ B = A" using card_subset_eq by blast thus ?thesis by blast qed lemma coprime_eq_empty_prime_inter: assumes "(n::nat) ≠ 0" "m ≠ 0" shows "coprime n m ⟷ (prime_factors n) ∩ (prime_factors m) = {}" proof show "coprime n m ⟹ prime_factors n ∩ prime_factors m = {}" proof (rule ccontr) assume cp: "coprime n m" assume pf: "prime_factors n ∩ prime_factors m ≠ {}" then obtain p where p: "p ∈ prime_factors n" "p ∈ prime_factors m" by blast then have p_dvd: "p dvd n" "p dvd m" by blast+ moreover have "¬is_unit p" using p using not_prime_unit by blast ultimately show "False" using cp unfolding coprime_def by simp qed assume assm: "prime_factors n ∩ prime_factors m = {}" show "coprime n m" unfolding coprime_def proof fix c show "c dvd n ⟶ c dvd m ⟶ is_unit c" proof(rule; rule) assume c: "c dvd n" "c dvd m" then have "prime_factors c ⊆ prime_factors n" "prime_factors c ⊆ prime_factors m" using assms dvd_prime_factors by blast+ then have "prime_factors c = {}" using assm by blast thus "is_unit c" using assms c by (metis dvd_0_left_iff prime_factorization_empty_iff set_mset_eq_empty_iff) qed qed qed lemma prime_factors_Prod: assumes "finite S" "⋀a. a ∈ S ⟹ f a ≠ 0" shows "prime_factors (prod f S) = ⋃(prime_factors ` f ` S)" using assms proof(induction S rule: finite_induct) case empty then show ?case by simp next case i: (insert x F) from i have x: "f x ≠ 0" by blast from i have F: "prod f F ≠ 0" by simp from i have "prime_factors(prod f F) = ⋃ (prime_factors ` f ` F)" by blast moreover have "prod f (insert x F) = (prod f F) * f x" using i mult.commute by force ultimately have "prime_factors (prod f (insert x F)) = (⋃(prime_factors ` f ` F)) ∪ prime_factors (f x)" using prime_factors_product[OF F x] by argo thus ?case by force qed lemma lcm_is_Min_multiple_nat: assumes "c ≠ 0" "(a::nat) dvd c" "(b::nat) dvd c" shows "c ≥ lcm a b" using lcm_least[of a c b] assms by fastforce lemma diff_prime_power_imp_coprime: assumes "p ≠ q" "Factorial_Ring.prime (p::nat)" "Factorial_Ring.prime q" shows "coprime (p ^ (n::nat)) (q ^ m)" using assms by (metis power_0 power_one_right prime_dvd_power prime_imp_power_coprime_nat prime_nat_iff prime_power_inj'') lemma "finite (prime_factors x)" using finite_set_mset by blast lemma card_ge_1_two_diff: assumes "card A > 1" obtains x y where "x ∈ A" "y ∈ A" "x ≠ y" proof - have fA: "finite A" using assms by (metis card.infinite not_one_less_zero) from assms obtain x where x: "x ∈ A" by fastforce with assms fA have "card (A - {x}) > 0" by simp then obtain y where y: "y ∈ (A - {x})" by (metis card_gt_0_iff ex_in_conv) thus ?thesis using that[of x y] x by blast qed lemma infinite_two_diff: assumes "infinite A" obtains x y where "x ∈ A" "y ∈ A" "x ≠ y" proof - from assms obtain x where x: "x ∈ A" by fastforce from assms have "infinite (A - {x})" by simp then obtain y where y: "y ∈ (A - {x})" by (metis ex_in_conv finite.emptyI) show ?thesis using that[of x y] using x y by blast qed lemma Inf_le: "Inf A ≤ x" if "x ∈ (A::nat set)" for x proof (cases "A = {}") case True then show ?thesis using that by simp next case False hence "Inf A ≤ Inf {x}" using that by (simp add: cInf_lower) also have "… = x" by simp finally show "Inf A ≤ x" by blast qed lemma switch_elem_card_le: assumes "a ∈ A" shows "card (A - {a} ∪ {b}) ≤ card A" using assms by (metis Diff_insert_absorb Set.set_insert Un_commute card.infinite card_insert_disjoint card_mono finite_insert insert_is_Un insert_subset order_refl) lemma pairwise_coprime_dvd: assumes "finite A" "pairwise coprime A" "(n::nat) = prod id A" "∀a∈A. a dvd j" shows "n dvd j" using assms proof (induction A arbitrary: n) case i: (insert x F) have "prod id F dvd j" "x dvd j" using i unfolding pairwise_def by auto moreover have "coprime (prod id F) x" by (metis i(2, 4) id_apply pairwise_insert prod_coprime_left) ultimately show ?case using i(1, 2, 5) by (simp add: coprime_commute divides_mult) qed simp lemma pairwise_coprime_dvd': assumes "finite A" "⋀i j. ⟦i ∈ A; j ∈ A; i ≠ j⟧ ⟹ coprime (f i) (f j)" "(n::nat) = prod f A" "∀a∈A. f a dvd j" shows "n dvd j" using assms proof (induction A arbitrary: n) case i: (insert x F) have "prod f F dvd j" "f x dvd j" using i unfolding pairwise_def by auto moreover have "coprime (prod f F) (f x)" by(intro prod_coprime_left, use i in blast) ultimately show ?case using i by (simp add: coprime_commute divides_mult) qed simp lemma transp_successively_remove1: assumes "transp f" "successively f l" shows "successively f (remove1 a l)" using assms(2) proof(induction l rule: induct_list012) case (3 x y zs) from 3(3)[unfolded successively.simps] have fs: "f x y" "successively f (y # zs)" by auto moreover from this(2) successively.simps have s: "successively f zs" by(cases zs, auto) ultimately have s2: "successively f (remove1 a zs)" "successively f (remove1 a (y # zs))" using 3 by auto consider (x) "x = a" | (y) "y = a ∧ x ≠ a" | (zs) "a ≠ x ∧ a ≠ y" by blast thus ?case proof (cases) case x then show ?thesis using 3 by simp next case y then show ?thesis proof (cases zs) case Nil then show ?thesis using fs by simp next case (Cons a list) hence "f y a" using fs by simp hence "f x a" using fs(1) assms(1)[unfolded transp_def] by blast then show ?thesis using Cons y s by auto qed next case zs then show ?thesis using s2 fs by auto qed qed auto lemma exp_one_2pi_iff: fixes x::real shows "exp (2 * of_real pi * 𝗂 * x) = 1 ⟷ x ∈ ℤ" proof - have c: "cis (2 * x * pi) = 1 ⟷ x ∈ ℤ" by (auto simp: complex_eq_iff sin_times_pi_eq_0 cos_one_2pi_int, meson Ints_cases) have "exp (2 * of_real pi * 𝗂 * x) = exp (𝗂 * complex_of_real (2 * x * pi))" proof - have "2 * of_real pi * 𝗂 * x = 𝗂 * complex_of_real (2 * x * pi)" by simp thus ?thesis by argo qed also from cis_conv_exp have "… = cis (2 * x * pi)" by simp finally show ?thesis using c by simp qed (* Manuel Eberl *) lemma of_int_divide_in_Ints_iff: assumes "b ≠ 0" shows "(of_int a / of_int b :: 'a :: field_char_0) ∈ ℤ ⟷ b dvd a" proof assume *: "(of_int a / of_int b :: 'a :: field_char_0) ∈ ℤ" from * obtain n where "of_int a / of_int b = (of_int n :: 'a)" by (elim Ints_cases) hence "of_int (b * n) = (of_int a :: 'a)" using assms by (subst of_int_mult) (auto simp: field_simps) hence "b * n = a" by (subst (asm) of_int_eq_iff) thus "b dvd a" by auto qed auto (* Manuel Eberl *) lemma of_nat_divide_in_Ints_iff: assumes "b ≠ 0" shows "(of_nat a / of_nat b :: 'a :: field_char_0) ∈ ℤ ⟷ b dvd a" using of_int_divide_in_Ints_iff[of "int b" "int a"] assms by simp lemma true_nth_unity_root: fixes n::nat obtains x::complex where "x ^ n = 1" "⋀m. ⟦0<m; m<n⟧ ⟹ x ^ m ≠ 1" proof(cases "n = 0") case False show ?thesis proof (rule that) show "cis (2 * pi / n) ^ n = 1" by (simp add: DeMoivre) next fix m assume m: "m > 0" "m < n" have "cis (2 * pi / n) ^ m = cis (2 * pi * m / n)" by (simp add: DeMoivre algebra_simps) also have "… = 1 ⟷ real m / real n ∈ ℤ" using exp_one_2pi_iff[of "m / n"] by (simp add: cis_conv_exp algebra_simps) also have "… ⟷ n dvd m" using m by (subst of_nat_divide_in_Ints_iff) auto also have "¬n dvd m" using m by auto finally show "cis (2 * pi / real n) ^ m ≠ 1" . qed qed simp lemma finite_bij_betwI: assumes "finite A" "finite B" "inj_on f A" "f ∈ A → B" "card A = card B" shows "bij_betw f A B" proof (intro bij_betw_imageI) show "inj_on f A" by fact show "f ` A = B" proof - have "card (f ` A) = card B" using assms by (simp add: card_image) moreover have "f ` A ⊆ B" using assms by blast ultimately show ?thesis using assms by (meson card_subset_eq) qed qed lemma powi_mod: "x powi m = x powi (m mod n)" if "x ^ n = 1" "n > 0" for x::complex and m::int proof - have xnz: "x ≠ 0" using that by (metis zero_neq_one zero_power) obtain k::int where k: "m = k*n + (m mod n)" using div_mod_decomp_int by blast have "x powi m = x powi (k*n) * x powi (m mod n)" by (subst k, intro power_int_add, use xnz in auto) moreover have "x powi (k*n) = 1" using that by (metis mult.commute power_int_1_left power_int_mult power_int_of_nat) ultimately show ?thesis by force qed (* Manuel Eberl *) lemma Sigma_insert: "Sigma (insert x A) B = (λy. (x, y)) ` B x ∪ Sigma A B" by auto end

# Theory IDirProds

(* File: IDirProds.thy Author: Joseph Thommes, TU München *) section ‹Internal direct product› theory IDirProds imports Generated_Groups_Extend General_Auxiliary begin subsection ‹Complementarity› text ‹We introduce the notion of complementarity, that plays a central role in the internal direct group product and prove some basic properties about it.› definition (in group) complementary :: "'a set ⇒ 'a set ⇒ bool" where "complementary H1 H2 ⟷ H1 ∩ H2 = {𝟭}" lemma (in group) complementary_symm: "complementary A B ⟷ complementary B A" unfolding complementary_def by blast lemma (in group) subgroup_carrier_complementary: assumes "complementary H J" "subgroup I (G⦇carrier := H⦈)" "subgroup K (G⦇carrier := J⦈)" shows "complementary I K" proof - have "𝟭 ∈ I" "𝟭 ∈ K" using subgroup.one_closed assms by fastforce+ moreover have "I ∩ K ⊆ H ∩ J" using subgroup.subset assms by force ultimately show ?thesis using assms unfolding complementary_def by blast qed lemma (in group) subgroup_subset_complementary: assumes "subgroup H G" "subgroup J G" "subgroup I G" and "I ⊆ J" "complementary H J" shows "complementary H I" by (intro subgroup_carrier_complementary[OF assms(5), of H I] subgroup_incl, use assms in auto) lemma (in group) complementary_subgroup_iff: assumes "subgroup H G" shows "complementary A B ⟷ group.complementary (G⦇carrier := H⦈) A B" proof - interpret H: group "G⦇carrier := H⦈" using subgroup.subgroup_is_group assms by blast have "𝟭⇘_{G}⇙ = 𝟭⇘_{G⦇carrier := H⦈}⇙" by simp then show ?thesis unfolding complementary_def H.complementary_def by simp qed lemma (in group) subgroups_card_coprime_imp_compl: assumes "subgroup H G" "subgroup J G" "coprime (card H) (card J)" shows "complementary H J" unfolding complementary_def proof - interpret JH: subgroup "(H ∩ J)" G using assms subgroups_Inter_pair by blast from subgroups_card_coprime_inter_card_one[OF assms] show "H ∩ J = {𝟭}" using JH.one_closed by (metis card_1_singletonE singletonD) qed lemma (in group) prime_power_complementary_groups: assumes "Factorial_Ring.prime p" "Factorial_Ring.prime q" "p ≠ q" and "subgroup P G" "card P = p ^ x" and "subgroup Q G" "card Q = q ^ y" shows "complementary P Q" proof - from assms have "coprime (card P) (card Q)" by (metis coprime_power_right_iff primes_coprime coprime_def) then show ?thesis using subgroups_card_coprime_imp_compl assms complementary_def by blast qed text ‹With the previous work from the theory about set multiplication we can characterize complementarity of two subgroups in abelian groups by the cardinality of their product.› lemma (in comm_group) compl_imp_diff_cosets: assumes "subgroup H G" "subgroup J G" "finite H" "finite J" and "complementary H J" shows "⋀a b. ⟦a ∈ J; b ∈ J; a ≠ b⟧ ⟹ (H #> a) ≠ (H #> b)" proof (rule ccontr; safe) fix a b assume ab: "a ∈ J" "b ∈ J" "a ≠ b" then have [simp]: "a ∈ carrier G" "b ∈ carrier G" using assms subgroup.subset by auto assume "H #> a = H #> b" then have "a ⊗ inv b ∈ H" using assms(1, 2) ab by (metis comm_group_axioms comm_group_def rcos_self subgroup.mem_carrier subgroup.rcos_module_imp) moreover have "a ⊗ inv b ∈ J" by (rule subgroup.m_closed[OF assms(2) ab(1) subgroup.m_inv_closed[OF assms(2) ab(2)]]) moreover have "a ⊗ inv b ≠ 𝟭" using ab inv_equality by fastforce ultimately have "H ∩ J ≠ {𝟭}" by blast thus False using assms(5) unfolding complementary_def by blast qed lemma (in comm_group) finite_sub_card_eq_mult_imp_comp: assumes "subgroup H G" "subgroup J G" "finite H" "finite J" and "card (H <#> J) = (card J * card H)" shows "complementary H J" unfolding complementary_def proof (rule ccontr) assume "H ∩ J ≠ {𝟭}" have "𝟭 ∈ H" using subgroup.one_closed assms(1) by blast moreover have "𝟭 ∈ J" using subgroup.one_closed assms(2) by blast ultimately have "𝟭 ∈ (H ∩ J)" by blast then obtain a where a_def: "a ∈ (H ∩ J) ∧ a ≠ 𝟭" using ‹H ∩ J ≠ {𝟭}› by blast then have aH: "a ∈ H" by blast then have a_inv_H: "inv a ∈ H ∧ inv a ≠ 𝟭" using assms(1) by (meson a_def inv_eq_1_iff subgroup.mem_carrier subgroupE(3)) from a_def have aJ: "a ∈ J" by blast then have a_inv_J: "inv a ∈ J ∧ inv a ≠ 𝟭" using assms(2) by (meson a_def inv_eq_1_iff subgroup.mem_carrier subgroupE(3)) from a_def have a_c: "a ∈ carrier G" using subgroup.subset[of J G] assms(2) by blast from set_mult_card_eq_impl_empty_inter'[of H J] have empty: "⋀a b. ⟦a ∈ H; b ∈ H; a ≠ b⟧ ⟹ (l_coset G a J) ∩ (l_coset G b J) = {}" using assms subgroup.subset[of _ G] by simp have "𝟭 ∈ 𝟭 <# J" using ‹𝟭 ∈ J› unfolding l_coset_def by force moreover have "𝟭 ∈ a <# J" using a_inv_J aJ a_c assms ‹𝟭 ∈ J› coset_join3 by blast ultimately have "(l_coset G 𝟭 J) ∩ (l_coset G a J) ≠ {}" by blast then show "False" using empty[of "𝟭" a] a_def aH ‹𝟭 ∈ H› by blast qed lemma (in comm_group) finite_sub_comp_imp_card_eq_mult: assumes "subgroup H G" "subgroup J G" "finite H" "finite J" and "complementary H J" shows "card (H <#> J) = card J * card H" proof - have carr: "H ⊆ carrier G" "J ⊆ carrier G" using assms subgroup.subset by auto from coset_neq_imp_empty_inter[OF assms(1)] compl_imp_diff_cosets[OF assms(1,2)] have em_inter: "⋀a b. ⟦a ∈ J; b ∈ J; a ≠ b⟧ ⟹ (H #> a) ∩ (H #> b) = {}" by (meson assms subgroup.mem_carrier) have "card (⋃a∈J. (H #> a)) = card J * card H" using assms(4) carr(2) em_inter proof (induction J rule: finite_induct) case empty then show ?case by auto next case i: (insert x F) then have cF:"card (⋃ ((#>) H ` F)) = card F * card H" by blast have xc[simp]: "x ∈ carrier G" using i(4) by simp let ?J = "insert x F" from i(2, 4, 5) have em:"(H #> x) ∩ (⋃y∈F. (H #> y)) = {}" by auto have "finite (H #> x)" by (meson carr(1) rcosetsI rcosets_finite assms(3) xc) moreover have "finite (H <#> F)" using set_mult_finite[OF assms(3) i(1) carr(1)] i(4) by blast moreover have "H <#> F = (⋃a∈F. (H #> a))" unfolding set_mult_def using r_coset_def[of G H] by auto ultimately have "card(H #> x) + card(⋃y∈F. (H #> y)) = card((H #> x) ∪ (⋃y∈F. (H #> y))) + card((H #> x) ∩ (⋃y∈F. (H #> y)))" using card_Un_Int by auto then have "card(H #> x) + card(⋃y∈F. (H #> y)) = card((H #> x) ∪ (⋃y∈F. (H #> y)))" using i(5) em by simp moreover have "card (H #> x) = card H" using card_rcosets_equal[of _ H] rcosetsI[of H] carr(1) xc by metis moreover have "card (insert x F) * card H = card F * card H + card H" by (simp add: i) ultimately show ?case using cF by simp qed moreover have "H <#> J = (⋃a∈J. (H #> a))" unfolding set_mult_def using r_coset_def[of G H] by auto ultimately show "card (H <#> J) = card J * card H" by argo qed lemma (in comm_group) finite_sub_comp_iff_card_eq_mult: assumes "subgroup H G" "subgroup J G" "finite H" "finite J" shows "card (H <#> J) = card J * card H ⟷ complementary H J" using finite_sub_comp_imp_card_eq_mult[OF assms] finite_sub_card_eq_mult_imp_comp[OF assms] by blast subsection ‹‹IDirProd› - binary internal direct product› text ‹We introduce the internal direct product formed by two subgroups (so in its binary form).› definition IDirProd :: "('a, 'b) monoid_scheme ⇒ 'a set ⇒ 'a set ⇒ 'a set" where "IDirProd G Y Z = generate G (Y ∪ Z)" text ‹Some trivial lemmas about the binary internal direct product.› lemma (in group) IDirProd_comm: "IDirProd G A B = IDirProd G B A" unfolding IDirProd_def by (simp add: sup_commute) lemma (in group) IDirProd_empty_right: assumes "A ⊆ carrier G" shows "IDirProd G A {} = generate G A" unfolding IDirProd_def by simp lemma (in group) IDirProd_empty_left: assumes "A ⊆ carrier G" shows "IDirProd G {} A = generate G A" unfolding IDirProd_def by simp lemma (in group) IDirProd_one_right: assumes "A ⊆ carrier G" shows "IDirProd G A {𝟭} = generate G A" unfolding IDirProd_def proof interpret sA: subgroup "(generate G A)" G using assms generate_is_subgroup by simp interpret sAone: subgroup "(generate G (A ∪ {𝟭}))" G using assms generate_is_subgroup by simp show "generate G (A ∪ {𝟭}) ⊆ generate G A" using generate_subgroup_incl[of "A ∪ {𝟭}" "generate G A"] generate.incl assms sA.one_closed sA.subgroup_axioms by fast show "generate G A ⊆ generate G (A ∪ {𝟭})" using mono_generate[of A "A ∪ {𝟭}"] by blast qed lemma (in group) IDirProd_one_left: assumes "A ⊆ carrier G" shows "IDirProd G {𝟭} A = generate G A" using IDirProd_one_right[of A] assms unfolding IDirProd_def by force lemma (in group) IDirProd_is_subgroup: assumes "Y ⊆ carrier G" "Z ⊆ carrier G" shows "subgroup (IDirProd G Y Z) G" unfolding IDirProd_def using generate_is_subgroup[of "Y ∪ Z"] assms by simp text ‹Using the theory about set multiplication we can also show the connection of the underlying set in the internal direct product with the set multiplication in the case of an abelian group. Together with the facts about complementarity and the set multiplication we can characterize complementarity by the cardinality of the internal direct product and vice versa.› lemma (in comm_group) IDirProd_eq_subgroup_mult: assumes "subgroup H G" "subgroup J G" shows "IDirProd G H J = H <#> J" unfolding IDirProd_def by (rule set_mult_eq_generate_subgroup[OF assms]) lemma (in comm_group) finite_sub_comp_iff_card_eq_IDirProd: assumes "subgroup H G" "subgroup J G" "finite H" "finite J" shows "card (IDirProd G H J) = card J * card H ⟷ complementary H J" using finite_sub_comp_iff_card_eq_mult IDirProd_eq_subgroup_mult assms by presburger subsection ‹‹IDirProds› - indexed internal direct product› text ‹The indexed version of the internal direct product acting on a family of subgroups.› definition IDirProds :: "('a, 'b) monoid_scheme ⇒ ('c ⇒ 'a set) ⇒ 'c set ⇒ 'a set" where "IDirProds G S I = generate G (⋃(S ` I))" text ‹Lemmas about the indexed internal direct product.› lemma (in group) IDirProds_incl: assumes "i ∈ I" shows "S i ⊆ IDirProds G S I" unfolding IDirProds_def using assms generate.incl[of _ "⋃(S ` I)" G] by blast lemma (in group) IDirProds_empty: "IDirProds G S {} = {𝟭}" unfolding IDirProds_def using generate_empty by simp lemma (in group) IDirProds_is_subgroup: assumes "⋃(S ` I) ⊆ (carrier G)" shows "subgroup (IDirProds G S I) G" unfolding IDirProds_def using generate_is_subgroup[of "⋃(S ` I)"] assms by auto lemma (in group) IDirProds_subgroup_id: "subgroup (S i) G ⟹ IDirProds G S {i} = S i" by (simp add: generate_subgroup_id IDirProds_def) lemma (in comm_group) IDirProds_Un: assumes "∀i∈A. subgroup (S i) G" "∀j∈B. subgroup (S j) G" shows "IDirProds G S (A ∪ B) = IDirProds G S A <#> IDirProds G S B" proof - have subset: "⋃ (S ` A) ⊆ carrier G" "⋃ (S ` B) ⊆ carrier G" using subgroup.subset assms(1, 2) by blast+ have "IDirProds G S A <#> IDirProds G S B = IDirProd G (IDirProds G S A) (IDirProds G S B)" using assms by (intro IDirProd_eq_subgroup_mult [symmetric] IDirProds_is_subgroup subset) also have "… = generate G (⋃ (S ` A) ∪ IDirProds G S B)" unfolding IDirProds_def IDirProd_def by (intro generate_idem' generate_incl subset) also have "… = generate G (⋃(S ` A) ∪ ⋃(S ` B))" unfolding IDirProds_def IDirProd_def by (intro generate_idem'_right generate_incl subset) also have "⋃(S ` A) ∪ ⋃(S ` B) = ⋃(S ` (A ∪ B))" by blast also have "generate G … = IDirProds G S (A ∪ B)" unfolding IDirProds_def .. finally show ?thesis .. qed lemma (in comm_group) IDirProds_finite: assumes "finite I" "∀i∈I. subgroup (S i) G" "∀i∈I. finite (S i)" shows "finite (IDirProds G S I)" using assms proof (induction I rule: finite_induct) case empty thus ?case using IDirProds_empty[of S] by simp next case i: (insert x I) interpret Sx: subgroup "S x" G using i by blast have cx: "(S x) ⊆ carrier G" by force have cI: "⋃(S ` I) ⊆ carrier G" using i subgroup.subset by blast interpret subgroup "IDirProds G S I" G using IDirProds_is_subgroup[OF cI] . have cIP: "(IDirProds G S I) ⊆ carrier G" by force from i have f: "finite (S x)" "finite (IDirProds G S I)" "finite {x}" by blast+ from IDirProds_Un[of "{x}" S I] have "IDirProds G S ({x} ∪ I) = IDirProds G S {x} <#> IDirProds G S I" using i by blast also have "… = S x <#> IDirProds G S I" using IDirProds_subgroup_id[of S x] Sx.subgroup_axioms by force also have "finite (…)" using set_mult_finite[OF f(1, 2) cx cIP] . finally show ?case unfolding insert_def by simp qed lemma (in comm_group) IDirProds_compl_imp_compl: assumes "∀i ∈ I. subgroup (S i) G" and "subgroup H G" assumes "complementary H (IDirProds G S I)" "i ∈ I" shows "complementary H (S i)" proof - have "S i ⊆ IDirProds G S I" using assms IDirProds_incl by fast then have "H ∩ (S i) ⊆ H ∩ IDirProds G S I" by blast moreover have "𝟭 ∈ H ∩ (S i)" using subgroup.one_closed assms by auto ultimately show "complementary H (S i)" using assms(3) unfolding complementary_def by blast qed text ‹Using the knowledge about the binary internal direct product, we can - in case that all subgroups in the family have coprime orders - also derive the cardinality of the indexed internal direct product.› lemma (in comm_group) IDirProds_card: assumes "finite I" "∀i∈I. subgroup (S i) G" "∀i∈I. finite (S i)" "pairwise (λx y. coprime (card (S x)) (card (S y))) I" shows "card (IDirProds G S I) = (∏i ∈ I. card (S i))" using assms proof (induction I rule: finite_induct) case empty then show ?case using IDirProds_empty[of S] by simp next case i: (insert x I) have sx: "subgroup (S x) G" using i(4) by blast have cx: "(S x) ⊆ carrier G" using subgroup.subset[OF sx] . have fx: "finite (S x)" using i by blast have cI: "⋃(S ` I) ⊆ carrier G" using subgroup.subset[of _ G] i(4) by blast from generate_is_subgroup[OF this] have sIP: "subgroup (IDirProds G S I) G" unfolding IDirProds_def . then have cIP: "(IDirProds G S I) ⊆ carrier G" using subgroup.subset by blast have fIP: "finite (IDirProds G S I)" using IDirProds_finite[OF i(1)] i by blast from i have ih: "card (IDirProds G S I) = (∏i∈I. card (S i))" unfolding pairwise_def by blast hence cop: "coprime (card (IDirProds G S I)) (card (S x))" proof - have cFI0: "card (IDirProds G S I) ≠ 0" using finite_subgroup_card_neq_0[OF sIP fIP] . moreover have cx0: "card (S x) ≠ 0" using finite_subgroup_card_neq_0[OF sx fx] . moreover have "prime_factors (card (IDirProds G S I)) ∩ prime_factors (card (S x)) = {}" proof (rule ccontr) have n0: "⋀i. i ∈ I ⟹ card (S i) ≠ 0" using finite_subgroup_card_neq_0 i(4, 5) by blast assume "prime_factors (card (IDirProds G S I)) ∩ prime_factors (card (S x)) ≠ {}" moreover have "prime_factors (card (IDirProds G S I)) = ⋃(prime_factors ` (card ∘ S) ` I)" using n0 prime_factors_Prod[OF i(1), of "card ∘ S"] by (subst ih; simp) moreover have "⋀i. i ∈ I ⟹ prime_factors (card (S i)) ∩ prime_factors (card (S x)) = {}" proof - fix i assume ind: "i ∈ I" then have coPx: "coprime (card (S i)) (card (S x))" using i(2, 6) unfolding pairwise_def by auto have "card (S i) ≠ 0" using n0 ind by blast from coprime_eq_empty_prime_inter[OF this cx0] show "prime_factors (card (S i)) ∩ prime_factors (card (S x)) = {}" using coPx by blast qed ultimately show "False" by auto qed ultimately show ?thesis using coprime_eq_empty_prime_inter by blast qed have "card (IDirProds G S (insert x I)) = card (S x) * card (IDirProds G S I)" proof - from finite_sub_comp_iff_card_eq_IDirProd[OF sIP sx fIP fx] subgroups_card_coprime_imp_compl[OF sIP sx cop] have "card (IDirProd G (IDirProds G S I) (S x)) = card (S x) * card (IDirProds G S I)" by blast moreover have "generate G (⋃ (S ` insert x I)) = generate G (generate G (⋃ (S ` I)) ∪ S x)" by (simp add: Un_commute cI cx generate_idem'_right) ultimately show ?thesis unfolding IDirProds_def IDirProd_def by argo qed also have "… = card (S x) * prod (card ∘ S) I" using ih by simp also have "… = prod (card ∘ S) ({x} ∪ I)" using i.hyps by auto finally show ?case by simp qed subsection "Complementary family of subgroups" text ‹The notion of a complementary family is introduced. Note that the subgroups are complementary not only to the other subgroups but to the product of the other subgroups.› definition (in group) compl_fam :: "('c ⇒ 'a set) ⇒ 'c set ⇒ bool" where "compl_fam S I = (∀i ∈ I. complementary (S i) (IDirProds G S (I - {i})))" text ‹Some lemmas about ‹compl_fam›.› lemma (in group) compl_fam_empty[simp]: "compl_fam S {}" unfolding compl_fam_def by simp lemma (in group) compl_fam_cong: assumes "compl_fam (f ∘ g) A" "inj_on g A" shows "compl_fam f (g ` A)" proof - have "((f ∘ g) ` (A - {i})) = (f ` (g ` A - {g i}))" if "i ∈ A" for i using assms that unfolding inj_on_def comp_def by blast thus ?thesis using assms unfolding compl_fam_def IDirProds_def complementary_def by simp qed text ‹We now connect ‹compl_fam› with ‹generate› as this will be its main application.› lemma (in comm_group) compl_fam_imp_generate_inj: assumes "gs ⊆ carrier G" "compl_fam (λg. generate G {g}) gs" shows "inj_on (λg. generate G {g}) gs" proof(rule, rule ccontr) fix x y assume xy: "x ∈ gs" "y ∈ gs" "x ≠ y" have gen: "generate G (⋃g∈gs - {y}. generate G {g}) = generate G (gs - {y})" by (intro generate_idem_Un, use assms in blast) assume g: "generate G {x} = generate G {y}" with xy have "generate G {y} ⊆ generate G (gs - {y})" using mono_generate[of "{x}" "gs - {y}"] by auto with xy have gyo: "generate G {y} = {𝟭}" using assms(2) generate.one gen unfolding compl_fam_def complementary_def IDirProds_def by blast hence yo: "y = 𝟭" using generate_singleton_one by simp from gyo g generate_singleton_one have xo: "x = 𝟭" by simp from xy yo xo show False by blast qed lemma (in comm_group) compl_fam_generate_subset: assumes "compl_fam (λg. generate G {g}) gs" "gs ⊆ carrier G" "A ⊆ gs" shows "compl_fam (λg. generate G {g}) A" proof(unfold compl_fam_def complementary_def IDirProds_def, subst generate_idem_Un) show "⋀i. A - {i} ⊆ carrier G" using assms by blast have "generate G {i} ∩ generate G (A - {i}) = {𝟭}" if "i ∈ A" for i proof - have "𝟭 ∈ generate G {i} ∩ generate G (A - {i})" using generate.one by blast moreover have "generate G (A - {i}) ⊆ generate G (gs - {i})" by (intro mono_generate, use assms in fast) moreover have "generate G {i} ∩ generate G (gs - {i}) = {𝟭}" using assms that generate_idem_Un[of "gs - {i}"] unfolding compl_fam_def IDirProds_def complementary_def by blast ultimately show ?thesis by blast qed thus "∀i∈A. generate G {i} ∩ generate G (A - {i}) = {𝟭}" by auto qed subsection ‹‹is_idirprod›› text ‹In order to identify a group as the internal direct product of a family of subgroups, they all have to be normal subgroups, complementary to the product of the rest of the subgroups and generate all of the group - this is captured in the definition of ‹is_idirprod›.› definition (in group) is_idirprod :: "'a set ⇒ ('c ⇒ 'a set) ⇒ 'c set ⇒ bool" where "is_idirprod A S I = ((∀i ∈ I. S i ⊲ G) ∧ A = IDirProds G S I ∧ compl_fam S I)" text ‹Very basic lemmas about ‹is_idirprod›.› lemma (in comm_group) is_idirprod_subgroup_suffices: assumes "A = IDirProds G S I" "∀i∈I. subgroup (S i) G" "compl_fam S I" shows "is_idirprod A S I" unfolding is_idirprod_def using assms subgroup_imp_normal by blast lemma (in comm_group) is_idirprod_generate: assumes "A = generate G gs" "gs ⊆ carrier G" "compl_fam (λg. generate G {g}) gs" shows "is_idirprod A (λg. generate G {g}) gs" proof(intro is_idirprod_subgroup_suffices) show "A = IDirProds G (λg. generate G {g}) gs" using assms generate_idem_Un[OF assms(2)] unfolding IDirProds_def by argo show "∀i∈gs. subgroup (generate G {i}) G" using assms generate_is_subgroup by auto show "compl_fam (λg. generate G {g}) gs" by fact qed lemma (in comm_group) is_idirprod_imp_compl_fam[simp]: assumes "is_idirprod A S I" shows "compl_fam S I" using assms unfolding is_idirprod_def by blast lemma (in comm_group) is_idirprod_generate_imp_generate[simp]: assumes "is_idirprod A (λg. generate G {g}) gs" shows "A = generate G gs" proof - have "gs ⊆ carrier G" proof show "g ∈ carrier G" if "g ∈ gs" for g proof - interpret g: subgroup "generate G {g}" G using assms that normal_imp_subgroup unfolding is_idirprod_def by blast show ?thesis using g.subset generate.incl by fast qed qed thus ?thesis using assms generate_idem_Un unfolding is_idirprod_def IDirProds_def by presburger qed end

# Theory Finite_Product_Extend

(* File: Finite_Product_Extend.thy Author: Joseph Thommes, TU München; Manuel Eberl, TU München *) section ‹Finite Product› theory Finite_Product_Extend imports IDirProds begin text ‹In this section, some general facts about ‹finprod› as well as some tailored for the rest of this entry are proven.› text ‹It is often needed to split a product in a single factor and the rest. Thus these two lemmas.› lemma (in comm_group) finprod_minus: assumes "a ∈ A" "f ∈ A → carrier G" "finite A" shows "finprod G f A = f a ⊗ finprod G f (A - {a})" proof - from assms have "A = insert a (A - {a})" by blast then have "finprod G f A = finprod G f (insert a (A - {a}))" by simp also have "… = f a ⊗ finprod G f (A - {a})" using assms by (intro finprod_insert, auto) finally show ?thesis . qed lemma (in comm_group) finprod_minus_symm: assumes "a ∈ A" "f ∈ A → carrier G" "finite A" shows "finprod G f A = finprod G f (A - {a}) ⊗ f a" proof - from assms have "A = insert a (A - {a})" by blast then have "finprod G f A = finprod G f (insert a (A - {a}))" by simp also have "… = f a ⊗ finprod G f (A - {a})" using assms by (intro finprod_insert, auto) also have "… = finprod G f (A - {a}) ⊗ f a" by (intro m_comm, use assms in blast, intro finprod_closed, use assms in blast) finally show ?thesis . qed text ‹This makes it very easy to show the following trivial fact.› lemma (in comm_group) finprod_singleton: assumes "f x ∈ carrier G" "finprod G f {x} = a" shows "f x = a" proof - have "finprod G f {x} = f x ⊗ finprod G f {}" using finprod_minus[of x "{x}" f] assms by auto thus ?thesis using assms by simp qed text ‹The finite product is consistent and closed concerning subgroups.› lemma (in comm_group) finprod_subgroup: assumes "f ∈ S → H" "subgroup H G" shows "finprod G f S = finprod (G⦇carrier := H⦈) f S" proof (cases "finite S") case True interpret H: comm_group "G⦇carrier := H⦈" using subgroup_is_comm_group[OF assms(2)] . show ?thesis using True assms proof (induction S rule: finite_induct) case empty then show ?case using finprod_empty H.finprod_empty by simp next case i: (insert x F) then have "finprod G f F = finprod (G⦇carrier := H⦈) f F" by blast moreover have "finprod G f (insert x F) = f x ⊗ finprod G f F" proof(intro finprod_insert[OF i(1, 2), of f]) show "f ∈ F → carrier G" "f x ∈ carrier G" using i(4) subgroup.subset[OF i(5)] by blast+ qed ultimately have "finprod G f (insert x F) = f x ⊗⇘_{G⦇carrier := H⦈}⇙ finprod (G⦇carrier := H⦈) f F" by auto moreover have "finprod (G⦇carrier := H⦈) f (insert x F) = …" proof(intro H.finprod_insert[OF i(1, 2)]) show "f ∈ F → carrier (G⦇carrier := H⦈)" "f x ∈ carrier (G⦇carrier := H⦈)" using i(4) by auto qed ultimately show ?case by simp qed next case False then show ?thesis unfolding finprod_def by simp qed lemma (in comm_group) finprod_closed_subgroup: assumes "subgroup H G" "f ∈ A → H" shows "finprod G f A ∈ H" using assms(2) proof (induct A rule: infinite_finite_induct) case (infinite A) then show ?case using subgroup.one_closed[OF assms(1)] by auto next case empty then show ?case using subgroup.one_closed[OF assms(1)] by auto next case i: (insert x F) from finprod_insert[OF i(1, 2), of f] i have fi: "finprod G f (insert x F) = f x ⊗ finprod G f F" using subgroup.subset[OF assms(1)] by blast from i have "finprod G f F ∈ H" "f x ∈ H" by blast+ with fi show ?case using subgroup.m_closed[OF assms(1)] by presburger qed text ‹It also does not matter if we exponentiate all elements taking part in the product or the result of the product.› lemma (in comm_group) finprod_exp: assumes "A ⊆ carrier G" "f ∈ A → carrier G" shows "(finprod G f A) [^] (k::int) = finprod G ((λa. a [^] k) ∘ f) A" using assms proof(induction A rule: infinite_finite_induct) case i: (insert x F) hence ih: "finprod G f F [^] k = finprod G ((λa. a [^] k) ∘ f) F" by blast have fpc: "finprod G f F ∈ carrier G" by (intro finprod_closed, use i in auto) have fxc: "f x ∈ carrier G" using i by auto have "finprod G f (insert x F) = f x ⊗ finprod G f F" by (intro finprod_insert, use i in auto) hence "finprod G f (insert x F) [^] k = (f x ⊗ finprod G f F) [^] k" by simp also have "… = f x [^] k ⊗ finprod G f F [^] k" using fpc fxc int_pow_distrib by blast also have "… = ((λa. a [^] k) ∘ f) x ⊗ finprod G ((λa. a [^] k) ∘ f) F" using ih by simp also have "… = finprod G ((λa. a [^] k) ∘ f) (insert x F)" by (intro finprod_insert[symmetric], use i in auto) finally show ?case . qed auto text ‹Some lemmas concerning different combinations of functions in the usage of ‹finprod›.› lemma (in comm_group) finprod_cong_split: assumes "⋀a. a ∈ A ⟹ f a ⊗ g a = h a" and "f ∈ A → carrier G" "g ∈ A → carrier G" "h ∈ A → carrier G" shows "finprod G h A = finprod G f A ⊗ finprod G g A" using assms proof(induct A rule: infinite_finite_induct) case (infinite A) then show ?case by simp next case empty then show ?case by simp next case i: (insert x F) then have iH: "finprod G h F = finprod G f F ⊗ finprod G g F" by fast have f: "finprod G f (insert x F) = f x ⊗ finprod G f F" by (intro finprod_insert[OF i(1, 2), of f]; use i(5) in simp) have g: "finprod G g (insert x F) = g x ⊗ finprod G g F" by (intro finprod_insert[OF i(1, 2), of g]; use i(6) in simp) have h: "finprod G h (insert x F) = h x ⊗ finprod G h F" by (intro finprod_insert[OF i(1, 2), of h]; use i(7) in simp) also have "… = h x ⊗ (finprod G f F ⊗ finprod G g F)" using iH by argo also have "… = f x ⊗ g x ⊗ (finprod G f F ⊗ finprod G g F)" using i(4) by simp also have "… = f x ⊗ finprod G f F ⊗ (g x ⊗ finprod G g F)" using m_comm m_assoc i(5-7) by simp also have "… = finprod G f (insert x F) ⊗ finprod G g (insert x F)" using f g by argo finally show ?case . qed lemma (in comm_group) finprod_comp: assumes "inj_on g A" "(f ∘ g) ` A ⊆ carrier G" shows "finprod G f (g ` A) = finprod G (f ∘ g) A" using finprod_reindex[OF _ assms(1), of f] using assms(2) unfolding comp_def by blast text ‹The subgroup generated by a set of generators (in an abelian group) is exactly the set of elements that can be written as a finite product using only powers of these elements.› lemma (in comm_group) generate_eq_finprod_PiE_image: assumes "finite gs" "gs ⊆ carrier G" shows "generate G gs = (λx. finprod G x gs) ` Pi⇩_{E}gs (λa. generate G {a})" (is "?g = ?fp") proof show "?g ⊆ ?fp" proof fix x assume x: "x ∈ ?g" thus "x ∈ ?fp" proof (induction rule: generate.induct) case one show ?case proof let ?r = "restrict (λ_. 𝟭) gs" show "?r ∈ (Π⇩_{E}a∈gs. generate G {a})" using generate.one by auto show "𝟭 = finprod G ?r gs" by(intro finprod_one_eqI[symmetric], simp) qed next case g: (incl g) show ?case proof let ?r = "restrict ((λ_. 𝟭)(g := g)) gs" show "?r ∈ (Π⇩_{E}a∈gs. generate G {a})" using generate.one generate.incl[of g "{g}" G] by fastforce show "g = finprod G ?r gs" proof - have "finprod G ?r gs = ?r g ⊗ finprod G ?r (gs - {g})" by (intro finprod_minus, use assms g in auto) moreover have "?r g = g" using g by simp moreover have "finprod G ?r (gs - {g}) = 𝟭" by(rule finprod_one_eqI; use g in simp) ultimately show ?thesis using assms g by auto qed qed next case g: (inv g) show ?case proof let ?r = "restrict ((λ_. 𝟭)(g := inv g)) gs" show "?r ∈ (Π⇩_{E}a∈gs. generate G {a})" using generate.one generate.inv[of g "{g}" G] by fastforce show "inv g = finprod G ?r gs" proof - have "finprod G ?r gs = ?r g ⊗ finprod G ?r (gs - {g})" by (intro finprod_minus, use assms g in auto) moreover have "?r g = inv g" using g by simp moreover have "finprod G ?r (gs - {g}) = 𝟭" by(rule finprod_one_eqI; use g in simp) ultimately show ?thesis using assms g by auto qed qed next case gh: (eng g h) from gh obtain i where i: "i ∈ (Π⇩_{E}a∈gs. generate G {a})" "g = finprod G i gs" by blast from gh obtain j where j: "j ∈ (Π⇩_{E}a∈gs. generate G {a})" "h = finprod G j gs" by blast from i j have "g ⊗ h = finprod G i gs ⊗ finprod G j gs" by blast also have "… = finprod G (λa. i a ⊗ j a) gs" proof(intro finprod_multf[symmetric]; rule) fix x assume x: "x ∈ gs" have "i x ∈ generate G {x}" "j x ∈ generate G {x}"using i(1) j(1) x by blast+ thus "i x ∈ carrier G" "j x ∈ carrier G" using generate_incl[of "{x}"] x assms(2) by blast+ qed also have "… = finprod G (restrict (λa. i a ⊗ j a) gs) gs" proof(intro finprod_cong) have ip: "i g ∈ generate G {g}" if "g ∈ gs" for g using i that by auto have jp: "j g ∈ generate G {g}" if "g ∈ gs" for g using j that by auto have "i g ⊗ j g ∈ generate G {g}" if "g ∈ gs" for g using generate.eng[OF ip[OF that] jp[OF that]] . thus "((λa. i a ⊗ j a) ∈ gs → carrier G) = True" using generate_incl assms(2) by blast qed auto finally have "g ⊗ h = finprod G (restrict (λa. i a ⊗ j a) gs) gs" . moreover have "(restrict (λa. i a ⊗ j a) gs) ∈ (Π⇩_{E}a∈gs. generate G {a})" proof - have ip: "i g ∈ generate G {g}" if "g ∈ gs" for g using i that by auto have jp: "j g ∈ generate G {g}" if "g ∈ gs" for g using j that by auto have "i g ⊗ j g ∈ generate G {g}" if "g ∈ gs" for g using generate.eng[OF ip[OF that] jp[OF that]] . thus ?thesis by auto qed ultimately show ?case using i j by blast qed qed show "?fp ⊆ ?g" proof fix x assume x: "x ∈ ?fp" then obtain f where f: "f ∈ (Pi⇩_{E}gs (λa. generate G {a}))" "x = finprod G f gs" by blast have sg: "subgroup ?g G" by(intro generate_is_subgroup, fact) have "finprod G f gs ∈ ?g" proof(intro finprod_closed_subgroup[OF sg]) have "f g ∈ generate G gs" if "g ∈ gs" for g proof - have "f g ∈ generate G {g}" using f(1) that by auto moreover have "generate G {g} ⊆ generate G gs" by(intro mono_generate, use that in simp) ultimately show ?thesis by fast qed thus "f ∈ gs → generate G gs" by simp qed thus "x ∈ ?g" using f by blast qed qed lemma (in comm_group) generate_eq_finprod_Pi_image: assumes "finite gs" "gs ⊆ carrier G" shows "generate G gs = (λx. finprod G x gs) ` Pi gs (λa. generate G {a})" (is "?g = ?fp") proof - have "(λx. finprod G x gs) ` Pi⇩_{E}gs (λa. generate G {a}) = (λx. finprod G x gs) ` Pi gs (λa. generate G {a})" proof have "Pi⇩_{E}gs (λa. generate G {a}) ⊆ Pi gs (λa. generate G {a})" by blast thus "(λx. finprod G x gs) ` Pi⇩_{E}gs (λa. generate G {a}) ⊆ (λx. finprod G x gs) ` Pi gs (λa. generate G {a})" by blast show "(λx. finprod G x gs) ` Pi gs (λa. generate G {a}) ⊆ (λx. finprod G x gs) ` Pi⇩_{E}gs (λa. generate G {a})" proof fix x assume x: "x ∈ (λx. finprod G x gs) ` Pi gs (λa. generate G {a})" then obtain f where f: "x = finprod G f gs" "f ∈ Pi gs (λa. generate G {a})" by blast moreover have "finprod G f gs = finprod G (restrict f gs) gs" proof(intro finprod_cong) have "f g ∈ carrier G" if "g ∈ gs" for g using that f(2) mono_generate[of "{g}" gs] generate_incl[OF assms(2)] by fast thus "(f ∈ gs → carrier G) = True" by blast qed auto moreover have "restrict f gs ∈ Pi⇩_{E}gs (λa. generate G {a})" using f(2) by simp ultimately show "x ∈ (λx. finprod G x gs) ` Pi⇩_{E}gs (λa. generate G {a})" by blast qed qed with generate_eq_finprod_PiE_image[OF assms] show ?thesis by auto qed lemma (in comm_group) generate_eq_finprod_Pi_int_image: assumes "finite gs" "gs ⊆ carrier G" shows "generate G gs = (λx. finprod G (λg. g [^] x g) gs) ` Pi gs (λ_. (UNIV::int set))" proof - from generate_eq_finprod_Pi_image[OF assms] have "generate G gs = (λx. finprod G x gs) ` (Π a∈gs. generate G {a})" . also have "… = (λx. finprod G (λg. g [^] x g) gs) ` Pi gs (λ_. (UNIV::int set))" proof(rule; rule) fix x assume x: "x ∈ (λx. finprod G x gs) ` (Π a∈gs. generate G {a})" then obtain f where f: "f ∈ (Π a∈gs. generate G {a})" "x = finprod G f gs" by blast hence "∃k::int. f a = a [^] k" if "a ∈ gs" for a using generate_pow[of a] that assms(2) by blast hence "∃(h::'a ⇒ int). ∀a∈gs. f a = a [^] h a" by meson then obtain h where h: "∀a∈gs. f a = a [^] h a" "h ∈ gs → (UNIV :: int set)" by auto have "finprod G (λg. g [^] h g) gs = finprod G f gs" by (intro finprod_cong, use int_pow_closed h assms(2) in auto) with f have "x = finprod G (λg. g [^] h g) gs" by argo with h(2) show "x ∈ (λx. finprod G (λg. g [^] x g) gs) ` (gs → (UNIV::int set))" by auto next fix x assume x: "x ∈ (λx. finprod G (λg. g [^] x g) gs) ` (gs → (UNIV::int set))" then obtain h where h: "x = finprod G (λg. g [^] h g) gs" "h ∈ gs → (UNIV :: int set)" by blast hence "∃k∈generate G {a}. a [^] h a = k" if "a ∈ gs" for a using generate_pow[of a] that assms(2) by blast then obtain f where f: "∀a∈gs. a [^] h a = f a" "f ∈ (Π a∈gs. generate G {a})" by fast have "finprod G f gs = finprod G (λg. g [^] h g) gs" proof(intro finprod_cong) have "f a ∈ carrier G" if "a ∈ gs" for a using generate_incl[of "{a}"] assms(2) that f(2) by fast thus "(f ∈ gs → carrier G) = True" by blast qed (use f in auto) with h have "x = finprod G f gs" by argo with f(2) show "x ∈ (λx. finprod G x gs) ` (Π a∈gs. generate G {a})" by blast qed finally show ?thesis . qed lemma (in comm_group) IDirProds_eq_finprod_PiE: assumes "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G" shows "IDirProds G S I = (λx. finprod G x I) ` (Pi⇩_{E}I S)" (is "?DP = ?fp") proof show "?fp ⊆ ?DP" proof fix x assume x: "x ∈ ?fp" then obtain f where f: "f ∈ (Pi⇩_{E}I S)" "x = finprod G f I" by blast have sDP: "subgroup ?DP G" by (intro IDirProds_is_subgroup; use subgroup.subset[OF assms(2)] in blast) have "finprod G f I ∈ ?DP" proof(intro finprod_closed_subgroup[OF sDP]) have "f i ∈ IDirProds G S I" if "i ∈ I" for i proof show "f i ∈ (S i)" using f(1) that by auto show "(S i) ⊆ IDirProds G S I" by (intro IDirProds_incl[OF that]) qed thus "f ∈ I → IDirProds G S I" by simp qed thus "x ∈ ?DP" using f by blast qed show "?DP ⊆ ?fp" proof(unfold IDirProds_def; rule subsetI) fix x assume x: "x ∈ generate G (⋃(S ` I))" thus "x ∈ ?fp" using assms proof (induction rule: generate.induct) case one define g where g: "g = (λx. if x ∈ I then 𝟭 else undefined)" then have "g ∈ Pi⇩_{E}I S" using subgroup.one_closed[OF one(2)] by auto moreover have "finprod G g I = 𝟭" by (intro finprod_one_eqI; use g in simp) ultimately show ?case unfolding image_def by (auto; metis) next case i: (incl h) from i obtain j where j: "j ∈ I" "h ∈ (S j)" by blast define hf where "hf = (λx. (if x ∈ I then 𝟭 else undefined))(j := h)" with j have "hf ∈ Pi⇩_{E}I S" using subgroup.one_closed[OF i(3)] by force moreover have "finprod G hf I = h" proof - have "finprod G hf I = hf j ⊗ finprod G hf (I - {j})" by (intro finprod_minus, use assms hf_def subgroup.subset[OF i(3)[OF j(1)]] j in auto) moreover have "hf j = h" using hf_def by simp moreover have "finprod G hf (I - {j}) = 𝟭" by (rule finprod_one_eqI; use hf_def in simp) ultimately show ?thesis using subgroup.subset[OF i(3)[OF j(1)]] j(2) by auto qed ultimately show ?case unfolding image_def by (auto; metis) next case i: (inv h) from i obtain j where j: "j ∈ I" "h ∈ (S j)" by blast have ih: "inv h ∈ (S j)" using subgroup.m_inv_closed[OF i(3)[OF j(1)] j(2)] . define hf where "hf = (λx. (if x ∈ I then 𝟭 else undefined))(j := inv h)" with j ih have "hf ∈ Pi⇩_{E}I S" using subgroup.one_closed[OF i(3)] by force moreover have "finprod G hf I = inv h" proof - have "finprod G hf I = hf j ⊗ finprod G hf (I - {j})" by (intro finprod_minus, use assms hf_def subgroup.subset[OF i(3)[OF j(1)]] j in auto) moreover have "hf j = inv h" using hf_def by simp moreover have "finprod G hf (I - {j}) = 𝟭" by (rule finprod_one_eqI; use hf_def in simp) ultimately show ?thesis using subgroup.subset[OF i(3)[OF j(1)]] j(2) by auto qed ultimately show ?case unfolding image_def by (auto; metis) next case e: (eng a b) from e obtain f where f: "f ∈ Pi⇩_{E}I S" "a = finprod G f I" by blast from e obtain g where g: "g ∈ Pi⇩_{E}I S" "b = finprod G g I" by blast from f g have "a ⊗ b = finprod G f I ⊗ finprod G g I" by blast also have "… = finprod G (λa. f a ⊗ g a) I" proof(intro finprod_multf[symmetric]) have "⋃(S ` I) ⊆ carrier G" using subgroup.subset[OF e(6)] by blast thus "f ∈ I → carrier G" "g ∈ I → carrier G" using f(1) g(1) unfolding PiE_def Pi_def by auto qed also have "… = finprod G (restrict (λa. f a ⊗ g a) I) I" proof(intro finprod_cong) show "I = I" by simp show "⋀i. i ∈ I =simp=> f i ⊗ g i = (λa∈I. f a ⊗ g a) i" by simp have fp: "f i ∈ (S i)" if "i ∈ I" for i using f that by auto have gp: "g i ∈ (S i)" if "i ∈ I" for i using g that by auto have "f i ⊗ g i ∈ (S i)" if "i ∈ I" for i using subgroup.m_closed[OF e(6)[OF that] fp[OF that] gp[OF that]] . thus "((λa. f a ⊗ g a) ∈ I → carrier G) = True" using subgroup.subset[OF e(6)] by auto qed finally have "a ⊗ b = finprod G (restrict (λa. f a ⊗ g a) I) I" . moreover have "(restrict (λa. f a ⊗ g a) I) ∈ Pi⇩_{E}I S" proof - have fp: "f i ∈ (S i)" if "i ∈ I" for i using f that by auto have gp: "g i ∈ (S i)" if "i ∈ I" for i using g that by auto have "f i ⊗ g i ∈ (S i)" if "i ∈ I" for i using subgroup.m_closed[OF e(6)[OF that] fp[OF that] gp[OF that]] . thus ?thesis by auto qed ultimately show ?case using f g by blast qed qed qed lemma (in comm_group) IDirProds_eq_finprod_Pi: assumes "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G" shows "IDirProds G S I = (λx. finprod G x I) ` (Pi I S)" (is "?DP = ?fp") proof - have "(λx. finprod G x I) ` (Pi I S) = (λx. finprod G x I) ` (Pi⇩_{E}I S)" proof have "Pi⇩_{E}I S ⊆ Pi I S" by blast thus "(λx. finprod G x I) ` Pi⇩_{E}I S ⊆ (λx. finprod G x I) ` Pi I S" by blast show "(λx. finprod G x I) ` Pi I S ⊆ (λx. finprod G x I) ` Pi⇩_{E}I S" proof fix x assume x: "x ∈ (λx. finprod G x I) ` Pi I S" then obtain f where f: "x = finprod G f I" "f ∈ Pi I S" by blast moreover have "finprod G f I = finprod G (restrict f I) I" by (intro finprod_cong; use f(2) subgroup.subset[OF assms(2)] in fastforce) moreover have "restrict f I ∈ Pi⇩_{E}I S" using f(2) by simp ultimately show "x ∈ (λx. finprod G x I) ` Pi⇩_{E}I S" by blast qed qed with IDirProds_eq_finprod_PiE[OF assms] show ?thesis by auto qed text ‹If we switch one element from a set of generators, the generated set stays the same if both elements can be generated from the others together with the switched element respectively.› lemma (in comm_group) generate_one_switched_exp_eqI: assumes "A ⊆ carrier G" "a ∈ A" "B = (A - {a}) ∪ {b}" and "f ∈ A → (UNIV::int set)" "g ∈ B → (UNIV::int set)" and "a = finprod G (λx. x [^] g x) B" "b = finprod G (λx. x [^] f x) A" shows "generate G A = generate G B" proof(intro generate_one_switched_eqI[OF assms(1, 2, 3)]; cases "finite A") case True hence fB: "finite B" using assms(3) by blast have cB: "B ⊆ carrier G" proof - have "b ∈ carrier G" by (subst assms(7), intro finprod_closed, use assms(1, 4) int_pow_closed in fast) thus ?thesis using assms(1, 3) by blast qed show "a ∈ generate G B" proof(subst generate_eq_finprod_Pi_image[OF fB cB], rule) show "a = finprod G (λx. x [^] g x) B" by fact have "x [^] g x ∈ generate G {x}" if "x ∈ B" for x using generate_pow[of x] cB that by blast thus "(λx. x [^] g x) ∈ (Π a∈B. generate G {a})" unfolding Pi_def by blast qed show "b ∈ generate G A" proof(subst generate_eq_finprod_Pi_image[OF True assms(1)], rule) show "b = finprod G (λx. x [^] f x) A" by fact have "x [^] f x ∈ generate G {x}" if "x ∈ A" for x using generate_pow[of x] assms(1) that by blast thus "(λx. x [^] f x) ∈ (Π a∈A. generate G {a})" unfolding Pi_def by blast qed next case False hence b: "b = 𝟭" using assms(7) unfolding finprod_def by simp from False assms(3) have "infinite B" by simp hence a: "a = 𝟭" using assms(6) unfolding finprod_def by simp show "a ∈ generate G B" using generate.one a by blast show "b ∈ generate G A" using generate.one b by blast qed text ‹We can characterize a complementary family of subgroups when the only way to form the neutral element as a product of picked elements from each subgroup is to pick the neutral element from each subgroup.› lemma (in comm_group) compl_fam_imp_triv_finprod: assumes "compl_fam S I" "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G" and "finprod G f I = 𝟭" "f ∈ Pi I S" shows "∀i∈I. f i = 𝟭" proof (rule ccontr; clarify) from assms(5) have f: "f i ∈ (S i)" if "i ∈ I" for i using that by fastforce fix i assume i: "i ∈ I" have si: "subgroup (S i) G" using assms(3)[OF i] . consider (triv) "(S i) = {𝟭}" | (not_triv) "(S i) ≠ {𝟭}" by blast thus "f i = 𝟭" proof (cases) case triv then show ?thesis using f[OF i] by blast next case not_triv show ?thesis proof (rule ccontr) have fc: "f i ∈ carrier G" using f[OF i] subgroup.subset[OF si] by blast assume no: "f i ≠ 𝟭" have fH: "f i ∈ (S i)" using f[OF i] . from subgroup.m_inv_closed[OF si this] have ifi: "inv (f i) ∈ (S i)" . moreover have "inv (f i) ≠ 𝟭" using no fc by simp moreover have "inv (f i) = finprod G f (I - {i})" proof - have "𝟭 = finprod G f I" using assms(4) by simp also have "… = finprod G f (insert i (I - {i}))" proof - have "I = insert i (I - {i})" using i by fast thus ?thesis by simp qed also have "… = f i ⊗ finprod G f (I - {i})" proof(intro finprod_insert) show "finite (I - {i})" using assms(2) by blast show "i ∉ I - {i}" by blast show "f ∈ I - {i} → carrier G" using assms(3) f subgroup.subset by blast show "f i ∈ carrier G" by fact qed finally have o: "𝟭 = f i ⊗ finprod G f (I - {i})" . show ?thesis proof(intro inv_equality) show "f i ∈ carrier G" by fact show "finprod G f (I - {i}) ∈ carrier G" by (intro finprod_closed; use assms(3) f subgroup.subset in blast) from m_comm[OF this fc] o show "finprod G f (I - {i}) ⊗ f i = 𝟭" by simp qed qed moreover have "finprod G f (I - {i}) ∈ IDirProds G S (I - {i})" proof (intro finprod_closed_subgroup IDirProds_is_subgroup) show "⋃ (S ` (I - {i})) ⊆ carrier G" using assms(3) subgroup.subset by auto have "f j ∈ (IDirProds G S (I - {i}))" if "j ∈ (I - {i})" for j using IDirProds_incl[OF that] f that by blast thus "f ∈ I - {i} → IDirProds G S (I - {i})" by blast qed ultimately have "¬complementary (S i) (IDirProds G S (I - {i}))" unfolding complementary_def by auto thus False using assms(1) i unfolding compl_fam_def by blast qed qed qed lemma (in comm_group) triv_finprod_imp_compl_fam: assumes "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G" and "∀f ∈ Pi I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭)" shows "compl_fam S I" proof (unfold compl_fam_def; rule) fix k assume k: "k ∈ I" let ?DP = "IDirProds G S (I - {k})" show "complementary (S k) ?DP" proof (rule ccontr; unfold complementary_def) have sk: "subgroup (S k) G" using assms(2)[OF k] . have sDP: "subgroup ?DP G" by (intro IDirProds_is_subgroup; use subgroup.subset[OF assms(2)] in blast) assume a: "(S k) ∩ IDirProds G S (I - {k}) ≠ {𝟭}" then obtain x where x: "x ∈ (S k)" "x ∈ IDirProds G S (I - {k})" "x ≠ 𝟭" using subgroup.one_closed sk sDP by blast then have "x ∈ (λx. finprod G x (I - {k})) ` (Pi (I - {k}) S)" using IDirProds_eq_finprod_Pi[of "(I - {k})"] assms(1, 2) by blast then obtain ht where ht: "finprod G ht (I - {k}) = x" "ht ∈ Pi (I - {k}) S" by blast define h where h: "h = (ht(k := inv x))" then have hPi: "h ∈ Pi I S" using ht subgroup.m_inv_closed[OF assms(2)[OF k] x(1)] by auto have "finprod G h (I - {k}) = x" proof (subst ht(1)[symmetric], intro finprod_cong) show "I - {k} = I - {k}" by simp show "(h ∈ I - {k} → carrier G) = True" using h ht(2) subgroup.subset[OF assms(2)] unfolding Pi_def id_def by auto show "⋀i. i ∈ I - {k} =simp=> h i = ht i" using ht(2) h by simp qed moreover have "finprod G h I = h k ⊗ finprod G h (I - {k})" by (intro finprod_minus; use k assms hPi subgroup.subset[OF assms(2)] Pi_def in blast) ultimately have "finprod G h I = inv x ⊗ x" using h by simp then have "finprod G h I = 𝟭" using subgroup.subset[OF sk] x(1) by auto moreover have "h k ≠ 𝟭" using h x(3) subgroup.subset[OF sk] x(1) by force ultimately show False using assms(3) k hPi by blast qed qed lemma (in comm_group) triv_finprod_iff_compl_fam_Pi: assumes "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G" shows "compl_fam S I ⟷ (∀f ∈ Pi I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭))" using compl_fam_imp_triv_finprod triv_finprod_imp_compl_fam assms by blast lemma (in comm_group) triv_finprod_iff_compl_fam_PiE: assumes "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G" shows "compl_fam S I ⟷ (∀f ∈ Pi⇩_{E}I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭))" proof show "compl_fam S I ⟹ ∀f∈Pi⇩_{E}I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭)" using triv_finprod_iff_compl_fam_Pi[OF assms] by auto have "∀f∈Pi⇩_{E}I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭) ⟹ ∀f∈Pi I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭)" proof(rule+) fix f i assume f: "f ∈ Pi I S" "finprod G f I = 𝟭" and i: "i ∈ I" assume allf: "∀f∈Pi⇩_{E}I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭)" have "f i = restrict f I i" using i by simp moreover have "finprod G (restrict f I) I = finprod G f I" using f subgroup.subset[OF assms(2)] unfolding Pi_def by (intro finprod_cong; auto) moreover have "restrict f I ∈ Pi⇩_{E}I S" using f by simp ultimately show "f i = 𝟭" using allf f i by metis qed thus "∀f∈Pi⇩_{E}I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭) ⟹ compl_fam S I" using triv_finprod_iff_compl_fam_Pi[OF assms] by presburger qed text ‹The finite product also distributes when nested.› (* Manuel Eberl, TODO: move to library *) lemma (in comm_monoid) finprod_Sigma: assumes "finite A" "⋀x. x ∈ A ⟹ finite (B x)" assumes "⋀x y. x ∈ A ⟹ y ∈ B x ⟹ g x y ∈ carrier G" shows "(⨂x∈A. ⨂y∈B x. g x y) = (⨂z∈Sigma A B. case z of (x, y) ⇒ g x y)" using assms proof (induction A rule: finite_induct) case (insert x A) have "(⨂z∈Sigma (insert x A) B. case z of (x, y) ⇒ g x y) = (⨂z∈Pair x ` B x. case z of (x, y) ⇒ g x y) ⊗ (⨂z∈Sigma A B. case z of (x, y) ⇒ g x y)" unfolding Sigma_insert using insert.prems insert.hyps by (subst finprod_Un_disjoint) auto also have "(⨂z∈Sigma A B. case z of (x, y) ⇒ g x y) = (⨂x∈A. ⨂y∈B x. g x y)" using insert.prems insert.hyps by (subst insert.IH [symmetric]) auto also have "(⨂z∈Pair x ` B x. case z of (x, y) ⇒ g x y) = (⨂y∈B x. g x y)" using insert.prems insert.hyps by (subst finprod_reindex) (auto intro: inj_onI) finally show ?case using insert.hyps insert.prems by simp qed auto text ‹With the now proven facts, we are able to provide criterias to inductively construct a group that is the internal direct product of a set of generators.› (* belongs to IDirProd, but uses finprod stuff *) lemma (in comm_group) idirprod_generate_ind: assumes "finite gs" "gs ⊆ carrier G" "g ∈ carrier G" "is_idirprod (generate G gs) (λg. generate G {g}) gs" "complementary (generate G {g}) (generate G gs)" shows "is_idirprod (generate G (gs ∪ {g})) (λg. generate G {g}) (gs ∪ {g})" proof(cases "g ∈ gs") case True hence "gs = (gs ∪ {g})" by blast thus ?thesis using assms(4) by auto next case gngs: False show ?thesis proof (intro is_idirprod_subgroup_suffices) have gsgc: "gs ∪ {g} ⊆ carrier G" using assms(2, 3) by blast thus "generate G (gs ∪ {g}) = IDirProds G (λg. generate G {g}) (gs ∪ {g})" unfolding IDirProds_def using generate_idem_Un by presburger show "∀i∈gs ∪ {g}. subgroup (generate G {i}) G" using generate_is_subgroup gsgc by auto have sg: "subgroup (generate G {g}) G" by (intro generate_is_subgroup, use assms(3) in blast) from assms(4) is_idirprod_def have ih: "∀x. x ∈ gs ⟶ generate G {x} ⊲ G" "compl_fam (λg. generate G {g}) gs" by fastforce+ hence ca: "complementary (generate G {a}) (generate G (gs - {a}))" if "a ∈ gs" for a unfolding compl_fam_def IDirProds_def using gsgc generate_idem_Un[of "gs - {a}"] that by fastforce have aux: "gs ∪ {g} - {i} ⊆ carrier G" for i using gsgc by blast show "compl_fam (λg. generate G {g}) (gs ∪ {g})" proof(unfold compl_fam_def IDirProds_def, subst generate_idem_Un[OF aux], rule, rule ccontr) fix h assume h: "h ∈ gs ∪ {g}" assume c: "¬ complementary (generate G {h}) (generate G (gs ∪ {g} - {h}))" show "False" proof (cases "h = g") case True with c have "¬ complementary (generate G {g}) (generate G (gs - {g}))" by auto moreover have "complementary (generate G {g}) (generate G (gs - {g}))" by (rule subgroup_subset_complementary[OF generate_is_subgroup generate_is_subgroup[of gs] generate_is_subgroup mono_generate], use assms(2, 3, 5) in auto) ultimately show False by blast next case hng: False hence h: "h ∈ gs" "h ≠ g" using h by blast+ hence "gs ∪ {g} - {h} = gs - {h} ∪ {g}" by blast with c have c: "¬ complementary (generate G {h}) (generate G (gs - {h} ∪ {g}))" by argo then obtain k where k: "k ∈ generate G {h}" "k ∈ generate G (gs - {h} ∪ {g})" "k ≠ 𝟭" unfolding complementary_def using generate.one by blast with ca have kngh: "k ∉ generate G (gs - {h})" using h unfolding complementary_def by blast from k(2) generate_eq_finprod_PiE_image[of "gs - {h} ∪ {g}"] assms(1) gsgc obtain f where f: "k = finprod G f (gs - {h} ∪ {g})" "f ∈ (Π⇩_{E}a∈gs - {h} ∪ {g}. generate G {a})" by blast have fg: "f a ∈ generate G {a}" if "a ∈ (gs - {h} ∪ {g})" for a using that f(2) by blast have fc: "f a ∈ carrier G" if "a ∈ (gs - {h} ∪ {g})" for a proof - have "generate G {a} ⊆ carrier G" if "a ∈ (gs - {h} ∪ {g})" for a using that generate_incl[of "{a}"] gsgc by blast thus "f a ∈ carrier G" using that fg by auto qed have kp: "k = f g ⊗ finprod G f (gs - {h})" proof - have "(gs - {h} ∪ {g}) = insert g (gs - {h})" by fast moreover have "finprod G f (insert g (gs - {h})) = f g ⊗ finprod G f (gs - {h})" by (intro finprod_insert, use fc assms(1) gngs in auto) ultimately show ?thesis using f(1) by argo qed have fgsh: "finprod G f (gs - {h}) ∈ generate G (gs - {h})" proof(intro finprod_closed_subgroup[OF generate_is_subgroup]) show "gs - {h} ⊆ carrier G" using gsgc by blast have "f a ∈ generate G (gs - {h})" if "a ∈ (gs - {h})" for a using mono_generate[of "{a}" "gs - {h}"] fg that by blast thus "f ∈ gs - {h} → generate G (gs - {h})" by blast qed have "f g ⊗ finprod G f (gs - {h}) ∉ generate G gs" proof assume fpgs: "f g ⊗ finprod G f (gs - {h}) ∈ generate G gs" from fgsh have fgsgs: "finprod G f (gs - {h}) ∈ generate G gs" using mono_generate[of "gs - {h}" gs] by blast have fPi: "f ∈ (Π a∈(gs - {h}). generate G {a})" using f by blast have gI: "generate G (gs - {h}) = (λx. finprod G x (gs - {h})) ` (Π a∈gs - {h}. generate G {a})" using generate_eq_finprod_Pi_image[of "gs - {h}"] assms(1, 2) by blast have fgno: "f g ≠ 𝟭" proof (rule ccontr) assume o: "¬ f g ≠ 𝟭" hence kf: "k = finprod G f (gs - {h})" using kp finprod_closed fc by auto hence "k ∈ generate G (gs - {h})" using fPi gI by blast thus False using k ca h unfolding complementary_def by blast qed from fpgs have "f g ∈ generate G gs" using subgroup.mult_in_cancel_right[OF generate_is_subgroup[OF assms(2)] fc[of g] fgsgs] by blast with fgno assms(5) fg[of g] show "False" unfolding complementary_def by blast qed moreover have "k ∈ generate G gs" using k(1) mono_generate[of "{h}" gs] h(1) by blast ultimately show False using kp by blast qed qed qed qed end

# Theory Group_Hom

(* File: Group_Hom.thy Author: Joseph Thommes, TU München *) section ‹Group Homomorphisms› theory Group_Hom imports Set_Multiplication begin text ‹This section extends the already existing library about group homomorphisms in HOL-Algebra by some useful lemmas. These were mainly inspired by the needs that arised throughout the other proofs.› lemma (in group_hom) generate_hom: assumes "A ⊆ carrier G" shows "h ` (generate G A) = generate H (h ` A)" using assms group_hom.generate_img group_hom_axioms by blast text ‹For two elements with the same image we can find an element in the kernel that maps one of the two elements on the other by multiplication.› lemma (in group_hom) kernel_assoc_elem: assumes "x ∈ carrier G" "y ∈ carrier G" "h x = h y" obtains z where "x = y ⊗⇘_{G}⇙ z" "z ∈ kernel G H h" proof - have c: "inv y ⊗⇘_{G}⇙ x ∈ carrier G" using assms by simp then have e: "x = y ⊗⇘_{G}⇙ (inv y ⊗⇘_{G}⇙ x)" using assms G.m_assoc using G.inv_solve_left by blast then have "h x = h (y ⊗⇘_{G}⇙ (inv y ⊗⇘_{G}⇙ x))" by simp then have "h x = h y ⊗⇘_{H}⇙ h (inv y ⊗⇘_{G}⇙ x)" using c assms by simp then have "𝟭⇘_{H}⇙ = h (inv y ⊗⇘_{G}⇙ x)" using assms by simp then have "(inv y ⊗⇘_{G}⇙ x) ∈ kernel G H h" unfolding kernel_def using c by simp thus ?thesis using e that by blast qed text ‹This can then be used to characterize the pre-image of a set $A$ under homomorphism as a product of $A$ itself with the kernel of the homomorphism.› lemma (in group_hom) vimage_eq_set_mult_kern_right: assumes "A ⊆ carrier G" shows "{x ∈ carrier G. h x ∈ h ` A} = A <#> kernel G H h" proof(intro equalityI subsetI) fix x assume assm: "x ∈ A <#> kernel G H h" then have xc: "x ∈ carrier G" unfolding kernel_def set_mult_def using assms by blast from assm obtain a b where ab: "a ∈ A" "b ∈ kernel G H h" "x = a ⊗⇘_{G}⇙ b" unfolding set_mult_def by blast then have abc: "a ∈ carrier G" "b ∈ carrier G" unfolding kernel_def using assms by auto from ab have "h x = h (a ⊗⇘_{G}⇙ b)" by blast also have "… = h a ⊗⇘_{H}⇙ h b" using abc by simp also have "… = h a ⊗⇘_{H}⇙ 𝟭⇘_{H}⇙" using ab(2) unfolding kernel_def by simp also have "… = h a" using abc by simp also have "… ∈ h ` A" using ab by blast finally have "h x ∈ h ` A" . thus "x ∈ {x ∈ carrier G. h x ∈ h ` A}" using xc by blast next fix x assume "x ∈ {x ∈ carrier G. h x ∈ h ` A}" then have x: "x ∈ carrier G" "h x ∈ h ` A" by simp+ then obtain y where y: "y ∈ A" "h x = h y" "y ∈ carrier G" using assms by auto with kernel_assoc_elem obtain z where "x = y ⊗⇘_{G}⇙ z" "z ∈ kernel G H h" using x by metis thus "x ∈ A <#> kernel G H h" unfolding set_mult_def using y by blast qed lemma (in group_hom) vimage_subset_generate_kern: assumes "A ⊆ carrier G" shows "{x ∈ carrier G. h x ∈ h ` A} ⊆ generate G (A ∪ kernel G H h)" using vimage_eq_set_mult_kern_right[of A] G.set_mult_subset_generate[of "A" "kernel G H h"] assms unfolding kernel_def by blast text ‹The preimage of a subgroup under a homomorphism is also a subgroup.› lemma (in group_hom) subgroup_vimage_is_subgroup: assumes "subgroup I H" shows "subgroup {x ∈ carrier G. h x ∈ I} G" (is "subgroup ?J G") proof show "?J ⊆ carrier G" by blast show "𝟭 ∈ ?J" using subgroup.one_closed[of I H] assms by simp fix x assume x: "x ∈ ?J" then have hx: "h x ∈ I" by blast show "inv x ∈ ?J" proof - from hx have "inv⇘_{H}⇙ (h x) ∈ I" using subgroup.m_inv_closed assms by fast moreover have "inv x ∈ carrier G" using x by simp moreover have "inv⇘_{H}⇙ (h x) = h (inv x)" using x by auto ultimately show "inv x ∈ ?J" by simp qed fix y assume y: "y ∈ ?J" then have hy: "h y ∈ I" by blast show "x ⊗ y ∈ {x ∈ carrier G. h x ∈ I}" proof - have "h (x ⊗ y) = h x ⊗⇘_{H}⇙ h y" using x y by simp also have "… ∈ I" using hx hy assms subgroup.m_closed by fast finally have "h (x ⊗ y) ∈ I" . moreover have "x ⊗ y ∈ carrier G" using x y by simp ultimately show ?thesis by blast qed qed lemma (in group_hom) iso_kernel: assumes "h ∈ iso G H" shows "kernel G H h = {𝟭⇘_{G}⇙}" unfolding kernel_def using assms using hom_one iso_iff by blast ✐‹contributor ‹Paulo Emílio de Vilhena›› (* adapted by Joseph Thommes *) lemma (in group_hom) induced_group_hom_same_group: assumes "subgroup I G" shows "group_hom (G ⦇ carrier := I ⦈) H h" proof - have "h ∈ hom (G ⦇ carrier := I ⦈) H" using homh subgroup.mem_carrier[OF assms] unfolding hom_def by auto thus ?thesis unfolding group_hom_def group_hom_axioms_def using subgroup.subgroup_is_group[OF assms G.is_group] by simp qed text ‹The order of an element under a homomorphism divides the order of the element.› lemma (in group_hom) hom_ord_dvd_ord: assumes "a ∈ carrier G" shows "H.ord (h a) dvd G.ord a" proof - have "h a [^]⇘_{H}⇙ (G.ord a) = h (a [^]⇘_{G}⇙ G.ord a)" using assms local.hom_nat_pow by presburger also have "… = h (𝟭⇘_{G}⇙)" using G.pow_ord_eq_1 assms by simp also have "… = 𝟭⇘_{H}⇙" by simp finally have "h a [^]⇘_{H}⇙ G.ord a = 𝟭⇘_{H}⇙" . then show ?thesis using pow_eq_id assms by simp qed text ‹In particular, this implies that the image of an element with a finite order also will have a finite order.› lemma (in group_hom) finite_ord_stays_finite: assumes "a ∈ carrier G" "G.ord a ≠ 0" shows "H.ord (h a) ≠ 0" using hom_ord_dvd_ord assms by fastforce text ‹For injective homomorphisms, the order stays the same.› lemma (in group_hom) inj_imp_ord_eq: assumes "a ∈ carrier G" "inj_on h (carrier G)" "G.ord a ≠ 0" shows "H.ord (h a) = G.ord a" proof (rule antisym) show "H.ord (h a) ≤ G.ord a" using hom_ord_dvd_ord assms by force show "G.ord a ≤ H.ord (h a)" proof - have "𝟭⇘_{H}⇙ = h (a [^]⇘_{G}⇙ H.ord(h a))" using H.pow_ord_eq_1 assms by (simp add: local.hom_nat_pow) then have "a [^]⇘_{G}⇙ H.ord (h a) = 𝟭⇘_{G}⇙" using assms inj_on_one_iff by simp then have "G.ord a dvd H.ord (h a)" using G.pow_eq_id assms(1) by blast thus ?thesis using assms finite_ord_stays_finite by fastforce qed qed lemma (in group_hom) one_in_kernel: "𝟭 ∈ kernel G H h" using subgroup.one_closed subgroup_kernel by blast lemma hom_in_carr: assumes "f ∈ hom G H" shows "⋀x. x ∈ carrier G ⟹ f x ∈ carrier H" using assms unfolding hom_def bij_betw_def by blast lemma iso_in_carr: assumes "f ∈ iso G H" shows "⋀x. x ∈ carrier G ⟹ f x ∈ carrier H" using assms unfolding iso_def bij_betw_def by blast lemma triv_iso: assumes "group G" "group H" "carrier G = {𝟭⇘_{G}⇙}" "carrier H = {𝟭⇘_{H}⇙}" shows "G ≅ H" proof(unfold is_iso_def iso_def) interpret G: group G by fact interpret H: group H by fact let ?f = "λ_. 𝟭⇘_{H}⇙" have "?f ∈ hom G H" by (intro homI, auto) moreover have "bij_betw ?f (carrier G) (carrier H)" unfolding bij_betw_def using assms(3, 4) by auto ultimately show "{h ∈ hom G H. bij_betw h (carrier G) (carrier H)} ≠ {}" by blast qed text ‹The cardinality of the image of a group homomorphism times the cardinality of its kernel is equal to the group order. This is basically another form of Lagrange's theorem.› lemma (in group_hom) image_kernel_product: "card (h ` (carrier G)) * card (kernel G H h) = order G" proof - interpret G: group G by simp interpret H: group H by simp interpret ih: subgroup "h ` (carrier G)" H using img_is_subgroup by blast interpret ih: group "H⦇carrier := h ` (carrier G)⦈" using subgroup.subgroup_is_group by blast interpret h: group_hom G "H⦇carrier := h ` (carrier G)⦈" by (unfold_locales, unfold hom_def, auto) interpret k: subgroup "kernel G (H⦇carrier := h ` carrier G⦈) h" G using h.subgroup_kernel by blast from h.FactGroup_iso have "G Mod kernel G (H⦇carrier := h ` carrier G⦈) h ≅ H⦇carrier := h ` carrier G⦈" by auto hence "card (h ` (carrier G)) = order (G Mod kernel G (H⦇carrier := h ` carrier G⦈) h)" using iso_same_card unfolding order_def by fastforce moreover have "order (G Mod kernel G (H⦇carrier := h ` carrier G⦈) h) * card (kernel G (H⦇carrier := h ` carrier G⦈) h) = order G" using G.lagrange[OF k.subgroup_axioms] unfolding order_def FactGroup_def by force moreover have "kernel G (H⦇carrier := h ` carrier G⦈) h = kernel G H h" unfolding kernel_def by auto ultimately show ?thesis by argo qed end

# Theory Finite_And_Cyclic_Groups

(* File: Finite_And_Cyclic_Groups.thy Author: Joseph Thommes, TU München; Manuel Eberl, TU München *) section ‹Finite and cyclic groups› theory Finite_And_Cyclic_Groups imports Group_Hom Generated_Groups_Extend General_Auxiliary begin subsection ‹Finite groups› text ‹We define the notion of finite groups and prove some trivial facts about them.› locale finite_group = group + assumes fin[simp]: "finite (carrier G)" (* Manuel Eberl *) lemma (in finite_group) ord_pos: assumes "x ∈ carrier G" shows "ord x > 0" using ord_ge_1[of x] assms by auto lemma (in finite_group) order_gt_0 [simp,intro]: "order G > 0" by (subst order_gt_0_iff_finite) auto lemma (in finite_group) finite_ord_conv_Least: assumes "x ∈ carrier G" shows "ord x = (LEAST n::nat. 0 < n ∧ x [^] n = 𝟭)" using pow_order_eq_1 order_gt_0_iff_finite ord_conv_Least assms by auto lemma (in finite_group) non_trivial_group_ord_gr_1: assumes "carrier G ≠ {𝟭}" shows "∃e ∈ carrier G. ord e > 1" proof - from one_closed obtain e where e: "e ≠ 𝟭" "e ∈ carrier G" using assms carrier_not_empty by blast thus ?thesis using ord_eq_1[of e] le_neq_implies_less ord_ge_1 by fastforce qed (* Manuel Eberl *) lemma (in finite_group) max_order_elem: obtains a where "a ∈ carrier G" "∀x ∈ carrier G. ord x ≤ ord a" proof - have "∃x. x ∈ carrier G ∧ (∀y. y ∈ carrier G ⟶ ord y ≤ ord x)" proof (rule ex_has_greatest_nat[of _ 𝟭 _ "order G + 1"], safe) show "𝟭 ∈ carrier G" by auto next fix x assume "x ∈ carrier G" hence "ord x ≤ order G" by (intro ord_le_group_order fin) also have "… < order G + 1" by simp finally show "ord x < order G + 1" . qed thus ?thesis using that by blast qed lemma (in finite_group) iso_imp_finite: assumes "G ≅ H" "group H" shows "finite_group H" proof - interpret H: group H by fact show ?thesis proof(unfold_locales) show "finite (carrier H)" using iso_same_card[OF assms(1)] by (metis card_gt_0_iff order_def order_gt_0) qed qed lemma (in finite_group) finite_FactGroup: assumes "H ⊲ G" shows "finite_group (G Mod H)" proof - interpret H: normal H G by fact interpret Mod: group "G Mod H" using H.factorgroup_is_group . show ?thesis by (unfold_locales, unfold FactGroup_def RCOSETS_def, simp) qed lemma (in finite_group) bigger_subgroup_is_group: assumes "subgroup H G" "card H ≥ order G" shows "H = carrier G" using subgroup.subset fin assms by (metis card_seteq order_def) text ‹All generated subgroups of a finite group are obviously also finite.› lemma (in finite_group) finite_generate: assumes "A ⊆ carrier G" shows "finite (generate G A)" using generate_incl[of A] rev_finite_subset[of "carrier G" "generate G A"] assms by simp text ‹We also provide an induction rule for finite groups inspired by Manuel Eberl's AFP entry "Dirichlet L-Functions and Dirichlet's Theorem" and the contained theory "Group\_Adjoin". A property that is true for a subgroup generated by some set and stays true when adjoining an element, is also true for the whole group.› lemma (in finite_group) generate_induct[consumes 1, case_names base adjoin]: assumes "A0 ⊆ carrier G" assumes "A0 ⊆ carrier G ⟹ P (G⦇carrier := generate G A0⦈)" assumes "⋀a A. ⟦A ⊆ carrier G; a ∈ carrier G - generate G A; A0 ⊆ A; P (G⦇carrier := generate G A⦈)⟧ ⟹ P (G⦇carrier := generate G (A ∪ {a})⦈)" shows "P G" proof - define A where A: "A = carrier G" hence gA: "generate G A = carrier G" using generate_incl[of "carrier G"] generate_sincl[of "carrier G"] by simp hence "finite A" using fin A by argo moreover have "A0 ⊆ A" using assms(1) A by argo moreover have "A ⊆ carrier G" using A by simp moreover have "generate G A0 ⊆ generate G A" using gA generate_incl[OF assms(1)] by argo ultimately have "P (G⦇carrier := generate G A⦈)" using assms(2, 3) proof (induction "A" taking: card rule: measure_induct_rule) case (less A) then show ?case proof(cases "generate G A0 = generate G A") case True thus ?thesis using less by force next case gA0: False with less(3) have s: "A0 ⊂ A" by blast then obtain a where a: "a ∈ A - A0" by blast have P1: "P (G⦇carrier := generate G (A - {a})⦈)" proof(rule less(1)) show "card (A - {a}) < card A" using a less(2) by (meson DiffD1 card_Diff1_less) show "A0 ⊆ A - {a}" using a s by blast thus "generate G A0 ⊆ generate G (A - {a})" using mono_generate by presburger qed (use less a s in auto) show ?thesis proof (cases "generate G A = generate G (A - {a})") case True then show ?thesis using P1 by simp next case False have "a ∈ carrier G - generate G (A - {a})" proof - have "a ∉ generate G (A - {a})" proof assume a2: "a ∈ generate G (A - {a})" have "generate G (A - {a}) = generate G A" proof (rule equalityI) show "generate G (A - {a}) ⊆ generate G A" using mono_generate by auto show "generate G A ⊆ generate G (A - {a})" proof(subst (2) generate_idem[symmetric]) show "generate G A ⊆ generate G (generate G (A - {a}))" by (intro mono_generate, use generate_sincl[of "A - {a}"] a2 in blast) qed (use less in auto) qed with False show False by argo qed with a less show ?thesis by fast qed from less(7)[OF _ this _ P1] less(4) s a have "P (G⦇carrier := generate G (A - {a} ∪ {a})⦈)" by blast moreover have "A - {a} ∪ {a} = A" using a by blast ultimately show ?thesis by auto qed qed qed with gA show ?thesis by simp qed subsection ‹Finite abelian groups› text ‹Another trivial locale: the finite abelian group with some trivial facts.› locale finite_comm_group = finite_group + comm_group lemma (in finite_comm_group) iso_imp_finite_comm: assumes "G ≅ H" "group H" shows "finite_comm_group H" proof - interpret H: group H by fact interpret H: comm_group H by (intro iso_imp_comm_group[OF assms(1)], unfold_locales) interpret H: finite_group H by (intro iso_imp_finite[OF assms(1)], unfold_locales) show ?thesis by unfold_locales qed lemma (in finite_comm_group) finite_comm_FactGroup: assumes "subgroup H G" shows "finite_comm_group (G Mod H)" unfolding finite_comm_group_def proof(safe) show "finite_group (G Mod H)" using finite_FactGroup[OF subgroup_imp_normal[OF assms]] . show "comm_group (G Mod H)" by (simp add: abelian_FactGroup assms) qed (* Manuel Eberl *) lemma (in finite_comm_group) subgroup_imp_finite_comm_group: assumes "subgroup H G" shows "finite_comm_group (G⦇carrier := H⦈)" proof - interpret G': group "G⦇carrier := H⦈" by (intro subgroup_imp_group) fact+ interpret H: subgroup H G by fact show ?thesis by standard (use finite_subset[OF H.subset] in ‹auto simp: m_comm›) qed subsection ‹Cyclic groups› text ‹Now, the central notion of a cyclic group is introduced: a group generated by a single element.› locale cyclic_group = group + fixes gen :: "'a" assumes gen_closed[intro, simp]: "gen ∈ carrier G" assumes generator: "carrier G = generate G {gen}" lemma (in cyclic_group) elem_is_gen_pow: assumes "x ∈ carrier G" shows "∃n :: int. x = gen [^] n" proof - from generator have x_g:"x ∈ generate G {gen}" using assms by fast with generate_pow[of gen] show ?thesis using gen_closed by blast qed text ‹Every cyclic group is commutative/abelian.› sublocale cyclic_group ⊆ comm_group proof(unfold_locales) fix x y assume "x ∈ carrier G" "y ∈ carrier G" then obtain a b where ab:"x = gen [^] (a::int)" "y = gen [^] (b::int)" using elem_is_gen_pow by presburger then have "x ⊗ y = gen [^] (a + b)" by (simp add: int_pow_mult) also have "… = y ⊗ x" using ab int_pow_mult by (metis add.commute gen_closed) finally show "x ⊗ y = y ⊗ x" . qed text ‹Some trivial intro rules for showing that a group is cyclic.› lemma (in group) cyclic_groupI0: assumes "a ∈ carrier G" "carrier G = generate G {a}" shows "cyclic_group G a" using assms by (unfold_locales; auto) lemma (in group) cyclic_groupI1: assumes "a ∈ carrier G" "carrier G ⊆ generate G {a}" shows "cyclic_group G a" using assms by (unfold_locales, use generate_incl[of "{a}"] in auto) lemma (in group) cyclic_groupI2: assumes "a ∈ carrier G" shows "cyclic_group (G⦇carrier := generate G {a}⦈) a" proof (intro group.cyclic_groupI0) show "group (G⦇carrier := generate G {a}⦈)" by (intro subgroup.subgroup_is_group group.generate_is_subgroup, use assms in simp_all) show "a ∈ carrier (G⦇carrier := generate G {a}⦈)" using generate.incl[of a "{a}"] by auto show "carrier (G⦇carrier := generate G {a}⦈) = generate (G⦇carrier := generate G {a}⦈) {a}" using assms by (simp add: generate_consistent generate.incl group.generate_is_subgroup) qed text ‹The order of the generating element is always the same as the group order.› lemma (in cyclic_group) ord_gen_is_group_order: shows "ord gen = order G" proof (cases "finite (carrier G)") case True with generator show "ord gen = order G" using generate_pow_card[of gen] order_def[of G] gen_closed by simp next case False thus ?thesis using generate_pow_card generator order_def[of G] card_eq_0_iff[of "carrier G"] by force qed text ‹In the case of a finite group, it is sufficient to have one element of group order to know that the group is cyclic.› lemma (in finite_group) element_ord_generates_cyclic: assumes "a ∈ carrier G" "ord a = order G" shows "cyclic_group G a" proof (unfold_locales) show "a ∈ carrier G" using assms(1) by simp show "carrier G = generate G {a}" using assms bigger_subgroup_is_group[OF generate_is_subgroup] by (metis empty_subsetI fin generate_pow_card insert_subset ord_le_group_order) qed text ‹Another useful fact is that a group of prime order is also cyclic.› lemma (in group) prime_order_group_is_cyc: assumes "Factorial_Ring.prime (order G)" obtains g where "cyclic_group G g" proof (unfold_locales) obtain p where order_p: "order G = p" and p_prime: "Factorial_Ring.prime p" using assms by blast then have "card (carrier G) ≥ 2" by (simp add: order_def prime_ge_2_nat) then obtain a where a_in: "a ∈ carrier G" and a_not_one: "a ≠ 𝟭" using one_unique by (metis (no_types, lifting) card_2_iff' obtain_subset_with_card_n subset_iff) interpret fin: finite_group G using assms order_gt_0_iff_finite unfolding order_def by unfold_locales auto have "ord a dvd p" using a_in order_p ord_dvd_group_order by blast hence "ord a = p" using prime_nat_iff[of p] p_prime ord_eq_1 a_in a_not_one by blast then interpret cyclic_group G a using fin.element_ord_generates_cyclic order_p a_in by simp show ?thesis using that cyclic_group_axioms . qed text ‹What follows is an induction principle for cyclic groups: a predicate is true for all elements of the group if it is true for all elements that can be formed by the generating element by just multiplication and if it also holds under the forming of the inverse (as we by this cover all elements of the group),› (* Manuel Eberl *) lemma (in cyclic_group) generator_induct [consumes 1, case_names generate inv]: assumes x: "x ∈ carrier G" assumes IH1: "⋀n::nat. P (gen [^] n)" assumes IH2: "⋀x. x ∈ carrier G ⟹ P x ⟹ P (inv x)" shows "P x" proof - from x obtain n :: int where n: "x = gen [^] n" using elem_is_gen_pow[of x] by auto show ?thesis proof (cases "n ≥ 0") case True have "P (gen [^] nat n)" by (rule IH1) with True n show ?thesis by simp next case False have "P (inv (gen [^] nat (-n)))" by (intro IH1 IH2) auto also have "gen [^] nat (-n) = gen [^] (-n)" using False by simp also have "inv … = x" using n by (simp add: int_pow_neg) finally show ?thesis . qed qed subsection ‹Finite cyclic groups› text ‹Additionally, the notion of the finite cyclic group is introduced.› locale finite_cyclic_group = finite_group + cyclic_group sublocale finite_cyclic_group ⊆ finite_comm_group by unfold_locales lemma (in finite_cyclic_group) ord_gen_gt_zero: "ord gen > 0" using ord_ge_1[OF fin gen_closed] by simp text ‹In order to prove something about an element in a finite abelian group, it is possible to show this property for the neutral element or the generating element and inductively for the elements that are formed by multiplying with the generator.› lemma (in finite_cyclic_group) generator_induct0 [consumes 1, case_names one step]: assumes x: "x ∈ carrier G" assumes IH1: "P 𝟭" assumes IH2: "⋀x. ⟦x ∈ carrier G; P x⟧ ⟹ P (x ⊗ gen)" shows "P x" proof - from ord_gen_gt_zero generate_nat_pow[OF _ gen_closed] obtain n::nat where n: "x = gen [^] n" using generator x by blast thus ?thesis by (induction n arbitrary: x, use assms in auto) qed lemma (in finite_cyclic_group) generator_induct1 [consumes 1, case_names gen step]: assumes x: "x ∈ carrier G" assumes IH1: "P gen" assumes IH2: "⋀x. ⟦x ∈ carrier G; P x⟧ ⟹ P (x ⊗ gen)" shows "P x" proof(rule generator_induct0[OF x]) show "⋀x. ⟦x ∈ carrier G; P x⟧ ⟹ P (x ⊗ gen)" using IH2 by blast have "P x" if "n > 0" "x = gen [^] n" for n::nat and x using that by (induction n arbitrary: x; use assms in fastforce) from this[OF ord_pos[OF gen_closed] pow_ord_eq_1[OF gen_closed, symmetric]] show "P 𝟭" . qed subsection ‹‹get_exp› - discrete logarithm› text ‹What now follows is the discrete logarithm for groups. It is used at several times througout this entry and is initially used to show that two cyclic groups of the same order are isomorphic.› definition (in group) get_exp where "get_exp g = (λa. SOME k::int. a = g [^] k)" text ‹For each element with itself as the basis the discrete logarithm indeed does what expected. This is not the strongest possible statement, but sufficient for our needs.› lemma (in group) get_exp_self_fulfills: assumes "a ∈ carrier G" shows "a = a [^] get_exp a a" proof - have "a = a [^] (1::int)" using assms by auto moreover have "a [^] (1::int) = a [^] (SOME x::int. a [^] (1::int) = a [^] x)" by (intro someI_ex[of "λx::int. a [^] (1::int) = a [^] x"]; blast) ultimately show ?thesis unfolding get_exp_def by simp qed lemma (in group) get_exp_self: assumes "a ∈ carrier G" shows "get_exp a a mod ord a = (1::int) mod ord a" by (intro pow_eq_int_mod[OF assms], use get_exp_self_fulfills[OF assms] assms in auto) text ‹For cyclic groups, the discrete logarithm "works" for every element.› lemma (in cyclic_group) get_exp_fulfills: assumes "a ∈ carrier G" shows "a = gen [^] get_exp gen a" proof - from elem_is_gen_pow[OF assms] obtain k::int where k: "a = gen [^] k" by blast moreover have "gen [^] k = gen [^] (SOME x::int. gen [^] k = gen [^] x)" by(intro someI_ex[of "λx::int. gen [^] k = gen [^] x"]; blast) ultimately show ?thesis unfolding get_exp_def by blast qed lemma (in cyclic_group) get_exp_non_zero: assumes"b ∈ carrier G" "b ≠ 𝟭" shows "get_exp gen b ≠ 0" using assms get_exp_fulfills[OF assms(1)] by auto text ‹One well-known logarithmic identity.› lemma (in cyclic_group) get_exp_mult_mod: assumes "a ∈ carrier G" "b ∈ carrier G" shows "get_exp gen (a ⊗ b) mod (ord gen) = (get_exp gen a + get_exp gen b) mod (ord gen)" proof (intro pow_eq_int_mod[OF gen_closed]) from get_exp_fulfills[of "a ⊗ b"] have "gen [^] get_exp gen (a ⊗ b) = a ⊗ b" using assms by simp moreover have "gen [^] (get_exp gen a + get_exp gen b) = a ⊗ b" proof - have "gen [^] (get_exp gen a + get_exp gen b) = gen [^] (get_exp gen a) ⊗ gen [^] (get_exp gen b)" using int_pow_mult by blast with get_exp_fulfills assms show ?thesis by simp qed ultimately show "gen [^] get_exp gen (a ⊗ b) = gen [^] (get_exp gen a + get_exp gen b)" by simp qed text ‹We now show that all functions from a group generated by 'a' to a group generated by 'b' that map elements from $a^k$ to $b^k$ in the other group are in fact isomorphisms between these two groups.› lemma (in group) iso_cyclic_groups_generate: assumes "a ∈ carrier G" "b ∈ carrier H" "group.ord G a = group.ord H b" "group H" shows "{f. ∀k ∈ (UNIV::int set). f (a [^] k) = b [^]⇘_{H}⇙ k} ⊆ iso (G⦇carrier := generate G {a}⦈) (H⦇carrier := generate H {b}⦈)" proof interpret H: group H by fact let ?A = "G⦇carrier := generate G {a}⦈" let ?B = "H⦇carrier := generate H {b}⦈" interpret A: cyclic_group ?A a by (intro group.cyclic_groupI2; use assms(1) in simp) interpret B: cyclic_group ?B b by (intro group.cyclic_groupI2; use assms(2) in simp) have sA: "subgroup (generate G {a}) G" by (intro generate_is_subgroup, use assms(1) in simp) have sB: "subgroup (generate H {b}) H" by (intro H.generate_is_subgroup, use assms(2) in simp) fix x assume x: "x ∈ {f. ∀k∈(UNIV::int set). f (a [^] k) = b [^]⇘_{H}⇙ k}" have hom: "x ∈ hom ?A ?B" proof (intro homI) fix c assume c: "c ∈ carrier ?A" from A.elem_is_gen_pow[OF this] obtain k::int where k: "c = a [^] k" using int_pow_consistent[OF sA generate.incl[of a]] by auto with x have "x c = b [^]⇘_{H}⇙ k" by blast thus "x c ∈ carrier ?B" using B.int_pow_closed H.int_pow_consistent[OF sB] generate.incl[of b "{b}" H] by simp fix d assume d: "d ∈ carrier ?A" from A.elem_is_gen_pow[OF this] obtain l::int where l: "d = a [^] l" using int_pow_consistent[OF sA generate.incl[of a]] by auto with k have "c ⊗ d = a [^] (k + l)" by (simp add: int_pow_mult assms(1)) with x have "x (c ⊗⇘_{?A}⇙ d) = b [^]⇘_{H}⇙ (k + l)" by simp also have "… = b [^]⇘_{H}⇙ k ⊗⇘_{H}⇙ b [^]⇘_{H}⇙ l" by (simp add: H.int_pow_mult assms(2)) finally show "x (c ⊗⇘_{?A}⇙ d) = x c ⊗⇘_{?B}⇙ x d" using x k l by simp qed then interpret xgh: group_hom ?A ?B x unfolding group_hom_def group_hom_axioms_def by blast have "kernel ?A ?B x = {𝟭}" proof(intro equalityI) show "{𝟭} ⊆ kernel ?A ?B x" using xgh.one_in_kernel by auto have "c = 𝟭" if "c ∈ kernel ?A ?B x" for c proof - from that have c: "c ∈ carrier ?A" unfolding kernel_def by blast from A.elem_is_gen_pow[OF this] obtain k::int where k: "c = a [^] k" using int_pow_consistent[OF sA generate.incl[of a]] by auto moreover have "x c = 𝟭⇘_{H}⇙" using that x unfolding kernel_def by auto ultimately have "𝟭⇘_{H}⇙ = b [^]⇘_{H}⇙ k" using x by simp with assms(3) have "a [^] k = 𝟭" using int_pow_eq_id[OF assms(1), of k] H.int_pow_eq_id[OF assms(2), of k] by simp thus "c = 𝟭" using k by blast qed thus "kernel ?A ?B x ⊆ {𝟭}" by blast qed moreover have "carrier ?B ⊆ x ` carrier ?A" proof fix c assume c: "c ∈ carrier ?B" from B.elem_is_gen_pow[OF this] obtain k::int where k: "c = b [^]⇘_{H}⇙ k" using H.int_pow_consistent[OF sB generate.incl[of b]] by auto then have "x (a [^] k) = c" using x by blast moreover have "a [^] k ∈ carrier ?A" using int_pow_consistent[OF sA generate.incl[of a]] A.int_pow_closed generate.incl[of a] by fastforce ultimately show "c ∈ x ` carrier ?A" by blast qed ultimately show "x ∈ iso ?A ?B" using hom xgh.iso_iff unfolding kernel_def by auto qed text ‹This is then used to derive the isomorphism of two cyclic groups of the same order as a direct consequence.› lemma (in cyclic_group) iso_cyclic_groups_same_order: assumes "cyclic_group H h" "order G = order H" shows "G ≅ H" proof(intro is_isoI) interpret H: cyclic_group H h by fact define f where "f = (λa. h [^]⇘_{H}⇙ get_exp gen a)" from assms(2) have o: "ord gen = H.ord h" using ord_gen_is_group_order H.ord_gen_is_group_order by simp have "∀k ∈ (UNIV::int set). f (gen [^] k) = h [^]⇘_{H}⇙ k" proof fix k assume k: "k ∈ (UNIV::int set)" have "gen [^] k = gen [^] (SOME x::int. gen [^] k = gen [^] x)" by(intro someI_ex[of "λx::int. gen [^] k = gen [^] x"]; blast) moreover have "(SOME x::int. gen [^] k = gen [^] x) = (SOME x::int. h [^]⇘_{H}⇙ k = h [^]⇘_{H}⇙ x)" proof - have "gen [^] k = gen [^] x ⟷ h [^]⇘_{H}⇙ k = h [^]⇘_{H}⇙ x" for x::int by (simp add: o group.int_pow_eq) thus ?thesis by simp qed moreover have "h [^]⇘_{H}⇙ k = h [^]⇘_{H}⇙ (SOME x::int. h [^]⇘_{H}⇙ k = h [^]⇘_{H}⇙ x)" by(intro someI_ex[of "λx::int. h [^]⇘_{H}⇙ k = h [^]⇘_{H}⇙ x"]; blast) ultimately show "f (gen [^] k) = h [^]⇘_{H}⇙ k" unfolding f_def get_exp_def by metis qed thus "f ∈ iso G H" using iso_cyclic_groups_generate[OF gen_closed H.gen_closed o H.is_group] by (auto simp flip: generator H.generator) qed subsection ‹Integer modular groups› text ‹We show that ‹integer_mod_group› (written as ‹Z n›) is in fact a cyclic group. For $n \neq 1$ it is generated by $1$ and in the other case by $0$.› notation integer_mod_group ("Z") lemma Zn_neq1_cyclic_group: assumes "n ≠ 1" shows "cyclic_group (Z n) 1" proof(unfold cyclic_group_def cyclic_group_axioms_def, safe) show "group (Z n)" using group_integer_mod_group . then interpret group "Z n" . show oc: "1 ∈ carrier (Z n)" unfolding integer_mod_group_def integer_group_def using assms by force show "x ∈ generate (Z n) {1}" if "x ∈ carrier (Z n)" for x using generate_pow[OF oc] that int_pow_integer_mod_group solve_equation subgroup_self by fastforce show "x ∈ carrier (Z n)" if "x ∈ generate (Z n) {1}" for x using generate_incl[of "{1}"] that oc by fast qed lemma Z1_cyclic_group: "cyclic_group (Z 1) 0" proof(unfold cyclic_group_def cyclic_group_axioms_def, safe) show "group (Z 1)" using group_integer_mod_group . then interpret group "Z 1" . show "0 ∈ carrier (Z 1)" unfolding integer_mod_group_def by simp thus "x ∈ carrier (Z 1)" if "x ∈ generate (Z 1) {0}" for x using generate_incl[of "{0}"] that by fast show "x ∈ generate (Z 1) {0}" if "x ∈ carrier (Z 1)" for x proof - from that have "x = 0" unfolding integer_mod_group_def by auto with generate.one[of "Z 1" "{0}"] show "x ∈ generate (Z 1) {0}" unfolding integer_mod_group_def by simp qed qed lemma Zn_cyclic_group: obtains x where "cyclic_group (Z n) x" using Z1_cyclic_group Zn_neq1_cyclic_group by metis text ‹Moreover, its order is just $n$.› lemma Zn_order: "order (Z n) = n" by (unfold integer_mod_group_def integer_group_def order_def, auto) text ‹Consequently, ‹Z n› is isomorphic to any cyclic group of order $n$.› lemma (in cyclic_group) Zn_iso: assumes "order G = n" shows "G ≅ Z n" using Zn_order Zn_cyclic_group iso_cyclic_groups_same_order assms by metis no_notation integer_mod_group ("Z") end

# Theory DirProds

(* File: DirProds.thy Author: Joseph Thommes, TU München *) section ‹Direct group product› theory DirProds imports Finite_Product_Extend Group_Hom Finite_And_Cyclic_Groups begin notation integer_mod_group ("Z") text ‹The direct group product is defined component-wise and provided in an indexed way.› definition DirProds :: "('a ⇒ ('b, 'c) monoid_scheme) ⇒ 'a set ⇒ ('a ⇒ 'b) monoid" where "DirProds G I = ⦇ carrier = Pi⇩_{E}I (carrier ∘ G), monoid.mult = (λx y. restrict (λi. x i ⊗⇘_{G i}⇙ y i) I), one = restrict (λi. 𝟭⇘_{G i}⇙) I ⦈" text ‹Basic lemmas about ‹DirProds›.› lemma DirProds_empty: "carrier (DirProds f {}) = {𝟭⇘_{DirProds f {}}⇙}" unfolding DirProds_def by auto lemma DirProds_order: assumes "finite I" shows "order (DirProds G I) = prod (order ∘ G) I" unfolding order_def DirProds_def using assms by (simp add: card_PiE) lemma DirProds_in_carrI: assumes "⋀i. i ∈ I ⟹ x i ∈ carrier (G i)" "⋀i. i ∉ I ⟹ x i = undefined" shows "x ∈ carrier (DirProds G I)" unfolding DirProds_def using assms by auto lemma comp_in_carr: assumes "x ∈ carrier (DirProds G I)" "i ∈ I" shows "x i ∈ carrier (G i)" using assms unfolding DirProds_def by auto lemma comp_mult: assumes "i ∈ I" shows "(x ⊗⇘_{DirProds G I}⇙ y) i = (x i ⊗⇘_{G i}⇙ y i)" using assms unfolding DirProds_def by simp lemma comp_exp_nat: fixes k::nat assumes "i ∈ I" shows "(x [^]⇘_{DirProds G I}⇙ k) i = x i [^]⇘_{G i}⇙ k" proof (induction k) case 0 then show ?case using assms unfolding DirProds_def by simp next case i: (Suc k) have "(x [^]⇘_{DirProds G I}⇙ k ⊗⇘_{DirProds G I}⇙ x) i = (x [^]⇘_{DirProds G I}⇙ k) i ⊗⇘_{G i}⇙ x i" by(rule comp_mult[OF assms]) also from i have "… = x i [^]⇘_{G i}⇙ k ⊗⇘_{G i}⇙ x i" by simp also have "… = x i [^]⇘_{G i}⇙ Suc k" by simp finally show ?case by simp qed lemma DirProds_m_closed: assumes "x ∈ carrier (DirProds G I)" "y ∈ carrier (DirProds G I)" "⋀i. i ∈ I ⟹ group (G i)" shows "x ⊗⇘_{DirProds G I}⇙ y ∈ carrier (DirProds G I)" using assms monoid.m_closed[OF group.is_monoid[OF assms(3)]] unfolding DirProds_def by fastforce lemma partial_restr: assumes "a ∈ carrier (DirProds G I)" "J ⊆ I" shows "restrict a J ∈ carrier (DirProds G J)" using assms unfolding DirProds_def by auto lemma eq_parts_imp_eq: assumes "a ∈ carrier (DirProds G I)" "b ∈ carrier (DirProds G I)" "⋀i. i ∈ I ⟹ a i = b i" shows "a = b" using assms unfolding DirProds_def by fastforce lemma mult_restr: assumes "a ∈ carrier (DirProds G I)" "b ∈ carrier (DirProds G I)" "J ⊆ I" shows "a ⊗⇘_{DirProds G J}⇙ b = restrict (a ⊗⇘_{DirProds G I}⇙ b) J" using assms unfolding DirProds_def by force lemma DirProds_one: assumes "x ∈ carrier (DirProds G I)" shows "(∀i ∈ I. x i = 𝟭⇘_{G i}⇙) ⟷ x = 𝟭⇘_{DirProds G I}⇙" using assms unfolding DirProds_def by fastforce lemma DirProds_one': "i∈I ⟹ 𝟭⇘_{DirProds G I}⇙ i = 𝟭⇘_{G i}⇙" unfolding DirProds_def by simp lemma DirProds_one'': "𝟭⇘_{DirProds G I}⇙ = restrict (λi. 𝟭⇘_{G i}⇙) I" by (unfold DirProds_def, simp) lemma DirProds_mult: "(⊗⇘_{DirProds G I}⇙) = (λx y. restrict (λi. x i ⊗⇘_{G i}⇙ y i) I)" unfolding DirProds_def by simp lemma DirProds_one_iso: "(λx. x G) ∈ iso (DirProds f {G}) (f G)" proof (intro isoI homI) show "bij_betw (λx. x G) (carrier (DirProds f {G})) (carrier (f G))" proof (unfold bij_betw_def, rule) show "inj_on (λx. x G) (carrier (DirProds f {G}))" by (intro inj_onI, unfold DirProds_def PiE_def Pi_def extensional_def, fastforce) show "(λx. x G) ` carrier (DirProds f {G}) = carrier (f G)" proof(intro equalityI subsetI) show "x ∈ carrier (f G)" if "x ∈ (λx. x G) ` carrier (DirProds f {G})" for x using that unfolding DirProds_def by auto show "x ∈ (λx. x G) ` carrier (DirProds f {G})" if xc: "x ∈ carrier (f G)" for x proof show "(λk∈{G}. x) ∈ carrier (DirProds f {G})" unfolding DirProds_def using xc by auto moreover show "x = (λk∈{G}. x) G" by simp qed qed qed qed (unfold DirProds_def PiE_def Pi_def extensional_def, auto) lemma DirProds_one_cong: "(DirProds f {G}) ≅ (f G)" using DirProds_one_iso is_isoI by fast lemma DirProds_one_iso_sym: "(λx. (λ_∈{G}. x)) ∈ iso (f G) (DirProds f {G})" proof (intro isoI homI) show "bij_betw (λx. λ_∈{G}. x) (carrier (f G)) (carrier (DirProds f {G}))" proof (unfold bij_betw_def, rule) show "inj_on (λx. (λ_∈{G}. x)) (carrier (f G))" by (intro inj_onI, metis imageI image_constant image_restrict_eq member_remove remove_def) show "(λx. (λ_∈{G}. x)) ` carrier (f G) = carrier (DirProds f {G})" unfolding DirProds_def by fastforce qed qed (unfold DirProds_def, auto) lemma DirProds_one_cong_sym: "(f G) ≅ (DirProds f {G})" using DirProds_one_iso_sym is_isoI by fast text ‹The direct product is a group iff all factors are groups.› lemma DirProds_is_group: assumes "⋀i. i ∈ I ⟹ group (G i)" shows "group (DirProds G I)" proof(rule groupI) show one_closed: "𝟭⇘_{DirProds G I}⇙ ∈ carrier (DirProds G I)" unfolding DirProds_def by (simp add: assms group.is_monoid) fix x assume x: "x ∈ carrier (DirProds G I)" have one_: "⋀i. i ∈ I ⟹ 𝟭⇘_{G i}⇙ = 𝟭⇘_{DirProds G I}⇙ i" unfolding DirProds_def by simp have "⋀i. i ∈ I ⟹ 𝟭⇘_{DirProds G I}⇙ i ⊗⇘_{G i}⇙ x i = x i" proof - fix i assume i: "i ∈ I" interpret group "G i" using assms[OF i] . have "x i ∈ carrier (G i)" using x i comp_in_carr by fast thus "𝟭⇘_{DirProds G I}⇙ i ⊗⇘_{G i}⇙ x i = x i" by(subst one_[OF i, symmetric]; simp) qed with one_ x show "𝟭⇘_{DirProds G I}⇙ ⊗⇘_{DirProds G I}⇙ x = x" unfolding DirProds_def by force have "restrict (λi. inv⇘_{G i}⇙ (x i)) I ∈ carrier (DirProds G I)" using x group.inv_closed[OF assms] unfolding DirProds_def by fastforce moreover have "restrict (λi. inv⇘_{G i}⇙ (x i)) I ⊗⇘_{DirProds G I}⇙ x = 𝟭⇘_{DirProds G I}⇙" using x group.l_inv[OF assms] unfolding DirProds_def by fastforce ultimately show "∃y∈carrier (DirProds G I). y ⊗⇘_{DirProds G I}⇙ x = 𝟭⇘_{DirProds G I}⇙" by blast fix y assume y: "y ∈ carrier (DirProds G I)" from DirProds_m_closed[OF x y assms] show m_closed: "x ⊗⇘_{DirProds G I}⇙ y ∈ carrier (DirProds G I)" by blast fix z assume z: "z ∈ carrier (DirProds G I)" have "⋀i. i ∈ I ⟹ (x ⊗⇘_{DirProds G I}⇙ y ⊗⇘_{DirProds G I}⇙ z) i = (x ⊗⇘_{DirProds G I}⇙ (y ⊗⇘_{DirProds G I}⇙ z)) i" proof - fix i assume i: "i ∈ I" have "(x ⊗⇘_{DirProds G I}⇙ y ⊗⇘_{DirProds G I}⇙ z) i = (x ⊗⇘_{DirProds G I}⇙ y) i ⊗⇘_{G i}⇙ z i" using assms by (simp add: comp_mult i m_closed z) also have "… = x i ⊗⇘_{G i}⇙ y i ⊗⇘_{G i}⇙ z i" by (simp add: assms comp_mult i x y) also have "… = x i ⊗⇘_{G i}⇙ (y i ⊗⇘_{G i}⇙ z i)" using i assms x y z by (meson Group.group_def comp_in_carr monoid.m_assoc) also have "… = (x ⊗⇘_{DirProds G I}⇙ (y ⊗⇘_{DirProds G I}⇙ z)) i" by (simp add: DirProds_def i) finally show "(x ⊗⇘_{DirProds G I}⇙ y ⊗⇘_{DirProds G I}⇙ z) i = (x ⊗⇘_{DirProds G I}⇙ (y ⊗⇘_{DirProds G I}⇙ z)) i" . qed thus "x ⊗⇘_{DirProds G I}⇙ y ⊗⇘_{DirProds G I}⇙ z = x ⊗⇘_{DirProds G I}⇙ (y ⊗⇘_{DirProds G I}⇙ z)" unfolding DirProds_def by auto qed lemma DirProds_obtain_elem_carr: assumes "group (DirProds G I)" "i ∈ I" "x ∈ carrier (G i)" obtains k where "k ∈ carrier (DirProds G I)" "k i = x" proof - interpret DP: group "DirProds G I" by fact from comp_in_carr[OF DP.one_closed] DirProds_one' have ao: "∀j∈I. 𝟭⇘_{G j}⇙ ∈ carrier (G j)" by metis let ?r = "restrict ((λj. 𝟭⇘_{G j}⇙)(i := x)) I" have "?r ∈ carrier (DirProds G I)" unfolding DirProds_def PiE_def Pi_def using assms(2, 3) ao by auto moreover have "?r i = x" using assms(2) by simp ultimately show "(⋀k. ⟦k ∈ carrier (DirProds G I); k i = x⟧ ⟹ thesis) ⟹ thesis" by blast qed lemma DirProds_group_imp_groups: assumes "group (DirProds G I)" and i: "i ∈ I" shows "group (G i)" proof (intro groupI) let ?DP = "DirProds G I" interpret DP: group ?DP by fact show "𝟭⇘_{G i}⇙ ∈ carrier (G i)" using DirProds_one' comp_in_carr[OF DP.one_closed i] i by metis show "x ⊗⇘_{G i}⇙ y ∈ carrier (G i)" if "x ∈ carrier (G i)" "y ∈ carrier (G i)" for x y proof - from DirProds_obtain_elem_carr[OF assms that(1)] obtain k where k: "k ∈ carrier ?DP" "k i = x" . from DirProds_obtain_elem_carr[OF assms that(2)] obtain l where l: "l ∈ carrier ?DP" "l i = y" . have "k ⊗⇘_{?DP}⇙ l ∈ carrier ?DP" using k l by fast from comp_in_carr[OF this i] comp_mult[OF i] show ?thesis using k l by metis qed show "x ⊗⇘_{G i}⇙ y ⊗⇘_{G i}⇙ z = x ⊗⇘_{G i}⇙ (y ⊗⇘_{G i}⇙ z)" if x: "x ∈ carrier (G i)" and y: "y ∈ carrier (G i)" and z: "z ∈ carrier (G i)" for x y z proof - from DirProds_obtain_elem_carr[OF assms x] obtain k where k: "k ∈ carrier ?DP" "k i = x" . from DirProds_obtain_elem_carr[OF assms y] obtain l where l: "l ∈ carrier ?DP" "l i = y" . from DirProds_obtain_elem_carr[OF assms z] obtain m where m: "m ∈ carrier ?DP" "m i = z" . have "x ⊗⇘_{G i}⇙ y ⊗⇘_{G i}⇙ z = (k i) ⊗⇘_{G i}⇙ (l i) ⊗⇘_{G i}⇙ (m i)" using k l m by argo also have "… = (k ⊗⇘_{?DP}⇙ l ⊗⇘_{?DP}⇙ m) i" using comp_mult[OF i] k l m by metis also have "… = (k ⊗⇘_{?DP}⇙ (l ⊗⇘_{?DP}⇙ m)) i" proof - have "k ⊗⇘_{?DP}⇙ l ⊗⇘_{?DP}⇙ m = k ⊗⇘_{?DP}⇙ (l ⊗⇘_{?DP}⇙ m)" using DP.m_assoc[OF k(1) l(1) m(1)] . thus ?thesis by simp qed also have "… = (k i) ⊗⇘_{G i}⇙ ((l i) ⊗⇘_{G i}⇙ (m i))" using comp_mult[OF i] k l m by metis finally show ?thesis using k l m by blast qed show "𝟭⇘_{G i}⇙ ⊗⇘_{G i}⇙ x = x" if "x ∈ carrier (G i)" for x proof - from DirProds_obtain_elem_carr[OF assms that(1)] obtain k where k: "k ∈ carrier ?DP" "k i = x" . hence "𝟭⇘_{?DP}⇙ ⊗⇘_{?DP}⇙ k = k" by simp with comp_mult k DirProds_one[OF DP.one_closed] that i show ?thesis by metis qed show "∃y∈carrier (G i). y ⊗⇘_{G i}⇙ x = 𝟭⇘_{G i}⇙" if "x ∈ carrier (G i)" for x proof - from DirProds_obtain_elem_carr[OF assms that(1)] obtain k where k: "k ∈ carrier ?DP" "k i = x" . hence ic: "inv⇘_{?DP}⇙ k ∈ carrier ?DP" by simp have "inv⇘_{?DP}⇙ k ⊗⇘_{?DP}⇙ k = 𝟭⇘_{?DP}⇙" using k by simp hence "(inv⇘_{?DP}⇙ k) i ⊗⇘_{G i}⇙ k i= 𝟭⇘_{G i}⇙" using comp_mult[OF i] DirProds_one'[OF i] by metis with k(2) comp_in_carr[OF ic i] show ?thesis by blast qed qed lemma DirProds_group_iff: "group (DirProds G I) ⟷ (∀i∈I. group (G i))" using DirProds_is_group DirProds_group_imp_groups by metis lemma comp_inv: assumes "group (DirProds G I)" and x: "x ∈ carrier (DirProds G I)" and i: "i ∈ I" shows "(inv⇘_{(DirProds G I)}⇙ x) i = inv⇘_{(G i)}⇙ (x i)" proof - interpret DP: group "DirProds G I" by fact interpret Gi: group "G i" using DirProds_group_imp_groups[OF DP.is_group i] . have ixc: "inv⇘_{(DirProds G I)}⇙ x ∈ carrier (DirProds G I)" using x by blast hence