Quelle Product_Groups.thy Sprache: Isabelle

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

section \<open>Product and Sum Groups\<close>

theory Product_Groups
  imports Elementary_Groups "HOL-Library.Equipollence"

begin

subsection \<open>Product of a Family of Groups\<close>

definition product_group:: "'a set \ ('a \ ('b, 'c) monoid_scheme) \ ('a \ 'b) monoid"
  where "product_group I G \ \carrier = (\\<^sub>E i\I. carrier (G i)),
                              monoid.mult = (\<lambda>x y. (\<lambda>i\<in>I. x i \<otimes>\<^bsub>G i\<^esub> y i)),
                              one = (\<lambda>i\<in>I. \<one>\<^bsub>G i\<^esub>)\<rparr>"

lemma carrier_product_group [simp]: "carrier(product_group I G) = (\\<^sub>E i\I. carrier (G i))"
  by (simp add: product_group_def)

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

lemma mult_product_group [simp]: "(\\<^bsub>product_group I G\<^esub>) = (\x y. \i\I. x i \\<^bsub>G i\<^esub> y 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 \\<^bsub>G i\<^esub> y i) \ (\ i\I. carrier (G i))"
    if "x \ (\\<^sub>E i\I. carrier (G i))" "y \ (\\<^sub>E i\I. carrier (G i))" for x y
    using that assms group.subgroup_self subgroup.m_closed by fastforce
  show "(\i. \\<^bsub>G i\<^esub>) \ (\ i\I. carrier (G i))"
    by (simp add: assms group.is_monoid)
  show "(\i\I. (if i \ I then x i \\<^bsub>G i\<^esub> y i else undefined) \\<^bsub>G i\<^esub> z i) =
        (\<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))"
    if "x \ (\\<^sub>E i\I. carrier (G i))" "y \ (\\<^sub>E i\I. carrier (G i))" "z \ (\\<^sub>E i\I. 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 "(\i\I. (if i \ I then \\<^bsub>G i\<^esub> else undefined) \\<^bsub>G i\<^esub> x i) = x"
    if "x \ (\\<^sub>E i\I. carrier (G i))" for x
    using assms that by (fastforce simp: Group.group_def PiE_iff)
  show "\y\\\<^sub>E i\I. carrier (G i). (\i\I. y i \\<^bsub>G i\<^esub> x i) = (\i\I. \\<^bsub>G i\<^esub>)"
    if "x \ (\\<^sub>E i\I. carrier (G i))" for x
    by (rule_tac x="\i\I. inv\<^bsub>G i\<^esub> x i" in bexI) (use assms that in \auto simp: PiE_iff group.l_inv\)
qed

lemma inv_product_group [simp]:
  assumes "f \ (\\<^sub>E i\I. carrier (G i))" "\i. i \ I \ group (G i)"
  shows "inv\<^bsub>product_group I G\<^esub> f = (\i\I. inv\<^bsub>G i\<^esub> f i)"
