Theory HOL-Algebra.Elementary_Groups

section ‹Elementary Group Constructions›

(*  Title:      HOL/Algebra/Elementary_Groups.thy
    Author:     LC Paulson, ported from HOL Light
*)

theory Elementary_Groups
imports Generated_Groups "HOL-Library.Infinite_Set"
begin

subsection‹Direct sum/product lemmas›

locale group_disjoint_sum = group G + AG: subgroup A G + BG: subgroup B G for G (structure) and A B
begin

lemma subset_one: "A  B  {𝟭}  A  B = {𝟭}"
  by  auto

lemma sub_id_iff: "A  B  {𝟭}  (xA. yB. x  y = 𝟭  x = 𝟭  y = 𝟭)"
        (is "?lhs = ?rhs")
proof -
  have "?lhs = (xA. yB. x  inv y = 𝟭  x = 𝟭  inv y = 𝟭)"
  proof (intro ballI iffI impI)
    fix x y
    assume "A  B  {𝟭}" "x  A" "y  B" "x  inv y = 𝟭"
    then have "y = x"
      using group.inv_equality group_l_invI by fastforce
    then show "x = 𝟭  inv y = 𝟭"
      using A  B  {𝟭} x  A y  B by fastforce
  next
    assume "xA. yB. x  inv y = 𝟭  x = 𝟭  inv y = 𝟭"
    then show "A  B  {𝟭}"
      by auto
  qed
  also have " = ?rhs"
    by (metis BG.mem_carrier BG.subgroup_axioms inv_inv subgroup_def)
  finally show ?thesis .
qed

lemma cancel: "A  B  {𝟭}  (xA. yB. x'A. y'B. x  y = x'  y'  x = x'  y = y')"
        (is "?lhs = ?rhs")
proof -
  have "(xA. yB. x  y = 𝟭  x = 𝟭  y = 𝟭) = ?rhs"
    (is "?med = _")
  proof (intro ballI iffI impI)
    fix x y x' y'
    assume * [rule_format]: "xA. yB. x  y = 𝟭  x = 𝟭  y = 𝟭"
      and AB: "x  A" "y  B" "x'  A" "y'  B" and eq: "x  y = x'  y'"
    then have carr: "x  carrier G" "x'  carrier G" "y  carrier G" "y'  carrier G"
      using AG.subset BG.subset by auto
    then have "inv x'  x  (y  inv y') = inv x'  (x  y)  inv y'"
      by (simp add: m_assoc)
    also have " = 𝟭"
      using carr  by (simp add: eq) (simp add: m_assoc)
    finally have 1: "inv x'  x  (y  inv y') = 𝟭" .
    show "x = x'  y = y'"
      using * [OF _ _ 1] AB by simp (metis carr inv_closed inv_inv local.inv_equality)
  next
    fix x y
    assume * [rule_format]: "xA. yB. x'A. y'B. x  y = x'  y'  x = x'  y = y'"
      and xy: "x  A" "y  B" "x  y = 𝟭"
    show "x = 𝟭  y = 𝟭"
      by (rule *) (use xy in auto)
  qed
  then show ?thesis
    by (simp add: sub_id_iff)
qed

lemma commuting_imp_normal1:
  assumes sub: "carrier G  A <#> B"
     and mult: "x y. x  A; y  B  x  y = y  x"
   shows "A  G"
proof -
  have AB: "A  carrier G  B  carrier G"
    by (simp add: AG.subset BG.subset)
  have "A #> x = x <# A"
    if x: "x  carrier G" for x
  proof -
    obtain a b where xeq: "x = a  b" and "a  A" "b  B" and carr: "a  carrier G" "b  carrier G"
      using x sub AB by (force simp: set_mult_def)
    have Ab: "A <#> {b} = {b} <#> A"
      using AB a  A b  B mult
      by (force simp: set_mult_def m_assoc subset_iff)
    have "A #> x = A <#> {a  b}"
      by (auto simp: l_coset_eq_set_mult r_coset_eq_set_mult xeq)
    also have " = A <#> {a} <#> {b}"
      using AB a  A b  B
      by (auto simp: set_mult_def m_assoc subset_iff)
    also have " = {a} <#> A <#> {b}"
      by (metis AG.rcos_const AG.subgroup_axioms a  A coset_join3 is_group l_coset_eq_set_mult r_coset_eq_set_mult subgroup.mem_carrier)
    also have " = {a} <#> {b} <#> A"
      by (simp add: is_group carr group.set_mult_assoc AB Ab)
    also have " = {x} <#> A"
      by (auto simp: set_mult_def xeq)
    finally show "A #> x = x <# A"
      by (simp add: l_coset_eq_set_mult)
  qed
  then show ?thesis
    by (auto simp: normal_def normal_axioms_def AG.subgroup_axioms is_group)
