Theory Product_Groups
section ‹Product and Sum Groups›
theory Product_Groups
imports Elementary_Groups "HOL-Library.Equipollence"
begin
subsection ‹Product of a Family of Groups›
definition product_group:: "'a set ⇒ ('a ⇒ ('b, 'c) monoid_scheme) ⇒ ('a ⇒ 'b) monoid"
where "product_group I G ≡ ⦇carrier = (Π⇩E i∈I. carrier (G i)),
monoid.mult = (λx y. (λi∈I. x i ⊗⇘G i⇙ y i)),
one = (λi∈I. 𝟭⇘G i⇙)⦈"
lemma carrier_product_group [simp]: "carrier(product_group I G) = (Π⇩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]: "(⊗⇘product_group I G⇙) = (λx y. λi∈I. x i ⊗⇘G i⇙ 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 ⊗⇘G i⇙ y i) ∈ (Π i∈I. carrier (G i))"
if "x ∈ (Π⇩E i∈I. carrier (G i))" "y ∈ (Π⇩E i∈I. carrier (G i))" for x y
using that assms group.subgroup_self subgroup.m_closed by fastforce
show "(λi. 𝟭⇘G i⇙) ∈ (Π i∈I. carrier (G i))"
by (simp add: assms group.is_monoid)
show "(λi∈I. (if i ∈ I then x i ⊗⇘G i⇙ y i else undefined) ⊗⇘G i⇙ z i) =
(λi∈I. x i ⊗⇘G i⇙ (if i ∈ I then y i ⊗⇘G i⇙ z i else undefined))"
if "x ∈ (Π⇩E i∈I. carrier (G i))" "y ∈ (Π⇩E i∈I. carrier (G i))" "z ∈ (Π⇩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 𝟭⇘G i⇙ else undefined) ⊗⇘G i⇙ x i) = x"
if "x ∈ (Π⇩E i∈I. carrier (G i))" for x
using assms that by (fastforce simp: Group.group_def PiE_iff)
show "∃y∈Π⇩E i∈I. carrier (G i). (λi∈I. y i ⊗⇘G i⇙ x i) = (λi∈I. 𝟭⇘G i⇙)"
if "x ∈ (Π⇩E i∈I. carrier (G i))" for x
by (rule_tac x="λi∈I. inv⇘G i⇙ x i" in bexI) (use assms that in ‹auto simp: PiE_iff group.l_inv›)
qed
lemma inv_product_group [simp]:
assumes "f ∈ (Π⇩E i∈I. carrier (G i))" "⋀i. i ∈ I ⟹ group (G i)"
shows "inv⇘product_group I G⇙ f = (λi∈I. inv⇘G i⇙ f i)"
proof (rule group.inv_equality)
show "Group.group (product_group I G)"
by (simp add: assms)
show "(λi∈I. inv⇘G i⇙ f i) ⊗⇘product_group I G⇙ f = 𝟭⇘product_group I G⇙"
using assms by (auto simp: PiE_iff group.l_inv)
show "f ∈ carrier (product_group I G)"
using assms by simp
show "(λi∈I. inv⇘G i⇙ 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⇘product_group I G⇙ (λa∈I. 𝟭⇘G a⇙) = 𝟭⇘product_group I G⇙"
by (metis group.is_monoid monoid.inv_one one_product_group trivial_group_def)
have [simp]: "𝟭⇘G i⇙ ⊗⇘G i⇙ 𝟭⇘G i⇙ = 𝟭⇘G i⇙" if "i ∈ I" for i
unfolding trivial_group_def
proof -
have 1: "(λa∈I. 𝟭⇘G a⇙) i = 𝟭⇘G i⇙"
by (simp add: that)
have "(λa∈I. 𝟭⇘G a⇙) = (λa∈I. 𝟭⇘G a⇙) ⊗⇘product_group I G⇙ (λa∈I. 𝟭⇘G a⇙)"
by (metis (no_types) L group.is_monoid monoid.l_one one_product_group singletonI trivial_group_def)
then show ?thesis
using 1 by (simp add: that)
qed
show ?rhs
using L
by (auto simp: trivial_group_def product_group_def PiE_eq_singleton intro: groupI)
next
assume ?rhs
then show ?lhs
by (simp add: PiE_eq_singleton trivial_group_def)
qed
lemma PiE_subgroup_product_group:
assumes "⋀i. i ∈ I ⟹ group (G i)"
shows "subgroup (PiE I H) (product_group I G) ⟷ (∀i ∈ I. subgroup (H i) (G i))"
(is "?lhs = ?rhs")
proof
assume L: ?lhs
then have [simp]: "PiE I H ≠ {}"
using subgroup_nonempty by force
show ?rhs
proof (clarify; unfold_locales)
show sub: "H i ⊆ carrier (G i)" if "i ∈ I" for i
using that L by (simp add: subgroup_def) (metis (no_types, lifting) L subgroup_nonempty subset_PiE)
show "x ⊗⇘G i⇙ y ∈ H i" if "i ∈ I" "x ∈ H i" "y ∈ H i" for i x y
proof -
have *: "⋀x. x ∈ Pi⇩E I H ⟹ (∀y ∈ Pi⇩E I H. ∀i∈I. x i ⊗⇘G i⇙ y i ∈ H i)"
using L by (auto simp: subgroup_def Pi_iff)
have "∀y∈H i. f i ⊗⇘G i⇙ y ∈ H i" if f: "f ∈ Pi⇩E I H" and "i ∈ I" for i f
using * [OF f] ‹i ∈ I›
by (subst(asm) all_PiE_elements) auto
then have "∀f ∈ Pi⇩E I H. ∀i ∈ I. ∀y∈H i. f i ⊗⇘G i⇙ y ∈ H i"
by blast
with that show ?thesis
by (subst(asm) all_PiE_elements) auto
qed
show "𝟭⇘G i⇙ ∈ H i" if "i ∈ I" for i
using L subgroup.one_closed that by fastforce
show "inv⇘G i⇙ x ∈ H i" if "i ∈ I" and x: "x ∈ H i" for i x
proof -
have *: "∀y ∈ Pi⇩E I H. ∀i∈I. inv⇘G i⇙ y i ∈ H i"
proof
fix y
assume y: "y ∈ Pi⇩E I H"
then have yc: "y ∈ carrier (product_group I G)"
by (metis (no_types) L subgroup_def subsetCE)
have "inv⇘product_group I G⇙ y ∈ Pi⇩E I H"
by (simp add: y L subgroup.m_inv_closed)
moreover have "inv⇘product_group I G⇙ y = (λi∈I. inv⇘G i⇙ y i)"
using yc by (simp add: assms)
ultimately show "∀i∈I. inv⇘G i⇙ y i ∈ H i"
by auto
qed
then have "∀i∈I. ∀x∈H i. inv⇘G i⇙ 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⇩E I H ⊆ carrier (product_group I G)"
using R by (force simp: subgroup_def)
show "x ⊗⇘product_group I G⇙ y ∈ Pi⇩E I H" if "x ∈ Pi⇩E I H" "y ∈ Pi⇩E I H" for x y
using R that by (auto simp: PiE_iff subgroup_def)
show "𝟭⇘product_group I G⇙ ∈ Pi⇩E I H"
using R by (force simp: subgroup_def)
show "inv⇘product_group I G⇙ x ∈ Pi⇩E I H" if "x ∈ Pi⇩E I H" for x
proof -
have x: "x ∈ (Π⇩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" "(Π⇩E i∈I. carrier (G i)) ∩ Pi⇩E I H = Pi⇩E I H"
using assms by (force simp: subgroup_def)+
have "(Π⇩E i∈I. generate (G i) (H i)) = generate (product_group I G) (Pi⇩E I H)"
proof (rule group.generateI)
show "Group.group (product_group I G)"
using assms by simp
show "subgroup (Π⇩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⇩E I H ⊆ (Π⇩E i∈I. generate (G i) (H i))"
using assms by (auto simp: PiE_iff generate.incl)
show "(Π⇩E i∈I. generate (G i) (H i)) ⊆ K"
if "subgroup K (product_group I G)" "Pi⇩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⇩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 ∈ I ∧ ~ trivial_group(G i)} ∧ (∀i ∈ I. finite(carrier(G i)))"
proof -
have [simp]: "⋀i. i ∈ I ⟹ carrier (G i) ≠ {}"
using assms group.is_monoid by blast
show ?thesis
by (auto simp: finite_PiE_iff PiE_eq_empty_iff group.trivial_group_alt [OF assms] cong: Collect_cong conj_cong)
qed
subsection ‹Sum of a Family of Groups›
definition sum_group :: "'a set ⇒ ('a ⇒ ('b, 'c) monoid_scheme) ⇒ ('a ⇒ 'b) monoid"
where "sum_group I G ≡
subgroup_generated
(product_group I G)
{x ∈ Π⇩E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 𝟭⇘G i⇙}}"
lemma subgroup_sum_group:
assumes "⋀i. i ∈ I ⟹ group (G i)"
shows "subgroup {x ∈ Π⇩E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 𝟭⇘G i⇙}}
(product_group I G)"
proof unfold_locales
fix x y
have *: "{i. (i ∈ I ⟶ x i ⊗⇘G i⇙ y i ≠ 𝟭⇘G i⇙) ∧ i ∈ I}
⊆ {i ∈ I. x i ≠ 𝟭⇘G i⇙} ∪ {i ∈ I. y i ≠ 𝟭⇘G i⇙}"
by (auto simp: Group.group_def dest: assms)
assume
"x ∈ {x ∈ Π⇩E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 𝟭⇘G i⇙}}"
"y ∈ {x ∈ Π⇩E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 𝟭⇘G i⇙}}"
then
show "x ⊗⇘product_group I G⇙ y ∈ {x ∈ Π⇩E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 𝟭⇘G i⇙}}"
using assms
apply (auto simp: Group.group_def monoid.m_closed PiE_iff)
apply (rule finite_subset [OF *])
by blast
next
fix x
assume "x ∈ {x ∈ Π⇩E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 𝟭⇘G i⇙}}"
then show "inv⇘product_group I G⇙ x ∈ {x ∈ Π⇩E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 𝟭⇘G i⇙}}"
using assms
by (auto simp: PiE_iff assms group.inv_eq_1_iff [OF assms] conj_commute cong: rev_conj_cong)
qed (use assms [unfolded Group.group_def] in auto)
lemma carrier_sum_group:
assumes "⋀i. i ∈ I ⟹ group (G i)"
shows "carrier(sum_group I G) = {x ∈ Π⇩E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 𝟭⇘G i⇙}}"
proof -
interpret SG: subgroup "{x ∈ Π⇩E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 𝟭⇘G i⇙}}" "(product_group I G)"
by (simp add: assms subgroup_sum_group)
show ?thesis
by (simp add: sum_group_def subgroup_sum_group carrier_subgroup_generated_alt)
qed
lemma one_sum_group [simp]: "𝟭⇘sum_group I G⇙ = (λi∈I. 𝟭⇘G i⇙)"
by (simp add: sum_group_def)
lemma mult_sum_group [simp]: "(⊗⇘sum_group I G⇙) = (λx y. (λi∈I. x i ⊗⇘G i⇙ 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 ⊗⇘sum_group I G⇙ 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 ⊗⇘G i⇙ y i ≠ 𝟭⇘G i⇙} ⊆ {i ∈ I. x i ≠ 𝟭⇘G i⇙} ∪ {i ∈ I. y i ≠ 𝟭⇘G i⇙}"
by auto
show ?thesis
using that
apply (simp add: assms carrier_sum_group PiE_iff monoid.m_closed conj_commute cong: rev_conj_cong)
apply (blast intro: finite_subset [OF *])
done
qed
show "𝟭⇘sum_group I G⇙ ⊗⇘sum_group I G⇙ 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 ⊗⇘sum_group I G⇙ x = 𝟭⇘sum_group I G⇙"
if "x ∈ carrier (sum_group I G)" for x
proof
let ?y = "λi∈I. m_inv (G i) (x i)"
show "?y ⊗⇘sum_group I G⇙ x = 𝟭⇘sum_group I G⇙"
using that assms
by (auto simp: carrier_sum_group PiE_iff group.l_inv)
show "?y ∈ carrier (sum_group I G)"
using that assms
by (auto simp: carrier_sum_group PiE_iff group.inv_eq_1_iff group.l_inv cong: conj_cong)
qed
qed (auto simp: assms carrier_sum_group PiE_iff group.is_monoid monoid.m_assoc)
lemma inv_sum_group [simp]:
assumes "⋀i. i ∈ I ⟹ group (G i)" and x: "x ∈ carrier (sum_group I G)"
shows "m_inv (sum_group I G) x = (λi∈I. m_inv (G i) (x i))"
proof (rule group.inv_equality)
show "(λi∈I. inv⇘G i⇙ x i) ⊗⇘sum_group I G⇙ x = 𝟭⇘sum_group I G⇙"
using x by (auto simp: carrier_sum_group PiE_iff group.l_inv assms intro: restrict_ext)
show "(λi∈I. inv⇘G i⇙ 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
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
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⇩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⇩E I H
⊆ carrier (subgroup_generated (product_group I G)
{x ∈ Π⇩E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 𝟭⇘G i⇙}})"
by (simp add: assms subgroup_sum_group subgroup.carrier_subgroup_generated_subgroup carrier_sum_group)
ultimately
have "subgroup (carrier (sum_group I G) ∩ Pi⇩E I H) (sum_group I G)"
by (simp add: assms sum_group_def group.subgroup_subgroup_generated_iff)
then have *: "{f ∈ Π⇩E i∈I. carrier (subgroup_generated (G i) (H i)). finite {i ∈ I. f i ≠ 𝟭⇘G i⇙}}
= carrier (subgroup_generated (sum_group I G) (carrier (sum_group I G) ∩ Pi⇩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⇩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 ⊗⇘?IG⇙ y) = h x ⊗⇘?IH⇙ 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 = 𝟭⇘G i⇙"
if γ: "γ ∈ (Π⇩E i∈I. carrier (G i))" and eq: "(λi∈I. f i (γ i)) = (λi∈I. 𝟭⇘H i⇙)" and "i ∈ I"
for γ i
proof -
have "inj_on (f i) (carrier (G i))" "f i ∈ hom (G i) (H i)"
using ‹i ∈ I› f by (auto simp: iso_def bij_betw_def)
then have *: "⋀x. ⟦f i x = 𝟭⇘H i⇙; x ∈ carrier (G i)⟧ ⟹ x = 𝟭⇘G i⇙"
by (metis G Group.group_def H hom_one inj_onD monoid.one_closed ‹i ∈ I›)
show ?thesis
using eq ‹i ∈ I› * γ by (simp add: fun_eq_iff) (meson PiE_iff)
qed
then show "inj_on h (carrier ?IG)"
apply (simp add: iso_def bij_betw_def GH.inj_on_one_iff flip: carrier_product_group)
apply (force simp: h_def)
done
next
show "h ` carrier ?IG ⊆ carrier ?IH"
unfolding h_def using f
by (force simp: PiE_def Pi_def Group.iso_def dest!: bij_betwE)
next
show "carrier ?IH ⊆ h ` carrier ?IG"
unfolding h_def
proof (clarsimp simp: iso_def bij_betw_def)
fix x
assume "x ∈ (Π⇩E i∈I. carrier (H i))"
with f have x: "x ∈ (Π⇩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)) ` (Π⇩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 ∈ (Π⇩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 ‹i ∈ I› f by (auto simp: iso_def bij_betw_def)
then have one: "⋀x. ⟦f i x = 𝟭⇘H i⇙; x ∈ carrier (G i)⟧ ⟹ x = 𝟭⇘G i⇙" if "i ∈ I" for i
by (metis G H group.subgroup_self hom_one inj_on_eq_iff subgroup.one_closed that)
have fin1: "finite {i ∈ I. x i ≠ 𝟭⇘G i⇙} ⟹ finite {i ∈ I. f i (x i) ≠ 𝟭⇘H i⇙}" for x
using homf by (auto simp: G H hom_one elim!: rev_finite_subset)
define h where "h ≡ λx. (λ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 ⊗⇘?IG⇙ y) = h x ⊗⇘?IH⇙ 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 γ: "γ i = 𝟭⇘G i⇙"
if "γ ∈ (Π⇩E i∈I. carrier (G i))" and eq: "(λi∈I. f i (γ i)) = (λi∈I. 𝟭⇘H i⇙)" and "i ∈ I"
for γ i
using ‹i ∈ I› one that by (simp add: fun_eq_iff) (meson PiE_iff)
show "inj_on h (carrier ?IG)"
apply (simp add: iso_def bij_betw_def GH.inj_on_one_iff assms one flip: carrier_sum_group)
apply (auto simp: h_def fun_eq_iff carrier_sum_group assms PiE_def Pi_def extensional_def one)
done
next
show "h ` carrier ?IG ⊆ carrier ?IH"
using homf GH.hom_closed
by (fastforce simp: h_def PiE_def Pi_def dest!: bij_betwE)
next
show "carrier ?IH ⊆ h ` carrier ?IG"
unfolding h_def
proof (clarsimp simp: iso_def bij_betw_def carrier_sum_group assms)
fix x
assume x: "x ∈ (Π⇩E i∈I. carrier (H i))" and fin: "finite {i ∈ I. x i ≠ 𝟭⇘H i⇙}"
with f have xf: "x ∈ (Π⇩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 ∈ Π⇩E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 𝟭⇘G i⇙}}"
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) ≠ 𝟭⇘G i⇙}"
apply (rule finite_subset [OF _ fin])
using G H group.subgroup_self hom_one homf injf inv_into_f_eq subgroup.one_closed by fastforce
with x show "?g ∈ {x ∈ Π⇩E i∈I. carrier (G i). finite {i ∈ I. x i ≠ 𝟭⇘G i⇙}}"
apply (auto simp: PiE_iff inv_into_into conj_commute cong: conj_cong)
by (metis (no_types, opaque_lifting) iso_iff f inv_into_into)
qed
qed
qed
qed
then show ?thesis
using is_iso_def by auto
qed
end