src/HOL/Algebra/Product_Groups.thy
author paulson <lp15@cam.ac.uk>
Wed, 03 Apr 2019 14:55:30 +0100
changeset 70040 6a9e2a82ea15
child 73932 fd21b4a93043
permissions -rw-r--r--
Products and sums of a family of groups
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
70040
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     1
(*  Title:      HOL/Algebra/Product_Groups.thy
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     2
    Author:     LC Paulson (ported from HOL Light)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     3
*)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     4
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     5
section \<open>Product and Sum Groups\<close>
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     6
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     7
theory Product_Groups
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     8
  imports Elementary_Groups "HOL-Library.Equipollence" 
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     9
  
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    10
begin
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    11
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    12
subsection \<open>Product of a Family of Groups\<close>
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    13
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    14
definition product_group:: "'a set \<Rightarrow> ('a \<Rightarrow> ('b, 'c) monoid_scheme) \<Rightarrow> ('a \<Rightarrow> 'b) monoid"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    15
  where "product_group I G \<equiv> \<lparr>carrier = (\<Pi>\<^sub>E i\<in>I. carrier (G i)),
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    16
                              monoid.mult = (\<lambda>x y. (\<lambda>i\<in>I. x i \<otimes>\<^bsub>G i\<^esub> y i)),
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    17
                              one = (\<lambda>i\<in>I. \<one>\<^bsub>G i\<^esub>)\<rparr>"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    18
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    19
lemma carrier_product_group [simp]: "carrier(product_group I G) = (\<Pi>\<^sub>E i\<in>I. carrier (G i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    20
  by (simp add: product_group_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    21
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    22
lemma one_product_group [simp]: "one(product_group I G) = (\<lambda>i\<in>I. one (G i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    23
  by (simp add: product_group_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    24
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    25
lemma mult_product_group [simp]: "(\<otimes>\<^bsub>product_group I G\<^esub>) = (\<lambda>x y. \<lambda>i\<in>I. x i \<otimes>\<^bsub>G i\<^esub> y i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    26
  by (simp add: product_group_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    27
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    28
lemma product_group [simp]:
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    29
  assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)" shows "group (product_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    30
proof (rule groupI; simp)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    31
  show "(\<lambda>i. x i \<otimes>\<^bsub>G i\<^esub> y i) \<in> (\<Pi> i\<in>I. carrier (G i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    32
    if "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" "y \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" for x y
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    33
    using that assms group.subgroup_self subgroup.m_closed by fastforce
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    34
  show "(\<lambda>i. \<one>\<^bsub>G i\<^esub>) \<in> (\<Pi> i\<in>I. carrier (G i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    35
    by (simp add: assms group.is_monoid)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    36
  show "(\<lambda>i\<in>I. (if i \<in> I then x i \<otimes>\<^bsub>G i\<^esub> y i else undefined) \<otimes>\<^bsub>G i\<^esub> z i) =
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    37
        (\<lambda>i\<in>I. x i \<otimes>\<^bsub>G i\<^esub> (if i \<in> I then y i \<otimes>\<^bsub>G i\<^esub> z i else undefined))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    38
    if "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" "y \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" "z \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" for x y z
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    39
    using that  by (auto simp: PiE_iff assms group.is_monoid monoid.m_assoc intro: restrict_ext)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    40
  show "(\<lambda>i\<in>I. (if i \<in> I then \<one>\<^bsub>G i\<^esub> else undefined) \<otimes>\<^bsub>G i\<^esub> x i) = x"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    41
    if "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" for x
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    42
    using assms that by (fastforce simp: Group.group_def PiE_iff)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    43
  show "\<exists>y\<in>\<Pi>\<^sub>E i\<in>I. carrier (G i). (\<lambda>i\<in>I. y i \<otimes>\<^bsub>G i\<^esub> x i) = (\<lambda>i\<in>I. \<one>\<^bsub>G i\<^esub>)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    44
    if "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" for x
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    45
    by (rule_tac x="\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> x i" in bexI) (use assms that in \<open>auto simp: PiE_iff group.l_inv\<close>)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    46
qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    47
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    48
lemma inv_product_group [simp]:
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    49
  assumes "f \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" "\<And>i. i \<in> I \<Longrightarrow> group (G i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    50
  shows "inv\<^bsub>product_group I G\<^esub> f = (\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> f i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    51
proof (rule group.inv_equality)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    52
  show "Group.group (product_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    53
    by (simp add: assms)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    54
  show "(\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> f i) \<otimes>\<^bsub>product_group I G\<^esub> f = \<one>\<^bsub>product_group I G\<^esub>"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    55
    using assms by (auto simp: PiE_iff group.l_inv)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    56
  show "f \<in> carrier (product_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    57
    using assms by simp
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    58
  show "(\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> f i) \<in> carrier (product_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    59
    using PiE_mem assms by fastforce
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    60
qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    61
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    62
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    63
lemma trivial_product_group: "trivial_group(product_group I G) \<longleftrightarrow> (\<forall>i \<in> I. trivial_group(G i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    64
 (is "?lhs = ?rhs")
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    65
proof
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    66
  assume L: ?lhs
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    67
  then have "inv\<^bsub>product_group I G\<^esub> (\<lambda>a\<in>I. \<one>\<^bsub>G a\<^esub>) = \<one>\<^bsub>product_group I G\<^esub>"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    68
    by (metis group.is_monoid monoid.inv_one one_product_group trivial_group_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    69
  have [simp]: "\<one>\<^bsub>G i\<^esub> \<otimes>\<^bsub>G i\<^esub> \<one>\<^bsub>G i\<^esub> = \<one>\<^bsub>G i\<^esub>" if "i \<in> I" for i
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    70
    unfolding trivial_group_def
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    71
  proof -
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    72
    have 1: "(\<lambda>a\<in>I. \<one>\<^bsub>G a\<^esub>) i = \<one>\<^bsub>G i\<^esub>"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    73
      by (simp add: that)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    74
    have "(\<lambda>a\<in>I. \<one>\<^bsub>G a\<^esub>) = (\<lambda>a\<in>I. \<one>\<^bsub>G a\<^esub>) \<otimes>\<^bsub>product_group I G\<^esub> (\<lambda>a\<in>I. \<one>\<^bsub>G a\<^esub>)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    75
      by (metis (no_types) L group.is_monoid monoid.l_one one_product_group singletonI trivial_group_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    76
    then show ?thesis
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    77
      using 1 by (simp add: that)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    78
  qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    79
  show ?rhs
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    80
    using L
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    81
    by (auto simp: trivial_group_def product_group_def PiE_eq_singleton intro: groupI)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    82
next
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    83
  assume ?rhs
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    84
  then show ?lhs
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    85
    by (simp add: PiE_eq_singleton trivial_group_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    86
qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    87
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    88
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    89
lemma PiE_subgroup_product_group:
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    90
  assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    91
  shows "subgroup (PiE I H) (product_group I G) \<longleftrightarrow> (\<forall>i \<in> I. subgroup (H i) (G i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    92
    (is "?lhs = ?rhs")
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    93
proof
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    94
  assume L: ?lhs
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    95
  then have [simp]: "PiE I H \<noteq> {}"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    96
    using subgroup_nonempty by force
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    97
  show ?rhs
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    98
  proof (clarify; unfold_locales)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    99
    show sub: "H i \<subseteq> carrier (G i)" if "i \<in> I" for i
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   100
      using that L by (simp add: subgroup_def) (metis (no_types, lifting) L subgroup_nonempty subset_PiE)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   101
    show "x \<otimes>\<^bsub>G i\<^esub> y \<in> H i" if "i \<in> I" "x \<in> H i" "y \<in> H i" for i x y
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   102
    proof -
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   103
      have *: "\<And>x. x \<in> Pi\<^sub>E I H \<Longrightarrow> (\<forall>y \<in> Pi\<^sub>E I H. \<forall>i\<in>I. x i \<otimes>\<^bsub>G i\<^esub> y i \<in> H i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   104
        using L by (auto simp: subgroup_def Pi_iff)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   105
      have "\<forall>y\<in>H i. f i \<otimes>\<^bsub>G i\<^esub> y \<in> H i" if f: "f \<in> Pi\<^sub>E I H" and "i \<in> I" for i f
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   106
        using * [OF f] \<open>i \<in> I\<close>
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   107
        by (subst(asm) all_PiE_elements) auto
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   108
      then have "\<forall>f \<in> Pi\<^sub>E I H. \<forall>i \<in> I. \<forall>y\<in>H i. f i \<otimes>\<^bsub>G i\<^esub> y \<in> H i"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   109
        by blast
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   110
      with that show ?thesis
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   111
        by (subst(asm) all_PiE_elements) auto
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   112
    qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   113
    show "\<one>\<^bsub>G i\<^esub> \<in> H i" if "i \<in> I" for i
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   114
      using L subgroup.one_closed that by fastforce
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   115
    show "inv\<^bsub>G i\<^esub> x \<in> H i" if "i \<in> I" and x: "x \<in> H i" for i x
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   116
    proof -
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   117
      have *: "\<forall>y \<in> Pi\<^sub>E I H. \<forall>i\<in>I. inv\<^bsub>G i\<^esub> y i \<in> H i"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   118
      proof
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   119
        fix y
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   120
        assume y: "y \<in> Pi\<^sub>E I H"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   121
        then have yc: "y \<in> carrier (product_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   122
          by (metis (no_types) L subgroup_def subsetCE)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   123
        have "inv\<^bsub>product_group I G\<^esub> y \<in> Pi\<^sub>E I H"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   124
          by (simp add: y L subgroup.m_inv_closed)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   125
        moreover have "inv\<^bsub>product_group I G\<^esub> y = (\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> y i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   126
          using yc by (simp add: assms)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   127
        ultimately show "\<forall>i\<in>I. inv\<^bsub>G i\<^esub> y i \<in> H i"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   128
          by auto
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   129
      qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   130
      then have "\<forall>i\<in>I. \<forall>x\<in>H i. inv\<^bsub>G i\<^esub> x \<in> H i"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   131
        by (subst(asm) all_PiE_elements) auto
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   132
      then show ?thesis
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   133
        using that(1) x by blast
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   134
    qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   135
  qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   136
next
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   137
  assume R: ?rhs
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   138
  show ?lhs
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   139
  proof
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   140
    show "Pi\<^sub>E I H \<subseteq> carrier (product_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   141
      using R by (force simp: subgroup_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   142
    show "x \<otimes>\<^bsub>product_group I G\<^esub> y \<in> Pi\<^sub>E I H" if "x \<in> Pi\<^sub>E I H" "y \<in> Pi\<^sub>E I H" for x y
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   143
      using R that by (auto simp: PiE_iff subgroup_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   144
    show "\<one>\<^bsub>product_group I G\<^esub> \<in> Pi\<^sub>E I H"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   145
      using R by (force simp: subgroup_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   146
    show "inv\<^bsub>product_group I G\<^esub> x \<in> Pi\<^sub>E I H" if "x \<in> Pi\<^sub>E I H" for x
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   147
    proof -
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   148
      have x: "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   149
        using R that by (force simp:  subgroup_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   150
      show ?thesis
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   151
        using assms R that by (fastforce simp: x assms subgroup_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   152
    qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   153
  qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   154
qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   155
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   156
lemma product_group_subgroup_generated:
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   157
  assumes "\<And>i. i \<in> I \<Longrightarrow> subgroup (H i) (G i)" and gp: "\<And>i. i \<in> I \<Longrightarrow> group (G i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   158
  shows "product_group I (\<lambda>i. subgroup_generated (G i) (H i))
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   159
       = subgroup_generated (product_group I G) (PiE I H)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   160
proof (rule monoid.equality)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   161
  have [simp]: "\<And>i. i \<in> I \<Longrightarrow> carrier (G i) \<inter> H i = H i" "(\<Pi>\<^sub>E i\<in>I. carrier (G i)) \<inter> Pi\<^sub>E I H = Pi\<^sub>E I H"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   162
    using assms by (force simp: subgroup_def)+
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   163
  have "(\<Pi>\<^sub>E i\<in>I. generate (G i) (H i)) = generate (product_group I G) (Pi\<^sub>E I H)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   164
  proof (rule group.generateI)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   165
    show "Group.group (product_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   166
      using assms by simp
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   167
    show "subgroup (\<Pi>\<^sub>E i\<in>I. generate (G i) (H i)) (product_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   168
      using assms by (simp add: PiE_subgroup_product_group group.generate_is_subgroup subgroup.subset)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   169
    show "Pi\<^sub>E I H \<subseteq> (\<Pi>\<^sub>E i\<in>I. generate (G i) (H i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   170
      using assms by (auto simp: PiE_iff generate.incl)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   171
    show "(\<Pi>\<^sub>E i\<in>I. generate (G i) (H i)) \<subseteq> K"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   172
      if "subgroup K (product_group I G)" "Pi\<^sub>E I H \<subseteq> K" for K
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   173
      using assms that group.generate_subgroup_incl by fastforce
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   174
  qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   175
  with assms
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   176
  show "carrier (product_group I (\<lambda>i. subgroup_generated (G i) (H i))) =
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   177
        carrier (subgroup_generated (product_group I G) (Pi\<^sub>E I H))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   178
    by (simp add: carrier_subgroup_generated cong: PiE_cong)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   179
qed auto
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   180
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   181
lemma finite_product_group:
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   182
  assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   183
  shows
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   184
   "finite (carrier (product_group I G)) \<longleftrightarrow>
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   185
    finite {i. i \<in> I \<and> ~ trivial_group(G i)} \<and> (\<forall>i \<in> I. finite(carrier(G i)))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   186
proof -
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   187
  have [simp]: "\<And>i. i \<in> I \<Longrightarrow> carrier (G i) \<noteq> {}"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   188
    using assms group.is_monoid by blast
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   189
  show ?thesis
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   190
    by (auto simp: finite_PiE_iff PiE_eq_empty_iff group.trivial_group_alt [OF assms] cong: Collect_cong conj_cong)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   191
qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   192
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   193
subsection \<open>Sum of a Family of Groups\<close>
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   194
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   195
definition sum_group :: "'a set \<Rightarrow> ('a \<Rightarrow> ('b, 'c) monoid_scheme) \<Rightarrow> ('a \<Rightarrow> 'b) monoid"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   196
  where "sum_group I G \<equiv>
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   197
        subgroup_generated
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   198
         (product_group I G)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   199
         {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   200
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   201
lemma subgroup_sum_group:
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   202
  assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   203
  shows "subgroup {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   204
                  (product_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   205
proof unfold_locales
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   206
  fix x y
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   207
  have *: "{i. (i \<in> I \<longrightarrow> x i \<otimes>\<^bsub>G i\<^esub> y i \<noteq> \<one>\<^bsub>G i\<^esub>) \<and> i \<in> I}
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   208
        \<subseteq> {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>} \<union> {i \<in> I. y i \<noteq> \<one>\<^bsub>G i\<^esub>}"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   209
    by (auto simp: Group.group_def dest: assms)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   210
  assume
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   211
    "x \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   212
    "y \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   213
  then
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   214
  show "x \<otimes>\<^bsub>product_group I G\<^esub> y \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   215
    using assms
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   216
    apply (auto simp: Group.group_def monoid.m_closed PiE_iff)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   217
    apply (rule finite_subset [OF *])
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   218
    by blast
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   219
next
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   220
  fix x
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   221
  assume "x \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   222
  then show "inv\<^bsub>product_group I G\<^esub> x \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   223
    using assms
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   224
    by (auto simp: PiE_iff assms group.inv_eq_1_iff [OF assms] conj_commute cong: rev_conj_cong)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   225
qed (use assms [unfolded Group.group_def] in auto)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   226
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   227
lemma carrier_sum_group:
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   228
  assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   229
  shows "carrier(sum_group I G) = {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   230
proof -
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   231
  interpret SG: subgroup "{x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}" "(product_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   232
    by (simp add: assms subgroup_sum_group)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   233
  show ?thesis
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   234
    by (simp add: sum_group_def subgroup_sum_group carrier_subgroup_generated_alt)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   235
qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   236
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   237
lemma one_sum_group [simp]: "\<one>\<^bsub>sum_group I G\<^esub> = (\<lambda>i\<in>I. \<one>\<^bsub>G i\<^esub>)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   238
  by (simp add: sum_group_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   239
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   240
lemma mult_sum_group [simp]: "(\<otimes>\<^bsub>sum_group I G\<^esub>) = (\<lambda>x y. (\<lambda>i\<in>I. x i \<otimes>\<^bsub>G i\<^esub> y i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   241
  by (auto simp: sum_group_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   242
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   243
lemma sum_group [simp]:
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   244
  assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)" shows "group (sum_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   245
proof (rule groupI)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   246
  note group.is_monoid [OF assms, simp]
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   247
  show "x \<otimes>\<^bsub>sum_group I G\<^esub> y \<in> carrier (sum_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   248
    if "x \<in> carrier (sum_group I G)" and
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   249
      "y \<in> carrier (sum_group I G)" for x y
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   250
  proof -
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   251
    have *: "{i \<in> I. x i \<otimes>\<^bsub>G i\<^esub> y i \<noteq> \<one>\<^bsub>G i\<^esub>} \<subseteq> {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>} \<union> {i \<in> I. y i \<noteq> \<one>\<^bsub>G i\<^esub>}"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   252
      by auto
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   253
    show ?thesis
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   254
      using that
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   255
      apply (simp add: assms carrier_sum_group PiE_iff monoid.m_closed conj_commute cong: rev_conj_cong)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   256
      apply (blast intro: finite_subset [OF *])
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   257
      done
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   258
  qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   259
  show "\<one>\<^bsub>sum_group I G\<^esub> \<otimes>\<^bsub>sum_group I G\<^esub> x = x"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   260
    if "x \<in> carrier (sum_group I G)" for x
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   261
    using that by (auto simp: assms carrier_sum_group PiE_iff extensional_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   262
  show "\<exists>y\<in>carrier (sum_group I G). y \<otimes>\<^bsub>sum_group I G\<^esub> x = \<one>\<^bsub>sum_group I G\<^esub>"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   263
    if "x \<in> carrier (sum_group I G)" for x
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   264
  proof
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   265
    let ?y = "\<lambda>i\<in>I. m_inv (G i) (x i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   266
    show "?y \<otimes>\<^bsub>sum_group I G\<^esub> x = \<one>\<^bsub>sum_group I G\<^esub>"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   267
      using that assms
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   268
      by (auto simp: carrier_sum_group PiE_iff group.l_inv)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   269
    show "?y \<in> carrier (sum_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   270
      using that assms
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   271
      by (auto simp: carrier_sum_group PiE_iff group.inv_eq_1_iff group.l_inv cong: conj_cong)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   272
  qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   273
qed (auto simp: assms carrier_sum_group PiE_iff group.is_monoid monoid.m_assoc)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   274
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   275
lemma inv_sum_group [simp]:
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   276
  assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)" and x: "x \<in> carrier (sum_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   277
  shows "m_inv (sum_group I G) x = (\<lambda>i\<in>I. m_inv (G i) (x i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   278
proof (rule group.inv_equality)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   279
  show "(\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> x i) \<otimes>\<^bsub>sum_group I G\<^esub> x = \<one>\<^bsub>sum_group I G\<^esub>"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   280
    using x by (auto simp: carrier_sum_group PiE_iff group.l_inv assms intro: restrict_ext)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   281
  show "(\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> x i) \<in> carrier (sum_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   282
    using x by (simp add: carrier_sum_group PiE_iff group.inv_eq_1_iff assms conj_commute cong: rev_conj_cong)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   283
qed (auto simp: assms)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   284
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   285
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   286
thm group.subgroups_Inter (*REPLACE*)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   287
theorem subgroup_Inter:
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   288
  assumes subgr: "(\<And>H. H \<in> A \<Longrightarrow> subgroup H G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   289
    and not_empty: "A \<noteq> {}"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   290
  shows "subgroup (\<Inter>A) G"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   291
proof
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   292
  show "\<Inter> A \<subseteq> carrier G"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   293
    by (simp add: Inf_less_eq not_empty subgr subgroup.subset)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   294
qed (auto simp: subgr subgroup.m_closed subgroup.one_closed subgroup.m_inv_closed)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   295
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   296
thm group.subgroups_Inter_pair (*REPLACE*)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   297
lemma subgroup_Int:
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   298
  assumes "subgroup I G" "subgroup J G"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   299
  shows "subgroup (I \<inter> J) G" using subgroup_Inter[ where ?A = "{I,J}"] assms by auto
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   300
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   301
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   302
lemma sum_group_subgroup_generated:
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   303
  assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)" and sg: "\<And>i. i \<in> I \<Longrightarrow> subgroup (H i) (G i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   304
  shows "sum_group I (\<lambda>i. subgroup_generated (G i) (H i)) = subgroup_generated (sum_group I G) (PiE I H)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   305
proof (rule monoid.equality)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   306
  have "subgroup (carrier (sum_group I G) \<inter> Pi\<^sub>E I H) (product_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   307
    by (rule subgroup_Int) (auto simp: assms carrier_sum_group subgroup_sum_group PiE_subgroup_product_group)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   308
  moreover have "carrier (sum_group I G) \<inter> Pi\<^sub>E I H
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   309
              \<subseteq> carrier (subgroup_generated (product_group I G)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   310
                    {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}})"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   311
    by (simp add: assms subgroup_sum_group subgroup.carrier_subgroup_generated_subgroup carrier_sum_group)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   312
  ultimately
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   313
  have "subgroup (carrier (sum_group I G) \<inter> Pi\<^sub>E I H) (sum_group I G)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   314
    by (simp add: assms sum_group_def group.subgroup_subgroup_generated_iff)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   315
  then have *: "{f \<in> \<Pi>\<^sub>E i\<in>I. carrier (subgroup_generated (G i) (H i)). finite {i \<in> I. f i \<noteq> \<one>\<^bsub>G i\<^esub>}}
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   316
      = carrier (subgroup_generated (sum_group I G) (carrier (sum_group I G) \<inter> Pi\<^sub>E I H))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   317
    apply (simp only: subgroup.carrier_subgroup_generated_subgroup)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   318
    using subgroup.subset [OF sg]
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   319
    apply (auto simp: set_eq_iff PiE_def Pi_def assms carrier_sum_group subgroup.carrier_subgroup_generated_subgroup)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   320
    done
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   321
  then show "carrier (sum_group I (\<lambda>i. subgroup_generated (G i) (H i))) =
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   322
        carrier (subgroup_generated (sum_group I G) (Pi\<^sub>E I H))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   323
    by simp (simp add: assms group.subgroupE(1) group.group_subgroup_generated carrier_sum_group)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   324
qed (auto simp: sum_group_def subgroup_generated_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   325
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   326
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   327
lemma iso_product_groupI:
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   328
  assumes iso: "\<And>i. i \<in> I \<Longrightarrow> G i \<cong> H i"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   329
    and G: "\<And>i. i \<in> I \<Longrightarrow> group (G i)" and H: "\<And>i. i \<in> I \<Longrightarrow> group (H i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   330
  shows "product_group I G \<cong> product_group I H" (is "?IG \<cong> ?IH")
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   331
proof -
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   332
  have "\<And>i. i \<in> I \<Longrightarrow> \<exists>h. h \<in> iso (G i) (H i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   333
    using iso by (auto simp: is_iso_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   334
  then obtain f where f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> iso (G i) (H i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   335
    by metis
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   336
  define h where "h \<equiv> \<lambda>x. (\<lambda>i\<in>I. f i (x i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   337
  have hom: "h \<in> iso ?IG ?IH"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   338
  proof (rule isoI)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   339
    show hom: "h \<in> hom ?IG ?IH"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   340
    proof (rule homI)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   341
      fix x
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   342
      assume "x \<in> carrier ?IG"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   343
      with f show "h x \<in> carrier ?IH"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   344
        using PiE by (fastforce simp add: h_def PiE_def iso_def hom_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   345
    next
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   346
      fix x y
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   347
      assume "x \<in> carrier ?IG" "y \<in> carrier ?IG"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   348
      with f show "h (x \<otimes>\<^bsub>?IG\<^esub> y) = h x \<otimes>\<^bsub>?IH\<^esub> h y"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   349
        apply (simp add: h_def PiE_def iso_def hom_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   350
        using PiE by (fastforce simp add: h_def PiE_def iso_def hom_def intro: restrict_ext)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   351
    qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   352
    with G H interpret GH : group_hom "?IG" "?IH" h
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   353
      by (simp add: group_hom_def group_hom_axioms_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   354
    show "bij_betw h (carrier ?IG) (carrier ?IH)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   355
      unfolding bij_betw_def
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   356
    proof (intro conjI subset_antisym)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   357
      have "\<gamma> i = \<one>\<^bsub>G i\<^esub>"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   358
        if \<gamma>: "\<gamma> \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" and eq: "(\<lambda>i\<in>I. f i (\<gamma> i)) = (\<lambda>i\<in>I. \<one>\<^bsub>H i\<^esub>)" and "i \<in> I"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   359
        for \<gamma> i
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   360
      proof -
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   361
        have "inj_on (f i) (carrier (G i))" "f i \<in> hom (G i) (H i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   362
          using \<open>i \<in> I\<close> f by (auto simp: iso_def bij_betw_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   363
        then have *: "\<And>x. \<lbrakk>f i x = \<one>\<^bsub>H i\<^esub>; x \<in> carrier (G i)\<rbrakk> \<Longrightarrow> x = \<one>\<^bsub>G i\<^esub>"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   364
          by (metis G Group.group_def H hom_one inj_onD monoid.one_closed \<open>i \<in> I\<close>)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   365
        show ?thesis
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   366
          using eq \<open>i \<in> I\<close> * \<gamma> by (simp add: fun_eq_iff) (meson PiE_iff)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   367
      qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   368
      then show "inj_on h (carrier ?IG)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   369
        apply (simp add: iso_def bij_betw_def GH.inj_on_one_iff flip: carrier_product_group)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   370
        apply (force simp: h_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   371
        done
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   372
    next
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   373
      show "h ` carrier ?IG \<subseteq> carrier ?IH"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   374
        unfolding h_def using f
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   375
        by (force simp: PiE_def Pi_def Group.iso_def dest!: bij_betwE)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   376
    next
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   377
      show "carrier ?IH \<subseteq> h ` carrier ?IG"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   378
        unfolding h_def
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   379
      proof (clarsimp simp: iso_def bij_betw_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   380
        fix x
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   381
        assume "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (H i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   382
        with f have x: "x \<in> (\<Pi>\<^sub>E i\<in>I. f i ` carrier (G i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   383
          unfolding h_def by (auto simp: iso_def bij_betw_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   384
        have "\<And>i. i \<in> I \<Longrightarrow> inj_on (f i) (carrier (G i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   385
          using f by (auto simp: iso_def bij_betw_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   386
        let ?g = "\<lambda>i\<in>I. inv_into (carrier (G i)) (f i) (x i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   387
        show "x \<in> (\<lambda>g. \<lambda>i\<in>I. f i (g i)) ` (\<Pi>\<^sub>E i\<in>I. carrier (G i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   388
        proof
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   389
          show "x = (\<lambda>i\<in>I. f i (?g i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   390
            using x by (auto simp: PiE_iff fun_eq_iff extensional_def f_inv_into_f)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   391
          show "?g \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   392
            using x by (auto simp: PiE_iff inv_into_into)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   393
        qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   394
      qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   395
    qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   396
  qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   397
  then show ?thesis
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   398
    using is_iso_def by auto
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   399
qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   400
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   401
lemma iso_sum_groupI:
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   402
  assumes iso: "\<And>i. i \<in> I \<Longrightarrow> G i \<cong> H i"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   403
    and G: "\<And>i. i \<in> I \<Longrightarrow> group (G i)" and H: "\<And>i. i \<in> I \<Longrightarrow> group (H i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   404
  shows "sum_group I G \<cong> sum_group I H" (is "?IG \<cong> ?IH")
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   405
proof -
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   406
  have "\<And>i. i \<in> I \<Longrightarrow> \<exists>h. h \<in> iso (G i) (H i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   407
    using iso by (auto simp: is_iso_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   408
  then obtain f where f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> iso (G i) (H i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   409
    by metis
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   410
  then have injf: "inj_on (f i) (carrier (G i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   411
    and homf: "f i \<in> hom (G i) (H i)" if "i \<in> I" for i
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   412
    using \<open>i \<in> I\<close> f by (auto simp: iso_def bij_betw_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   413
  then have one: "\<And>x. \<lbrakk>f i x = \<one>\<^bsub>H i\<^esub>; x \<in> carrier (G i)\<rbrakk> \<Longrightarrow> x = \<one>\<^bsub>G i\<^esub>" if "i \<in> I" for i
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   414
    by (metis G H group.subgroup_self hom_one inj_on_eq_iff subgroup.one_closed that)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   415
  have fin1: "finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>} \<Longrightarrow> finite {i \<in> I. f i (x i) \<noteq> \<one>\<^bsub>H i\<^esub>}" for x
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   416
    using homf by (auto simp: G H hom_one elim!: rev_finite_subset)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   417
  define h where "h \<equiv> \<lambda>x. (\<lambda>i\<in>I. f i (x i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   418
  have hom: "h \<in> iso ?IG ?IH"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   419
  proof (rule isoI)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   420
    show hom: "h \<in> hom ?IG ?IH"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   421
    proof (rule homI)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   422
      fix x
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   423
      assume "x \<in> carrier ?IG"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   424
      with f fin1 show "h x \<in> carrier ?IH"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   425
        by (force simp: h_def PiE_def iso_def hom_def carrier_sum_group assms conj_commute cong: conj_cong)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   426
    next
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   427
      fix x y
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   428
      assume "x \<in> carrier ?IG" "y \<in> carrier ?IG"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   429
      with homf show "h (x \<otimes>\<^bsub>?IG\<^esub> y) = h x \<otimes>\<^bsub>?IH\<^esub> h y"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   430
        by (fastforce simp add: h_def PiE_def hom_def carrier_sum_group assms intro: restrict_ext)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   431
    qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   432
    with G H interpret GH : group_hom "?IG" "?IH" h
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   433
      by (simp add: group_hom_def group_hom_axioms_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   434
    show "bij_betw h (carrier ?IG) (carrier ?IH)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   435
      unfolding bij_betw_def
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   436
    proof (intro conjI subset_antisym)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   437
      have \<gamma>: "\<gamma> i = \<one>\<^bsub>G i\<^esub>"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   438
        if "\<gamma> \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" and eq: "(\<lambda>i\<in>I. f i (\<gamma> i)) = (\<lambda>i\<in>I. \<one>\<^bsub>H i\<^esub>)" and "i \<in> I"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   439
        for \<gamma> i
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   440
        using \<open>i \<in> I\<close> one that by (simp add: fun_eq_iff) (meson PiE_iff)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   441
      show "inj_on h (carrier ?IG)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   442
        apply (simp add: iso_def bij_betw_def GH.inj_on_one_iff assms one flip: carrier_sum_group)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   443
        apply (auto simp: h_def fun_eq_iff carrier_sum_group assms PiE_def Pi_def extensional_def one)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   444
        done
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   445
    next
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   446
      show "h ` carrier ?IG \<subseteq> carrier ?IH"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   447
        using homf GH.hom_closed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   448
        by (fastforce simp: h_def PiE_def Pi_def dest!: bij_betwE)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   449
    next
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   450
      show "carrier ?IH \<subseteq> h ` carrier ?IG"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   451
        unfolding h_def
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   452
      proof (clarsimp simp: iso_def bij_betw_def carrier_sum_group assms)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   453
        fix x
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   454
        assume x: "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (H i))" and fin: "finite {i \<in> I. x i \<noteq> \<one>\<^bsub>H i\<^esub>}"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   455
        with f have xf: "x \<in> (\<Pi>\<^sub>E i\<in>I. f i ` carrier (G i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   456
          unfolding h_def
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   457
          by (auto simp: iso_def bij_betw_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   458
        have "\<And>i. i \<in> I \<Longrightarrow> inj_on (f i) (carrier (G i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   459
          using f by (auto simp: iso_def bij_betw_def)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   460
        let ?g = "\<lambda>i\<in>I. inv_into (carrier (G i)) (f i) (x i)"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   461
        show "x \<in> (\<lambda>g. \<lambda>i\<in>I. f i (g i))
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   462
                 ` {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   463
        proof
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   464
          show xeq: "x = (\<lambda>i\<in>I. f i (?g i))"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   465
            using x by (clarsimp simp: PiE_iff fun_eq_iff extensional_def) (metis iso_iff f_inv_into_f f)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   466
          have "finite {i \<in> I. inv_into (carrier (G i)) (f i) (x i) \<noteq> \<one>\<^bsub>G i\<^esub>}"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   467
            apply (rule finite_subset [OF _ fin])
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   468
            using G H group.subgroup_self hom_one homf injf inv_into_f_eq subgroup.one_closed by fastforce
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   469
          with x show "?g \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   470
            apply (auto simp: PiE_iff inv_into_into conj_commute cong: conj_cong)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   471
            by (metis (no_types, hide_lams) iso_iff f inv_into_into)
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   472
        qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   473
      qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   474
    qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   475
  qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   476
  then show ?thesis
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   477
    using is_iso_def by auto
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   478
qed
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   479
6a9e2a82ea15 Products and sums of a family of groups
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   480
end