qed

lemma commuting_imp_normal2:
  assumes"carrier G  A <#> B"  "x y. x  A; y  B  x  y = y  x"
  shows "B  G"
proof (rule group_disjoint_sum.commuting_imp_normal1)
  show "group_disjoint_sum G B A"
  proof qed
next
  show "carrier G  B <#> A"
    using BG.subgroup_axioms assms commut_normal commuting_imp_normal1 by blast
qed (use assms in auto)


lemma (in group) normal_imp_commuting:
  assumes "A  G" "B  G" "A  B  {𝟭}" "x  A" "y  B"
  shows "x  y = y  x"
proof -
  interpret AG: normal A G
    using assms by auto
  interpret BG: normal B G
    using assms by auto
  interpret group_disjoint_sum G A B
  proof qed
  have * [rule_format]: "(xA. yB. x'A. y'B. x  y = x'  y'  x = x'  y = y')"
    using cancel assms by (auto simp: normal_def)
  have carr: "x  carrier G" "y  carrier G"
    using assms AG.subset BG.subset by auto
  then show ?thesis
    using * [of x _ _ y] AG.coset_eq [rule_format, of y] BG.coset_eq [rule_format, of x]
    by (clarsimp simp: l_coset_def r_coset_def set_eq_iff) (metis x  A y  B)
qed

lemma normal_eq_commuting:
  assumes "carrier G  A <#> B" "A  B  {𝟭}"
  shows "A  G  B  G  (xA. yB. x  y = y  x)"
  by (metis assms commuting_imp_normal1 commuting_imp_normal2 normal_imp_commuting)

lemma (in group) hom_group_mul_rev:
  assumes "(λ(x,y). x  y)  hom (subgroup_generated G A ×× subgroup_generated G B) G"
          (is "?h  hom ?P G")
   and "x  carrier G" "y  carrier G" "x  A" "y  B"
 shows "x  y = y  x"
proof -
  interpret P: group_hom ?P G ?h
    by (simp add: assms DirProd_group group_hom.intro group_hom_axioms.intro is_group)
  have xy: "(x,y)  carrier ?P"
    by (auto simp: assms carrier_subgroup_generated generate.incl)
  have "x  (x  (y  y)) = x  (y  (x  y))"
    using P.hom_mult [OF xy xy] by (simp add: m_assoc assms)
  then have "x  (y  y) = y  (x  y)"
    using assms by simp
  then show ?thesis
    by (simp add: assms flip: m_assoc)
qed

lemma hom_group_mul_eq:
   "(λ(x,y). x  y)  hom (subgroup_generated G A ×× subgroup_generated G B) G
      (xA. yB. x  y = y  x)"
         (is "?lhs = ?rhs")
proof
  assume ?lhs then show ?rhs
    using hom_group_mul_rev AG.subset BG.subset by blast
next
  assume R: ?rhs
  have subG: "generate G (carrier G  A)  carrier G" for A
    by (simp add: generate_incl)
  have *: "x  u  (y  v) = x  y  (u  v)"
    if eq [rule_format]: "xA. yB. x  y = y  x"
      and gen: "x  generate G (carrier G  A)" "y  generate G (carrier G  B)"
      "u  generate G (carrier G  A)" "v  generate G (carrier G  B)"
    for x y u v
  proof -
    have "u  y = y  u"
      by (metis AG.carrier_subgroup_generated_subgroup BG.carrier_subgroup_generated_subgroup carrier_subgroup_generated eq that(3) that(4))
    then have "x  u  y = x  y  u"
      using gen by (simp add: m_assoc subsetD [OF subG])
    then show ?thesis
      using gen by (simp add: subsetD [OF subG] flip: m_assoc)
  qed
  show ?lhs
    using R by (auto simp: hom_def carrier_subgroup_generated subsetD [OF subG] *)
