Theory Finite_Product_Extend
section ‹Finite Product›
theory Finite_Product_Extend
imports IDirProds
begin
text ‹In this section, some general facts about ‹finprod› as well as some tailored for the rest of
this entry are proven.›
text ‹It is often needed to split a product in a single factor and the rest. Thus these two lemmas.›
lemma (in comm_group) finprod_minus:
assumes "a ∈ A" "f ∈ A → carrier G" "finite A"
shows "finprod G f A = f a ⊗ finprod G f (A - {a})"
proof -
from assms have "A = insert a (A - {a})" by blast
then have "finprod G f A = finprod G f (insert a (A - {a}))" by simp
also have "… = f a ⊗ finprod G f (A - {a})" using assms by (intro finprod_insert, auto)
finally show ?thesis .
qed
lemma (in comm_group) finprod_minus_symm:
assumes "a ∈ A" "f ∈ A → carrier G" "finite A"
shows "finprod G f A = finprod G f (A - {a}) ⊗ f a"
proof -
from assms have "A = insert a (A - {a})" by blast
then have "finprod G f A = finprod G f (insert a (A - {a}))" by simp
also have "… = f a ⊗ finprod G f (A - {a})" using assms by (intro finprod_insert, auto)
also have "… = finprod G f (A - {a}) ⊗ f a"
by (intro m_comm, use assms in blast, intro finprod_closed, use assms in blast)
finally show ?thesis .
qed
text ‹This makes it very easy to show the following trivial fact.›
lemma (in comm_group) finprod_singleton:
assumes "f x ∈ carrier G" "finprod G f {x} = a"
shows "f x = a"
proof -
have "finprod G f {x} = f x ⊗ finprod G f {}" using finprod_minus[of x "{x}" f] assms by auto
thus ?thesis using assms by simp
qed
text ‹The finite product is consistent and closed concerning subgroups.›
lemma (in comm_group) finprod_subgroup:
assumes "f ∈ S → H" "subgroup H G"
shows "finprod G f S = finprod (G⦇carrier := H⦈) f S"
proof (cases "finite S")
case True
interpret H: comm_group "G⦇carrier := H⦈" using subgroup_is_comm_group[OF assms(2)] .
show ?thesis using True assms
proof (induction S rule: finite_induct)
case empty
then show ?case using finprod_empty H.finprod_empty by simp
next
case i: (insert x F)
then have "finprod G f F = finprod (G⦇carrier := H⦈) f F" by blast
moreover have "finprod G f (insert x F) = f x ⊗ finprod G f F"
proof(intro finprod_insert[OF i(1, 2), of f])
show "f ∈ F → carrier G" "f x ∈ carrier G" using i(4) subgroup.subset[OF i(5)] by blast+
qed
ultimately have "finprod G f (insert x F) = f x ⊗⇘G⦇carrier := H⦈⇙ finprod (G⦇carrier := H⦈) f F"
by auto
moreover have "finprod (G⦇carrier := H⦈) f (insert x F) = …"
proof(intro H.finprod_insert[OF i(1, 2)])
show "f ∈ F → carrier (G⦇carrier := H⦈)" "f x ∈ carrier (G⦇carrier := H⦈)" using i(4) by auto
qed
ultimately show ?case by simp
qed
next
case False
then show ?thesis unfolding finprod_def by simp
qed
lemma (in comm_group) finprod_closed_subgroup:
assumes "subgroup H G" "f ∈ A → H"
shows "finprod G f A ∈ H"
using assms(2)
proof (induct A rule: infinite_finite_induct)
case (infinite A)
then show ?case using subgroup.one_closed[OF assms(1)] by auto
next
case empty
then show ?case using subgroup.one_closed[OF assms(1)] by auto
next
case i: (insert x F)
from finprod_insert[OF i(1, 2), of f] i have fi: "finprod G f (insert x F) = f x ⊗ finprod G f F"
using subgroup.subset[OF assms(1)] by blast
from i have "finprod G f F ∈ H" "f x ∈ H" by blast+
with fi show ?case using subgroup.m_closed[OF assms(1)] by presburger
qed
text ‹It also does not matter if we exponentiate all elements taking part in the product or the
result of the product.›
lemma (in comm_group) finprod_exp:
assumes "A ⊆ carrier G" "f ∈ A → carrier G"
shows "(finprod G f A) [^] (k::int) = finprod G ((λa. a [^] k) ∘ f) A"
using assms
proof(induction A rule: infinite_finite_induct)
case i: (insert x F)
hence ih: "finprod G f F [^] k = finprod G ((λa. a [^] k) ∘ f) F" by blast
have fpc: "finprod G f F ∈ carrier G" by (intro finprod_closed, use i in auto)
have fxc: "f x ∈ carrier G" using i by auto
have "finprod G f (insert x F) = f x ⊗ finprod G f F" by (intro finprod_insert, use i in auto)
hence "finprod G f (insert x F) [^] k = (f x ⊗ finprod G f F) [^] k" by simp
also have "… = f x [^] k ⊗ finprod G f F [^] k" using fpc fxc int_pow_distrib by blast
also have "… = ((λa. a [^] k) ∘ f) x ⊗ finprod G ((λa. a [^] k) ∘ f) F" using ih by simp
also have "… = finprod G ((λa. a [^] k) ∘ f) (insert x F)"
by (intro finprod_insert[symmetric], use i in auto)
finally show ?case .
qed auto
text ‹Some lemmas concerning different combinations of functions in the usage of ‹finprod›.›
lemma (in comm_group) finprod_cong_split:
assumes "⋀a. a ∈ A ⟹ f a ⊗ g a = h a"
and "f ∈ A → carrier G" "g ∈ A → carrier G" "h ∈ A → carrier G"
shows "finprod G h A = finprod G f A ⊗ finprod G g A" using assms
proof(induct A rule: infinite_finite_induct)
case (infinite A)
then show ?case by simp
next
case empty
then show ?case by simp
next
case i: (insert x F)
then have iH: "finprod G h F = finprod G f F ⊗ finprod G g F" by fast
have f: "finprod G f (insert x F) = f x ⊗ finprod G f F"
by (intro finprod_insert[OF i(1, 2), of f]; use i(5) in simp)
have g: "finprod G g (insert x F) = g x ⊗ finprod G g F"
by (intro finprod_insert[OF i(1, 2), of g]; use i(6) in simp)
have h: "finprod G h (insert x F) = h x ⊗ finprod G h F"
by (intro finprod_insert[OF i(1, 2), of h]; use i(7) in simp)
also have "… = h x ⊗ (finprod G f F ⊗ finprod G g F)" using iH by argo
also have "… = f x ⊗ g x ⊗ (finprod G f F ⊗ finprod G g F)" using i(4) by simp
also have "… = f x ⊗ finprod G f F ⊗ (g x ⊗ finprod G g F)" using m_comm m_assoc i(5-7) by simp
also have "… = finprod G f (insert x F) ⊗ finprod G g (insert x F)" using f g by argo
finally show ?case .
qed
lemma (in comm_group) finprod_comp:
assumes "inj_on g A" "(f ∘ g) ` A ⊆ carrier G"
shows "finprod G f (g ` A) = finprod G (f ∘ g) A"
using finprod_reindex[OF _ assms(1), of f] using assms(2) unfolding comp_def by blast
text ‹The subgroup generated by a set of generators (in an abelian group) is exactly the set of
elements that can be written as a finite product using only powers of these elements.›
lemma (in comm_group) generate_eq_finprod_PiE_image:
assumes "finite gs" "gs ⊆ carrier G"
shows "generate G gs = (λx. finprod G x gs) ` Pi⇩E gs (λa. generate G {a})" (is "?g = ?fp")
proof
show "?g ⊆ ?fp"
proof
fix x
assume x: "x ∈ ?g"
thus "x ∈ ?fp"
proof (induction rule: generate.induct)
case one
show ?case
proof
let ?r = "restrict (λ_. 𝟭) gs"
show "?r ∈ (Π⇩E a∈gs. generate G {a})" using generate.one by auto
show "𝟭 = finprod G ?r gs" by(intro finprod_one_eqI[symmetric], simp)
qed
next
case g: (incl g)
show ?case
proof
let ?r = "restrict ((λ_. 𝟭)(g := g)) gs"
show "?r ∈ (Π⇩E a∈gs. generate G {a})" using generate.one generate.incl[of g "{g}" G]
by fastforce
show "g = finprod G ?r gs"
proof -
have "finprod G ?r gs = ?r g ⊗ finprod G ?r (gs - {g})"
by (intro finprod_minus, use assms g in auto)
moreover have "?r g = g" using g by simp
moreover have "finprod G ?r (gs - {g}) = 𝟭" by(rule finprod_one_eqI; use g in simp)
ultimately show ?thesis using assms g by auto
qed
qed
next
case g: (inv g)
show ?case
proof
let ?r = "restrict ((λ_. 𝟭)(g := inv g)) gs"
show "?r ∈ (Π⇩E a∈gs. generate G {a})" using generate.one generate.inv[of g "{g}" G]
by fastforce
show "inv g = finprod G ?r gs"
proof -
have "finprod G ?r gs = ?r g ⊗ finprod G ?r (gs - {g})"
by (intro finprod_minus, use assms g in auto)
moreover have "?r g = inv g" using g by simp
moreover have "finprod G ?r (gs - {g}) = 𝟭" by(rule finprod_one_eqI; use g in simp)
ultimately show ?thesis using assms g by auto
qed
qed
next
case gh: (eng g h)
from gh obtain i where i: "i ∈ (Π⇩E a∈gs. generate G {a})" "g = finprod G i gs" by blast
from gh obtain j where j: "j ∈ (Π⇩E a∈gs. generate G {a})" "h = finprod G j gs" by blast
from i j have "g ⊗ h = finprod G i gs ⊗ finprod G j gs" by blast
also have "… = finprod G (λa. i a ⊗ j a) gs"
proof(intro finprod_multf[symmetric]; rule)
fix x
assume x: "x ∈ gs"
have "i x ∈ generate G {x}" "j x ∈ generate G {x}"using i(1) j(1) x by blast+
thus "i x ∈ carrier G" "j x ∈ carrier G" using generate_incl[of "{x}"] x assms(2) by blast+
qed
also have "… = finprod G (restrict (λa. i a ⊗ j a) gs) gs"
proof(intro finprod_cong)
have ip: "i g ∈ generate G {g}" if "g ∈ gs" for g using i that by auto
have jp: "j g ∈ generate G {g}" if "g ∈ gs" for g using j that by auto
have "i g ⊗ j g ∈ generate G {g}" if "g ∈ gs" for g
using generate.eng[OF ip[OF that] jp[OF that]] .
thus "((λa. i a ⊗ j a) ∈ gs → carrier G) = True" using generate_incl assms(2) by blast
qed auto
finally have "g ⊗ h = finprod G (restrict (λa. i a ⊗ j a) gs) gs" .
moreover have "(restrict (λa. i a ⊗ j a) gs) ∈ (Π⇩E a∈gs. generate G {a})"
proof -
have ip: "i g ∈ generate G {g}" if "g ∈ gs" for g using i that by auto
have jp: "j g ∈ generate G {g}" if "g ∈ gs" for g using j that by auto
have "i g ⊗ j g ∈ generate G {g}" if "g ∈ gs" for g
using generate.eng[OF ip[OF that] jp[OF that]] .
thus ?thesis by auto
qed
ultimately show ?case using i j by blast
qed
qed
show "?fp ⊆ ?g"
proof
fix x
assume x: "x ∈ ?fp"
then obtain f where f: "f ∈ (Pi⇩E gs (λa. generate G {a}))" "x = finprod G f gs" by blast
have sg: "subgroup ?g G" by(intro generate_is_subgroup, fact)
have "finprod G f gs ∈ ?g"
proof(intro finprod_closed_subgroup[OF sg])
have "f g ∈ generate G gs" if "g ∈ gs" for g
proof -
have "f g ∈ generate G {g}" using f(1) that by auto
moreover have "generate G {g} ⊆ generate G gs" by(intro mono_generate, use that in simp)
ultimately show ?thesis by fast
qed
thus "f ∈ gs → generate G gs" by simp
qed
thus "x ∈ ?g" using f by blast
qed
qed
lemma (in comm_group) generate_eq_finprod_Pi_image:
assumes "finite gs" "gs ⊆ carrier G"
shows "generate G gs = (λx. finprod G x gs) ` Pi gs (λa. generate G {a})" (is "?g = ?fp")
proof -
have "(λx. finprod G x gs) ` Pi⇩E gs (λa. generate G {a})
= (λx. finprod G x gs) ` Pi gs (λa. generate G {a})"
proof
have "Pi⇩E gs (λa. generate G {a}) ⊆ Pi gs (λa. generate G {a})" by blast
thus "(λx. finprod G x gs) ` Pi⇩E gs (λa. generate G {a})
⊆ (λx. finprod G x gs) ` Pi gs (λa. generate G {a})" by blast
show "(λx. finprod G x gs) ` Pi gs (λa. generate G {a})
⊆ (λx. finprod G x gs) ` Pi⇩E gs (λa. generate G {a})"
proof
fix x
assume x: "x ∈ (λx. finprod G x gs) ` Pi gs (λa. generate G {a})"
then obtain f where f: "x = finprod G f gs" "f ∈ Pi gs (λa. generate G {a})" by blast
moreover have "finprod G f gs = finprod G (restrict f gs) gs"
proof(intro finprod_cong)
have "f g ∈ carrier G" if "g ∈ gs" for g
using that f(2) mono_generate[of "{g}" gs] generate_incl[OF assms(2)] by fast
thus "(f ∈ gs → carrier G) = True" by blast
qed auto
moreover have "restrict f gs ∈ Pi⇩E gs (λa. generate G {a})" using f(2) by simp
ultimately show "x ∈ (λx. finprod G x gs) ` Pi⇩E gs (λa. generate G {a})" by blast
qed
qed
with generate_eq_finprod_PiE_image[OF assms] show ?thesis by auto
qed
lemma (in comm_group) generate_eq_finprod_Pi_int_image:
assumes "finite gs" "gs ⊆ carrier G"
shows "generate G gs = (λx. finprod G (λg. g [^] x g) gs) ` Pi gs (λ_. (UNIV::int set))"
proof -
from generate_eq_finprod_Pi_image[OF assms]
have "generate G gs = (λx. finprod G x gs) ` (Π a∈gs. generate G {a})" .
also have "… = (λx. finprod G (λg. g [^] x g) gs) ` Pi gs (λ_. (UNIV::int set))"
proof(rule; rule)
fix x
assume x: "x ∈ (λx. finprod G x gs) ` (Π a∈gs. generate G {a})"
then obtain f where f: "f ∈ (Π a∈gs. generate G {a})" "x = finprod G f gs" by blast
hence "∃k::int. f a = a [^] k" if "a ∈ gs" for a using generate_pow[of a] that assms(2) by blast
hence "∃(h::'a ⇒ int). ∀a∈gs. f a = a [^] h a" by meson
then obtain h where h: "∀a∈gs. f a = a [^] h a" "h ∈ gs → (UNIV :: int set)" by auto
have "finprod G (λg. g [^] h g) gs = finprod G f gs"
by (intro finprod_cong, use int_pow_closed h assms(2) in auto)
with f have "x = finprod G (λg. g [^] h g) gs" by argo
with h(2) show "x ∈ (λx. finprod G (λg. g [^] x g) gs) ` (gs → (UNIV::int set))" by auto
next
fix x
assume x: "x ∈ (λx. finprod G (λg. g [^] x g) gs) ` (gs → (UNIV::int set))"
then obtain h where h: "x = finprod G (λg. g [^] h g) gs" "h ∈ gs → (UNIV :: int set)" by blast
hence "∃k∈generate G {a}. a [^] h a = k" if "a ∈ gs" for a
using generate_pow[of a] that assms(2) by blast
then obtain f where f: "∀a∈gs. a [^] h a = f a" "f ∈ (Π a∈gs. generate G {a})" by fast
have "finprod G f gs = finprod G (λg. g [^] h g) gs"
proof(intro finprod_cong)
have "f a ∈ carrier G" if "a ∈ gs" for a
using generate_incl[of "{a}"] assms(2) that f(2) by fast
thus "(f ∈ gs → carrier G) = True" by blast
qed (use f in auto)
with h have "x = finprod G f gs" by argo
with f(2) show "x ∈ (λx. finprod G x gs) ` (Π a∈gs. generate G {a})" by blast
qed
finally show ?thesis .
qed
lemma (in comm_group) IDirProds_eq_finprod_PiE:
assumes "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G"
shows "IDirProds G S I = (λx. finprod G x I) ` (Pi⇩E I S)" (is "?DP = ?fp")
proof
show "?fp ⊆ ?DP"
proof
fix x
assume x: "x ∈ ?fp"
then obtain f where f: "f ∈ (Pi⇩E I S)" "x = finprod G f I" by blast
have sDP: "subgroup ?DP G"
by (intro IDirProds_is_subgroup; use subgroup.subset[OF assms(2)] in blast)
have "finprod G f I ∈ ?DP"
proof(intro finprod_closed_subgroup[OF sDP])
have "f i ∈ IDirProds G S I" if "i ∈ I" for i
proof
show "f i ∈ (S i)" using f(1) that by auto
show "(S i) ⊆ IDirProds G S I" by (intro IDirProds_incl[OF that])
qed
thus "f ∈ I → IDirProds G S I" by simp
qed
thus "x ∈ ?DP" using f by blast
qed
show "?DP ⊆ ?fp"
proof(unfold IDirProds_def; rule subsetI)
fix x
assume x: "x ∈ generate G (⋃(S ` I))"
thus "x ∈ ?fp" using assms
proof (induction rule: generate.induct)
case one
define g where g: "g = (λx. if x ∈ I then 𝟭 else undefined)"
then have "g ∈ Pi⇩E I S"
using subgroup.one_closed[OF one(2)] by auto
moreover have "finprod G g I = 𝟭" by (intro finprod_one_eqI; use g in simp)
ultimately show ?case unfolding image_def by (auto; metis)
next
case i: (incl h)
from i obtain j where j: "j ∈ I" "h ∈ (S j)" by blast
define hf where "hf = (λx. (if x ∈ I then 𝟭 else undefined))(j := h)"
with j have "hf ∈ Pi⇩E I S"
using subgroup.one_closed[OF i(3)] by force
moreover have "finprod G hf I = h"
proof -
have "finprod G hf I = hf j ⊗ finprod G hf (I - {j})"
by (intro finprod_minus, use assms hf_def subgroup.subset[OF i(3)[OF j(1)]] j in auto)
moreover have "hf j = h" using hf_def by simp
moreover have "finprod G hf (I - {j}) = 𝟭" by (rule finprod_one_eqI; use hf_def in simp)
ultimately show ?thesis using subgroup.subset[OF i(3)[OF j(1)]] j(2) by auto
qed
ultimately show ?case unfolding image_def by (auto; metis)
next
case i: (inv h)
from i obtain j where j: "j ∈ I" "h ∈ (S j)" by blast
have ih: "inv h ∈ (S j)" using subgroup.m_inv_closed[OF i(3)[OF j(1)] j(2)] .
define hf where "hf = (λx. (if x ∈ I then 𝟭 else undefined))(j := inv h)"
with j ih have "hf ∈ Pi⇩E I S"
using subgroup.one_closed[OF i(3)] by force
moreover have "finprod G hf I = inv h"
proof -
have "finprod G hf I = hf j ⊗ finprod G hf (I - {j})"
by (intro finprod_minus, use assms hf_def subgroup.subset[OF i(3)[OF j(1)]] j in auto)
moreover have "hf j = inv h" using hf_def by simp
moreover have "finprod G hf (I - {j}) = 𝟭" by (rule finprod_one_eqI; use hf_def in simp)
ultimately show ?thesis using subgroup.subset[OF i(3)[OF j(1)]] j(2) by auto
qed
ultimately show ?case unfolding image_def by (auto; metis)
next
case e: (eng a b)
from e obtain f where f: "f ∈ Pi⇩E I S" "a = finprod G f I" by blast
from e obtain g where g: "g ∈ Pi⇩E I S" "b = finprod G g I" by blast
from f g have "a ⊗ b = finprod G f I ⊗ finprod G g I" by blast
also have "… = finprod G (λa. f a ⊗ g a) I"
proof(intro finprod_multf[symmetric])
have "⋃(S ` I) ⊆ carrier G" using subgroup.subset[OF e(6)] by blast
thus "f ∈ I → carrier G" "g ∈ I → carrier G"
using f(1) g(1) unfolding PiE_def Pi_def by auto
qed
also have "… = finprod G (restrict (λa. f a ⊗ g a) I) I"
proof(intro finprod_cong)
show "I = I" by simp
show "⋀i. i ∈ I =simp=> f i ⊗ g i = (λa∈I. f a ⊗ g a) i" by simp
have fp: "f i ∈ (S i)" if "i ∈ I" for i using f that by auto
have gp: "g i ∈ (S i)" if "i ∈ I" for i using g that by auto
have "f i ⊗ g i ∈ (S i)" if "i ∈ I" for i
using subgroup.m_closed[OF e(6)[OF that] fp[OF that] gp[OF that]] .
thus "((λa. f a ⊗ g a) ∈ I → carrier G) = True" using subgroup.subset[OF e(6)] by auto
qed
finally have "a ⊗ b = finprod G (restrict (λa. f a ⊗ g a) I) I" .
moreover have "(restrict (λa. f a ⊗ g a) I) ∈ Pi⇩E I S"
proof -
have fp: "f i ∈ (S i)" if "i ∈ I" for i using f that by auto
have gp: "g i ∈ (S i)" if "i ∈ I" for i using g that by auto
have "f i ⊗ g i ∈ (S i)" if "i ∈ I" for i
using subgroup.m_closed[OF e(6)[OF that] fp[OF that] gp[OF that]] .
thus ?thesis by auto
qed
ultimately show ?case using f g by blast
qed
qed
qed
lemma (in comm_group) IDirProds_eq_finprod_Pi:
assumes "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G"
shows "IDirProds G S I = (λx. finprod G x I) ` (Pi I S)" (is "?DP = ?fp")
proof -
have "(λx. finprod G x I) ` (Pi I S) = (λx. finprod G x I) ` (Pi⇩E I S)"
proof
have "Pi⇩E I S ⊆ Pi I S" by blast
thus "(λx. finprod G x I) ` Pi⇩E I S ⊆ (λx. finprod G x I) ` Pi I S" by blast
show "(λx. finprod G x I) ` Pi I S ⊆ (λx. finprod G x I) ` Pi⇩E I S"
proof
fix x
assume x: "x ∈ (λx. finprod G x I) ` Pi I S"
then obtain f where f: "x = finprod G f I" "f ∈ Pi I S" by blast
moreover have "finprod G f I = finprod G (restrict f I) I"
by (intro finprod_cong; use f(2) subgroup.subset[OF assms(2)] in fastforce)
moreover have "restrict f I ∈ Pi⇩E I S" using f(2) by simp
ultimately show "x ∈ (λx. finprod G x I) ` Pi⇩E I S" by blast
qed
qed
with IDirProds_eq_finprod_PiE[OF assms] show ?thesis by auto
qed
text ‹If we switch one element from a set of generators, the generated set stays the same if both
elements can be generated from the others together with the switched element respectively.›
lemma (in comm_group) generate_one_switched_exp_eqI:
assumes "A ⊆ carrier G" "a ∈ A" "B = (A - {a}) ∪ {b}"
and "f ∈ A → (UNIV::int set)" "g ∈ B → (UNIV::int set)"
and "a = finprod G (λx. x [^] g x) B" "b = finprod G (λx. x [^] f x) A"
shows "generate G A = generate G B"
proof(intro generate_one_switched_eqI[OF assms(1, 2, 3)]; cases "finite A")
case True
hence fB: "finite B" using assms(3) by blast
have cB: "B ⊆ carrier G"
proof -
have "b ∈ carrier G"
by (subst assms(7), intro finprod_closed, use assms(1, 4) int_pow_closed in fast)
thus ?thesis using assms(1, 3) by blast
qed
show "a ∈ generate G B"
proof(subst generate_eq_finprod_Pi_image[OF fB cB], rule)
show "a = finprod G (λx. x [^] g x) B" by fact
have "x [^] g x ∈ generate G {x}" if "x ∈ B" for x using generate_pow[of x] cB that by blast
thus "(λx. x [^] g x) ∈ (Π a∈B. generate G {a})" unfolding Pi_def by blast
qed
show "b ∈ generate G A"
proof(subst generate_eq_finprod_Pi_image[OF True assms(1)], rule)
show "b = finprod G (λx. x [^] f x) A" by fact
have "x [^] f x ∈ generate G {x}" if "x ∈ A" for x
using generate_pow[of x] assms(1) that by blast
thus "(λx. x [^] f x) ∈ (Π a∈A. generate G {a})" unfolding Pi_def by blast
qed
next
case False
hence b: "b = 𝟭" using assms(7) unfolding finprod_def by simp
from False assms(3) have "infinite B" by simp
hence a: "a = 𝟭" using assms(6) unfolding finprod_def by simp
show "a ∈ generate G B" using generate.one a by blast
show "b ∈ generate G A" using generate.one b by blast
qed
text ‹We can characterize a complementary family of subgroups when the only way to form the neutral
element as a product of picked elements from each subgroup is to pick the neutral element from each
subgroup.›
lemma (in comm_group) compl_fam_imp_triv_finprod:
assumes "compl_fam S I" "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G"
and "finprod G f I = 𝟭" "f ∈ Pi I S"
shows "∀i∈I. f i = 𝟭"
proof (rule ccontr; clarify)
from assms(5) have f: "f i ∈ (S i)" if "i ∈ I" for i using that by fastforce
fix i
assume i: "i ∈ I"
have si: "subgroup (S i) G" using assms(3)[OF i] .
consider (triv) "(S i) = {𝟭}" | (not_triv) "(S i) ≠ {𝟭}" by blast
thus "f i = 𝟭"
proof (cases)
case triv
then show ?thesis using f[OF i] by blast
next
case not_triv
show ?thesis
proof (rule ccontr)
have fc: "f i ∈ carrier G" using f[OF i] subgroup.subset[OF si] by blast
assume no: "f i ≠ 𝟭"
have fH: "f i ∈ (S i)" using f[OF i] .
from subgroup.m_inv_closed[OF si this] have ifi: "inv (f i) ∈ (S i)" .
moreover have "inv (f i) ≠ 𝟭" using no fc by simp
moreover have "inv (f i) = finprod G f (I - {i})"
proof -
have "𝟭 = finprod G f I" using assms(4) by simp
also have "… = finprod G f (insert i (I - {i}))"
proof -
have "I = insert i (I - {i})" using i by fast
thus ?thesis by simp
qed
also have "… = f i ⊗ finprod G f (I - {i})"
proof(intro finprod_insert)
show "finite (I - {i})" using assms(2) by blast
show "i ∉ I - {i}" by blast
show "f ∈ I - {i} → carrier G" using assms(3) f subgroup.subset by blast
show "f i ∈ carrier G" by fact
qed
finally have o: "𝟭 = f i ⊗ finprod G f (I - {i})" .
show ?thesis
proof(intro inv_equality)
show "f i ∈ carrier G" by fact
show "finprod G f (I - {i}) ∈ carrier G"
by (intro finprod_closed; use assms(3) f subgroup.subset in blast)
from m_comm[OF this fc] o show "finprod G f (I - {i}) ⊗ f i = 𝟭" by simp
qed
qed
moreover have "finprod G f (I - {i}) ∈ IDirProds G S (I - {i})"
proof (intro finprod_closed_subgroup IDirProds_is_subgroup)
show "⋃ (S ` (I - {i})) ⊆ carrier G" using assms(3) subgroup.subset by auto
have "f j ∈ (IDirProds G S (I - {i}))" if "j ∈ (I - {i})" for j
using IDirProds_incl[OF that] f that by blast
thus "f ∈ I - {i} → IDirProds G S (I - {i})" by blast
qed
ultimately have "¬complementary (S i) (IDirProds G S (I - {i}))"
unfolding complementary_def by auto
thus False using assms(1) i unfolding compl_fam_def by blast
qed
qed
qed
lemma (in comm_group) triv_finprod_imp_compl_fam:
assumes "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G"
and "∀f ∈ Pi I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭)"
shows "compl_fam S I"
proof (unfold compl_fam_def; rule)
fix k
assume k: "k ∈ I"
let ?DP = "IDirProds G S (I - {k})"
show "complementary (S k) ?DP"
proof (rule ccontr; unfold complementary_def)
have sk: "subgroup (S k) G" using assms(2)[OF k] .
have sDP: "subgroup ?DP G"
by (intro IDirProds_is_subgroup; use subgroup.subset[OF assms(2)] in blast)
assume a: "(S k) ∩ IDirProds G S (I - {k}) ≠ {𝟭}"
then obtain x where x: "x ∈ (S k)" "x ∈ IDirProds G S (I - {k})" "x ≠ 𝟭"
using subgroup.one_closed sk sDP by blast
then have "x ∈ (λx. finprod G x (I - {k})) ` (Pi (I - {k}) S)"
using IDirProds_eq_finprod_Pi[of "(I - {k})"] assms(1, 2) by blast
then obtain ht where ht: "finprod G ht (I - {k}) = x" "ht ∈ Pi (I - {k}) S" by blast
define h where h: "h = (ht(k := inv x))"
then have hPi: "h ∈ Pi I S" using ht subgroup.m_inv_closed[OF assms(2)[OF k] x(1)] by auto
have "finprod G h (I - {k}) = x"
proof (subst ht(1)[symmetric], intro finprod_cong)
show "I - {k} = I - {k}" by simp
show "(h ∈ I - {k} → carrier G) = True" using h ht(2) subgroup.subset[OF assms(2)]
unfolding Pi_def id_def by auto
show "⋀i. i ∈ I - {k} =simp=> h i = ht i" using ht(2) h by simp
qed
moreover have "finprod G h I = h k ⊗ finprod G h (I - {k})"
by (intro finprod_minus; use k assms hPi subgroup.subset[OF assms(2)] Pi_def in blast)
ultimately have "finprod G h I = inv x ⊗ x" using h by simp
then have "finprod G h I = 𝟭" using subgroup.subset[OF sk] x(1) by auto
moreover have "h k ≠ 𝟭" using h x(3) subgroup.subset[OF sk] x(1) by force
ultimately show False using assms(3) k hPi by blast
qed
qed
lemma (in comm_group) triv_finprod_iff_compl_fam_Pi:
assumes "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G"
shows "compl_fam S I ⟷ (∀f ∈ Pi I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭))"
using compl_fam_imp_triv_finprod triv_finprod_imp_compl_fam assms by blast
lemma (in comm_group) triv_finprod_iff_compl_fam_PiE:
assumes "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G"
shows "compl_fam S I ⟷ (∀f ∈ Pi⇩E I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭))"
proof
show "compl_fam S I ⟹ ∀f∈Pi⇩E I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭)"
using triv_finprod_iff_compl_fam_Pi[OF assms] by auto
have "∀f∈Pi⇩E I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭)
⟹ ∀f∈Pi I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭)"
proof(rule+)
fix f i
assume f: "f ∈ Pi I S" "finprod G f I = 𝟭" and i: "i ∈ I"
assume allf: "∀f∈Pi⇩E I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭)"
have "f i = restrict f I i" using i by simp
moreover have "finprod G (restrict f I) I = finprod G f I"
using f subgroup.subset[OF assms(2)] unfolding Pi_def by (intro finprod_cong; auto)
moreover have "restrict f I ∈ Pi⇩E I S" using f by simp
ultimately show "f i = 𝟭" using allf f i by metis
qed
thus "∀f∈Pi⇩E I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭) ⟹ compl_fam S I"
using triv_finprod_iff_compl_fam_Pi[OF assms] by presburger
qed
text ‹The finite product also distributes when nested.›
lemma (in comm_monoid) finprod_Sigma:
assumes "finite A" "⋀x. x ∈ A ⟹ finite (B x)"
assumes "⋀x y. x ∈ A ⟹ y ∈ B x ⟹ g x y ∈ carrier G"
shows "(⨂x∈A. ⨂y∈B x. g x y) = (⨂z∈Sigma A B. case z of (x, y) ⇒ g x y)"
using assms
proof (induction A rule: finite_induct)
case (insert x A)
have "(⨂z∈Sigma (insert x A) B. case z of (x, y) ⇒ g x y) =
(⨂z∈Pair x ` B x. case z of (x, y) ⇒ g x y) ⊗ (⨂z∈Sigma A B. case z of (x, y) ⇒ g x y)"
unfolding Sigma_insert using insert.prems insert.hyps
by (subst finprod_Un_disjoint) auto
also have "(⨂z∈Sigma A B. case z of (x, y) ⇒ g x y) = (⨂x∈A. ⨂y∈B x. g x y)"
using insert.prems insert.hyps by (subst insert.IH [symmetric]) auto
also have "(⨂z∈Pair x ` B x. case z of (x, y) ⇒ g x y) = (⨂y∈B x. g x y)"
using insert.prems insert.hyps by (subst finprod_reindex) (auto intro: inj_onI)
finally show ?case
using insert.hyps insert.prems by simp
qed auto
text ‹With the now proven facts, we are able to provide criterias to inductively construct a
group that is the internal direct product of a set of generators.›
lemma (in comm_group) idirprod_generate_ind:
assumes "finite gs" "gs ⊆ carrier G" "g ∈ carrier G"
"is_idirprod (generate G gs) (λg. generate G {g}) gs"
"complementary (generate G {g}) (generate G gs)"
shows "is_idirprod (generate G (gs ∪ {g})) (λg. generate G {g}) (gs ∪ {g})"
proof(cases "g ∈ gs")
case True
hence "gs = (gs ∪ {g})" by blast
thus ?thesis using assms(4) by auto
next
case gngs: False
show ?thesis
proof (intro is_idirprod_subgroup_suffices)
have gsgc: "gs ∪ {g} ⊆ carrier G" using assms(2, 3) by blast
thus "generate G (gs ∪ {g}) = IDirProds G (λg. generate G {g}) (gs ∪ {g})"
unfolding IDirProds_def using generate_idem_Un by presburger
show "∀i∈gs ∪ {g}. subgroup (generate G {i}) G" using generate_is_subgroup gsgc by auto
have sg: "subgroup (generate G {g}) G" by (intro generate_is_subgroup, use assms(3) in blast)
from assms(4) is_idirprod_def have ih: "∀x. x ∈ gs ⟶ generate G {x} ⊲ G"
"compl_fam (λg. generate G {g}) gs"
by fastforce+
hence ca: "complementary (generate G {a}) (generate G (gs - {a}))" if "a ∈ gs" for a
unfolding compl_fam_def IDirProds_def
using gsgc generate_idem_Un[of "gs - {a}"] that by fastforce
have aux: "gs ∪ {g} - {i} ⊆ carrier G" for i using gsgc by blast
show "compl_fam (λg. generate G {g}) (gs ∪ {g})"
proof(unfold compl_fam_def IDirProds_def, subst generate_idem_Un[OF aux],
rule, rule ccontr)
fix h
assume h: "h ∈ gs ∪ {g}"
assume c: "¬ complementary (generate G {h}) (generate G (gs ∪ {g} - {h}))"
show "False"
proof (cases "h = g")
case True
with c have "¬ complementary (generate G {g}) (generate G (gs - {g}))" by auto
moreover have "complementary (generate G {g}) (generate G (gs - {g}))"
by (rule subgroup_subset_complementary[OF generate_is_subgroup generate_is_subgroup[of gs]
generate_is_subgroup mono_generate], use assms(2, 3, 5) in auto)
ultimately show False by blast
next
case hng: False
hence h: "h ∈ gs" "h ≠ g" using h by blast+
hence "gs ∪ {g} - {h} = gs - {h} ∪ {g}" by blast
with c have c: "¬ complementary (generate G {h}) (generate G (gs - {h} ∪ {g}))" by argo
then obtain k where k: "k ∈ generate G {h}" "k ∈ generate G (gs - {h} ∪ {g})" "k ≠ 𝟭"
unfolding complementary_def using generate.one by blast
with ca have kngh: "k ∉ generate G (gs - {h})" using h unfolding complementary_def by blast
from k(2) generate_eq_finprod_PiE_image[of "gs - {h} ∪ {g}"] assms(1) gsgc
obtain f where f:
"k = finprod G f (gs - {h} ∪ {g})" "f ∈ (Π⇩E a∈gs - {h} ∪ {g}. generate G {a})"
by blast
have fg: "f a ∈ generate G {a}" if "a ∈ (gs - {h} ∪ {g})" for a using that f(2) by blast
have fc: "f a ∈ carrier G" if "a ∈ (gs - {h} ∪ {g})" for a
proof -
have "generate G {a} ⊆ carrier G" if "a ∈ (gs - {h} ∪ {g})" for a
using that generate_incl[of "{a}"] gsgc by blast
thus "f a ∈ carrier G" using that fg by auto
qed
have kp: "k = f g ⊗ finprod G f (gs - {h})"
proof -
have "(gs - {h} ∪ {g}) = insert g (gs - {h})" by fast
moreover have "finprod G f (insert g (gs - {h})) = f g ⊗ finprod G f (gs - {h})"
by (intro finprod_insert, use fc assms(1) gngs in auto)
ultimately show ?thesis using f(1) by argo
qed
have fgsh: "finprod G f (gs - {h}) ∈ generate G (gs - {h})"
proof(intro finprod_closed_subgroup[OF generate_is_subgroup])
show "gs - {h} ⊆ carrier G" using gsgc by blast
have "f a ∈ generate G (gs - {h})" if "a ∈ (gs - {h})" for a
using mono_generate[of "{a}" "gs - {h}"] fg that by blast
thus "f ∈ gs - {h} → generate G (gs - {h})" by blast
qed
have "f g ⊗ finprod G f (gs - {h}) ∉ generate G gs"
proof
assume fpgs: "f g ⊗ finprod G f (gs - {h}) ∈ generate G gs"
from fgsh have fgsgs: "finprod G f (gs - {h}) ∈ generate G gs"
using mono_generate[of "gs - {h}" gs] by blast
have fPi: "f ∈ (Π a∈(gs - {h}). generate G {a})" using f by blast
have gI: "generate G (gs - {h})
= (λx. finprod G x (gs - {h})) ` (Π a∈gs - {h}. generate G {a})"
using generate_eq_finprod_Pi_image[of "gs - {h}"] assms(1, 2) by blast
have fgno: "f g ≠ 𝟭"
proof (rule ccontr)
assume o: "¬ f g ≠ 𝟭"
hence kf: "k = finprod G f (gs - {h})" using kp finprod_closed fc by auto
hence "k ∈ generate G (gs - {h})" using fPi gI by blast
thus False using k ca h unfolding complementary_def by blast
qed
from fpgs have "f g ∈ generate G gs"
using subgroup.mult_in_cancel_right[OF generate_is_subgroup[OF assms(2)] fc[of g] fgsgs]
by blast
with fgno assms(5) fg[of g] show "False" unfolding complementary_def by blast
qed
moreover have "k ∈ generate G gs" using k(1) mono_generate[of "{h}" gs] h(1) by blast
ultimately show False using kp by blast
qed
qed
qed
qed
end