Theory HOL-Algebra.Product_Groups

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

section ‹Product and Sum Groups›

theory Product_Groups
  imports Elementary_Groups "HOL-Library.Equipollence" 
  
begin

subsection ‹Product of a Family of Groups›

definition product_group:: "'a set  ('a  ('b, 'c) monoid_scheme)  ('a  'b) monoid"
  where "product_group I G  carrier = (ΠE iI. carrier (G i)),
                              monoid.mult = (λx y. (λiI. x i G iy i)),
                              one = (λiI. 𝟭G i)"

lemma carrier_product_group [simp]: "carrier(product_group I G) = (ΠE iI. carrier (G i))"
  by (simp add: product_group_def)

lemma one_product_group [simp]: "one(product_group I G) = (λiI. one (G i))"
  by (simp add: product_group_def)

lemma mult_product_group [simp]: "(⊗product_group I G) = (λx y. λiI. x i G iy i)"
  by (simp add: product_group_def)

lemma product_group [simp]:
  assumes "i. i  I  group (G i)" shows "group (product_group I G)"
proof (rule groupI; simp)
  show "(λi. x i G iy i)  (Π iI. carrier (G i))"
    if "x  (ΠE iI. carrier (G i))" "y  (ΠE iI. carrier (G i))" for x y
    using that assms group.subgroup_self subgroup.m_closed by fastforce
  show "(λi. 𝟭G i)  (Π iI. carrier (G i))"
    by (simp add: assms group.is_monoid)
  show "(λiI. (if i  I then x i G iy i else undefined) G iz i) =
        (λiI. x i G i(if i  I then y i G iz i else undefined))"
    if "x  (ΠE iI. carrier (G i))" "y  (ΠE iI. carrier (G i))" "z  (ΠE iI. carrier (G i))" for x y z
    using that  by (auto simp: PiE_iff assms group.is_monoid monoid.m_assoc intro: restrict_ext)
  show "(λiI. (if i  I then 𝟭G ielse undefined) G ix i) = x"
    if "x  (ΠE iI. carrier (G i))" for x
    using assms that by (fastforce simp: Group.group_def PiE_iff)
  show "yΠE iI. carrier (G i). (λiI. y i G ix i) = (λiI. 𝟭G i)"
    if "x  (ΠE iI. carrier (G i))" for x
    by (rule_tac x="λiI. invG ix i" in bexI) (use assms that in auto simp: PiE_iff group.l_inv)
qed

lemma inv_product_group [simp]:
  assumes "f  (ΠE iI. carrier (G i))" "i. i  I  group (G i)"
  shows "invproduct_group I Gf = (λiI. invG if i)"
proof (rule group.inv_equality)
  show "Group.group (product_group I G)"
    by (simp add: assms)
  show "(λiI. invG if i) product_group I Gf = 𝟭product_group I G⇙"
    using assms by (auto simp: PiE_iff group.l_inv)
  show "f  carrier (product_group I G)"
    using assms by simp
  show "(λiI. invG if i)  carrier (product_group I G)"
    using PiE_mem assms by fastforce
qed