qed


lemma epi_group_mul_eq:
   "(λ(x,y). x  y)  epi (subgroup_generated G A ×× subgroup_generated G B) G
      A <#> B = carrier G  (xA. yB. x  y = y  x)"
proof -
  have subGA: "generate G (carrier G  A)  A"
    by (simp add: AG.subgroup_axioms generate_subgroup_incl)
  have subGB: "generate G (carrier G  B)  B"
    by (simp add: BG.subgroup_axioms generate_subgroup_incl)
  have "(((λ(x, y). x  y) ` (generate G (carrier G  A) × generate G (carrier G  B)))) = ((A <#> B))"
    by (auto simp: set_mult_def generate.incl pair_imageI dest: subsetD [OF subGA] subsetD [OF subGB])
  then show ?thesis
    by (auto simp: epi_def hom_group_mul_eq carrier_subgroup_generated)
qed

lemma mon_group_mul_eq:
    "(λ(x,y). x  y)  mon (subgroup_generated G A ×× subgroup_generated G B) G
      A  B = {𝟭}  (xA. yB. x  y = y  x)"
proof -
  have subGA: "generate G (carrier G  A)  A"
    by (simp add: AG.subgroup_axioms generate_subgroup_incl)
  have subGB: "generate G (carrier G  B)  B"
    by (simp add: BG.subgroup_axioms generate_subgroup_incl)
  show ?thesis
    apply (auto simp: mon_def hom_group_mul_eq simp flip: subset_one)
     apply (simp_all (no_asm_use) add: inj_on_def AG.carrier_subgroup_generated_subgroup BG.carrier_subgroup_generated_subgroup)
    using cancel apply blast+
    done
qed

lemma iso_group_mul_alt:
    "(λ(x,y). x  y)  iso (subgroup_generated G A ×× subgroup_generated G B) G
      A  B = {𝟭}  A <#> B = carrier G  (xA. yB. x  y = y  x)"
  by (auto simp: iso_iff_mon_epi mon_group_mul_eq epi_group_mul_eq)

lemma iso_group_mul_eq:
    "(λ(x,y). x  y)  iso (subgroup_generated G A ×× subgroup_generated G B) G
      A  B = {𝟭}  A <#> B = carrier G  A  G  B  G"
  by (simp add: iso_group_mul_alt normal_eq_commuting cong: conj_cong)


lemma (in group) iso_group_mul_gen:
  assumes "A  G" "B  G"
  shows "(λ(x,y). x  y)  iso (subgroup_generated G A ×× subgroup_generated G B) G
      A  B  {𝟭}  A <#> B = carrier G"
proof -
  interpret group_disjoint_sum G A B
    using assms by (auto simp: group_disjoint_sum_def normal_def)
  show ?thesis
    by (simp add: subset_one iso_group_mul_eq assms)
qed


lemma iso_group_mul:
  assumes "comm_group G"
  shows "((λ(x,y). x  y)  iso (DirProd (subgroup_generated G A) (subgroup_generated G B)) G
      A  B  {𝟭}  A <#> B = carrier G)"
proof (rule iso_group_mul_gen)
  interpret comm_group
    by (rule assms)
  show "A  G"
    by (simp add: AG.subgroup_axioms subgroup_imp_normal)
  show "B  G"
    by (simp add: BG.subgroup_axioms subgroup_imp_normal)
qed

end


subsection‹The one-element group on a given object›

definition singleton_group :: "'a  'a monoid"
  where "singleton_group a = carrier = {a}, monoid.mult = (λx y. a), one = a"

lemma singleton_group [simp]: "group (singleton_group a)"
  unfolding singleton_group_def by (auto intro: groupI)

lemma singleton_abelian_group [simp]: "comm_group (singleton_group a)"
  by (metis group.group_comm_groupI monoid.simps(1) singleton_group singleton_group_def)

lemma carrier_singleton_group [simp]: "carrier (singleton_group a) = {a}"
  by (auto simp: singleton_group_def)

lemma (in group) hom_into_singleton_iff [simp]:
  "h  hom G (singleton_group a)  h  carrier G  {a}"
  by (auto simp: hom_def singleton_group_def)

declare group.hom_into_singleton_iff [simp]

