(* 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