proof (rule group.inv_equality)
  show "Group.group (product_group I G)"
    by (simp add: assms)
  show "(\i\I. inv\<^bsub>G i\<^esub> f i) \\<^bsub>product_group I G\<^esub> f = \\<^bsub>product_group I G\<^esub>"
    using assms by (auto simp: PiE_iff group.l_inv)
  show "f \ carrier (product_group I G)"
    using assms by simp
  show "(\i\I. inv\<^bsub>G i\<^esub> f 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 "inv\<^bsub>product_group I G\<^esub> (\a\I. \\<^bsub>G a\<^esub>) = \\<^bsub>product_group I G\<^esub>"
    by (metis group.is_monoid monoid.inv_one one_product_group trivial_group_def)
  have [simp]: "\\<^bsub>G i\<^esub> \\<^bsub>G i\<^esub> \\<^bsub>G i\<^esub> = \\<^bsub>G i\<^esub>" if "i \ I" for i
    unfolding trivial_group_def
  proof -
    have 1: "(\a\I. \\<^bsub>G a\<^esub>) i = \\<^bsub>G i\<^esub>"
      by (simp add: that)
    have "(\a\I. \\<^bsub>G a\<^esub>) = (\a\I. \\<^bsub>G a\<^esub>) \\<^bsub>product_group I G\<^esub> (\a\I. \\<^bsub>G a\<^esub>)"
      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 \\<^bsub>G i\<^esub> y \ H i" if "i \ I" "x \ H i" "y \ H i" for i x y
    proof -
      have *: "\x. x \ Pi\<^sub>E I H \ (\y \ Pi\<^sub>E I H. \i\I. x i \\<^bsub>G i\<^esub> y i \ H i)"
        using L by (auto simp: subgroup_def Pi_iff)
      have "\y\H i. f i \\<^bsub>G i\<^esub> y \ H i" if f: "f \ Pi\<^sub>E I H" and "i \ I" for i f
        using * [OF f] \<open>i \<in> I\<close>
        by (subst(asm) all_PiE_elements) auto
      then have "\f \ Pi\<^sub>E I H. \i \ I. \y\H i. f i \\<^bsub>G i\<^esub> y \ H i"
        by blast
      with that show ?thesis
        by (subst(asm) all_PiE_elements) auto
    qed
    show "\\<^bsub>G i\<^esub> \ H i" if "i \ I" for i
      using L subgroup.one_closed that by fastforce
    show "inv\<^bsub>G i\<^esub> x \ H i" if "i \ I" and x: "x \ H i" for i x
    proof -
      have *: "\y \ Pi\<^sub>E I H. \i\I. inv\<^bsub>G i\<^esub> y i \ H i"
      proof
        fix y
        assume y: "y \ Pi\<^sub>E I H"
        then have yc: "y \ carrier (product_group I G)"
          by (metis (no_types) L subgroup_def subsetCE)
        have "inv\<^bsub>product_group I G\<^esub> y \ Pi\<^sub>E I H"
          by (simp add: y L subgroup.m_inv_closed)
        moreover have "inv\<^bsub>product_group I G\<^esub> y = (\i\I. inv\<^bsub>G i\<^esub> y i)"
          using yc by (simp add: assms)
        ultimately show "\i\I. inv\<^bsub>G i\<^esub> y i \ H i"
          by auto
      qed
      then have "\i\I. \x\H i. inv\<^bsub>G i\<^esub> x \ 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 "Pi\<^sub>E I H \ carrier (product_group I G)"
      using R by (force simp: subgroup_def)
    show "x \\<^bsub>product_group I G\<^esub> y \ Pi\<^sub>E I H" if "x \ Pi\<^sub>E I H" "y \ Pi\<^sub>E I H" for x y
      using R that by (auto simp: PiE_iff subgroup_def)
    show "\\<^bsub>product_group I G\<^esub> \ Pi\<^sub>E I H"
      using R by (force simp: subgroup_def)
    show "inv\<^bsub>product_group I G\<^esub> x \ Pi\<^sub>E I H" if "x \ Pi\<^sub>E I H" for x
    proof -
      have x: "x \ (\\<^sub>E i\I. 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" "(\\<^sub>E i\I. carrier (G i)) \ Pi\<^sub>E I H = Pi\<^sub>E I H"
    using assms by (force simp: subgroup_def)+
  have "(\\<^sub>E i\I. generate (G i) (H i)) = generate (product_group I G) (Pi\<^sub>E I H)"
  proof (rule group.generateI)
    show "Group.group (product_group I G)"
      using assms by simp
    show "subgroup (\\<^sub>E i\I. 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 "Pi\<^sub>E I H \ (\\<^sub>E i\I. generate (G i) (H i))"
      using assms by (auto simp: PiE_iff generate.incl)
    show "(\\<^sub>E i\I. generate (G i) (H i)) \ K"
      if "subgroup K (product_group I G)" "Pi\<^sub>E 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) (Pi\<^sub>E 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 \<in> I \<and> ~ trivial_group(G i)} \<and> (\<forall>i \<in> 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 \<open>Sum of a Family of Groups\<close>

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 \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"