lemma (in group) id_hom_singleton: "id  hom (singleton_group 𝟭) G"
  by (simp add: hom_def singleton_group_def)

subsection‹Similarly, trivial groups›

definition trivial_group :: "('a, 'b) monoid_scheme  bool"
  where "trivial_group G  group G  carrier G = {one G}"

lemma trivial_imp_finite_group:
   "trivial_group G  finite(carrier G)"
  by (simp add: trivial_group_def)

lemma trivial_singleton_group [simp]: "trivial_group(singleton_group a)"
  by (metis monoid.simps(2) partial_object.simps(1) singleton_group singleton_group_def trivial_group_def)

lemma (in group) trivial_group_subset:
   "trivial_group G  carrier G  {one G}"
  using is_group trivial_group_def by fastforce

lemma (in group) trivial_group: "trivial_group G  (a. carrier G = {a})"
  unfolding trivial_group_def using one_closed is_group by fastforce

lemma (in group) trivial_group_alt:
   "trivial_group G  (a. carrier G  {a})"
  by (auto simp: trivial_group)

lemma (in group) trivial_group_subgroup_generated:
  assumes "S  {one G}"
  shows "trivial_group(subgroup_generated G S)"
proof -
  have "carrier (subgroup_generated G S)  {𝟭}"
    using generate_empty generate_one subset_singletonD assms
    by (fastforce simp add: carrier_subgroup_generated)
  then show ?thesis
    by (simp add: group.trivial_group_subset)
qed

lemma (in group) trivial_group_subgroup_generated_eq:
  "trivial_group(subgroup_generated G s)  carrier G  s  {one G}"
  apply (rule iffI)
   apply (force simp: trivial_group_def carrier_subgroup_generated generate.incl)
  by (metis subgroup_generated_restrict trivial_group_subgroup_generated)

lemma isomorphic_group_triviality1:
  assumes "G  H" "group H" "trivial_group G"
  shows "trivial_group H"
  using assms
  by (auto simp: trivial_group_def is_iso_def iso_def group.is_monoid Group.group_def bij_betw_def hom_one)

lemma isomorphic_group_triviality:
  assumes "G  H" "group G" "group H"
  shows "trivial_group G  trivial_group H"
  by (meson assms group.iso_sym isomorphic_group_triviality1)

lemma (in group_hom) kernel_from_trivial_group:
   "trivial_group G  kernel G H h = carrier G"
  by (auto simp: trivial_group_def kernel_def)

lemma (in group_hom) image_from_trivial_group:
   "trivial_group G  h ` carrier G = {one H}"
  by (auto simp: trivial_group_def)

lemma (in group_hom) kernel_to_trivial_group:
   "trivial_group H  kernel G H h = carrier G"
  unfolding kernel_def trivial_group_def
  using hom_closed by blast


subsection‹The additive group of integers›

definition integer_group
  where "integer_group = carrier = UNIV, monoid.mult = (+), one = (0::int)"

lemma group_integer_group [simp]: "group integer_group"
  unfolding integer_group_def
proof (rule groupI; simp)
  show "x::int. y. y + x = 0"
  by presburger
qed

lemma carrier_integer_group [simp]: "carrier integer_group = UNIV"
  by (auto simp: integer_group_def)

lemma one_integer_group [simp]: "𝟭integer_group= 0"
  by (auto simp: integer_group_def)

lemma mult_integer_group [simp]: "x integer_groupy = x + y"
  by (auto simp: integer_group_def)

lemma inv_integer_group [simp]: "invinteger_groupx = -x"
  by (rule group.inv_equality [OF group_integer_group]) (auto simp: integer_group_def)

lemma abelian_integer_group: "comm_group integer_group"
  by (rule group.group_comm_groupI [OF group_integer_group]) (auto simp: integer_group_def)

lemma group_nat_pow_integer_group [simp]:
  fixes n::nat and x::int
  shows "pow integer_group x n = int n * x"
  by (induction n) (auto simp: integer_group_def algebra_simps)

lemma group_int_pow_integer_group [simp]:
  fixes n::int and x::int
  shows "pow integer_group x n = n * x"
  by (simp add: int_pow_def2)

lemma (in group) hom_integer_group_pow:
   "x  carrier G  pow G x  hom integer_group G"
  by (rule homI) (auto simp: int_pow_mult)

