Theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups

(*
    File:     Miscellaneous_Groups.thy
    Author:   Joseph Thommes, TU München
*)
section ‹Miscellaneous group facts›

theory Miscellaneous_Groups
  imports Set_Multiplication
begin

text ‹As the name suggests, this section contains several smaller lemmas about groups.›

(* Manuel Eberl *)
lemma (in subgroup) nat_pow_closed [simp,intro]: "a  H  pow G a (n::nat)  H"
  by (induction n) (auto simp: nat_pow_def)

(* Manuel Eberl *)
lemma nat_pow_modify_carrier: "a [^]Gcarrier := Hb = a [^]G(b::nat)"
  by (simp add: nat_pow_def)

lemma (in group) subgroup_card_dvd_group_ord:
  assumes "subgroup H G"
  shows "card H dvd order G"
  using Coset.group.lagrange[of G H] assms group_axioms by (metis dvd_triv_right)

lemma (in group) subgroup_card_eq_order:
  assumes "subgroup H G"
  shows "card H = order (Gcarrier := H)"
  unfolding order_def by simp

lemma (in group) finite_subgroup_card_neq_0:
  assumes "subgroup H G" "finite H"
  shows "card H  0"
  using subgroup_nonempty assms by auto

lemma (in group) subgroup_order_dvd_group_order:
  assumes "subgroup H G"
  shows "order (Gcarrier := H) dvd order G"
  by (metis subgroup_card_dvd_group_ord[of H] assms subgroup_card_eq_order)

lemma (in group) sub_subgroup_dvd_card:
  assumes "subgroup H G" "subgroup J G" "J  H"
  shows "card J dvd card H"
  by (metis subgroup_incl[of J H] subgroup_card_eq_order[of H]
            group.subgroup_card_dvd_group_ord[of "(Gcarrier := H)" J] assms
            subgroup.subgroup_is_group[of H G] group_axioms)

lemma (in group) inter_subgroup_dvd_card:
  assumes "subgroup H G" "subgroup J G"
  shows "card (H  J) dvd card H"
  using subgroups_Inter_pair[of H J] assms sub_subgroup_dvd_card[of H "H  J"] by blast

lemma (in group) subgroups_card_coprime_inter_card_one:
  assumes "subgroup H G" "subgroup J G" "coprime (card H) (card J)"
  shows "card (H  J) = 1"
proof -
  from assms inter_subgroup_dvd_card have "is_unit (card (H  J))" unfolding coprime_def
    by (metis assms(3) coprime_common_divisor inf_commute)
  then show ?thesis by simp
qed

lemma (in group) coset_neq_imp_empty_inter:
  assumes "subgroup H G" "a  carrier G" "b  carrier G"
  shows "H #> a  H #> b  (H #> a)  (H #> b) = {}"
  by (metis Int_emptyI assms repr_independence)

lemma (in comm_group) subgroup_is_comm_group:
  assumes "subgroup H G"
  shows "comm_group (Gcarrier := H)" unfolding comm_group_def
proof
  interpret H: subgroup H G by fact
  interpret H: submonoid H G using H.subgroup_is_submonoid .
  show "Group.group (Gcarrier := H)" by blast
  show "comm_monoid (Gcarrier := H)" using submonoid_is_comm_monoid H.submonoid_axioms by blast
qed

lemma (in group) pow_int_mod_ord:
  assumes [simp]:"a  carrier G" "ord a  0"
  shows "a [^] (n::int) = a [^] (n mod ord a)"
proof -
  obtain q r where d: "q = n div ord a" "r = n mod ord a" "n = q * ord a + r"
    using mod_div_decomp by blast
  hence "a [^] n = (a [^] int (ord a)) [^] q  a [^] r"
    using assms(1) int_pow_mult int_pow_pow
    by (metis mult_of_nat_commute)
  also have " = 𝟭 [^] q  a [^] r"
    by (simp add: int_pow_int)
  also have " = a [^] r" by simp
  finally show ?thesis using d(2) by blast
qed

lemma (in group) pow_nat_mod_ord:
  assumes [simp]:"a  carrier G" "ord a  0"
  shows "a [^] (n::nat) = a [^] (n mod ord a)"
proof -
  obtain q r where d: "q = n div ord a" "r = n mod ord a" "n = q * ord a + r"
    using mod_div_decomp by blast
  hence "a [^] n = (a [^] ord a) [^] q  a [^] r"
    using assms(1) nat_pow_mult nat_pow_pow by presburger
  also have " = 𝟭 [^] q  a [^] r" by auto
  also have " = a [^] r" by simp
  finally show ?thesis using d(2) by blast
qed

lemma (in group) ord_min:
  assumes "m  1" "x  carrier G" "x [^] m = 𝟭"
  shows   "ord x  m"
  using assms pow_eq_id by auto

(* Manuel Eberl *)
lemma (in group) bij_betw_mult_left[intro]:
  assumes [simp]: "x  carrier G"
  shows "bij_betw (λy. x  y) (carrier G) (carrier G)"
  by (intro bij_betwI[where ?g = "λy. inv x  y"])
     (auto simp: m_assoc [symmetric])

(* Manuel Eberl *)
lemma (in subgroup) inv_in_iff:
  assumes "x  carrier G" "group G"
  shows   "inv x  H  x  H"
