Theory Generators

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 
general place. It defines the subgroup generated by a set of generators and
that homomorphisms agree on the generated subgroup if they agree on the
generators.›

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
be defined inductively or as the intersection of all subgroups containing the
generators. 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]: "𝟭⇘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)
qed

lemma (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 "⋂{H. H ≤ G ∧ gens ⊆ H} = ⟨gens⟩⇘G⇙"
proof
  show "⟨gens⟩⇘G⇙ ⊆ ⋂{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
  qed
next
  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 "⋂{H. H ≤ G ∧ gens ⊆ H} ⊆ ⟨gens⟩⇘G⇙"
    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⟩⇘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 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
generating 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 auto
qed

lemma (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 simp
next
  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)
qed


subsection ‹Product of a list of group elements›

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

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

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
isomorphism.›

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 auto
qed

lemma (in group_hom) hom_injI:
  assumes "∀x∈carrier G. h x = 𝟭⇘H⇙ ⟶ x = 𝟭⇘G⇙"
  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) = 𝟭⇘H⇙" and "x ⊗ inv y ∈ carrier G"
    by auto
  with assms
  have "x ⊗ inv y = 𝟭" 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 = 𝟭⇘H⇙ ⟶ x = 𝟭⇘G⇙"
      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 = 𝟭⇘H⇙ ⟶ x = 𝟭⇘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 ∈ 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