lemma trivial_product_group: "trivial_group(product_group I G)  (i  I. trivial_group(G i))"
 (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  then have "invproduct_group I G(λaI. 𝟭G a) = 𝟭product_group I G⇙"
    by (metis group.is_monoid monoid.inv_one one_product_group trivial_group_def)
  have [simp]: "𝟭G iG i𝟭G i= 𝟭G i⇙" if "i  I" for i
    unfolding trivial_group_def
  proof -
    have 1: "(λaI. 𝟭G a) i = 𝟭G i⇙"
      by (simp add: that)
    have "(λaI. 𝟭G a) = (λaI. 𝟭G a) product_group I G(λaI. 𝟭G a)"
      by (metis (no_types) L group.is_monoid monoid.l_one one_product_group singletonI trivial_group_def)
    then show ?thesis
      using 1 by (simp add: that)
  qed
  show ?rhs
    using L
    by (auto simp: trivial_group_def product_group_def PiE_eq_singleton intro: groupI)
next
  assume ?rhs
  then show ?lhs
    by (simp add: PiE_eq_singleton trivial_group_def)
qed


lemma PiE_subgroup_product_group:
  assumes "i. i  I  group (G i)"
  shows "subgroup (PiE I H) (product_group I G)  (i  I. subgroup (H i) (G i))"
    (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  then have [simp]: "PiE I H  {}"
    using subgroup_nonempty by force
  show ?rhs
  proof (clarify; unfold_locales)
    show sub: "H i  carrier (G i)" if "i  I" for i
      using that L by (simp add: subgroup_def) (metis (no_types, lifting) L subgroup_nonempty subset_PiE)
    show "x G iy  H i" if "i  I" "x  H i" "y  H i" for i x y
    proof -
      have *: "x. x  PiE I H  (y  PiE I H. iI. x i G iy i  H i)"
        using L by (auto simp: subgroup_def Pi_iff)
      have "yH i. f i G iy  H i" if f: "f  PiE I H" and "i  I" for i f
        using * [OF f] i  I
        by (subst(asm) all_PiE_elements) auto
      then have "f  PiE I H. i  I. yH i. f i G iy  H i"
        by blast
      with that show ?thesis
        by (subst(asm) all_PiE_elements) auto
    qed
    show "𝟭G i H i" if "i  I" for i
      using L subgroup.one_closed that by fastforce
    show "invG ix  H i" if "i  I" and x: "x  H i" for i x
    proof -
      have *: "y  PiE I H. iI. invG iy i  H i"
      proof
        fix y
        assume y: "y  PiE I H"
        then have yc: "y  carrier (product_group I G)"
          by (metis (no_types) L subgroup_def subsetCE)
        have "invproduct_group I Gy  PiE I H"
          by (simp add: y L subgroup.m_inv_closed)
        moreover have "invproduct_group I Gy = (λiI. invG iy i)"
          using yc by (simp add: assms)
        ultimately show "iI. invG iy i  H i"
          by auto
      qed
      then have "iI. xH i. invG ix  H i"
        by (subst(asm) all_PiE_elements) auto
      then show ?thesis
        using that(1) x by blast
    qed
  qed
next
  assume R: ?rhs
  show ?lhs
  proof
    show "PiE I H  carrier (product_group I G)"
      using R by (force simp: subgroup_def)
    show "x product_group I Gy  PiE I H" if "x  PiE I H" "y  PiE I H" for x y
      using R that by (auto simp: PiE_iff subgroup_def)
    show "𝟭product_group I G PiE I H"
      using R by (force simp: subgroup_def)
    show "invproduct_group I Gx  PiE I H" if "x  PiE I H" for x
    proof -
      have x: "x  (ΠE iI. carrier (G i))"
        using R that by (force simp:  subgroup_def)
      show ?thesis
        using assms R that by (fastforce simp: x assms subgroup_def)
    qed
  qed
qed

lemma product_group_subgroup_generated:
  assumes "i. i  I  subgroup (H i) (G i)" and gp: "i. i  I  group (G i)"
  shows "product_group I (λi. subgroup_generated (G i) (H i))
       = subgroup_generated (product_group I G) (PiE I H)"
proof (rule monoid.equality)
  have [simp]: "i. i  I  carrier (G i)  H i = H i" "(ΠE iI. carrier (G i))  PiE I H = PiE I H"
    using assms by (force simp: subgroup_def)+
  have "(ΠE iI. generate (G i) (H i)) = generate (product_group I G) (PiE I H)"
  proof (rule group.generateI)
    show "Group.group (product_group I G)"
      using assms by simp
    show "subgroup (ΠE iI. generate (G i) (H i)) (product_group I G)"
      using assms by (simp add: PiE_subgroup_product_group group.generate_is_subgroup subgroup.subset)
    show "PiE I H  (ΠE iI. generate (G i) (H i))"
      using assms by (auto simp: PiE_iff generate.incl)
    show "(ΠE iI. generate (G i) (H i))  K"
      if "subgroup K (product_group I G)" "PiE I H  K" for K
      using assms that group.generate_subgroup_incl by fastforce
  qed
  with assms
  show "carrier (product_group I (λi. subgroup_generated (G i) (H i))) =
        carrier (subgroup_generated (product_group I G) (PiE I H))"
    by (simp add: carrier_subgroup_generated cong: PiE_cong)
qed auto

lemma finite_product_group:
  assumes "i. i  I  group (G i)"
  shows
   "finite (carrier (product_group I G)) 
    finite {i. i  I  ~ trivial_group(G i)}  (i  I. finite(carrier(G i)))"
proof -
  have [simp]: "i. i  I  carrier (G i)  {}"
    using assms group.is_monoid by blast
  show ?thesis
    by (auto simp: finite_PiE_iff PiE_eq_empty_iff group.trivial_group_alt [OF assms] cong: Collect_cong conj_cong)
qed

subsection ‹Sum of a Family of Groups›

definition sum_group :: "'a set  ('a  ('b, 'c) monoid_scheme)  ('a  'b) monoid"
  where "sum_group I G 
        subgroup_generated
         (product_group I G)
         {x  ΠE iI. carrier (G i). finite {i  I. x i  𝟭G i}}"

lemma subgroup_sum_group:
  assumes "i. i  I  group (G i)"
  shows "subgroup {x  ΠE iI. carrier (G i). finite {i  I. x i  𝟭G i}}
                  (product_group I G)"
proof unfold_locales
  fix x y
  have *: "{i. (i  I  x i G iy i  𝟭G i)  i  I}
         {i  I. x i  𝟭G i}  {i  I. y i  𝟭G i}"
    by (auto simp: Group.group_def dest: assms)
  assume
    "x  {x  ΠE iI. carrier (G i). finite {i  I. x i  𝟭G i}}"
    "y  {x  ΠE iI. carrier (G i). finite {i  I. x i  𝟭G i}}"
  then
  show "x product_group I Gy  {x  ΠE iI. carrier (G i). finite {i  I. x i  𝟭G i}}"
    using assms
    apply (auto simp: Group.group_def monoid.m_closed PiE_iff)
    apply (rule finite_subset [OF *])
    by blast
next
  fix x
  assume "x  {x  ΠE iI. carrier (G i). finite {i  I. x i  𝟭G i}}"
  then show "invproduct_group I Gx  {x  ΠE iI. carrier (G i). finite {i  I. x i  𝟭G i}}"
    using assms
    by (auto simp: PiE_iff assms group.inv_eq_1_iff [OF assms] conj_commute cong: rev_conj_cong)
qed (use assms [unfolded Group.group_def] in auto)

lemma carrier_sum_group:
  assumes "i. i  I  group (G i)"
  shows "carrier(sum_group I G) = {x  ΠE iI. carrier (G i). finite {i  I. x i  𝟭G i}}"
proof -
  interpret SG: subgroup "{x  ΠE iI. carrier (G i). finite {i  I. x i  𝟭G i}}" "(product_group I G)"
    by (simp add: assms subgroup_sum_group)
  show ?thesis
    by (simp add: sum_group_def subgroup_sum_group carrier_subgroup_generated_alt)
qed

lemma one_sum_group [simp]: "𝟭sum_group I G= (λiI. 𝟭G i)"
  by (simp add: sum_group_def)

lemma mult_sum_group [simp]: "(⊗sum_group I G) = (λx y. (λiI. x i G iy i))"
  by (auto simp: sum_group_def)

lemma sum_group [simp]:
  assumes "i. i  I  group (G i)" shows "group (sum_group I G)"
proof (rule groupI)
  note group.is_monoid [OF assms, simp]
  show "x sum_group I Gy  carrier (sum_group I G)"
    if "x  carrier (sum_group I G)" and
      "y  carrier (sum_group I G)" for x y
  proof -
    have *: "{i  I. x i G iy i  𝟭G i}  {i  I. x i  𝟭G i}  {i  I. y i  𝟭G i}"
      by auto
    show ?thesis
      using that
      apply (simp add: assms carrier_sum_group PiE_iff monoid.m_closed conj_commute cong: rev_conj_cong)
      apply (blast intro: finite_subset [OF *])
      done
  qed
  show "𝟭sum_group I Gsum_group I Gx = x"
    if "x  carrier (sum_group I G)" for x
    using that by (auto simp: assms carrier_sum_group PiE_iff extensional_def)
  show "ycarrier (sum_group I G). y sum_group I Gx = 𝟭sum_group I G⇙"
    if "x  carrier (sum_group I G)" for x
  proof
    let ?y = "λiI. m_inv (G i) (x i)"
    show "?y sum_group I Gx = 𝟭sum_group I G⇙"
      using that assms
      by (auto simp: carrier_sum_group PiE_iff group.l_inv)
    show "?y  carrier (sum_group I G)"
      using that assms
      by (auto simp: carrier_sum_group PiE_iff group.inv_eq_1_iff group.l_inv cong: conj_cong)
  qed
qed (auto simp: assms carrier_sum_group PiE_iff group.is_monoid monoid.m_assoc)

lemma inv_sum_group [simp]:
  assumes "i. i  I  group (G i)" and x: "x  carrier (sum_group I G)"
  shows "m_inv (sum_group I G) x = (λiI. m_inv (G i) (x i))"
proof (rule group.inv_equality)
  show "(λiI. invG ix i) sum_group I Gx = 𝟭sum_group I G⇙"
    using x by (auto simp: carrier_sum_group PiE_iff group.l_inv assms intro: restrict_ext)
  show "(λiI. invG ix i)  carrier (sum_group I G)"
    using x by (simp add: carrier_sum_group PiE_iff group.inv_eq_1_iff assms conj_commute cong: rev_conj_cong)
qed (auto simp: assms)


thm group.subgroups_Inter (*REPLACE*)
theorem subgroup_Inter:
  assumes subgr: "(H. H  A  subgroup H G)"
    and not_empty: "A  {}"
  shows "subgroup (A) G"
proof
  show " A  carrier G"
    by (simp add: Inf_less_eq not_empty subgr subgroup.subset)
qed (auto simp: subgr subgroup.m_closed subgroup.one_closed subgroup.m_inv_closed)

thm group.subgroups_Inter_pair (*REPLACE*)
lemma subgroup_Int:
  assumes "subgroup I G" "subgroup J G"
  shows "subgroup (I  J) G" using subgroup_Inter[ where ?A = "{I,J}"] assms by auto


lemma sum_group_subgroup_generated:
  assumes "i. i  I  group (G i)" and sg: "i. i  I  subgroup (H i) (G i)"
  shows "sum_group I (λi. subgroup_generated (G i) (H i)) = subgroup_generated (sum_group I G) (PiE I H)"
proof (rule monoid.equality)
  have "subgroup (carrier (sum_group I G)  PiE I H) (product_group I G)"
    by (rule subgroup_Int) (auto simp: assms carrier_sum_group subgroup_sum_group PiE_subgroup_product_group)
  moreover have "carrier (sum_group I G)  PiE I H
               carrier (subgroup_generated (product_group I G)
                    {x  ΠE iI. carrier (G i). finite {i  I. x i  𝟭G i}})"
    by (simp add: assms subgroup_sum_group subgroup.carrier_subgroup_generated_subgroup carrier_sum_group)
  ultimately
  have "subgroup (carrier (sum_group I G)  PiE I H) (sum_group I G)"
    by (simp add: assms sum_group_def group.subgroup_subgroup_generated_iff)
  then have *: "{f  ΠE iI. carrier (subgroup_generated (G i) (H i)). finite {i  I. f i  𝟭G i}}
      = carrier (subgroup_generated (sum_group I G) (carrier (sum_group I G)  PiE I H))"
    apply (simp only: subgroup.carrier_subgroup_generated_subgroup)
    using subgroup.subset [OF sg]
    apply (auto simp: set_eq_iff PiE_def Pi_def assms carrier_sum_group subgroup.carrier_subgroup_generated_subgroup)
    done
  then show "carrier (sum_group I (λi. subgroup_generated (G i) (H i))) =
        carrier (subgroup_generated (sum_group I G) (PiE I H))"
    by simp (simp add: assms group.subgroupE(1) group.group_subgroup_generated carrier_sum_group)
qed (auto simp: sum_group_def subgroup_generated_def)


lemma iso_product_groupI:
  assumes iso: "i. i  I  G i  H i"
    and G: "i. i  I  group (G i)" and H: "i. i  I  group (H i)"
  shows "product_group I G  product_group I H" (is "?IG  ?IH")
proof -
  have "i. i  I  h. h  iso (G i) (H i)"
    using iso by (auto simp: is_iso_def)
  then obtain f where f: "i. i  I  f i  iso (G i) (H i)"
    by metis
  define h where "h  λx. (λiI. f i (x i))"
  have hom: "h  iso ?IG ?IH"
  proof (rule isoI)
    show hom: "h  hom ?IG ?IH"
    proof (rule homI)
      fix x
      assume "x  carrier ?IG"
      with f show "h x  carrier ?IH"
        using PiE by (fastforce simp add: h_def PiE_def iso_def hom_def)
    next
      fix x y
      assume "x  carrier ?IG" "y  carrier ?IG"
      with f show "h (x ?IGy) = h x ?IHh y"
        apply (simp add: h_def PiE_def iso_def hom_def)
        using PiE by (fastforce simp add: h_def PiE_def iso_def hom_def intro: restrict_ext)
    qed
    with G H interpret GH : group_hom "?IG" "?IH" h
      by (simp add: group_hom_def group_hom_axioms_def)
    show "bij_betw h (carrier ?IG) (carrier ?IH)"
      unfolding bij_betw_def
    proof (intro conjI subset_antisym)
      have "γ i = 𝟭G i⇙"
        if γ: "γ  (ΠE iI. carrier (G i))" and eq: "(λiI. f i (γ i)) = (λiI. 𝟭H i)" and "i  I"
        for γ i
      proof -
        have "inj_on (f i) (carrier (G i))" "f i  hom (G i) (H i)"
          using i  I f by (auto simp: iso_def bij_betw_def)
        then have *: "x. f i x = 𝟭H i; x  carrier (G i)  x = 𝟭G i⇙"
          by (metis G Group.group_def H hom_one inj_onD monoid.one_closed i  I)
        show ?thesis
          using eq i  I * γ by (simp add: fun_eq_iff) (meson PiE_iff)
      qed
      then show "inj_on h (carrier ?IG)"
        apply (simp add: iso_def bij_betw_def GH.inj_on_one_iff flip: carrier_product_group)
        apply (force simp: h_def)
        done
    next
      show "h ` carrier ?IG  carrier ?IH"
        unfolding h_def using f
        by (force simp: PiE_def Pi_def Group.iso_def dest!: bij_betwE)
    next
      show "carrier ?IH  h ` carrier ?IG"
        unfolding h_def
      proof (clarsimp simp: iso_def bij_betw_def)
        fix x
        assume "x  (ΠE iI. carrier (H i))"
        with f have x: "x  (ΠE iI. f i ` carrier (G i))"
          unfolding h_def by (auto simp: iso_def bij_betw_def)
        have "i. i  I  inj_on (f i) (carrier (G i))"
          using f by (auto simp: iso_def bij_betw_def)
        let ?g = "λiI. inv_into (carrier (G i)) (f i) (x i)"
        show "x  (λg. λiI. f i (g i)) ` (ΠE iI. carrier (G i))"
        proof
          show "x = (λiI. f i (?g i))"
            using x by (auto simp: PiE_iff fun_eq_iff extensional_def f_inv_into_f)
          show "?g  (ΠE iI. carrier (G i))"
            using x by (auto simp: PiE_iff inv_into_into)
        qed
      qed
    qed
  qed
  then show ?thesis
    using is_iso_def by auto
qed

lemma iso_sum_groupI:
  assumes iso: "i. i  I  G i  H i"
    and G: "i. i  I  group (G i)" and H: "i. i  I  group (H i)"
  shows "sum_group I G  sum_group I H" (is "?IG  ?IH")
proof -
  have "i. i  I  h. h  iso (G i) (H i)"
    using iso by (auto simp: is_iso_def)
  then obtain f where f: "i. i  I  f i  iso (G i) (H i)"
    by metis
  then have injf: "inj_on (f i) (carrier (G i))"
    and homf: "f i  hom (G i) (H i)" if "i  I" for i
    using i  I f by (auto simp: iso_def bij_betw_def)
  then have one: "x. f i x = 𝟭H i; x  carrier (G i)  x = 𝟭G i⇙" if "i  I" for i
    by (metis G H group.subgroup_self hom_one inj_on_eq_iff subgroup.one_closed that)
  have fin1: "finite {i  I. x i  𝟭G i}  finite {i  I. f i (x i)  𝟭H i}" for x
    using homf by (auto simp: G H hom_one elim!: rev_finite_subset)
  define h where "h  λx. (λiI. f i (x i))"
  have hom: "h  iso ?IG ?IH"
  proof (rule isoI)
    show hom: "h  hom ?IG ?IH"
    proof (rule homI)
      fix x
      assume "x  carrier ?IG"
      with f fin1 show "h x  carrier ?IH"
        by (force simp: h_def PiE_def iso_def hom_def carrier_sum_group assms conj_commute cong: conj_cong)
    next
      fix x y
      assume "x  carrier ?IG" "y  carrier ?IG"
      with homf show "h (x ?IGy) = h x ?IHh y"
        by (fastforce simp add: h_def PiE_def hom_def carrier_sum_group assms intro: restrict_ext)
    qed
    with G H interpret GH : group_hom "?IG" "?IH" h
      by (simp add: group_hom_def group_hom_axioms_def)
    show "bij_betw h (carrier ?IG) (carrier ?IH)"
      unfolding bij_betw_def
    proof (intro conjI subset_antisym)
      have γ: "γ i = 𝟭G i⇙"
        if "γ  (ΠE iI. carrier (G i))" and eq: "(λiI. f i (γ i)) = (λiI. 𝟭H i)" and "i  I"
        for γ i
        using i  I one that by (simp add: fun_eq_iff) (meson PiE_iff)
      show "inj_on h (carrier ?IG)"
        apply (simp add: iso_def bij_betw_def GH.inj_on_one_iff assms one flip: carrier_sum_group)
        apply (auto simp: h_def fun_eq_iff carrier_sum_group assms PiE_def Pi_def extensional_def one)
        done
    next
      show "h ` carrier ?IG  carrier ?IH"
        using homf GH.hom_closed
        by (fastforce simp: h_def PiE_def Pi_def dest!: bij_betwE)
    next
      show "carrier ?IH  h ` carrier ?IG"
        unfolding h_def
      proof (clarsimp simp: iso_def bij_betw_def carrier_sum_group assms)
        fix x
        assume x: "x  (ΠE iI. carrier (H i))" and fin: "finite {i  I. x i  𝟭H i}"
        with f have xf: "x  (ΠE iI. f i ` carrier (G i))"
          unfolding h_def
          by (auto simp: iso_def bij_betw_def)
        have "i. i  I  inj_on (f i) (carrier (G i))"
          using f by (auto simp: iso_def bij_betw_def)
        let ?g = "λiI. inv_into (carrier (G i)) (f i) (x i)"
        show "x  (λg. λiI. f i (g i))
                 ` {x  ΠE iI. carrier (G i). finite {i  I. x i  𝟭G i}}"
        proof
          show xeq: "x = (λiI. f i (?g i))"
            using x by (clarsimp simp: PiE_iff fun_eq_iff extensional_def) (metis iso_iff f_inv_into_f f)
          have "finite {i  I. inv_into (carrier (G i)) (f i) (x i)  𝟭G i}"
            apply (rule finite_subset [OF _ fin])
            using G H group.subgroup_self hom_one homf injf inv_into_f_eq subgroup.one_closed by fastforce
          with x show "?g  {x  ΠE iI. carrier (G i). finite {i  I. x i  𝟭G i}}"
            apply (auto simp: PiE_iff inv_into_into conj_commute cong: conj_cong)
            by (metis (no_types, opaque_lifting) iso_iff f inv_into_into)
        qed
      qed
    qed
  qed
  then show ?thesis
    using is_iso_def by auto
qed

end