Theory Set_Multiplication

(*
    File:     Set_Multiplication.thy
    Author:   Joseph Thommes, TU München
*)
section ‹Set Multiplication›

theory Set_Multiplication
  imports "HOL-Algebra.Multiplicative_Group"
begin

text ‹This theory/section is of auxiliary nature and is mainly used to establish a connection
between the set multiplication and the multiplication of subgroups via the ‹IDirProd› (although this
particular notion is introduced later). However, as in every section of this entry, there are some
lemmas that do not have any further usage in this entry, but are of interest just by themselves.›

lemma (in group) set_mult_union:
  "A <#> (B ∪ C) = (A <#> B) ∪ (A <#> C)"
  unfolding set_mult_def by auto

lemma (in group) set_mult_card_single_el_eq:
  assumes "J ⊆ carrier G" "x ∈ carrier G"
  shows "card (l_coset G x J) = card J" unfolding l_coset_def
proof -
  have "card ((⊗) x ` J) = card J"
    using inj_on_cmult[of x] card_image[of "(⊗) x" J] assms inj_on_subset[of "(⊗) x" "carrier G" J]
    by blast
  moreover have "(⋃y∈J. {x ⊗ y}) = (⊗) x ` J" using image_def[of "(⊗) x" J] by blast
  ultimately show "card (⋃h∈J. {x ⊗ h}) = card J" by presburger
qed

text ‹We find an upper bound for the cardinality of a set product.›

lemma (in group) set_mult_card_le:
  assumes "finite H" "H ⊆ carrier G" "J ⊆ carrier G"
  shows "card (H <#> J) ≤ card H * card J"
  using assms
proof (induction "card H" arbitrary: H)
  case 0
  then have "H = {}" by force
  then show ?case using set_mult_def[of G H J] by simp
next
  case (Suc n)
  then obtain a where a_def: "a ∈ H" by fastforce
  then have c_n: "card (H - {a}) = n" using Suc by force
  then have "card ((H - {a}) <#> J) ≤ card (H - {a}) * card J" using Suc by blast
  moreover have "card ({a} <#> J) = card J"
    using Suc(4, 5) a_def set_mult_card_single_el_eq[of J a] l_coset_eq_set_mult[of G a J] by auto
  moreover have "H <#> J = (H - {a} <#> J) ∪ ({a} <#> J)" using set_mult_def[of G _ J] a_def by auto
  moreover have "card (H - {a}) * card J + card J = Suc n * card J" using c_n mult_Suc by presburger
  ultimately show ?case using card_Un_le[of "H - {a} <#> J" "{a} <#> J"] c_n ‹Suc n = card H› by auto
qed

lemma (in group) set_mult_finite:
  assumes "finite H" "finite J" "H ⊆ carrier G" "J ⊆ carrier G"
  shows "finite (H <#> J)"
  using assms set_mult_def[of G H J] by auto

text ‹The next lemma allows us to later to derive that two finite subgroups $J$ and $H$ are complementary
if and only if their product has the cardinality $|J| \cdot |H|$.›

lemma (in group) set_mult_card_eq_impl_empty_inter:
  assumes "finite H" "finite J" "H ⊆ carrier G" "J ⊆ carrier G" "card (H <#> J) = card H * card J"
  shows "⋀a b. ⟦a ∈ H; b ∈ H; a ≠ b⟧ ⟹ ((⊗) a ` J) ∩ ((⊗) b ` J) = {}"
  using assms
proof (induction H rule: finite_induct)
  case empty
  then show ?case by fast
