# Theory Generators

Up to index of Isabelle/HOL/Free-Groups

theory Generators
imports Group
`header {* Generators *}theory "Generators"imports   "~~/src/HOL/Algebra/Group"   "~~/src/HOL/Algebra/Lattice"begintext {* This theory is not specific to Free Groups and could be moved to a more general place. It defines the subgroup generated by a set of generators andthat homomorphisms agree on the generated subgroup if they agree on thegenerators. *}notation subgroup (infix "≤" 80)subsection {* The subgroup generated by a set *}text {* The span of a set of subgroup generators, i.e. the generated subgroup, canbe defined inductively or as the intersection of all subgroups containing thegenerators. Here, we define it inductively and proof the equivalence *}inductive_set gen_span :: "('a,'b) monoid_scheme => 'a set => 'a set" ("⟨_⟩\<index>")  for G and genswhere gen_one [intro!, simp]: "\<one>⇘G⇙ ∈ ⟨gens⟩⇘G⇙"    | gen_gens: "x ∈ gens ==> x ∈ ⟨gens⟩⇘G⇙"    | gen_inv: "x ∈ ⟨gens⟩⇘G⇙ ==> inv⇘G⇙ x ∈ ⟨gens⟩⇘G⇙"    | gen_mult: "[| x ∈ ⟨gens⟩⇘G⇙; y ∈ ⟨gens⟩⇘G⇙ |] ==>  x ⊗⇘G⇙ y ∈ ⟨gens⟩⇘G⇙"lemma (in group) gen_span_closed:  assumes "gens ⊆ carrier G"  shows "⟨gens⟩⇘G⇙ ⊆ carrier G"proof (* How can I do this in one "by" line? *)  fix x  from assms show "x ∈ ⟨gens⟩⇘G⇙ ==> x ∈ carrier G"    by -(induct rule:gen_span.induct, auto)qedlemma (in group) gen_subgroup_is_subgroup:       "gens ⊆ carrier G ==> ⟨gens⟩⇘G⇙ ≤ G"by(rule subgroupI)(auto intro:gen_span.intros simp add:gen_span_closed)lemma (in group) gen_subgroup_is_smallest_containing:  assumes "gens ⊆ carrier G"    shows "\<Inter>{H. H ≤ G ∧ gens ⊆ H} = ⟨gens⟩⇘G⇙"proof  show "⟨gens⟩⇘G⇙ ⊆ \<Inter>{H. H ≤ G ∧ gens ⊆ H}"  proof(rule Inf_greatest)    fix H    assume "H ∈ {H. H ≤ G ∧ gens ⊆ H}"    hence "H ≤ G" and "gens ⊆ H" by auto    show "⟨gens⟩⇘G⇙ ⊆ H"    proof      fix x      from `H ≤ G` and `gens ⊆ H`      show "x ∈ ⟨gens⟩⇘G⇙ ==> x ∈ H"       unfolding subgroup_def       by -(induct rule:gen_span.induct, auto)    qed  qednext  from `gens ⊆ carrier G`  have "⟨gens⟩⇘G⇙ ≤ G" by (rule gen_subgroup_is_subgroup)  moreover  have "gens ⊆ ⟨gens⟩⇘G⇙" by (auto intro:gen_span.intros)  ultimately  show "\<Inter>{H. H ≤ G ∧ gens ⊆ H} ⊆ ⟨gens⟩⇘G⇙"    by(auto intro:Inter_lower)qedsubsection {* Generators and homomorphisms *}text {* Two homorphisms agreeing on some elements agree on the span of those elements.*}lemma hom_unique_on_span:  assumes "group G"      and "group H"      and "gens ⊆ carrier G"      and "h ∈ hom G H"      and "h' ∈ hom G H"      and "∀g ∈ gens. h g = h' g"  shows "∀x ∈ ⟨gens⟩⇘G⇙. h x = h' x"proof  interpret G: group G by fact  interpret H: group H by fact  interpret h: group_hom G H h by unfold_locales fact  interpret h': group_hom G H h' by unfold_locales fact  fix x  from `gens ⊆ carrier G` have "⟨gens⟩⇘G⇙ ⊆ carrier G" by (rule G.gen_span_closed)  with assms show "x ∈ ⟨gens⟩⇘G⇙ ==> h x = h' x" apply -  proof(induct rule:gen_span.induct)    case (gen_mult x y)      hence x: "x ∈ carrier G" and y: "y ∈ carrier G" and            hx: "h x = h' x" and hy: "h y = h' y" by auto      thus "h (x ⊗⇘G⇙ y) = h' (x ⊗⇘G⇙ y)" by simp  qed autoqedsubsection {* Sets of generators *}text {* There is no definition for ``@{text gens} is a generating set of@{text G}''. This is easily expressed by @{text "⟨gens⟩ = carrier G"}. *}text {* The following is an application of @{text hom_unique_on_span} on agenerating set of the whole group. *}lemma (in group) hom_unique_by_gens:  assumes "group H"      and gens: "⟨gens⟩⇘G⇙ = carrier G"      and "h ∈ hom G H"      and "h' ∈ hom G H"      and "∀g ∈ gens. h g = h' g"  shows "∀x ∈ carrier G. h x = h' x"proof  fix x  from gens have "gens ⊆ carrier G" by (auto intro:gen_span.gen_gens)  with assms and group_axioms have r: "∀x ∈ ⟨gens⟩⇘G⇙. h x = h' x"    by -(erule hom_unique_on_span, auto)  with gens show "x ∈ carrier G ==> h x = h' x" by autoqedlemma (in group_hom) hom_span:  assumes "gens ⊆ carrier G"  shows "h ` (⟨gens⟩⇘G⇙) = ⟨h ` gens⟩⇘H⇙"proof(rule Set.set_eqI, rule iffI)  from `gens ⊆ carrier G`  have "⟨gens⟩⇘G⇙ ⊆ carrier G" by (rule G.gen_span_closed)  fix y  assume "y ∈ h ` ⟨gens⟩⇘G⇙"  then obtain x where "x ∈ ⟨gens⟩⇘G⇙" and "y = h x" by auto  from `x ∈ ⟨gens⟩⇘G⇙`  have "h x ∈ ⟨h ` gens⟩⇘H⇙"  proof(induct x)    case (gen_inv x)    hence "x ∈ carrier G" and "h x ∈ ⟨h ` gens⟩⇘H⇙"      using `⟨gens⟩⇘G⇙ ⊆ carrier G`      by auto    thus ?case by (auto intro:gen_span.intros)  next    case (gen_mult x y)    hence "x ∈ carrier G" and "h x ∈ ⟨h ` gens⟩⇘H⇙"    and   "y ∈ carrier G" and "h y ∈ ⟨h ` gens⟩⇘H⇙"      using `⟨gens⟩⇘G⇙ ⊆ carrier G`      by auto    thus ?case by (auto intro:gen_span.intros)  qed(auto intro: gen_span.intros)  with `y = h x`  show "y ∈ ⟨h ` gens⟩⇘H⇙" by simpnext  fix x  show "x ∈ ⟨h ` gens⟩⇘H⇙ ==> x ∈ h ` ⟨gens⟩"  proof(induct x rule:gen_span.induct)    case (gen_inv y)      then  obtain x where "y = h x" and "x ∈ ⟨gens⟩" by auto      moreover      hence "x ∈ carrier G"  using `gens ⊆ carrier G`         by (auto dest:G.gen_span_closed)      ultimately show ?case         by (auto intro:hom_inv[THEN sym] rev_image_eqI gen_span.gen_inv simp del:group_hom.hom_inv hom_inv)  next   case (gen_mult y y')      then  obtain x and x'        where "y = h x" and "x ∈ ⟨gens⟩"        and "y' = h x'" and "x' ∈ ⟨gens⟩" by auto      moreover      hence "x ∈ carrier G" and "x' ∈ carrier G" using `gens ⊆ carrier G`         by (auto dest:G.gen_span_closed)      ultimately show ?case        by (auto intro:hom_mult[THEN sym] rev_image_eqI gen_span.gen_mult simp del:group_hom.hom_mult hom_mult)  qed(auto intro:rev_image_eqI intro:gen_span.intros)qedsubsection {* Product of a list of group elements *}text {* Not strictly related to generators of groups, this is still a generalgroup concept and not related to Free Groups. *}abbreviation (in monoid) m_concat  where "m_concat l ≡ foldr (op ⊗) l \<one>"lemma (in monoid) m_concat_closed[simp]: "set l ⊆ carrier G ==> m_concat l ∈ carrier G"  by (induct l, auto)lemma (in monoid) m_concat_append[simp]:  assumes "set a ⊆ carrier G"      and "set b ⊆ carrier G"  shows "m_concat (a@b) = m_concat a ⊗ m_concat b"using assmsby(induct a)(auto simp add: m_assoc)lemma (in monoid) m_concat_cons[simp]:  "[| x ∈ carrier G ; set xs ⊆ carrier G |] ==> m_concat (x#xs) = x ⊗ m_concat xs"by(induct xs)(auto simp add: m_assoc)lemma (in monoid) nat_pow_mult1l:  assumes x: "x ∈ carrier G"  shows "x ⊗ x (^) n = x (^) Suc n"proof-  have "x ⊗ x (^) n = x (^) (1::nat) ⊗ x (^) n " using x by auto  also have "… = x (^) (1 + n)" using x        by (auto dest:nat_pow_mult simp del:One_nat_def)  also have "… = x (^) Suc n" by simp  finally show "x ⊗ x (^) n = x (^) Suc n" .qedlemma (in monoid) m_concat_power[simp]: "x ∈ carrier G ==> m_concat (replicate n x) = x (^) n"by(induct n, auto simp add:nat_pow_mult1l)subsection {* Isomorphisms *}text {* A nicer way of proving that something is a group homomorphism orisomorphism. *}lemma group_homI[intro]:  assumes range: "h ` (carrier g1) ⊆ carrier g2"      and hom: "∀x∈carrier g1. ∀y∈carrier g1. h (x ⊗⇘g1⇙ y) = h x ⊗⇘g2⇙ h y"  shows "h ∈ hom g1 g2"proof-  have "h ∈ carrier g1 -> carrier g2" using range  by auto  thus "h ∈ hom g1 g2" using hom unfolding hom_def by autoqedlemma (in group_hom) hom_injI:  assumes "∀x∈carrier G. h x = \<one>⇘H⇙ --> x = \<one>⇘G⇙"  shows "inj_on h (carrier G)"unfolding inj_on_defproof(rule ballI, rule ballI, rule impI)  fix x  fix y  assume x: "x∈carrier G"     and y: "y∈carrier G"     and "h x = h y"  hence "h (x ⊗ inv y) = \<one>⇘H⇙" and "x ⊗ inv y ∈ carrier G"    by auto  with assms  have "x ⊗ inv y = \<one>" by auto  thus "x = y" using x and y     by(auto dest: G.inv_equality)qedlemma (in group_hom) group_hom_isoI:  assumes inj1: "∀x∈carrier G. h x = \<one>⇘H⇙ --> x = \<one>⇘G⇙"      and surj: "h ` (carrier G) = carrier H"  shows "h ∈ G ≅ H"proof-  from inj1  have "inj_on h (carrier G)"     by(auto intro: hom_injI)  hence bij: "bij_betw h (carrier G) (carrier H)"    using surj  unfolding bij_betw_def by auto  thus "h ∈ G ≅ H"    unfolding iso_def by autoqedlemma group_isoI[intro]:  assumes G: "group G"      and H: "group H"      and inj1: "∀x∈carrier G. h x = \<one>⇘H⇙ --> x = \<one>⇘G⇙"      and surj: "h ` (carrier G) = carrier H"      and hom: "∀x∈carrier G. ∀y∈carrier G. h (x ⊗⇘G⇙ y) = h x ⊗⇘H⇙ h y"  shows "h ∈ G ≅ H"proof-  from surj  have "h ∈ carrier G -> carrier H"    by auto  then interpret group_hom G H h using G and H and hom    by (auto intro!: group_hom.intro group_hom_axioms.intro)  show ?thesis  using assms unfolding hom_def by (auto intro: group_hom_isoI)qedend`