lemma subgroup_sum_group:
  assumes "\i. i \ I \ group (G i)"
  shows "subgroup {x \ \\<^sub>E i\I. carrier (G i). finite {i \ I. x i \ \\<^bsub>G i\<^esub>}}
                  (product_group I G)"
proof unfold_locales
  fix x y
  have *: "{i. (i \ I \ x i \\<^bsub>G i\<^esub> y i \ \\<^bsub>G i\<^esub>) \ i \ I}
        \<subseteq> {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>} \<union> {i \<in> I. y i \<noteq> \<one>\<^bsub>G i\<^esub>}"
    by (auto simp: Group.group_def dest: assms)
  assume
    "x \ {x \ \\<^sub>E i\I. carrier (G i). finite {i \ I. x i \ \\<^bsub>G i\<^esub>}}"
    "y \ {x \ \\<^sub>E i\I. carrier (G i). finite {i \ I. x i \ \\<^bsub>G i\<^esub>}}"
  then
  show "x \\<^bsub>product_group I G\<^esub> y \ {x \ \\<^sub>E i\I. carrier (G i). finite {i \ I. x i \ \\<^bsub>G i\<^esub>}}"
    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 \ \\<^sub>E i\I. carrier (G i). finite {i \ I. x i \ \\<^bsub>G i\<^esub>}}"
  then show "inv\<^bsub>product_group I G\<^esub> x \ {x \ \\<^sub>E i\I. carrier (G i). finite {i \ I. x i \ \\<^bsub>G i\<^esub>}}"
    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 \ \\<^sub>E i\I. carrier (G i). finite {i \ I. x i \ \\<^bsub>G i\<^esub>}}"
proof -
  interpret SG: subgroup "{x \ \\<^sub>E i\I. carrier (G i). finite {i \ I. x i \ \\<^bsub>G i\<^esub>}}" "(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]: "\\<^bsub>sum_group I G\<^esub> = (\i\I. \\<^bsub>G i\<^esub>)"
  by (simp add: sum_group_def)

lemma mult_sum_group [simp]: "(\\<^bsub>sum_group I G\<^esub>) = (\x y. (\i\I. x i \\<^bsub>G i\<^esub> y 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 \\<^bsub>sum_group I G\<^esub> y \ 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 \\<^bsub>G i\<^esub> y i \ \\<^bsub>G i\<^esub>} \ {i \ I. x i \ \\<^bsub>G i\<^esub>} \ {i \ I. y i \ \\<^bsub>G i\<^esub>}"
      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 "\\<^bsub>sum_group I G\<^esub> \\<^bsub>sum_group I G\<^esub> x = x"
    if "x \ carrier (sum_group I G)" for x
    using that by (auto simp: assms carrier_sum_group PiE_iff extensional_def)
  show "\y\carrier (sum_group I G). y \\<^bsub>sum_group I G\<^esub> x = \\<^bsub>sum_group I G\<^esub>"
    if "x \ carrier (sum_group I G)" for x
  proof
    let ?y = "\i\I. m_inv (G i) (x i)"
    show "?y \\<^bsub>sum_group I G\<^esub> x = \\<^bsub>sum_group I G\<^esub>"
      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 = (\i\I. m_inv (G i) (x i))"