subsection‹Additive group of integers modulo n (n = 0 gives just the integers)›

definition integer_mod_group :: "nat  int monoid"
  where
  "integer_mod_group n 
     if n = 0 then integer_group
     else carrier = {0..<int n}, monoid.mult = (λx y. (x+y) mod int n), one = 0"

lemma carrier_integer_mod_group:
  "carrier(integer_mod_group n) = (if n=0 then UNIV else {0..<int n})"
  by (simp add: integer_mod_group_def)

lemma one_integer_mod_group[simp]: "one(integer_mod_group n) = 0"
  by (simp add: integer_mod_group_def)

lemma mult_integer_mod_group[simp]: "monoid.mult(integer_mod_group n) = (λx y. (x + y) mod int n)"
  by (simp add: integer_mod_group_def integer_group_def)

lemma group_integer_mod_group [simp]: "group (integer_mod_group n)"
proof -
  have *: "y0. y < int n  (y + x) mod int n = 0" if "x < int n" "0  x" for x
  proof (cases "x=0")
    case False
    with that show ?thesis
      by (rule_tac x="int n - x" in exI) auto
  qed (use that in auto)
  show ?thesis
    apply (rule groupI)
        apply (auto simp: integer_mod_group_def Bex_def *, presburger+)
    done
qed

lemma inv_integer_mod_group[simp]:
  "x  carrier (integer_mod_group n)  m_inv(integer_mod_group n) x = (-x) mod int n"
  by (rule group.inv_equality [OF group_integer_mod_group]) (auto simp: integer_mod_group_def add.commute mod_add_right_eq)


lemma pow_integer_mod_group [simp]:
  fixes m::nat
  shows "pow (integer_mod_group n) x m = (int m * x) mod int n"
proof (cases "n=0")
  case False
  show ?thesis
    by (induction m) (auto simp: add.commute mod_add_right_eq distrib_left mult.commute)
qed (simp add: integer_mod_group_def)

lemma int_pow_integer_mod_group:
  "pow (integer_mod_group n) x m = (m * x) mod int n"
proof -
  have "invinteger_mod_group n(- (m * x) mod int n) = m * x mod int n"
    by (simp add: carrier_integer_mod_group mod_minus_eq)
  then show ?thesis
    by (simp add: int_pow_def2)
qed

lemma abelian_integer_mod_group [simp]: "comm_group(integer_mod_group n)"
  by (simp add: add.commute group.group_comm_groupI)

lemma integer_mod_group_0 [simp]: "0  carrier(integer_mod_group n)"
  by (simp add: integer_mod_group_def)

lemma integer_mod_group_1 [simp]: "1  carrier(integer_mod_group n)  (n  1)"
  by (auto simp: integer_mod_group_def)

lemma trivial_integer_mod_group: "trivial_group(integer_mod_group n)  n = 1"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
  by (simp add: trivial_group_def carrier_integer_mod_group set_eq_iff split: if_split_asm) (presburger+)
next
  assume ?rhs
  then show ?lhs
    by (force simp: trivial_group_def carrier_integer_mod_group)
qed


subsection‹Cyclic groups›

lemma (in group) subgroup_of_powers:
  "x  carrier G  subgroup (range (λn::int. x [^] n)) G"
  apply (auto simp: subgroup_def image_iff simp flip: int_pow_mult int_pow_neg)
  apply (metis group.int_pow_diff int_pow_closed is_group r_inv)
  done

lemma (in group) carrier_subgroup_generated_by_singleton:
  assumes "x  carrier G"
  shows "carrier(subgroup_generated G {x}) = (range (λn::int. x [^] n))"
proof
  show "carrier (subgroup_generated G {x})  range (λn::int. x [^] n)"
  proof (rule subgroup_generated_minimal)
    show "subgroup (range (λn::int. x [^] n)) G"
      using assms subgroup_of_powers by blast
    show "{x}  range (λn::int. x [^] n)"
      by clarify (metis assms int_pow_1 range_eqI)
  qed
  have x: "x  carrier (subgroup_generated G {x})"
    using assms subgroup_generated_subset_carrier_subset by auto
  show "range (λn::int. x [^] n)  carrier (subgroup_generated G {x})"
  proof clarify
    fix n :: "int"
    show "x [^] n  carrier (subgroup_generated G {x})"
        by (simp add: x subgroup_int_pow_closed subgroup_subgroup_generated)
  qed