next
  case step: (insert x H)
  from step have x_c: "x ∈ carrier G" by simp
  from step have H_c: "H ⊆ carrier G" by simp
  from set_mult_card_single_el_eq[of J x] have card_x: "card ({x} <#> J) = card J"
    using ‹J ⊆ carrier G› x_c l_coset_eq_set_mult by metis
  moreover have ins: "(insert x H) <#> J = (H <#> J) ∪ ({x} <#> J)"
    using set_mult_def[of G _ J] by auto
  ultimately have "card (H <#> J) ≥ card H * card J"
    using card_Un_le[of "H <#> J" "{x} <#> J"] ‹card (insert x H <#> J) = card (insert x H) * card J›
    by (simp add: step.hyps(1) step.hyps(2))
  then have card_eq:"card (H <#> J) = card H * card J"
    using set_mult_card_le[of H J] step H_c by linarith
  then have ih: "⋀a b. ⟦a ∈ H; b ∈ H; a ≠ b⟧ ⟹ ((⊗) a ` J) ∩ ((⊗) b ` J) = {}"
    using step H_c by presburger

  have "card (insert x H) * card J = card H * card J + card J" using ‹x ∉ H› using step by simp
  then have "({x} <#> J) ∩ (H <#> J) = {}"
    using card_eq card_x ins card_Un_Int[of "H <#> J" "{x} <#> J"] step set_mult_finite by auto
  then have "⋀a. a ∈ H ⟹ (⋃y∈J. {a ⊗ y}) ∩ (⋃y∈J. {x ⊗ y}) = {}"
    using set_mult_def[of G _ J] by blast
  then have "⋀a b. ⟦a ∈ (insert x H); b ∈ (insert x H); a ≠ b⟧ ⟹ ((⊗) a ` J) ∩ ((⊗) b ` J) = {}"
    using ‹x ∉ H› ih by blast
  then show ?case using step by presburger
qed

lemma (in group) set_mult_card_eq_impl_empty_inter':
  assumes "finite H" "finite J" "H ⊆ carrier G" "J ⊆ carrier G" "card (H <#> J) = card H * card J"
  shows "⋀a b. ⟦a ∈ H; b ∈ H; a ≠ b⟧ ⟹ (l_coset G a J) ∩ (l_coset G b J) = {}"
  unfolding l_coset_def
  using set_mult_card_eq_impl_empty_inter image_def[of "(⊗) _" J] assms by blast

lemma (in comm_group) set_mult_comm:
  assumes "H ⊆ carrier G" "J ⊆ carrier G"
  shows "(H <#> J) = (J <#> H)"
  unfolding set_mult_def
proof -
  have 1: "⋀a b. ⟦a ∈ carrier G; b ∈ carrier G⟧ ⟹ {a ⊗ b} = {b ⊗ a}" using m_comm by simp
  then have "⋀a b.⟦a ∈ H; b ∈ J⟧ ⟹ {a ⊗ b} = {b ⊗ a}" using assms by auto
  moreover have "⋀a b.⟦b ∈ H; a ∈ J⟧ ⟹ {a ⊗ b} = {b ⊗ a}" using assms 1 by auto
  ultimately show "(⋃h∈H. ⋃k∈J. {h ⊗ k}) = (⋃k∈J. ⋃h∈H. {k ⊗ h})"  by fast
qed

lemma (in group) set_mult_one_imp_inc:
  assumes "𝟭 ∈ A" "A ⊆ carrier G" "B ⊆ carrier G"
  shows "B ⊆ (B <#> A)"
proof
  fix x
  assume "x ∈ B"
  thus "x ∈ (B <#> A)" using assms unfolding set_mult_def by force
qed

text ‹In all cases, we know that the product of two sets is always contained in the subgroup
generated by them.›
lemma (in group) set_mult_subset_generate:
  assumes "A ⊆ carrier G" "B ⊆ carrier G"
  shows "A <#> B ⊆ generate G (A ∪ B)"
proof
  fix x
  assume "x ∈ A <#> B"
  then obtain a b where ab: "a ∈ A" "b ∈ B" "x = a ⊗ b" unfolding set_mult_def by blast
  then have "a ∈ generate G (A ∪ B)" "b ∈ generate G (A ∪ B)"
    using generate.incl[of _ "A ∪ B" G] by simp+
  thus "x ∈ generate G (A ∪ B)" using ab generate.eng by metis
qed

text ‹In the case of subgroups, the set product is just the subgroup generated by both
of the subgroups.›

lemma (in comm_group) set_mult_eq_generate_subgroup:
  assumes "subgroup H G" "subgroup J G"
  shows "generate G (H ∪ J) = H <#> J" (is "?L = ?R")
proof
  show "?L ⊆ ?R"
  proof
    fix x
    assume "x ∈ ?L"
    then show "x ∈ ?R"
    proof(induction rule: generate.induct)
      case one
      have "𝟭 ⊗ 𝟭 = 𝟭" using nat_pow_one[of 2] by simp
      thus ?case
        using assms subgroup.one_closed[OF assms(1)]
              subgroup.one_closed[OF assms(2)] set_mult_def[of G H J] by fastforce
    next
      case (incl x)
      have H1: "𝟭 ∈ H" using assms subgroup.one_closed by auto
      have J1: "𝟭 ∈ J" using assms subgroup.one_closed by auto
      have lx: "x ⊗ 𝟭 = x" using r_one[of x] incl subgroup.subset assms by blast
      have rx: "𝟭 ⊗ x = x" using l_one[of x] incl subgroup.subset assms by blast
      show ?case
      proof (cases "x ∈ H")
        case True
        then show ?thesis using set_mult_def J1 lx by fastforce
      next
        case False
        then show ?thesis using set_mult_def H1 rx incl by fastforce
      qed
    next
      case (inv h)
      then have inv_in:"(inv h) ∈ H ∪ J" (is "?iv ∈ H ∪ J")
        using assms subgroup.m_inv_closed[of _ G h] by (cases "h ∈ H"; blast)
      have H1: "𝟭 ∈ H" using assms subgroup.one_closed by auto
      have J1: "𝟭 ∈ J" using assms subgroup.one_closed by auto
      have lx: "?iv ⊗ 𝟭 = ?iv" using r_one[of "?iv"] subgroup.subset inv_in assms by blast
      have rx: "𝟭 ⊗ ?iv = ?iv" using l_one[of "?iv"] incl subgroup.subset inv_in assms by blast
      show ?case
      proof (cases "?iv ∈ H")
        case True
        then show ?thesis using set_mult_def[of G H J] J1 lx by fastforce
      next
        case False
        then show ?thesis using set_mult_def[of G H J] H1 rx inv_in by fastforce
      qed
    next
      case (eng h g)
      from eng(3) obtain a b where aH: "a ∈ H" and bJ: "b ∈ J" and h_def: "h = a ⊗ b"
        using set_mult_def[of G H J] by fast
      have a_carr: "a ∈ carrier G" by (metis subgroup.mem_carrier assms(1) aH)
      have b_carr: "b ∈ carrier G" by (metis subgroup.mem_carrier assms(2) bJ)
      from eng(4) obtain c d where cH: "c ∈ H" and dJ: "d ∈ J" and g_def: "g = c ⊗ d"
        using set_mult_def[of G H J] by fast
      have c_carr: "c ∈ carrier G" by (metis subgroup.mem_carrier assms(1) cH)
      have d_carr: "d ∈ carrier G" by (metis subgroup.mem_carrier assms(2) dJ)
      then have "h ⊗ g = (a ⊗ c) ⊗ (b ⊗ d)"
        using a_carr b_carr c_carr d_carr g_def h_def m_assoc m_comm by force
      moreover have "a ⊗ c ∈ H" using assms(1) aH cH subgroup.m_closed by fast
      moreover have "b ⊗ d ∈ J" using assms(2) bJ dJ subgroup.m_closed by fast
      ultimately show ?case using set_mult_def by fast
    qed
  qed
next
  show "?R ⊆ ?L" using set_mult_subset_generate[of H J] subgroup.subset assms by blast
qed

end