(* Title: Rank_Exercise.thy Author: Clara L\"oh *) text \We introduce the rank of finitely generated groups and prove subadditivity for products.\ theory Rank_Exercise imports Complex_Main "HOL-Algebra.Generated_Groups" Product_GenSet (*of course, it would be cleaner to have is_fin_gen_set_of in a different location, but we keep it like this for now for backwards compatibility*) begin section \Ranks of finitely generated groups\ text \The rank of a (finitely generated) group is the minimal size of a generating set, i.e., the least element of the set of all natural numbers that occur as cardinalities of finite generating sets of the given group.\ definition fin_gen_sets_of :: "('a,_) monoid_scheme => 'a set set" where "fin_gen_sets_of G = { S | S . is_fin_gen_set_of G S }" definition is_finitely_generated :: "('a,_) monoid_scheme => bool" where "is_finitely_generated G = (fin_gen_sets_of G ~= {})" definition cards_of_fin_gen_sets_of :: "('a,_) monoid_scheme => nat set" where "cards_of_fin_gen_sets_of G = { card S | S . S \ fin_gen_sets_of G }" definition is_card_of_fin_gen_set_of :: "('a,_) monoid_scheme => nat => bool" where "is_card_of_fin_gen_set_of G c = (c \ cards_of_fin_gen_sets_of G)" definition rank :: "('a,_) monoid_scheme => nat" where "rank G = Least (is_card_of_fin_gen_set_of G)" section \Basic facts on ranks of graoups\ text \Every finite generating set gives an upper bound for the rank:\ lemma rank_le_I: fixes G :: "('a,_) monoid_scheme" and S assumes S_fin_gen: "is_fin_gen_set_of G S" shows "rank G <= card S" proof - have "card S \ cards_of_fin_gen_sets_of G" proof - have "S \ fin_gen_sets_of G" using S_fin_gen fin_gen_sets_of_def by auto then show ?thesis using cards_of_fin_gen_sets_of_def by auto qed then show ?thesis using rank_def[of G] is_card_of_fin_gen_set_of_def Least_le[of "is_card_of_fin_gen_set_of G"] (* Orderings wellorder_Least_lemma *) by auto qed text \In a finitely generated group, there always exists a finite generating set whose cardinality equals the rank:\ lemma optimal_gen_set_ex: fixes G :: "('a,_) monoid_scheme" assumes G_is_group: "group G" and G_is_fingen: "is_finitely_generated G" shows "\ S. is_fin_gen_set_of G S \ card S = rank G" proof - text \We show first that the rank occurs as cardinality of a finite generating set of the group; in order to do that we have to establish that the set of cardinalities of finite generating sets is non-empty.\ have "\ c. is_card_of_fin_gen_set_of G c" proof - (* Complete this proof *) qed then obtain c where c_card: "is_card_of_fin_gen_set_of G c" by auto text \We then only need to pick an associated finite generating set.\ have "is_card_of_fin_gen_set_of G (rank G)" using c_card rank_def[of G] LeastI_ex by auto then have "rank G \ cards_of_fin_gen_sets_of G" using is_card_of_fin_gen_set_of_def by auto then obtain S where "S \ fin_gen_sets_of G \ card S = rank G" using cards_of_fin_gen_sets_of_def[of G] by auto then have "is_fin_gen_set_of G S \ card S = rank G" using fin_gen_sets_of_def[of G] by auto then show ?thesis by auto qed section \Subadditivity of ranks of products\ text \The rank of groups is subadditive with respect to taking product groups. As a preparation, we already established how generating sets of the factors can be combined into a generating set of the product group. We will now first have a closer look at the sizes of these sets. Finally, we will use this size estimate to prove subadditivity of the rank.\ lemma gen_sets_product_size: fixes G :: "('a, _) monoid_scheme" and H :: "('b, _) monoid_scheme" and S T ST assumes G_is_group: "group G" and H_is_group: "group H" and S_gen_G: "is_fin_gen_set_of G S" and T_gen_H: "is_fin_gen_set_of H T" and ST_def: "ST = { (g, one H) | g . g \ S} \ {(one G, h) | h . h \ T }" shows "card ST <= card S + card T" proof - (* Setup for the three groups G, H, and the product group *) interpret H: group H using H_is_group by simp interpret G: group G using G_is_group by simp text \We write \ST\ as a union of images of \S\ and \T\. We can then use monotonicity of cardinality under maps and subadditivity of the cardinality of unions to prove the claimed estimate.\ define Se where "Se = { (g, one H) | g. g \ S }" define eT where "eT = { (one G, h) | h. h \ T }" have ST_Se_eT: "ST = Se \ eT" using ST_def Se_def eT_def by simp have Se_card: "card Se <= card S" proof - define i_1 where "i_1 = (\ x :: 'a. (x, one H))" have Se_img_i_1: "Se = i_1 ` S" using Se_def i_1_def image_def by auto have S_finite: "finite S" using S_gen_G is_fin_gen_set_of_def by auto then show ?thesis using Se_img_i_1 card_image_le by simp (* monotonicity of cardinality under maps: Finite_Set card_image_le *) qed have eT_card: "card eT <= card T" proof - (* Complete this proof *) qed then show ?thesis proof - have "card ST <= card Se + card eT" using ST_Se_eT card_Un_le by simp then show "card ST <= card S + card T" using Se_card eT_card by simp qed qed theorem rank_product_subadditivity: fixes G H assumes G_is_group: "group G" and G_is_fingen: "is_finitely_generated G" and H_is_group: "group H" and H_is_fingen: "is_finitely_generated H" shows "rank (DirProd G H) <= rank G + rank H" proof - (* Setup for the three groups G, H, and the product group *) interpret H: group H using H_is_group by simp interpret G: group G using G_is_group by simp define GH where "GH = DirProd G H" have GH_is_group: "group GH" using GH_def G_is_group H_is_group DirProd_group by auto interpret GH: group GH using GH_is_group GH_def by simp text \We pick optimal generating sets and combine them into a generating set of the product\ from G_is_fingen obtain S where S_gen_G: "is_fin_gen_set_of G S \ card S = rank G" using optimal_gen_set_ex[of G] by auto from H_is_fingen obtain T where T_gen_H: "is_fin_gen_set_of H T \ card T = rank H" using optimal_gen_set_ex[of H] by auto define ST where "ST = { (g, one H) | g . g \ S} \ {(one G, h) | h . h \ T }" text \The previous lemmas now allow us to conclude:\ (* Complete this proof *) qed end