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 [^]⇘G⦇carrier := H⦈⇙ b = 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 (G⦇carrier := 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 (G⦇carrier := 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 "(G⦇carrier := 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 (G⦇carrier := 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 (G⦇carrier := H⦈)" by blast
  show "comm_monoid (G⦇carrier := 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 (G⦇carrier := H⦈) x = ord x"
  using nat_pow_consistent ord_def group.ord_def[of "(G⦇carrier := 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 "𝟭⇘G⦇carrier := 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