qed


definition cyclic_group
  where "cyclic_group G  x  carrier G. subgroup_generated G {x} = G"

lemma (in group) cyclic_group:
  "cyclic_group G  (x  carrier G. carrier G = range (λn::int. x [^] n))"
proof -
  have "x. x  carrier G; carrier G = range (λn::int. x [^] n)
          xcarrier G. subgroup_generated G {x} = G"
    by (rule_tac x=x in bexI) (auto simp: generate_pow subgroup_generated_def intro!: monoid.equality)
  then show ?thesis
    unfolding cyclic_group_def
    using carrier_subgroup_generated_by_singleton by fastforce
qed

lemma cyclic_integer_group [simp]: "cyclic_group integer_group"
proof -
  have *: "int n  generate integer_group {1}" for n
  proof (induction n)
    case 0
    then show ?case
    using generate.simps by force
  next
    case (Suc n)
    then show ?case
    by simp (metis generate.simps insert_subset integer_group_def monoid.simps(1) subsetI)
  qed
  have **: "i  generate integer_group {1}" for i
  proof (cases i rule: int_cases)
    case (nonneg n)
    then show ?thesis
      by (simp add: *)
  next
    case (neg n)
    then have "-i  generate integer_group {1}"
      by (metis "*" add.inverse_inverse)
    then have "- (-i)  generate integer_group {1}"
      by (metis UNIV_I group.generate_m_inv_closed group_integer_group integer_group_def inv_integer_group partial_object.select_convs(1) subsetI)
    then show ?thesis
      by simp
  qed
  show ?thesis
    unfolding cyclic_group_def
    by (rule_tac x=1 in bexI)
       (auto simp: carrier_subgroup_generated ** intro: monoid.equality)
qed

lemma nontrivial_integer_group [simp]: "¬ trivial_group integer_group"
  using integer_mod_group_def trivial_integer_mod_group by presburger


lemma (in group) cyclic_imp_abelian_group:
  "cyclic_group G  comm_group G"
  apply (auto simp: cyclic_group comm_group_def is_group intro!: monoid_comm_monoidI)
  apply (metis add.commute int_pow_mult rangeI)
  done

lemma trivial_imp_cyclic_group:
   "trivial_group G  cyclic_group G"
  by (metis cyclic_group_def group.subgroup_generated_group_carrier insertI1 trivial_group_def)

lemma (in group) cyclic_group_alt:
   "cyclic_group G  (x. subgroup_generated G {x} = G)"
proof safe
  fix x
  assume *: "subgroup_generated G {x} = G"
  show "cyclic_group G"
  proof (cases "x  carrier G")
    case True
    then show ?thesis
      using subgroup_generated G {x} = G cyclic_group_def by blast
  next
    case False
    then show ?thesis
      by (metis "*" Int_empty_right Int_insert_right_if0 carrier_subgroup_generated generate_empty trivial_group trivial_imp_cyclic_group)
  qed
qed (auto simp: cyclic_group_def)

lemma (in group) cyclic_group_generated:
  "cyclic_group (subgroup_generated G {x})"
  using group.cyclic_group_alt group_subgroup_generated subgroup_generated2 by blast

lemma (in group) cyclic_group_epimorphic_image:
  assumes "h  epi G H" "cyclic_group G" "group H"
  shows "cyclic_group H"
proof -
  interpret h: group_hom
    using assms
    by (simp add: group_hom_def group_hom_axioms_def is_group epi_def)
  obtain x where "x  carrier G" and x: "carrier G = range (λn::int. x [^] n)" and eq: "carrier H = h ` carrier G"
    using assms by (auto simp: cyclic_group epi_def)
  have "h ` carrier G = range (λn::int. h x [^]Hn)"
    by (metis (no_types, lifting) x  carrier G h.hom_int_pow image_cong image_image x)
  then show ?thesis
    using x  carrier G eq h.cyclic_group by blast
qed

lemma isomorphic_group_cyclicity:
   "G  H; group G; group H  cyclic_group G  cyclic_group H"
  by (meson ex_in_conv group.cyclic_group_epimorphic_image group.iso_sym is_iso_def iso_iff_mon_epi)


end