Theory Finitely_Generated_Abelian_Groups.DirProds
section ‹Direct group product›
theory DirProds
imports Finite_Product_Extend Group_Hom Finite_And_Cyclic_Groups
begin
notation integer_mod_group (‹Z›)
text ‹The direct group product is defined component-wise and provided in an indexed way.›
definition DirProds :: "('a ⇒ ('b, 'c) monoid_scheme) ⇒ 'a set ⇒ ('a ⇒ 'b) monoid" where
"DirProds G I = ⦇ carrier = Pi⇩E I (carrier ∘ G),
monoid.mult = (λx y. restrict (λi. x i ⊗⇘G i⇙ y i) I),
one = restrict (λi. 𝟭⇘G i⇙) I ⦈"
text ‹Basic lemmas about ‹DirProds›.›
lemma DirProds_empty:
"carrier (DirProds f {}) = {𝟭⇘DirProds f {}⇙}"
unfolding DirProds_def by auto
lemma DirProds_order:
assumes "finite I"
shows "order (DirProds G I) = prod (order ∘ G) I"
unfolding order_def DirProds_def using assms by (simp add: card_PiE)
lemma DirProds_in_carrI:
assumes "⋀i. i ∈ I ⟹ x i ∈ carrier (G i)" "⋀i. i ∉ I ⟹ x i = undefined"
shows "x ∈ carrier (DirProds G I)"
unfolding DirProds_def using assms by auto
lemma comp_in_carr:
assumes "x ∈ carrier (DirProds G I)" "i ∈ I"
shows "x i ∈ carrier (G i)"
using assms unfolding DirProds_def by auto
lemma comp_mult:
assumes "i ∈ I"
shows "(x ⊗⇘DirProds G I⇙ y) i = (x i ⊗⇘G i⇙ y i)"
using assms unfolding DirProds_def by simp
lemma comp_exp_nat:
fixes k::nat
assumes "i ∈ I"
shows "(x [^]⇘DirProds G I⇙ k) i = x i [^]⇘G i⇙ k"
proof (induction k)
case 0
then show ?case using assms unfolding DirProds_def by simp
next
case i: (Suc k)
have "(x [^]⇘DirProds G I⇙ k ⊗⇘DirProds G I⇙ x) i = (x [^]⇘DirProds G I⇙ k) i ⊗⇘G i⇙ x i"
by(rule comp_mult[OF assms])
also from i have "… = x i [^]⇘G i⇙ k ⊗⇘G i⇙ x i" by simp
also have "… = x i [^]⇘G i⇙ Suc k" by simp
finally show ?case by simp
qed
lemma DirProds_m_closed:
assumes "x ∈ carrier (DirProds G I)" "y ∈ carrier (DirProds G I)" "⋀i. i ∈ I ⟹ group (G i)"
shows "x ⊗⇘DirProds G I⇙ y ∈ carrier (DirProds G I)"
using assms monoid.m_closed[OF group.is_monoid[OF assms(3)]] unfolding DirProds_def by fastforce
lemma partial_restr:
assumes "a ∈ carrier (DirProds G I)" "J ⊆ I"
shows "restrict a J ∈ carrier (DirProds G J)"
using assms unfolding DirProds_def by auto
lemma eq_parts_imp_eq:
assumes "a ∈ carrier (DirProds G I)" "b ∈ carrier (DirProds G I)" "⋀i. i ∈ I ⟹ a i = b i"
shows "a = b"
using assms unfolding DirProds_def by fastforce
lemma mult_restr:
assumes "a ∈ carrier (DirProds G I)" "b ∈ carrier (DirProds G I)" "J ⊆ I"
shows "a ⊗⇘DirProds G J⇙ b = restrict (a ⊗⇘DirProds G I⇙ b) J"
using assms unfolding DirProds_def by force
lemma DirProds_one:
assumes "x ∈ carrier (DirProds G I)"
shows "(∀i ∈ I. x i = 𝟭⇘G i⇙) ⟷ x = 𝟭⇘DirProds G I⇙"
using assms unfolding DirProds_def by fastforce
lemma DirProds_one':
"i∈I ⟹ 𝟭⇘DirProds G I⇙ i = 𝟭⇘G i⇙"
unfolding DirProds_def by simp
lemma DirProds_one'':
"𝟭⇘DirProds G I⇙ = restrict (λi. 𝟭⇘G i⇙) I"
by (unfold DirProds_def, simp)
lemma DirProds_mult:
"(⊗⇘DirProds G I⇙) = (λx y. restrict (λi. x i ⊗⇘G i⇙ y i) I)"
unfolding DirProds_def by simp
lemma DirProds_one_iso: "(λx. x G) ∈ iso (DirProds f {G}) (f G)"
proof (intro isoI homI)
show "bij_betw (λx. x G) (carrier (DirProds f {G})) (carrier (f G))"
proof (unfold bij_betw_def, rule)
show "inj_on (λx. x G) (carrier (DirProds f {G}))"
by (intro inj_onI, unfold DirProds_def PiE_def Pi_def extensional_def, fastforce)
show "(λx. x G) ` carrier (DirProds f {G}) = carrier (f G)"
proof(intro equalityI subsetI)
show "x ∈ carrier (f G)" if "x ∈ (λx. x G) ` carrier (DirProds f {G})" for x
using that unfolding DirProds_def by auto
show "x ∈ (λx. x G) ` carrier (DirProds f {G})" if xc: "x ∈ carrier (f G)" for x
proof
show "(λk∈{G}. x) ∈ carrier (DirProds f {G})" unfolding DirProds_def using xc by auto
moreover show "x = (λk∈{G}. x) G" by simp
qed
qed
qed
qed (unfold DirProds_def PiE_def Pi_def extensional_def, auto)
lemma DirProds_one_cong: "(DirProds f {G}) ≅ (f G)"
using DirProds_one_iso is_isoI by fast
lemma DirProds_one_iso_sym: "(λx. (λ_∈{G}. x)) ∈ iso (f G) (DirProds f {G})"
proof (intro isoI homI)
show "bij_betw (λx. λ_∈{G}. x) (carrier (f G)) (carrier (DirProds f {G}))"
proof (unfold bij_betw_def, rule)
show "inj_on (λx. (λ_∈{G}. x)) (carrier (f G))"
by (intro inj_onI, metis imageI image_constant image_restrict_eq member_remove remove_def)
show "(λx. (λ_∈{G}. x)) ` carrier (f G) = carrier (DirProds f {G})"
unfolding DirProds_def by fastforce
qed
qed (unfold DirProds_def, auto)
lemma DirProds_one_cong_sym: "(f G) ≅ (DirProds f {G})"
using DirProds_one_iso_sym is_isoI by fast
text ‹The direct product is a group iff all factors are groups.›
lemma DirProds_is_group:
assumes "⋀i. i ∈ I ⟹ group (G i)"
shows "group (DirProds G I)"
proof(rule groupI)
show one_closed: "𝟭⇘DirProds G I⇙ ∈ carrier (DirProds G I)" unfolding DirProds_def
by (simp add: assms group.is_monoid)
fix x
assume x: "x ∈ carrier (DirProds G I)"
have one_: "⋀i. i ∈ I ⟹ 𝟭⇘G i⇙ = 𝟭⇘DirProds G I⇙ i" unfolding DirProds_def by simp
have "⋀i. i ∈ I ⟹ 𝟭⇘DirProds G I⇙ i ⊗⇘G i⇙ x i = x i"
proof -
fix i
assume i: "i ∈ I"
interpret group "G i" using assms[OF i] .
have "x i ∈ carrier (G i)" using x i comp_in_carr by fast
thus "𝟭⇘DirProds G I⇙ i ⊗⇘G i⇙ x i = x i" by(subst one_[OF i, symmetric]; simp)
qed
with one_ x show "𝟭⇘DirProds G I⇙ ⊗⇘DirProds G I⇙ x = x" unfolding DirProds_def by force
have "restrict (λi. inv⇘G i⇙ (x i)) I ∈ carrier (DirProds G I)" using x group.inv_closed[OF assms]
unfolding DirProds_def by fastforce
moreover have "restrict (λi. inv⇘G i⇙ (x i)) I ⊗⇘DirProds G I⇙ x = 𝟭⇘DirProds G I⇙"
using x group.l_inv[OF assms] unfolding DirProds_def by fastforce
ultimately show "∃y∈carrier (DirProds G I). y ⊗⇘DirProds G I⇙ x = 𝟭⇘DirProds G I⇙" by blast
fix y
assume y: "y ∈ carrier (DirProds G I)"
from DirProds_m_closed[OF x y assms] show m_closed: "x ⊗⇘DirProds G I⇙ y ∈ carrier (DirProds G I)"
by blast
fix z
assume z: "z ∈ carrier (DirProds G I)"
have "⋀i. i ∈ I ⟹ (x ⊗⇘DirProds G I⇙ y ⊗⇘DirProds G I⇙ z) i
= (x ⊗⇘DirProds G I⇙ (y ⊗⇘DirProds G I⇙ z)) i"
proof -
fix i
assume i: "i ∈ I"
have "(x ⊗⇘DirProds G I⇙ y ⊗⇘DirProds G I⇙ z) i = (x ⊗⇘DirProds G I⇙ y) i ⊗⇘G i⇙ z i"
using assms by (simp add: comp_mult i m_closed z)
also have "… = x i ⊗⇘G i⇙ y i ⊗⇘G i⇙ z i" by (simp add: assms comp_mult i x y)
also have "… = x i ⊗⇘G i⇙ (y i ⊗⇘G i⇙ z i)" using i assms x y z
by (meson Group.group_def comp_in_carr monoid.m_assoc)
also have "… = (x ⊗⇘DirProds G I⇙ (y ⊗⇘DirProds G I⇙ z)) i" by (simp add: DirProds_def i)
finally show "(x ⊗⇘DirProds G I⇙ y ⊗⇘DirProds G I⇙ z) i
= (x ⊗⇘DirProds G I⇙ (y ⊗⇘DirProds G I⇙ z)) i" .
qed
thus "x ⊗⇘DirProds G I⇙ y ⊗⇘DirProds G I⇙ z = x ⊗⇘DirProds G I⇙ (y ⊗⇘DirProds G I⇙ z)"
unfolding DirProds_def by auto
qed
lemma DirProds_obtain_elem_carr:
assumes "group (DirProds G I)" "i ∈ I" "x ∈ carrier (G i)"
obtains k where "k ∈ carrier (DirProds G I)" "k i = x"
proof -
interpret DP: group "DirProds G I" by fact
from comp_in_carr[OF DP.one_closed] DirProds_one' have ao: "∀j∈I. 𝟭⇘G j⇙ ∈ carrier (G j)" by metis
let ?r = "restrict ((λj. 𝟭⇘G j⇙)(i := x)) I"
have "?r ∈ carrier (DirProds G I)"
unfolding DirProds_def PiE_def Pi_def using assms(2, 3) ao by auto
moreover have "?r i = x" using assms(2) by simp
ultimately show "(⋀k. ⟦k ∈ carrier (DirProds G I); k i = x⟧ ⟹ thesis) ⟹ thesis" by blast
qed
lemma DirProds_group_imp_groups:
assumes "group (DirProds G I)" and i: "i ∈ I"
shows "group (G i)"
proof (intro groupI)
let ?DP = "DirProds G I"
interpret DP: group ?DP by fact
show "𝟭⇘G i⇙ ∈ carrier (G i)" using DirProds_one' comp_in_carr[OF DP.one_closed i] i by metis
show "x ⊗⇘G i⇙ y ∈ carrier (G i)" if "x ∈ carrier (G i)" "y ∈ carrier (G i)" for x y
proof -
from DirProds_obtain_elem_carr[OF assms that(1)] obtain k where k: "k ∈ carrier ?DP" "k i = x" .
from DirProds_obtain_elem_carr[OF assms that(2)] obtain l where l: "l ∈ carrier ?DP" "l i = y" .
have "k ⊗⇘?DP⇙ l ∈ carrier ?DP" using k l by fast
from comp_in_carr[OF this i] comp_mult[OF i] show ?thesis using k l by metis
qed
show "x ⊗⇘G i⇙ y ⊗⇘G i⇙ z = x ⊗⇘G i⇙ (y ⊗⇘G i⇙ z)"
if x: "x ∈ carrier (G i)" and y: "y ∈ carrier (G i)" and z: "z ∈ carrier (G i)" for x y z
proof -
from DirProds_obtain_elem_carr[OF assms x] obtain k where k: "k ∈ carrier ?DP" "k i = x" .
from DirProds_obtain_elem_carr[OF assms y] obtain l where l: "l ∈ carrier ?DP" "l i = y" .
from DirProds_obtain_elem_carr[OF assms z] obtain m where m: "m ∈ carrier ?DP" "m i = z" .
have "x ⊗⇘G i⇙ y ⊗⇘G i⇙ z = (k i) ⊗⇘G i⇙ (l i) ⊗⇘G i⇙ (m i)" using k l m by argo
also have "… = (k ⊗⇘?DP⇙ l ⊗⇘?DP⇙ m) i" using comp_mult[OF i] k l m by metis
also have "… = (k ⊗⇘?DP⇙ (l ⊗⇘?DP⇙ m)) i"
proof -
have "k ⊗⇘?DP⇙ l ⊗⇘?DP⇙ m = k ⊗⇘?DP⇙ (l ⊗⇘?DP⇙ m)" using DP.m_assoc[OF k(1) l(1) m(1)] .
thus ?thesis by simp
qed
also have "… = (k i) ⊗⇘G i⇙ ((l i) ⊗⇘G i⇙ (m i))" using comp_mult[OF i] k l m by metis
finally show ?thesis using k l m by blast
qed
show "𝟭⇘G i⇙ ⊗⇘G i⇙ x = x" if "x ∈ carrier (G i)" for x
proof -
from DirProds_obtain_elem_carr[OF assms that(1)] obtain k where k: "k ∈ carrier ?DP" "k i = x" .
hence "𝟭⇘?DP⇙ ⊗⇘?DP⇙ k = k" by simp
with comp_mult k DirProds_one[OF DP.one_closed] that i show ?thesis by metis
qed
show "∃y∈carrier (G i). y ⊗⇘G i⇙ x = 𝟭⇘G i⇙" if "x ∈ carrier (G i)" for x
proof -
from DirProds_obtain_elem_carr[OF assms that(1)] obtain k where k: "k ∈ carrier ?DP" "k i = x" .
hence ic: "inv⇘?DP⇙ k ∈ carrier ?DP" by simp
have "inv⇘?DP⇙ k ⊗⇘?DP⇙ k = 𝟭⇘?DP⇙" using k by simp
hence "(inv⇘?DP⇙ k) i ⊗⇘G i⇙ k i= 𝟭⇘G i⇙" using comp_mult[OF i] DirProds_one'[OF i] by metis
with k(2) comp_in_carr[OF ic i] show ?thesis by blast
qed
qed
lemma DirProds_group_iff: "group (DirProds G I) ⟷ (∀i∈I. group (G i))"
using DirProds_is_group DirProds_group_imp_groups by metis
lemma comp_inv:
assumes "group (DirProds G I)" and x: "x ∈ carrier (DirProds G I)" and i: "i ∈ I"
shows "(inv⇘(DirProds G I)⇙ x) i = inv⇘(G i)⇙ (x i)"
proof -
interpret DP: group "DirProds G I" by fact
interpret Gi: group "G i" using DirProds_group_imp_groups[OF DP.is_group i] .
have ixc: "inv⇘(DirProds G I)⇙ x ∈ carrier (DirProds G I)" using x by blast
hence "inv⇘(DirProds G I)⇙ x ⊗⇘DirProds G I⇙ x = 𝟭⇘DirProds G I⇙" using x by simp
hence "(inv⇘(DirProds G I)⇙ x ⊗⇘DirProds G I⇙ x) i = 𝟭⇘G i⇙" by (simp add: DirProds_one' i)
moreover from comp_mult[OF i]
have "(inv⇘(DirProds G I)⇙ x ⊗⇘DirProds G I⇙ x) i = ((inv⇘(DirProds G I)⇙ x) i) ⊗⇘G i⇙ (x i)"
by blast
ultimately show ?thesis using x ixc by (simp add: comp_in_carr[OF _ i] group.inv_equality)
qed
text ‹The same is true for abelian groups.›
lemma DirProds_is_comm_group:
assumes "⋀i. i ∈ I ⟹ comm_group (G i)"
shows "comm_group (DirProds G I)" (is "comm_group ?DP")
proof
interpret group ?DP using assms DirProds_is_group unfolding comm_group_def by metis
show "carrier ?DP ⊆ Units ?DP" "𝟭⇘?DP⇙ ∈ carrier ?DP" by simp_all
fix x
assume x[simp]: "x ∈ carrier ?DP"
show "𝟭⇘?DP⇙ ⊗⇘?DP⇙ x = x" "x ⊗⇘?DP⇙ 𝟭⇘?DP⇙ = x" by simp_all
fix y
assume y[simp]: "y ∈ carrier ?DP"
show "x ⊗⇘?DP⇙ y ∈ carrier ?DP" by simp
show "x ⊗⇘DirProds G I⇙ y = y ⊗⇘DirProds G I⇙ x"
proof (rule eq_parts_imp_eq[of _ G I])
show "x ⊗⇘?DP⇙ y ∈ carrier ?DP" by simp
show "y ⊗⇘?DP⇙ x ∈ carrier ?DP" by simp
show "⋀i. i∈I ⟹ (x ⊗⇘DirProds G I⇙ y) i = (y ⊗⇘DirProds G I⇙ x) i"
proof -
fix i
assume i: "i ∈ I"
interpret gi: comm_group "(G i)" using assms(1)[OF i] .
have "(x ⊗⇘?DP⇙ y) i = x i ⊗⇘G i⇙ y i"
by (intro comp_mult[OF i])
also have "… = y i ⊗⇘G i⇙ x i" using comp_in_carr[OF _ i] x y gi.m_comm by metis
also have "… = (y ⊗⇘?DP⇙ x) i" by (intro comp_mult[symmetric, OF i])
finally show "(x ⊗⇘DirProds G I⇙ y) i = (y ⊗⇘DirProds G I⇙ x) i" .
qed
qed
fix z
assume z[simp]: "z ∈ carrier ?DP"
show "x ⊗⇘?DP⇙ y ⊗⇘?DP⇙ z = x ⊗⇘?DP⇙ (y ⊗⇘?DP⇙ z)" using m_assoc by simp
qed
lemma DirProds_comm_group_imp_comm_groups:
assumes "comm_group (DirProds G I)" and i: "i ∈ I"
shows "comm_group (G i)"
proof -
interpret DP: comm_group "DirProds G I" by fact
interpret Gi: group "G i" using DirProds_group_imp_groups[OF DP.is_group i] .
show "comm_group (G i)"
proof
show "x ⊗⇘G i⇙ y = y ⊗⇘G i⇙ x" if x: "x ∈ carrier (G i)" and y: "y ∈ carrier (G i)" for x y
proof -
obtain a where a[simp]: "a ∈ carrier (DirProds G I)" "a i = x"
using DirProds_obtain_elem_carr[OF DP.is_group i x] .
obtain b where b[simp]: "b ∈ carrier (DirProds G I)" "b i = y"
using DirProds_obtain_elem_carr[OF DP.is_group i y] .
have "a ⊗⇘DirProds G I⇙ b = b ⊗⇘DirProds G I⇙ a" using DP.m_comm by simp
hence "(a ⊗⇘DirProds G I⇙ b) i = (b ⊗⇘DirProds G I⇙ a) i" by argo
with comp_mult[OF i] have "a i ⊗⇘G i⇙ b i = b i ⊗⇘G i⇙ a i" by metis
with a b show "x ⊗⇘G i⇙ y = y ⊗⇘G i⇙ x" by blast
qed
qed
qed
lemma DirProds_comm_group_iff: "comm_group (DirProds G I) ⟷ (∀i∈I. comm_group (G i))"
using DirProds_is_comm_group DirProds_comm_group_imp_comm_groups by metis
text ‹And also for finite groups.›
lemma DirProds_is_finite_group:
assumes "⋀i. i∈I ⟹ finite_group (G i)" "finite I"
shows "finite_group (DirProds G I)"
proof -
have "group (G i)" if "i∈I" for i using assms(1)[OF that] unfolding finite_group_def by blast
from DirProds_is_group[OF this] interpret DP: group "DirProds G I" by fast
show ?thesis
proof(unfold_locales)
have "order (DirProds G I) ≠ 0"
proof(unfold DirProds_order[OF assms(2)])
have "(order ∘ G) i ≠ 0" if "i∈I" for i
using assms(1)[OF that] by (simp add: finite_group.order_gt_0)
thus "prod (order ∘ G) I ≠ 0" by (simp add: assms(2))
qed
thus "finite (carrier (DirProds G I))" unfolding order_def by (meson card.infinite)
qed
qed
lemma DirProds_finite_imp_finite_groups:
assumes "finite_group (DirProds G I)" "finite I"
shows "⋀i. i∈I ⟹ finite_group (G i)"
proof -
fix i assume i: "i ∈ I"
interpret DP: finite_group "DirProds G I" by fact
interpret group "G i" by (rule DirProds_group_imp_groups[OF DP.is_group i])
show "finite_group (G i)"
proof(unfold_locales)
have oDP: "order (DirProds G I) ≠ 0" by blast
with DirProds_order[OF assms(2), of G] have "order (G i) ≠ 0" using i assms(2) by force
thus "finite (carrier (G i))" unfolding order_def by (meson card_eq_0_iff)
qed
qed
lemma DirProds_finite_group_iff:
assumes "finite I"
shows "finite_group (DirProds G I) ⟷ (∀i∈I. finite_group (G i))"
using DirProds_is_finite_group DirProds_finite_imp_finite_groups assms by metis
lemma DirProds_finite_comm_group_iff:
assumes "finite I"
shows "finite_comm_group (DirProds G I) ⟷ (∀i∈I. finite_comm_group (G i))"
using DirProds_finite_group_iff[OF assms] DirProds_comm_group_iff unfolding finite_comm_group_def by fast
text ‹If a group is an internal direct product of a family of subgroups, it is isomorphic to the
direct product of these subgroups.›
lemma (in comm_group) subgroup_iso_DirProds_IDirProds:
assumes "subgroup J G" "is_idirprod J S I" "finite I"
shows "(λx. ⨂⇘G⇙i∈I. x i) ∈ iso (DirProds (λi. G⦇carrier := (S i)⦈) I) (G⦇carrier := J⦈)"
(is "?fp ∈ iso ?DP ?J")
proof -
from assms(2) have assm: "J = IDirProds G S I"
"compl_fam S I"
unfolding is_idirprod_def by auto
from assms(1, 2) have assm': "⋀i. i ∈ I ⟹ subgroup (S i) (G⦇carrier := J⦈)"
using normal_imp_subgroup subgroup_incl by (metis IDirProds_incl assms(2) is_idirprod_def)
interpret J: comm_group ?J using subgroup_is_comm_group[OF assms(1)] .
interpret DP: comm_group ?DP
by (intro DirProds_is_comm_group; use J.subgroup_is_comm_group[OF assm'] in simp)
have inJ: "S i ⊆ J" if "i ∈ I" for i using subgroup.subset[OF assm'[OF that]] by simp
have hom: "?fp ∈ hom ?DP ?J"
proof (rule homI)
fix x
assume x[simp]: "x ∈ carrier ?DP"
show "finprod G x I ∈ carrier ?J"
proof (subst finprod_subgroup[OF _ assms(1)])
show "x ∈ I → J" using inJ comp_in_carr[OF x] by auto
thus "finprod ?J x I ∈ carrier ?J" by (intro J.finprod_closed; simp)
qed
fix y
assume y[simp]: "y ∈ carrier ?DP"
show "finprod G (x ⊗⇘?DP⇙ y) I = finprod G x I ⊗⇘?J⇙ finprod G y I"
proof(subst (1 2 3) finprod_subgroup[of _ _ J])
show xyJ: "x ∈ I → J" "y ∈ I → J" using x y inJ comp_in_carr[OF x] comp_in_carr[OF y]
by auto
show xyJ1: "x ⊗⇘?DP⇙ y ∈ I → J" using inJ x y comp_in_carr[of "x ⊗⇘?DP⇙ y"] by fastforce
show "subgroup J G" using assms(1) .
show "finprod ?J (x ⊗⇘?DP⇙ y) I = finprod ?J x I ⊗⇘?J⇙ finprod ?J y I"
proof (rule J.finprod_cong_split)
show "x ∈ I → carrier ?J" "y ∈ I → carrier ?J" using xyJ by simp_all
show "x ⊗⇘?DP⇙ y ∈ I → carrier ?J" using xyJ1 by simp
fix i
assume i: "i ∈ I"
then have "x i ⊗⇘G⦇carrier := (S i) ⦈⇙ y i = (x ⊗⇘?DP⇙ y) i"
by (intro comp_mult[symmetric])
thus "x i ⊗⇘?J⇙ y i = (x ⊗⇘?DP⇙ y) i" by simp
qed
qed
qed
then interpret fp: group_hom ?DP ?J ?fp unfolding group_hom_def group_hom_axioms_def by blast
have s: "subgroup (S i) G" if "i ∈ I" for i using incl_subgroup[OF assms(1) assm'[OF that]] .
have "kernel ?DP ?J ?fp = {𝟭⇘?DP⇙}"
proof -
have "a = 𝟭⇘?DP⇙" if "a ∈ kernel ?DP ?J ?fp" for a
proof -
from that have a: "finprod G a I = 𝟭" "a ∈ carrier ?DP" unfolding kernel_def by simp_all
from compl_fam_imp_triv_finprod[OF assm(2) assms(3) s a(1)] comp_in_carr[OF a(2)]
have "∀i∈I. a i = 𝟭" by simp
then show ?thesis using DirProds_one[OF a(2)] by fastforce
qed
thus ?thesis using fp.one_in_kernel by blast
qed
moreover have "J ⊆ ?fp ` carrier ?DP"
using assm(1) IDirProds_eq_finprod_PiE[OF assms(3) incl_subgroup[OF assms(1) assm']]
unfolding DirProds_def PiE_def Pi_def by simp
ultimately show ?thesis using hom fp.iso_iff unfolding kernel_def by auto
qed
lemma (in comm_group) iso_DirProds_IDirProds:
assumes "is_idirprod (carrier G) S I" "finite I"
shows "(λx. ⨂⇘G⇙i∈I. x i) ∈ iso (DirProds (λi. G⦇carrier := (S i)⦈) I) G"
using subgroup_iso_DirProds_IDirProds[OF subgroup_self assms(1, 2)] by auto
lemma (in comm_group) cong_DirProds_IDirProds:
assumes "is_idirprod (carrier G) S I" "finite I"
shows "DirProds (λi. G⦇carrier := (S i)⦈) I ≅ G"
by (intro is_isoI, use iso_DirProds_IDirProds[OF assms] in blast)
text ‹In order to prove the isomorphism between two direct products, the following lemmas provide
some criterias.›
lemma DirProds_iso:
assumes "bij_betw f I J" "⋀i. i∈I ⟹ Gs i ≅ Hs (f i)"
"⋀i. i∈I ⟹ group (Gs i)" "⋀j. j∈J ⟹ group (Hs j)"
shows "DirProds Gs I ≅ DirProds Hs J"
proof -
interpret DG: group "DirProds Gs I" using DirProds_is_group assms(3) by blast
interpret DH: group "DirProds Hs J" using DirProds_is_group assms(4) by blast
from assms(1) obtain g where g: "g = inv_into I f" "bij_betw g J I" by (meson bij_betw_inv_into)
hence fgi: "⋀i. i ∈ I ⟹ g (f i) = i" "⋀j. j ∈ J ⟹ f (g j) = j"
using assms(1) bij_betw_inv_into_left[OF assms(1)] bij_betw_inv_into_right[OF assms(1)] by auto
from assms(2) have "⋀i. i ∈ I ⟹ (∃h. h ∈ iso (Gs i) (Hs (f i)))" unfolding is_iso_def by blast
then obtain h where h: "⋀i. i ∈ I ⟹ h i ∈ iso (Gs i) (Hs (f i))" by metis
let ?h = "(λx. (λj. if j∈J then (h (g j)) (x (g j)) else undefined))"
have hc: "?h x ∈ carrier (DirProds Hs J)" if "x ∈ carrier (DirProds Gs I)" for x
proof -
have xc: "x ∈ carrier (DirProds Gs I)" by fact
have "h (g j) (x (g j)) ∈ carrier (Hs j)" if "j ∈ J" for j
proof(intro iso_in_carr[OF _ comp_in_carr[OF xc], of "h (g j)" "g j" "Hs j"])
show "g j ∈ I" using g(2)[unfolded bij_betw_def] that by blast
from h[OF this] show "h (g j) ∈ Group.iso (Gs (g j)) (Hs j)" using fgi(2)[OF that] by simp
qed
thus ?thesis using xc unfolding DirProds_def PiE_def extensional_def by auto
qed
moreover have "?h (x ⊗⇘DirProds Gs I⇙ y)= ?h x ⊗⇘DirProds Hs J⇙ ?h y"
if "x ∈ carrier (DirProds Gs I)" "y ∈ carrier (DirProds Gs I)" for x y
proof(intro eq_parts_imp_eq[OF hc[OF DG.m_closed[OF that]] DH.m_closed[OF hc[OF that(1)] hc[OF that(2)]]])
fix j
assume j: "j ∈ J"
hence gj: "g j ∈ I" using g unfolding bij_betw_def by blast
from assms(3)[OF gj] assms(4)[OF j] have g: "group (Gs (g j))" "Group.group (Hs j)" .
from iso_imp_homomorphism[OF h[OF gj]] fgi(2)[OF j] g
interpret hjh: group_hom "Gs (g j)" "Hs j" "h (g j)"
unfolding group_hom_def group_hom_axioms_def by simp
show "(?h (x ⊗⇘DirProds Gs I⇙ y)) j = (?h x ⊗⇘DirProds Hs J⇙ ?h y) j"
proof(subst comp_mult)
show "(if j ∈ J then h (g j) (x (g j) ⊗⇘Gs (g j)⇙ y (g j)) else undefined)
= (?h x ⊗⇘DirProds Hs J⇙ ?h y) j"
proof(subst comp_mult)
have "h (g j) (x (g j) ⊗⇘Gs (g j)⇙ y (g j)) = h (g j) (x (g j)) ⊗⇘Hs j⇙ h (g j) (y (g j))"
using comp_in_carr[OF that(1) gj] comp_in_carr[OF that(2) gj] by simp
thus "(if j ∈ J then h (g j) (x (g j) ⊗⇘Gs (g j)⇙ y (g j)) else undefined) =
(if j ∈ J then h (g j) (x (g j)) else undefined)
⊗⇘Hs j⇙ (if j ∈ J then h (g j) (y (g j)) else undefined)"
using j by simp
qed (use j g that hc in auto)
qed (use gj g that in auto)
qed
ultimately interpret hgh: group_hom "DirProds Gs I" "DirProds Hs J" ?h
unfolding group_hom_def group_hom_axioms_def by (auto intro: homI)
have "carrier (DirProds Hs J) ⊆ ?h ` carrier (DirProds Gs I)"
proof
show "x ∈ ?h ` carrier (DirProds Gs I)" if xc: "x ∈ carrier (DirProds Hs J)" for x
proof -
from h obtain k where k: "⋀i. i∈I ⟹ k i = inv_into (carrier (Gs i)) (h i)" by fast
hence kiso: "⋀i. i∈I ⟹ k i ∈ iso (Hs (f i)) (Gs i)"
using h by (simp add: assms(3) group.iso_set_sym)
hence hk: "y = (h (g j) ∘ (k (g j))) y" if "j ∈ J" "y ∈ carrier (Hs j)" for j y
proof -
have gj: "g j ∈ I" using that g[unfolded bij_betw_def] by blast
thus ?thesis
using h[OF gj, unfolded iso_def] k[OF gj] that fgi(2)[OF that(1)] bij_betw_inv_into_right
unfolding comp_def by fastforce
qed
let ?k = "(λi. if i∈I then k i else (λ_. undefined))"
let ?y = "(λi. (?k i) (x (f i)))"
have "x j = (λj. if j ∈ J then h (g j) (?y (g j)) else undefined) j" for j
proof (cases "j ∈ J")
case True
thus ?thesis using hk[OF True comp_in_carr[OF that True]]
fgi(2)[OF True] g[unfolded bij_betw_def] by auto
next
case False
thus ?thesis using that[unfolded DirProds_def] by auto
qed
moreover have "?y ∈ carrier (DirProds Gs I)"
proof -
have "?y i ∈ carrier (Gs i)" if i: "i ∈ I" for i
using k[OF i] h[OF i] comp_in_carr[OF xc] assms(1) bij_betwE iso_in_carr kiso that
by fastforce
moreover have "?y i = undefined" if i: "i ∉ I" for i using i by simp
ultimately show ?thesis unfolding DirProds_def PiE_def Pi_def extensional_def by simp
qed
ultimately show ?thesis by fast
qed
qed
moreover have "x = 𝟭⇘DirProds Gs I⇙"
if "x ∈ carrier (DirProds Gs I)" "?h x = 𝟭⇘DirProds Hs J⇙" for x
proof -
have "∀i∈I. x i = 𝟭⇘Gs i⇙"
proof
fix i
assume i: "i ∈ I"
interpret gi: group "Gs i" using assms(3)[OF i] .
interpret hfi: group "Hs (f i)" using assms(4) i assms(1)[unfolded bij_betw_def] by blast
from h[OF i] interpret hi: group_hom "(Gs i)" "Hs (f i)" "h i"
unfolding group_hom_def group_hom_axioms_def iso_def by blast
from that have hx: "?h x ∈ carrier (DirProds Hs J)" by simp
from DirProds_one[OF this] that(2)
have "(if j ∈ J then h (g j) (x (g j)) else undefined) = 𝟭⇘Hs j⇙" if "j ∈ J" for j
using that by blast
hence "h (g (f i)) (x (g (f i))) = 𝟭⇘Hs (f i)⇙" using i assms(1)[unfolded bij_betw_def] by auto
hence "h i (x i) = 𝟭⇘Hs (f i)⇙" using fgi(1)[OF i] by simp
with hi.iso_iff h[OF i] comp_in_carr[OF that(1) i] show "x i = 𝟭⇘Gs i⇙" by fast
qed
with DirProds_one that show ?thesis using assms(3) by blast
qed
ultimately show ?thesis unfolding is_iso_def using hgh.iso_iff by blast
qed
lemma DirProds_iso1:
assumes "⋀i. i∈I ⟹ Gs i ≅ (f ∘ Gs) i" "⋀i. i∈I ⟹ group (Gs i)" "⋀i. i∈I ⟹ group ((f ∘ Gs) i)"
shows "DirProds Gs I ≅ DirProds (f ∘ Gs) I"
proof -
interpret DP: group "DirProds Gs I" using DirProds_is_group assms by metis
interpret fDP: group "DirProds (f ∘ Gs) I" using DirProds_is_group assms by metis
from assms have "∀i∈I. (∃g. g ∈ iso (Gs i) ((f ∘ Gs) i))" unfolding is_iso_def by blast
then obtain J where J: "∀i∈I. J i ∈ iso (Gs i) ((f ∘ Gs) i)" by metis
let ?J = "(λi. if i∈I then J i else (λ_. undefined))"
from J obtain K where K: "∀i∈I. K i = inv_into (carrier (Gs i)) (J i)" by fast
hence K_iso: "∀i∈I. K i ∈ iso ((f ∘ Gs) i) (Gs i)" using group.iso_set_sym assms J by metis
let ?K = "(λi. if i∈I then K i else (λ_. undefined))"
have JKi: "(?J i) ((?K i) (x i)) = x i" if "x ∈ carrier (DirProds (f ∘ Gs) I)" for i x
proof -
have "(J i) ((K i) (x i)) = x i" if "x ∈ carrier (DirProds (f ∘ Gs) I)" "i ∈ I" for i x
proof -
from J that have "(J i) ` (carrier (Gs i)) = carrier ((f ∘ Gs) i)"
unfolding iso_def bij_betw_def by blast
hence "∃y. y ∈ carrier (Gs i) ∧ (J i) y = x i" using that by (metis comp_in_carr imageE)
with someI_ex[OF this] that show "(J i) ((K i) (x i)) = x i"
using K J K_iso unfolding inv_into_def by auto
qed
moreover have "(?J i) ((K i) (x i)) = x i" if "x ∈ carrier (DirProds (f ∘ Gs) I)" "i ∉ I" for i x
using that unfolding DirProds_def PiE_def extensional_def by force
ultimately show ?thesis using that by simp
qed
let ?r = "(λe. restrict (λi. ?J i (e i)) I)"
have hom: "?r ∈ hom (DirProds Gs I) (DirProds (f ∘ Gs) I)"
proof (intro homI)
show "?r x ∈ carrier (DirProds (f ∘ Gs) I)" if "x ∈ carrier (DirProds Gs I)" for x
using that J comp_in_carr[OF that] unfolding DirProds_def iso_def bij_betw_def by fastforce
show "?r (x ⊗⇘DirProds Gs I⇙ y) = ?r x ⊗⇘DirProds (f ∘ Gs) I⇙ ?r y"
if "x ∈ carrier (DirProds Gs I)" "y ∈ carrier (DirProds Gs I)" for x y
using that J comp_in_carr[OF that(1)] comp_in_carr[OF that(2)]
unfolding DirProds_def iso_def hom_def by force
qed
then interpret r: group_hom "(DirProds Gs I)" "(DirProds (f ∘ Gs) I)" ?r
unfolding group_hom_def group_hom_axioms_def by blast
have "carrier (DirProds (f ∘ Gs) I) ⊆ ?r ` carrier (DirProds Gs I)"
proof
show "x ∈ ?r ` carrier (DirProds Gs I)" if "x ∈ carrier (DirProds (f ∘ Gs) I)" for x
proof
show "x = (λi∈I. ?J i ((?K i) (x i)))"
using JKi[OF that] that unfolding DirProds_def PiE_def by (simp add: extensional_restrict)
show "(λi. ?K i (x i)) ∈ carrier (DirProds Gs I)" using K_iso iso_in_carr that
unfolding DirProds_def PiE_def Pi_def extensional_def by fastforce
qed
qed
moreover have "x = 𝟭⇘DirProds Gs I⇙"
if "x ∈ carrier (DirProds Gs I)" "?r x = 𝟭⇘DirProds (f ∘ Gs) I⇙" for x
proof -
have "∀i∈I. x i = 𝟭⇘Gs i⇙"
proof
fix i
assume i: "i ∈ I"
with J assms interpret Ji: group_hom "(Gs i)" "(f ∘ Gs) i" "J i"
unfolding group_hom_def group_hom_axioms_def iso_def by blast
from that have rx: "?r x ∈ carrier (DirProds (f ∘ Gs) I)" by simp
from i DirProds_one[OF this] that
have "(λi∈I. (if i ∈ I then J i else (λ_. undefined)) (x i)) i = 𝟭⇘(f ∘ Gs) i⇙" by blast
hence "(J i) (x i) = 𝟭⇘(f ∘ Gs) i⇙" using i by simp
with Ji.iso_iff mp[OF spec[OF J[unfolded Ball_def]] i] comp_in_carr[OF that(1) i]
show "x i = 𝟭⇘Gs i⇙" by fast
qed
with DirProds_one[OF that(1)] show ?thesis by blast
qed
ultimately show ?thesis unfolding is_iso_def using r.iso_iff by blast
qed
lemma DirProds_iso2:
assumes "inj_on f A" "group (DirProds g (f ` A))"
shows "DirProds (g ∘ f) A ≅ DirProds g (f ` A)"
proof (intro DirProds_iso[of f])
show "bij_betw f A (f ` A)" using assms(1) unfolding bij_betw_def by blast
show "⋀i. i ∈ A ⟹ (g ∘ f) i ≅ g (f i)" unfolding comp_def using iso_refl by simp
from assms(2) show "⋀i. i ∈ (f ` A) ⟹ group (g i)" using DirProds_group_imp_groups by fast
with assms(1) show "⋀i. i ∈ A ⟹ group ((g ∘ f) i)" by auto
qed
text ‹The direct group product distributes when nested.›
lemma DirProds_Sigma:
"DirProds (λi. DirProds (G i) (J i)) I ≅ DirProds (λ(i,j). G i j) (Sigma I J)" (is "?L ≅ ?R")
proof (intro is_isoI isoI)
let ?f = "λx. restrict (case_prod x) (Sigma I J)"
show hom: "?f ∈ hom ?L ?R"
proof(intro homI)
show "?f a ∈ carrier ?R" if "a ∈ carrier ?L" for a
using that unfolding DirProds_def PiE_def Pi_def extensional_def by auto
show "?f (a ⊗⇘?L⇙ b) = ?f a ⊗⇘?R⇙ ?f b" if "a ∈ carrier ?L" and "b ∈ carrier ?L" for a b
using that unfolding DirProds_def PiE_def Pi_def extensional_def by auto
qed
show "bij_betw ?f (carrier ?L) (carrier ?R)"
proof (intro bij_betwI)
let ?g = "λx. (λi. if i∈I then (λj. if j∈(J i) then x(i, j) else undefined) else undefined)"
show "?f ∈ carrier ?L → carrier ?R" unfolding DirProds_def by fastforce
show "?g ∈ carrier ?R → carrier ?L" unfolding DirProds_def by fastforce
show "?f (?g x) = x" if "x ∈ carrier ?R" for x
using that unfolding DirProds_def PiE_def Pi_def extensional_def by auto
show "?g (?f x) = x" if "x ∈ carrier ?L" for x
using that unfolding DirProds_def PiE_def Pi_def extensional_def by force
qed
qed
no_notation integer_mod_group (‹Z›)
end