proof (rule group.inv_equality)
  show "(\i\I. inv\<^bsub>G i\<^esub> x i) \\<^bsub>sum_group I G\<^esub> x = \\<^bsub>sum_group I G\<^esub>"
    using x by (auto simp: carrier_sum_group PiE_iff group.l_inv assms intro: restrict_ext)
  show "(\i\I. inv\<^bsub>G i\<^esub> x 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) \ Pi\<^sub>E 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) \ Pi\<^sub>E I H
              \<subseteq> carrier (subgroup_generated (product_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>}})"
    by (simp add: assms subgroup_sum_group subgroup.carrier_subgroup_generated_subgroup carrier_sum_group)
  ultimately
  have "subgroup (carrier (sum_group I G) \ Pi\<^sub>E I H) (sum_group I G)"
    by (simp add: assms sum_group_def group.subgroup_subgroup_generated_iff)
  then have *: "{f \ \\<^sub>E i\I. carrier (subgroup_generated (G i) (H i)). finite {i \ I. f i \ \\<^bsub>G i\<^esub>}}
      = carrier (subgroup_generated (sum_group I G) (carrier (sum_group I G) \<inter> Pi\<^sub>E 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) (Pi\<^sub>E 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. (\i\I. 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 \\<^bsub>?IG\<^esub> y) = h x \\<^bsub>?IH\<^esub> h 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 = \\<^bsub>G i\<^esub>"
        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"
        for \<gamma> i
      proof -
        have "inj_on (f i) (carrier (G i))" "f i \ hom (G i) (H i)"
          using \<open>i \<in> I\<close> f by (auto simp: iso_def bij_betw_def)
        then have *: "\x. \f i x = \\<^bsub>H i\<^esub>; x \ carrier (G i)\ \ x = \\<^bsub>G i\<^esub>"
          by (metis G Group.group_def H hom_one inj_onD monoid.one_closed \<open>i \<in> I\<close>)
        show ?thesis
          using eq \<open>i \<in> I\<close> * \<gamma> 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 \ (\\<^sub>E i\I. carrier (H i))"
        with f have x: "x \ (\\<^sub>E i\I. 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 = "\i\I. inv_into (carrier (G i)) (f i) (x i)"
        show "x \ (\g. \i\I. f i (g i)) ` (\\<^sub>E i\I. carrier (G i))"
        proof
          show "x = (\i\I. f i (?g i))"
            using x by (auto simp: PiE_iff fun_eq_iff extensional_def f_inv_into_f)
          show "?g \ (\\<^sub>E i\I. 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 \<open>i \<in> I\<close> f by (auto simp: iso_def bij_betw_def)
  then have one: "\x. \f i x = \\<^bsub>H i\<^esub>; x \ carrier (G i)\ \ x = \\<^bsub>G i\<^esub>" 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 \ \\<^bsub>G i\<^esub>} \ finite {i \ I. f i (x i) \ \\<^bsub>H i\<^esub>}" for x
    using homf by (auto simp: G H hom_one elim!: rev_finite_subset)
  define h where "h \ \x. (\i\I. 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 \\<^bsub>?IG\<^esub> y) = h x \\<^bsub>?IH\<^esub> h 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 \<gamma>: "\<gamma> i = \<one>\<^bsub>G i\<^esub>"
        if "\ \ (\\<^sub>E i\I. carrier (G i))" and eq: "(\i\I. f i (\ i)) = (\i\I. \\<^bsub>H i\<^esub>)" and "i \ I"
        for \<gamma> i
        using \<open>i \<in> I\<close> 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 \ (\\<^sub>E i\I. carrier (H i))" and fin: "finite {i \ I. x i \ \\<^bsub>H i\<^esub>}"
        with f have xf: "x \ (\\<^sub>E i\I. 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 = "\i\I. inv_into (carrier (G i)) (f i) (x i)"
        show "x \ (\g. \i\I. f i (g i))
                 ` {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}"
        proof
          show xeq: "x = (\i\I. 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) \ \\<^bsub>G i\<^esub>}"
            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 \ \\<^sub>E i\I. carrier (G i). finite {i \ I. x i \ \\<^bsub>G i\<^esub>}}"
            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

quality100%

¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.