Quelle  Generators.thy

section ‹Generators›

theory "Generators"
imports
   "HOL-Algebra.Group"
   "HOL-Algebra.Lattice"
begin


text ‹This theory is not specific to Free Groups and could be moved to a more
  place. It defines the subgroup generated by a set of generators and
  homomorphisms agree on the generated subgroup if they agree on the
 .›

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, can
  defined inductively or as the intersection of all subgroups containing the
 . Here, we define it inductively and proof the equivalence›

inductive_set gen_span :: "('a,'b) monoid_scheme ==> 'a set ==> 'a set" (‹⟨_⟩🍋›)
  for G and gens
where gen_one [intro!, simp]: "1 ∈ ⟨gens⟩"
    | gen_gens: "x ∈ gens ==> x ∈ ⟨gens⟩"
    | gen_inv: "x ∈ ⟨gens⟩ ==> inv x ∈ ⟨gens⟩"
    | gen_mult: "[ x ∈ ⟨gens⟩; y ∈ ⟨gens⟩ ] ==> x ⊗ y ∈ ⟨gens⟩"

lemma (in group) gen_span_closed:
  assumes "gens ⊆ carrier G"
  shows "⟨gens⟩ ⊆ carrier G"
proof (* How can I do this in one "by" line? *)
  fix x
  from assms show "x ∈ ⟨gens⟩ ==> x ∈ carrier G"
    by -(induct rule:gen_span.induct, auto)
qed

lemma (in group) gen_subgroup_is_subgroup: 
      "gens ⊆ carrier G ==> ⟨gens⟩ ≤ 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 "∩{H. H ≤ G ∧ gens ⊆ H} = ⟨gens⟩"
proof
  show "⟨gens⟩ ⊆ ∩{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⟩ ⊆ H"
    proof
      fix x
      from ‹H ≤ G› and ‹gens ⊆ H›
      show "x ∈ ⟨gens⟩ ==> x ∈ H"
       unfolding subgroup_def
       by -(induct rule:gen_span.induct, auto)
    qed
  qed
next
  from ‹gens ⊆ carrier G›
  have "⟨gens⟩ ≤ G" by (rule gen_subgroup_is_subgroup)
  moreover
  have "gens ⊆ ⟨gens⟩" by (auto intro:gen_span.intros)
  ultimately
  show "∩{H. H ≤ G ∧ gens ⊆ H} ⊆ ⟨gens⟩"
    by(auto intro:Inter_lower)
qed

subsection ‹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⟩. 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⟩ ⊆ carrier G" by (rule G.gen_span_closed)
  with assms show "x ∈ ⟨gens⟩ ==> 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 ⊗ y) = h' (x ⊗ y)" by simp
  qed auto
qed

subsection ‹Sets of generators›

text ‹There is no definition for ``‹gens› is a generating set of
 ‹G›''. This is easily expressed by ‹⟨gens⟩ = carrier G›.›

text ‹The following is an application of ‹hom_unique_on_span› on a
  set of the whole group.›

lemma (in group) hom_unique_by_gens:
  assumes "group H"
      and gens: "⟨gens⟩ = 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⟩. h x = h' x"
    by -(erule hom_unique_on_span, auto)
  with gens show "x ∈ carrier G ==> h x = h' x" by auto
qed

lemma (in group_hom) hom_span:
  assumes "gens ⊆ carrier G"
  shows "h ` (⟨gens⟩) = ⟨h ` gens⟩"
proof(rule Set.set_eqI, rule iffI)
  from ‹gens ⊆ carrier G›
  have "⟨gens⟩ ⊆ carrier G" by (rule G.gen_span_closed)

  fix y
  assume "y ∈ h ` ⟨gens⟩"
  then obtain x where "x ∈ ⟨gens⟩" and "y = h x" by auto
  from ‹x ∈ ⟨gens⟩›
  have "h x ∈ ⟨h ` gens⟩"
  proof(induct x)
    case (gen_inv x)
    hence "x ∈ carrier G" and "h x ∈ ⟨h ` gens⟩"
      using ‹⟨gens⟩ ⊆ 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⟩"
    and   "y ∈ carrier G" and "h y ∈ ⟨h ` gens⟩"
      using ‹⟨gens⟩ ⊆ 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⟩" by simp
next
  fix x
  show "x ∈ ⟨h ` gens⟩ ==> 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)
qed


subsection ‹Product of a list of group elements›

text ‹Not strictly related to generators of groups, this is still a general
  concept and not related to Free Groups.›

abbreviation (in monoid) m_concat
  where "m_concat l ≡ foldr (⊗) l 1"

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 assms
by(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" .
qed

lemma (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 or
 .›

lemma group_homI[intro]:
  assumes range: "h ` (carrier g1) ⊆ carrier g2"
      and hom: "∀x∈carrier g1. ∀y∈carrier g1. h (x ⊗ y) = h x ⊗ 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 auto
qed

lemma (in group_hom) hom_injI:
  assumes "∀x∈carrier G. h x = 1 ⟶ x = 1"
  shows "inj_on h (carrier G)"
unfolding inj_on_def
proof(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) = 1" and "x ⊗ inv y ∈ carrier G"
    by auto
  with assms
  have "x ⊗ inv y = 1" by auto
  thus "x = y" using x and y 
    by(auto dest: G.inv_equality)
qed

lemma (in group_hom) group_hom_isoI:
  assumes inj1: "∀x∈carrier G. h x = 1 ⟶ x = 1"
      and surj: "h ` (carrier G) = carrier H"
  shows "h ∈ iso 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 ?thesis
    unfolding iso_def by auto
qed

lemma group_isoI[intro]:
  assumes G: "group G"
      and H: "group H"
      and inj1: "∀x∈carrier G. h x = 1 ⟶ x = 1"
      and surj: "h ` (carrier G) = carrier H"
      and hom: "∀x∈carrier G. ∀y∈carrier G. h (x ⊗ y) = h x ⊗ h y"
  shows "h ∈ iso 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)
qed
end