proof safe
  assume "inv x  H"
  hence "inv (inv x)  H" by blast
  also have "inv (inv x) = x"
    by (intro group.inv_inv) (use assms in auto)
  finally show "x  H" .
qed auto

(* Manuel Eberl *)
lemma (in subgroup) mult_in_cancel_left:
  assumes "y  carrier G" "x  H" "group G"
  shows   "x  y  H  y  H"
proof safe
  assume "x  y  H"
  hence "inv x  (x  y)  H"
    using assms by blast
  also have "inv x  (x  y) = y"
    using assms by (simp add: x  y  H group.inv_solve_left')
  finally show "y  H" .
qed (use assms in auto)

(* Manuel Eberl *)
lemma (in subgroup) mult_in_cancel_right:
  assumes "x  carrier G" "y  H" "group G"
  shows   "x  y  H  x  H"
proof safe
  assume "x  y  H"
  hence "(x  y)  inv y  H"
    using assms by blast
  also have "(x  y)  inv y = x"
    using assms by (simp add: x  y  H group.inv_solve_right')
  finally show "x  H" .
qed (use assms in auto)

lemma (in group) (* Manuel Eberl *)
  assumes "x  carrier G" and "x [^] n = 𝟭" and "n > 0"
  shows   ord_le: "ord x  n" and ord_pos: "ord x > 0"
proof -
  have "ord x dvd n"
    using pow_eq_id[of x n] assms by auto
  thus "ord x  n" "ord x > 0"
    using assms by (auto intro: dvd_imp_le)
qed

lemma (in group) ord_conv_Least: (* Manuel Eberl *)
  assumes "x  carrier G" "n::nat > 0. x [^] n = 𝟭"
  shows   "ord x = (LEAST n::nat. 0 < n  x [^] n = 𝟭)"
proof (rule antisym)
  show "ord x  (LEAST n::nat. 0 < n  x [^] n = 𝟭)"
    using assms LeastI_ex[OF assms(2)] by (intro ord_le) auto
  show "ord x  (LEAST n::nat. 0 < n  x [^] n = 𝟭)"
    using assms by (intro Least_le) (auto intro: pow_ord_eq_1 ord_pos)
qed

lemma (in group) ord_conv_Gcd: (* Manuel Eberl *)
  assumes "x  carrier G"
  shows   "ord x = Gcd {n. x [^] n = 𝟭}"
  by (rule sym, rule Gcd_eqI) (use assms in auto simp: pow_eq_id)

lemma (in group) subgroup_ord_eq:
  assumes "subgroup H G" "x  H"
  shows "group.ord (Gcarrier := H) x = ord x"
  using nat_pow_consistent ord_def group.ord_def[of "(Gcarrier := H)" x]
        subgroup.subgroup_is_group[of H G] assms by simp

lemma (in group) ord_FactGroup:
  assumes "subgroup P G" "group (G Mod P)"
  shows "order (G Mod P) * card P = order G"
  using lagrange[of P] FactGroup_def[of G P] assms order_def[of "(G Mod P)"] by fastforce

lemma (in group) one_is_same:
  assumes "subgroup H G"
  shows "𝟭Gcarrier := H= 𝟭"
  by simp

lemma (in group) kernel_FactGroup:
  assumes "P  G"
  shows "kernel G (G Mod P) (λx. P #> x) = P"
proof(rule equalityI; rule subsetI)
  fix x
  assume "x  kernel G (G Mod P) ((#>) P)"
  then have "P #> x = 𝟭G Mod P⇙" "x  carrier G" unfolding kernel_def by simp+
  with coset_join1[of P x] show "x  P" using assms unfolding normal_def by simp
next
  fix x
  assume x:"x  P"
  then have xc: "x  carrier G" using assms subgroup.subset unfolding normal_def by fast
  from x have "P #> x = P" using assms
    by (simp add: normal_imp_subgroup subgroup.rcos_const)
  thus "x  kernel G (G Mod P) ((#>) P)" unfolding kernel_def using xc by simp
qed

lemma (in group) sub_subgroup_coprime:
  assumes "subgroup H G" "subgroup J G" "coprime (card H) (card J)"
  and "subgroup sH G" "subgroup sJ G" "sH  H" "sJ  J"
shows "coprime (card sH) (card sJ)"
  using assms by (meson coprime_divisors sub_subgroup_dvd_card)

lemma (in group) pow_eq_nat_mod:
  assumes "a  carrier G" "a [^] n = a [^] m"
  shows "n mod (ord a) = m mod (ord a)"
proof -
  from assms have "a [^] (n - m) = 𝟭" using pow_eq_div2 by blast
  hence "ord a dvd n - m" using assms(1) pow_eq_id by blast
  thus ?thesis
    by (metis assms mod_eq_dvd_iff_nat nat_le_linear pow_eq_div2 pow_eq_id)
qed

lemma (in group) pow_eq_int_mod:
  fixes n m::int
  assumes "a  carrier G" "a [^] n = a [^] m"
  shows "n mod (ord a) = m mod (ord a)"
proof -
  from assms have "a [^] (n - m) = 𝟭" using int_pow_closed int_pow_diff r_inv by presburger
  hence "ord a dvd n - m" using assms(1) int_pow_eq_id by blast
  thus ?thesis by (meson mod_eq_dvd_iff)
qed

end