Theory Finitely_Generated_Abelian_Groups
section ‹Fundamental Theorem of Finitely Generated Abelian Groups›
theory Finitely_Generated_Abelian_Groups
imports DirProds Group_Relations
begin
notation integer_mod_group ("Z")
locale fin_gen_comm_group = comm_group +
fixes gen :: "'a set"
assumes gens_closed: "gen ⊆ carrier G"
and fin_gen: "finite gen"
and generators: "carrier G = generate G gen"
text ‹Every finite abelian group is also finitely generated.›
sublocale finite_comm_group ⊆ fin_gen_comm_group G "carrier G"
using generate_incl generate_sincl by (unfold_locales, auto)
text ‹This lemma contains the proof of Kemper from his lecture notes on algebra~\<^cite>‹"kemper"›.
However, the proof is not done in the context of a finitely generated group but for a finitely
generated subgroup in a commutative group.›
lemma (in comm_group) ex_idirgen:
fixes A :: "'a set"
assumes "finite A" "A ⊆ carrier G"
shows "∃gs. set gs ⊆ generate G A ∧ distinct gs ∧ is_idirprod (generate G A) (λg. generate G {g}) (set gs)
∧ successively (dvd) (map ord gs) ∧ card (set gs) ≤ card A"
(is "?t A")
using assms
proof (induction "card A" arbitrary: A rule: nat_less_induct)
case i: 1
show ?case
proof (cases "relations A = {restrict (λ_. 0::int) A}")
case True
have fi: "finite A" by fact
then obtain gs where gs: "set gs = A" "distinct gs" by (meson finite_distinct_list)
have o: "ord g = 0" if "g ∈ set gs" for g
by (intro relations_zero_imp_ord_zero[OF that], use i(3) that True gs in auto)
have m: "map ord gs = replicate (length gs) 0" using o
by (induction gs; auto)
show ?thesis
proof(rule, safe)
show "⋀x. x ∈ set gs ⟹ x ∈ generate G A" using gs generate.incl[of _ A G] by blast
show "distinct gs" by fact
show "is_idirprod (generate G A) (λg. generate G {g}) (set gs)"
proof(unfold is_idirprod_def, intro conjI, rule)
show "generate G {g} ⊲ G" if "g ∈ set gs" for g
by (intro subgroup_imp_normal, use that generate_is_subgroup i(3) gs in auto)
show "generate G A = IDirProds G (λg. generate G {g}) (set gs)" unfolding IDirProds_def
by (subst gs(1), use generate_idem_Un i(3) in blast)
show "compl_fam (λg. generate G {g}) (set gs)" using compl_fam_iff_relations_triv[OF i(2, 3)] o gs(1) True
by blast
qed
show "successively (dvd) (map ord gs)" using m
proof (induction gs)
case c: (Cons a gs)
thus ?case by(cases gs; simp)
qed simp
show "card (set gs) ≤ card A" using gs by blast
qed
next
case ntrel: False
then have Ane: "A ≠ {}"
using i(2) triv_rel[of A] unfolding relations_def extensional_def by fastforce
from ntrel obtain a where a: "a ∈ A" "∃r ∈relations A. r a ≠ 0" using i(2) triv_rel[of A]
unfolding relations_def extensional_def by fastforce
hence ac: "a ∈ carrier G" using i(3) by blast
have iH: "⋀B.⟦card B < card A; finite B; B ⊆ carrier G⟧ ⟹ ?t B"
using i(1) by blast
have iH2: "⋀B. ⟦?t B; generate G A = generate G B; card B < card A⟧ ⟹ ?t A"
by fastforce
show ?thesis
proof(cases "inv a ∈ (A - {a})")
case True
have "generate G A = generate G (A - {a})"
proof(intro generate_subset_eqI[OF i(3)])
show "A - (A - {a}) ⊆ generate G (A - {a})"
proof -
have "A - (A - {a}) = {a}" using a True by auto
also have "… ⊆ generate G {inv a}" using generate.inv[of "inv a" "{inv a}" G] ac by simp
also have "… ⊆ generate G (A - {a})" by (intro mono_generate, use True in simp)
finally show ?thesis .
qed
qed simp
moreover have "?t (A - {a})"
by (intro iH[of "A - {a}"], use i(2, 3) a(1) in auto, meson Ane card_gt_0_iff diff_Suc_less)
ultimately show ?thesis using card.remove[OF i(2) a(1)] by fastforce
next
case inv: False
define n where n: "n = card A"
define all_gens where
"all_gens = {gs∈Pow (generate G A). finite gs ∧ card gs ≤ n ∧ generate G gs = generate G A}"
define exps where "exps = (⋃gs'∈all_gens. ⋃rel∈relations gs'. nat ` {e∈rel`gs'. e > 0})"
define min_exp where "min_exp = Inf exps"
have "exps ≠ {}"
proof -
let ?B = "A - {a} ∪ {inv a}"
have "A ∈ all_gens" unfolding all_gens_def using generate.incl n i(2) by fast
moreover have "?B ∈ all_gens"
proof -
have "card (A - {a}) = n - 1" using a n by (meson card_Diff_singleton_if i(2))
hence "card ?B = n" using inv i(2, 3) n a(1)
by (metis Un_empty_right Un_insert_right card.remove card_insert_disjoint finite_Diff)
moreover have "generate G A = generate G ?B"
proof(intro generate_one_switched_eqI[OF i(3) a(1), of _ "inv a"])
show "inv a ∈ generate G A" using generate.inv[OF a(1), of G] .
show "a ∈ generate G ?B"
proof -
have "a ∈ generate G {inv a}" using generate.inv[of "inv a" "{inv a}" G] ac by simp
also have "… ⊆ generate G ?B" by (intro mono_generate, blast)
finally show ?thesis .
qed
qed simp
moreover hence "?B ⊆ generate G A" using generate_sincl by simp
ultimately show ?thesis unfolding all_gens_def using i(2) by blast
qed
moreover have "(∃r ∈ relations A. r a > 0) ∨ (∃r ∈ relations ?B. r (inv a) > 0)"
proof(cases "∃r ∈ relations A. r a > 0")
case True
then show ?thesis by blast
next
case False
with a obtain r where r: "r ∈ relations A" "r a < 0" by force
have rc: "(λx. x [^] r x) ∈ A → carrier G" using i(3) int_pow_closed by fast
let ?r = "restrict (r(inv a := - r a)) ?B"
have "?r ∈ relations ?B"
proof
have "finprod G (λx. x [^] ?r x) ?B = finprod G (λx. x [^] r x) A"
proof -
have "finprod G (λx. x [^] ?r x) ?B
= finprod G (λx. x [^] ?r x) (insert (inv a) (A - {a}))" by simp
also have "… = (inv a) [^] ?r (inv a) ⊗ finprod G (λx. x [^] ?r x) (A - {a})"
proof(intro finprod_insert[OF _ inv])
show "finite (A - {a})" using i(2) by fast
show "inv a [^] ?r (inv a) ∈ carrier G"
using int_pow_closed[OF inv_closed[OF ac]] by fast
show "(λx. x [^] ?r x) ∈ A - {a} → carrier G" using int_pow_closed i(3) by fast
qed
also have "… = a [^] r a ⊗ finprod G (λx. x [^] r x) (A - {a})"
proof -
have "(inv a) [^] ?r (inv a) = a [^] r a"
by (simp add: int_pow_inv int_pow_neg ac)
moreover have "finprod G (λx. x [^] r x) (A - {a})
= finprod G (λx. x [^] ?r x) (A - {a})"
proof(intro finprod_cong)
show "((λx. x [^] r x) ∈ A - {a} → carrier G) = True" using rc by blast
have "i [^] r i = i [^] ?r i" if "i ∈ A - {a}" for i using that inv by auto
thus "⋀i. i ∈ A - {a} =simp=> i [^] r i = i [^] restrict (r(inv a := - r a)) (A - {a} ∪ {inv a}) i"
by algebra
qed simp
ultimately show ?thesis by argo
qed
also have "… = finprod G (λx. x [^] r x) A"
by (intro finprod_minus[symmetric, OF a(1) rc i(2)])
finally show ?thesis .
qed
also have "… = 𝟭" using r unfolding relations_def by fast
finally show "finprod G (λx. x [^] ?r x) ?B = 𝟭" .
qed simp
then show ?thesis using r by fastforce
qed
ultimately show ?thesis unfolding exps_def using a by blast
qed
hence me: "min_exp ∈ exps"
unfolding min_exp_def using Inf_nat_def1 by force
from cInf_lower min_exp_def have le: "⋀x. x ∈ exps ⟹ min_exp ≤ x" by blast
from me obtain gs rel g
where gr: "gs ∈ all_gens" "rel ∈ relations gs" "g ∈ gs" "rel g = min_exp" "min_exp > 0"
unfolding exps_def by auto
from gr(1) have cgs: "card gs ≤ card A" unfolding all_gens_def n by blast
with gr(3) have cgsg: "card (gs - {g}) < card A"
by (metis Ane card.infinite card_Diff1_less card_gt_0_iff finite.emptyI
finite.insertI finite_Diff2 i.prems(1) le_neq_implies_less less_trans)
from gr(1) have fgs: "finite gs" and gsg: "generate G gs = generate G A"
unfolding all_gens_def n using i(2) card.infinite Ane by force+
from gsg have gsc: "gs ⊆ carrier G" unfolding all_gens_def
using generate_incl[OF i(3)] generate_sincl[of gs] by simp
hence gc: "g ∈ carrier G" using gr(3) by blast
have ihgsg: "?t (gs - {g})"
by (intro iH, use cgs fgs gsc gr(3) cgsg in auto)
then obtain hs where
hs: "set hs ⊆ generate G (gs - {g})" "distinct hs"
"is_idirprod (generate G (gs - {g})) (λg. generate G {g}) (set hs)"
"successively (dvd) (map ord hs)" "card (set hs) ≤ card (gs - {g})" by blast
hence hsc: "set hs ⊆ carrier G"
using generate_sincl[of "set hs"] generate_incl[of "gs - {g}"] gsc by blast
from hs(3) have ghs: "generate G (gs - {g}) = generate G (set hs)"
unfolding is_idirprod_def IDirProds_def using generate_idem_Un[OF hsc] by argo
have dvot: "?t A ∨ (∀e∈rel`gs. rel g dvd e)"
proof(intro disjCI)
assume na: "¬ (∀e∈rel ` gs. rel g dvd e)"
have "⋀x. ⟦x ∈ gs; ¬rel g dvd rel x⟧ ⟹ ?t A"
proof -
fix x
assume x: "x ∈ gs" "¬ rel g dvd rel x"
hence xng: "x ≠ g" by auto
from x have xc: "x ∈ carrier G" using gsc by blast
have rg: "rel g > 0" using gr by simp
define r::int where r: "r = rel x mod rel g"
define q::int where q: "q = rel x div rel g"
from r rg x have "r > 0"
using mod_int_pos_iff[of "rel x" "rel g"] mod_eq_0_iff_dvd by force
moreover have "r < rel g" using r rg by simp
moreover have "rel x = q * rel g + r" using r q by presburger
ultimately have rq: "rel x = q * (rel g) + r" "0 < r" "r < rel g" by auto
define t where t: "t = g ⊗ x [^] q"
hence tc: "t ∈ carrier G" using gsc gr(3) x by fast
define s where s: "s = gs - {g} ∪ {t}"
hence fs: "finite s" using fgs by blast
have sc: "s ⊆ carrier G" using s tc gsc by blast
have g: "generate G gs = generate G s"
proof(unfold s, intro generate_one_switched_eqI[OF gsc gr(3), of _ t])
show "t ∈ generate G gs"
proof(unfold t, intro generate.eng)
show "g ∈ generate G gs" using gr(3) generate.incl by fast
show "x [^] q ∈ generate G gs"
using x generate_pow[OF xc] generate_sincl[of "{x}"] mono_generate[of "{x}" gs]
by fast
qed
show "g ∈ generate G (gs - {g} ∪ {t})"
proof -
have gti: "g = t ⊗ inv (x [^] q)"
using inv_solve_right[OF gc tc int_pow_closed[OF xc, of q]] t by blast
moreover have "t ∈ generate G (gs - {g} ∪ {t})" by (intro generate.incl[of t], simp)
moreover have "inv (x [^] q) ∈ generate G (gs - {g})"
proof -
have "x [^] q ∈ generate G {x}" using generate_pow[OF xc] by blast
from generate_m_inv_closed[OF _ this] xc
have "inv (x [^] q) ∈ generate G {x}" by blast
moreover have "generate G {x} ⊆ generate G (gs - {g})"
by (intro mono_generate, use x a in force)
finally show ?thesis .
qed
ultimately show ?thesis
using generate.eng mono_generate[of "gs - {g}" "gs - {g} ∪ {t}"] by fast
qed
qed simp
show "⟦x ∈ gs; ¬ rel g dvd rel x⟧ ⟹ ?t A"
proof (cases "t ∈ gs - {g}")
case xt: True
from xt have gts: "s = gs - {g}" using x s by auto
moreover have "card (gs - {g}) < card gs" using fgs gr(3) by (meson card_Diff1_less)
ultimately have "card (set hs) < card A" using hs(5) cgs by simp
moreover have "set hs ⊆ generate G (set hs)" using generate_sincl by simp
moreover have "distinct hs" by fact
moreover have "is_idirprod (generate G (set hs)) (λg. generate G {g}) (set hs)"
using hs ghs unfolding is_idirprod_def by blast
moreover have "generate G A = generate G (set hs)" using g gts ghs gsg by argo
moreover have "successively (dvd) (map ord hs)" by fact
ultimately show "?t A" using iH2 by blast
next
case tngsg: False
hence xnt: "x ≠ t" using x xng by blast
have "rel g dvd rel x"
proof (rule ccontr)
have "nat r ∈ exps" unfolding exps_def
proof
show "s ∈ all_gens" unfolding all_gens_def
using gsg g fgs generate_sincl[of s] switch_elem_card_le[OF gr(3), of t] cgs n s
by auto
have xs: "x ∈ s" using s xng x(1) by blast
have ts: "t ∈ s" using s by fast
show "nat r ∈ (⋃rel∈relations s. nat ` {e ∈ rel ` s. 0 < e})"
proof
let ?r = "restrict (rel(x := r, t := rel g)) s"
show "?r ∈ relations s"
proof
have "finprod G (λx. x [^] ?r x) s = finprod G (λx. x [^] rel x) gs"
proof -
have "finprod G (λx. x [^] ?r x) s = x [^] r ⊗ (t [^] rel g ⊗ finprod G (λx. x [^] rel x) (gs - {g} - {x}))"
proof -
have "finprod G (λx. x [^] ?r x) s = x [^] ?r x ⊗ finprod G (λx. x [^] ?r x) (s - {x})"
by (intro finprod_minus[OF xs _ fs], use sc in auto)
moreover have "finprod G (λx. x [^] ?r x) (s - {x}) = t [^] ?r t ⊗ finprod G (λx. x [^] ?r x) (s - {x} - {t})"
by (intro finprod_minus, use ts xnt fs sc in auto)
moreover have "finprod G (λx. x [^] ?r x) (s - {x} - {t}) = finprod G (λx. x [^] rel x) (s - {x} - {t})"
unfolding s by (intro finprod_cong', use gsc in auto)
moreover have "s - {x} - {t} = gs - {g} - {x}" unfolding s using tngsg by blast
moreover hence "finprod G (λx. x [^] rel x) (s - {x} - {t}) = finprod G (λx. x [^] rel x) (gs - {g} - {x})" by simp
moreover have "x [^] ?r x = x [^] r" using xs xnt by auto
moreover have "t [^] ?r t = t [^] rel g" using ts by simp
ultimately show ?thesis by argo
qed
also have "… = x [^] r ⊗ t [^] rel g ⊗ finprod G (λx. x [^] rel x) (gs - {g} - {x})"
by (intro m_assoc[symmetric], use xc tc in simp_all, intro finprod_closed, use gsc in fast)
also have "… = g [^] rel g ⊗ x [^] rel x ⊗ finprod G (λx. x [^] rel x) (gs - {g} - {x})"
proof -
have "x [^] r ⊗ t [^] rel g = g [^] rel g ⊗ x [^] rel x"
proof -
have "x [^] r ⊗ t [^] rel g = x [^] r ⊗ (g ⊗ x [^] q) [^] rel g" using t by blast
also have "… = x [^] r ⊗ x [^] (q * rel g) ⊗ g [^] rel g"
proof -
have "(g ⊗ x [^] q) [^] rel g = g [^] rel g ⊗ (x [^] q) [^] rel g"
using gc xc int_pow_distrib by auto
moreover have "(x [^] q) [^] rel g = x [^] (q * rel g)" using xc int_pow_pow by auto
moreover have "g [^] rel g ⊗ x [^] (q * rel g) = x [^] (q * rel g) ⊗ g [^] rel g"
using m_comm[OF int_pow_closed[OF xc] int_pow_closed[OF gc]] by simp
ultimately have "(g ⊗ x [^] q) [^] rel g = x [^] (q * rel g) ⊗ g [^] rel g" by argo
thus ?thesis by (simp add: gc m_assoc xc)
qed
also have "… = x [^] rel x ⊗ g [^] rel g"
proof -
have "x [^] r ⊗ x [^] (q * rel g) = x [^] (q * rel g + r)"
by (simp add: add.commute int_pow_mult xc)
also have "… = x [^] rel x" using rq by argo
finally show ?thesis by argo
qed
finally show ?thesis by (simp add: gc m_comm xc)
qed
thus ?thesis by simp
qed
also have "… = g [^] rel g ⊗ (x [^] rel x ⊗ finprod G (λx. x [^] rel x) (gs - {g} - {x}))"
by (intro m_assoc, use xc gc in simp_all, intro finprod_closed, use gsc in fast)
also have "… = g [^] rel g ⊗ finprod G (λx. x [^] rel x) (gs - {g})"
proof -
have "finprod G (λx. x [^] rel x) (gs - {g}) = x [^] rel x ⊗ finprod G (λx. x [^] rel x) (gs - {g} - {x})"
by (intro finprod_minus, use xng x(1) fgs gsc in auto)
thus ?thesis by argo
qed
also have "… = finprod G (λx. x [^] rel x) gs" by (intro finprod_minus[symmetric, OF gr(3) _ fgs], use gsc in auto)
finally show ?thesis .
qed
thus "finprod G (λx. x [^] ?r x) s = 𝟭" using gr(2) unfolding relations_def by simp
qed auto
show "nat r ∈ nat ` {e ∈ ?r ` s. 0 < e}" using xs xnt rq(2) by fastforce
qed
qed
from le[OF this] rq(3) gr(4, 5) show False by linarith
qed
thus "⟦x ∈ gs; ¬ rel g dvd rel x⟧ ⟹ ?t A" by blast
qed
qed
thus "?t A" using na by blast
qed
show "?t A"
proof (cases "∀e∈rel`gs. rel g dvd e")
case dv: True
define tau where "tau = finprod G (λx. x [^] ((rel x) div rel g)) gs"
have tc: "tau ∈ carrier G"
by (subst tau_def, intro finprod_closed[of "(λx. x [^] ((rel x) div rel g))" gs], use gsc in fast)
have gts: "generate G gs = generate G (gs - {g} ∪ {tau})"
proof(intro generate_one_switched_eqI[OF gsc gr(3), of _ tau])
show "tau ∈ generate G gs" by (subst generate_eq_finprod_Pi_int_image[OF fgs gsc], unfold tau_def, fast)
show "g ∈ generate G (gs - {g} ∪ {tau})"
proof -
have "tau = g ⊗ finprod G (λx. x [^] ((rel x) div rel g)) (gs - {g})"
proof -
have "finprod G (λx. x [^] ((rel x) div rel g)) gs = g [^] (rel g div rel g) ⊗ finprod G (λx. x [^] ((rel x) div rel g)) (gs - {g})"
by (intro finprod_minus[OF gr(3) _ fgs], use gsc in fast)
moreover have "g [^] (rel g div rel g) = g" using gr gsc by auto
ultimately show ?thesis unfolding tau_def by argo
qed
hence gti: "g = tau ⊗ inv finprod G (λx. x [^] ((rel x) div rel g)) (gs - {g})"
using inv_solve_right[OF gc tc finprod_closed[of "(λx. x [^] ((rel x) div rel g))" "gs - {g}"]] gsc
by fast
have "tau ∈ generate G (gs - {g} ∪ {tau})" by (intro generate.incl[of tau], simp)
moreover have "inv finprod G (λx. x [^] ((rel x) div rel g)) (gs - {g}) ∈ generate G (gs - {g})"
proof -
have "finprod G (λx. x [^] ((rel x) div rel g)) (gs - {g}) ∈ generate G (gs - {g})"
using generate_eq_finprod_Pi_int_image[of "gs - {g}"] fgs gsc by fast
from generate_m_inv_closed[OF _ this] gsc show ?thesis by blast
qed
ultimately show ?thesis by (subst gti, intro generate.eng, use mono_generate[of "gs - {g}"] in auto)
qed
qed simp
with gr(1) have gt: "generate G (gs - {g} ∪ {tau}) = generate G A" unfolding all_gens_def by blast
have trgo: "tau [^] rel g = 𝟭"
proof -
have "tau [^] rel g = finprod G (λx. x [^] ((rel x) div rel g)) gs [^] rel g" unfolding tau_def by blast
also have "… = finprod G ((λx. x [^] rel g) ∘ (λx. x [^] ((rel x) div rel g))) gs"
by (intro finprod_exp, use gsc in auto)
also have "… = finprod G (λa. a [^] rel a) gs"
proof(intro finprod_cong')
show "((λx. x [^] rel g) ∘ (λx. x [^] ((rel x) div rel g))) x = x [^] rel x" if "x ∈ gs" for x
proof -
have "((λx. x [^] rel g) ∘ (λx. x [^] ((rel x) div rel g))) x = x [^] (((rel x) div rel g) * rel g)"
using that gsc int_pow_pow by auto
also have "… = x [^] rel x" using dv that by auto
finally show ?thesis .
qed
qed (use gsc in auto)
also have "… = 𝟭" using gr(2) unfolding relations_def by blast
finally show ?thesis .
qed
hence otdrg: "ord tau dvd rel g" using tc int_pow_eq_id by force
have ot: "ord tau = rel g"
proof -
from gr(4, 5) have "rel g > 0" by simp
with otdrg have "ord tau ≤ rel g" by (meson zdvd_imp_le)
moreover have "¬ord tau < rel g"
proof
assume a: "int (ord tau) < rel g"
define T where T: "T = gs - {g} ∪ {tau}"
hence tT: "tau ∈ T" by blast
let ?r = "restrict ((λ_.(0::int))(tau := int(ord tau))) T"
from T have "T ∈ all_gens"
using gt generate_sincl[of "gs - {g} ∪ {tau}"] switch_elem_card_le[OF gr(3), of tau] fgs cgs n
unfolding all_gens_def by auto
moreover have "?r ∈ relations T"
proof(intro in_relationsI finprod_one_eqI)
have "tau [^] int (ord tau) = 𝟭" using tc pow_ord_eq_1[OF tc] int_pow_int by metis
thus "x [^] ?r x = 𝟭" if "x ∈ T" for x using tT that by(cases "¬x = tau", auto)
qed auto
moreover have "?r tau = ord tau" using tT by auto
moreover have "ord tau > 0" using dvd_nat_bounds gr(4) gr(5) int_dvd_int_iff otdrg by presburger
ultimately have "ord tau ∈ exps" unfolding exps_def using tT by (auto, force)
with le a gr(4) show False by force
qed
ultimately show ?thesis by auto
qed
hence otnz: "ord tau ≠ 0" using gr me exps_def by linarith
define l where l: "l = tau#hs"
hence ls: "set l = set hs ∪ {tau}" by auto
with hsc tc have slc: "set l ⊆ carrier G" by auto
have gAhst: "generate G A = generate G (set hs ∪ {tau})"
proof -
have "generate G A = generate G (gs - {g} ∪ {tau})" using gt by simp
also have "… = generate G (set hs ∪ {tau})"
by (rule generate_subset_change_eqI, use hsc gsc tc ghs in auto)
finally show ?thesis .
qed
have glgA: "generate G (set l) = generate G A" using gAhst ls by simp
have lgA: "set l ⊆ generate G A"
using ls gt gts hs(1)
mono_generate[of "gs - {g}" gs] generate.incl[of tau "gs - {g} ∪ {tau}"]
by fast
show ?thesis
proof (cases "ord tau = 1")
case True
hence "tau = 𝟭" using ord_eq_1 tc by blast
hence "generate G A = generate G (gs - {g})"
using gAhst generate_one_irrel hs(3) ghs by auto
from iH2[OF ihgsg this cgsg] show ?thesis .
next
case otau: False
consider (nd) "¬distinct l" | (ltn) "length l < n ∧ distinct l" | (dn) "length l = n ∧ distinct l"
proof -
have "length l ≤ n"
proof -
have "length l = length hs + 1" using l by simp
moreover have "length hs ≤ card (gs - {g})" using hs(2, 5) by (metis distinct_card)
moreover have "card (gs - {g}) + 1 ≤ n"
using n cgsg gr(3) fgs Ane i(2) by (simp add: card_gt_0_iff)
ultimately show ?thesis by linarith
qed
thus "⟦¬ distinct l ⟹ thesis; length l < n ∧ distinct l ⟹ thesis; length l = n ∧ distinct l ⟹ thesis⟧ ⟹ thesis"
by linarith
qed
thus ?thesis
proof(cases)
case nd
with hs(2) l have ths: "set hs = set hs ∪ {tau}" by auto
hence "set l = set hs" using l by auto
hence "generate G (gs - {g}) = generate G A" using gAhst ths ghs by argo
moreover have "card (set hs) ≤ card A"
by (metis Diff_iff card_mono cgs dual_order.trans fgs hs(5) subsetI)
ultimately show ?thesis using hs by auto
next
case ltn
then have cl: "card (set l) < card A" using n by (metis distinct_card)
from iH[OF this] hsc tc ls have "?t (set l)" by blast
thus ?thesis by (subst (1 2) gAhst, use cl ls in fastforce)
next
case dn
hence ln: "length l = n" and dl: "distinct l" by auto
have c: "complementary (generate G {tau}) (generate G (gs - {g}))"
proof -
have "x = 𝟭" if "x ∈ generate G {tau} ∩ generate G (set hs)" for x
proof -
from that generate_incl[OF hsc] have xc: "x ∈ carrier G" by blast
from that have xgt: "x ∈ generate G {tau}" and xgs: "x ∈ generate G (set hs)"
by auto
from generate_nat_pow[OF otnz tc] xgt have "∃a. a ≥ 0 ∧ a < ord tau ∧ x = tau [^] a"
unfolding atLeastAtMost_def atLeast_def atMost_def
by (auto, metis Suc_pred less_Suc_eq_le neq0_conv otnz)
then obtain a where a: "0 ≤ a" "a < ord tau" "x = tau [^] a" by blast
then have ix: "inv x ∈ generate G (set hs)"
using xgs generate_m_inv_closed ghs hsc by blast
with generate_eq_finprod_Pi_int_image[OF _ hsc] obtain f where
f: "f ∈ Pi (set hs) (λ_. (UNIV::int set))" "inv x = finprod G (λg. g [^] f g) (set hs)"
by blast
let ?f = "restrict (f(tau := a)) (set l)"
have fr: "?f ∈ relations (set l)"
proof(intro in_relationsI)
from ls dl l have sh: "set hs = set l - {tau}" by auto
have "finprod G (λa. a [^] ?f a) (set l) = tau [^] ?f tau ⊗ finprod G (λa. a [^] ?f a) (set hs)"
by (subst sh, intro finprod_minus, use l slc in auto)
moreover have "tau [^] ?f tau = x" using a l int_pow_int by fastforce
moreover have "finprod G (λa. a [^] ?f a) (set hs) = finprod G (λg. g [^] f g) (set hs)"
by (intro finprod_cong', use slc dl l in auto)
ultimately have "finprod G (λa. a [^] ?f a) (set l) = x ⊗ inv x" using f by argo
thus "finprod G (λa. a [^] ?f a) (set l) = 𝟭" using xc by auto
qed blast
have "¬a > 0"
proof
assume ag: "0 < a"
have "set l ∈ all_gens" unfolding all_gens_def using glgA lgA dn distinct_card
by fastforce
moreover have "int a = ?f tau" using l by auto
moreover have "tau ∈ set l" using l by simp
ultimately have "a ∈ exps" using fr ag unfolding exps_def by (auto, force)
from le[OF this] a(2) ot gr(4) show False by simp
qed
hence "a = 0" using a by blast
thus "x = 𝟭" using tc a by force
qed
thus ?thesis unfolding complementary_def using generate.one ghs by blast
qed
moreover have idl: "is_idirprod (generate G A) (λg. generate G {g}) (set l)"
proof -
have "is_idirprod (generate G (set hs ∪ {tau})) (λg. generate G {g}) (set hs ∪ {tau})"
by (intro idirprod_generate_ind, use tc hsc hs(3) ghs c in auto)
thus ?thesis using ls gAhst by auto
qed
moreover have "¬?t A ⟹ successively (dvd) (map ord l)"
proof (cases hs)
case Nil
thus ?thesis using l by simp
next
case (Cons a list)
hence ac: "a ∈ carrier G" using hsc by auto
assume nA: "¬?t A"
have "ord tau dvd ord a"
proof (rule ccontr)
assume nd: "¬ ord tau dvd ord a"
then have ‹0 < ord a mod ord tau›
using mod_eq_0_iff_dvd by auto
have "int (ord tau) > 0" using otnz by simp
obtain r q :: int where rq: "ord a = q * (ord tau) + r" "0 < r" "r < ord tau"
by (rule that [of ‹ord a div ord tau› ‹ord a mod ord tau›])
(use otnz ‹0 < ord a mod ord tau› in ‹simp_all add: div_mult_mod_eq flip: of_nat_mult of_nat_add›)
define b where b: "b = tau ⊗ a [^] q"
hence bc: "b ∈ carrier G" using hsc tc Cons by auto
have g: "generate G (set (b#hs)) = generate G (set l)"
proof -
have se: "set (b#hs) = set l - {tau} ∪ {b}" using l Cons dl by auto
show ?thesis
proof(subst se, intro generate_one_switched_eqI[symmetric, of _ tau _ b])
show "b ∈ generate G (set l)"
proof -
have "tau ∈ generate G (set l)" using l generate.incl[of tau "set l"] by auto
moreover have "a [^] q ∈ generate G (set l)"
using mono_generate[of "{a}" "set l"] generate_pow[OF ac] Cons l by auto
ultimately show ?thesis using b generate.eng by fast
qed
show "tau ∈ generate G (set l - {tau} ∪ {b})"
proof -
have "tau = b ⊗ inv(a [^] q)" by (simp add: ac b m_assoc tc)
moreover have "b ∈ generate G (set l - {tau} ∪ {b})"
using generate.incl[of b "set l - {tau} ∪ {b}"] by blast
moreover have "inv(a [^] q) ∈ generate G (set l - {tau} ∪ {b})"
proof -
have "generate G {a} ⊆ generate G (set l - {tau} ∪ {b})"
using mono_generate[of "{a}" "set l - {tau} ∪ {b}"] dl Cons l by auto
moreover have "inv(a [^] q) ∈ generate G {a}"
by (subst generate_pow[OF ac], subst int_pow_neg[OF ac, of q, symmetric], blast)
ultimately show ?thesis by fast
qed
ultimately show ?thesis using generate.eng by fast
qed
qed (use bc tc hsc dl Cons l in auto)
qed
show False
proof (cases "card (set (b#hs)) ≠ n")
case True
hence cln: "card (set (b#hs)) < n"
using l Cons ln by (metis card_length list.size(4) nat_less_le)
hence seq: "set (b#hs) = set hs"
proof -
from dn l Cons True have "b ∈ set hs"
by (metis distinct.simps(2) distinct_card list.size(4))
thus ?thesis by auto
qed
with cln have clA: "card (set hs) < card A" using n by auto
moreover have "set hs ⊆ generate G (set hs)" using generate_sincl by simp
moreover have "distinct hs" by fact
moreover have "is_idirprod (generate G (set hs)) (λg. generate G {g}) (set hs)"
by (intro is_idirprod_generate, use hs[unfolded is_idirprod_def] hsc in auto)
moreover have "generate G A = generate G (set hs)" using glgA g seq by argo
moreover have "successively (dvd) (map ord hs)" by fact
ultimately show False using iH2 nA by blast
next
case False
hence anb: "a ≠ b"
by (metis card_distinct distinct_length_2_or_more l list.size(4) ln local.Cons)
have "nat r ∈ exps" unfolding exps_def
proof(rule)
show "set (b#hs) ∈ all_gens" unfolding all_gens_def
using gAhst g ls generate_sincl[of "set (b#hs)"] False by simp
let ?r = "restrict ((λ_. 0::int)(b := ord tau, a := r)) (set (b#hs))"
have "?r ∈ relations (set (b#hs))"
proof(intro in_relationsI)
show "finprod G (λx. x [^] ?r x) (set (b#hs)) = 𝟭"
proof -
have "finprod G (λx. x [^] ?r x) (set (b#hs)) = b [^] ?r b ⊗ finprod G (λx. x[^] ?r x) (set (b#hs) - {b})"
by (intro finprod_minus, use hsc Cons bc in auto)
moreover have "finprod G (λx. x[^] ?r x) (set (b#hs) - {b}) = a [^] ?r a ⊗ finprod G (λx. x[^] ?r x) (set (b#hs) - {b} - {a})"
by (intro finprod_minus, use hsc Cons False n anb in auto)
moreover have "finprod G (λx. x[^] ?r x) (set (b#hs) - {b} - {a}) = 𝟭"
by (intro finprod_one_eqI, simp)
ultimately have "finprod G (λx. x [^] ?r x) (set (b#hs)) = b [^] ?r b ⊗ (a [^] ?r a ⊗ 𝟭)"
by argo
also have "… = b [^] ?r b ⊗ a [^] ?r a" using Cons hsc by simp
also have "… = b [^] int(ord tau) ⊗ a [^] r" using anb Cons by simp
also have "… = 𝟭"
proof -
have "b [^] int (ord tau) = tau [^] int (ord tau) ⊗ (a [^] q) [^] int (ord tau)"
using b bc hsc int_pow_distrib local.Cons tc by force
also have "… = (a [^] q) [^] int (ord tau)"
using trgo hsc local.Cons ot by force
finally have "b [^] int (ord tau) ⊗ a [^] r = (a [^] q) [^] int (ord tau) ⊗ a [^] r"
by argo
also have "… = a [^] (q * int (ord tau) + r)" using Cons hsc
by (metis comm_group_axioms comm_group_def group.int_pow_pow
int_pow_mult list.set_intros(1) subsetD)
also have "… = a [^] int (ord a)" using rq by argo
finally show ?thesis using Cons hsc int_pow_eq_id by simp
qed
finally show ?thesis .
qed
qed simp
moreover have "r ∈ {e ∈ ?r ` set (b # hs). 0 < e}"
proof (rule, rule, rule)
show "0 < r" by fact
show "a ∈ set (b#hs)" using Cons by simp
thus "r = ?r a" by auto
qed
ultimately show "nat r ∈ (⋃rel∈relations (set (b # hs)). nat ` {e ∈ rel ` set (b # hs). 0 < e})"
by fast
qed
moreover have "nat r < min_exp" using ot rq(2, 3) gr(4) by linarith
ultimately show False using le by fastforce
qed
qed
thus ?thesis using hs(4) Cons l by simp
qed
ultimately show ?thesis using lgA n dn by (metis card_length)
qed
qed
qed (use dvot in blast)
qed
qed
qed
lemma (in comm_group) fundamental_subgr:
fixes A :: "'a set"
assumes "finite A" "A ⊆ carrier G"
obtains gs where
"set gs ⊆ generate G A" "distinct gs" "is_idirprod (generate G A) (λg. generate G {g}) (set gs)"
"successively (dvd) (map ord gs)" "card (set gs) ≤ card A"
using assms ex_idirgen by meson
text ‹As every group is a subgroup of itself, the theorem follows directly. However, for reasons of
convenience and uniqueness (although not completely proved), we strengthen the result by proving
that the decomposition can be done without having the trivial factor in the product.
We formulate the theorem in various ways: firstly, the invariant factor decomposition.›
theorem (in fin_gen_comm_group) invariant_factor_decomposition_idirprod:
obtains gs where
"set gs ⊆ carrier G" "distinct gs" "is_idirprod (carrier G) (λg. generate G {g}) (set gs)"
"successively (dvd) (map ord gs)" "card (set gs) ≤ card gen" "𝟭 ∉ set gs"
proof -
from fundamental_subgr[OF fin_gen gens_closed] obtain gs where
gs: "set gs ⊆ carrier G" "distinct gs" "is_idirprod (carrier G) (λg. generate G {g}) (set gs)"
"successively (dvd) (map ord gs)" "card (set gs) ≤ card gen" using generators by auto
hence cf: "compl_fam (λg. generate G {g}) (set gs)" by simp
let ?r = "remove1 𝟭 gs"
have r: "set ?r = set gs - {𝟭}" using gs by auto
have "set ?r ⊆ carrier G" using gs by auto
moreover have "distinct ?r" using gs by auto
moreover have "is_idirprod (carrier G) (λg. generate G {g}) (set ?r)"
proof (intro is_idirprod_generate)
show "set ?r ⊆ carrier G" using gs by auto
show "compl_fam (λg. generate G {g}) (set (remove1 𝟭 gs))"
by (rule compl_fam_generate_subset[OF cf gs(1)], use set_remove1_subset in fastforce)
show "carrier G = generate G (set ?r)"
proof -
have "generate G (set ?r) = generate G (set gs)" using generate_one_irrel' r by simp
with gs(3) show ?thesis by simp
qed
qed
moreover have "successively (dvd) (map ord ?r)"
proof (cases gs)
case (Cons a list)
have r: "(map ord (remove1 𝟭 gs)) = remove1 1 (map ord gs)" using gs(1)
proof(induction gs)
case (Cons a gs)
hence "a ∈ carrier G" by simp
with Cons ord_eq_1[OF this] show ?case by auto
qed simp
show ?thesis by (unfold r,
rule transp_successively_remove1[OF _ gs(4), unfolded transp_def],
auto)
qed simp
moreover have "card (set ?r) ≤ card gen" using gs(5) r
by (metis List.finite_set card_Diff1_le dual_order.trans)
moreover have "𝟭 ∉ set ?r" using gs(2) by auto
ultimately show ?thesis using that by blast
qed
corollary (in fin_gen_comm_group) invariant_factor_decomposition_dirprod:
obtains gs where
"set gs ⊆ carrier G" "distinct gs"
"DirProds (λg. G⦇carrier := generate G {g}⦈) (set gs) ≅ G"
"successively (dvd) (map ord gs)" "card (set gs) ≤ card gen"
"compl_fam (λg. generate G {g}) (set gs)" "𝟭 ∉ set gs"
proof -
from invariant_factor_decomposition_idirprod obtain gs where
gs: "set gs ⊆ carrier G" "distinct gs" "is_idirprod (carrier G) (λg. generate G {g}) (set gs)"
"successively (dvd) (map ord gs)" "card (set gs) ≤ card gen" "𝟭 ∉ set gs" by blast
with cong_DirProds_IDirProds[OF gs(3)] gs
have "DirProds (λg. G⦇carrier := generate G {g}⦈) (set gs) ≅ G" by blast
with gs that show ?thesis by auto
qed
corollary (in fin_gen_comm_group) invariant_factor_decomposition_dirprod_fam:
obtains Hs where
"⋀H. H ∈ set Hs ⟹ subgroup H G" "distinct Hs"
"DirProds (λH. G⦇carrier := H⦈) (set Hs) ≅ G" "successively (dvd) (map card Hs)"
"card (set Hs) ≤ card gen" "compl_fam id (set Hs)" "{𝟭} ∉ set Hs"
proof -
from invariant_factor_decomposition_dirprod obtain gs where
gs: "set gs ⊆ carrier G" "distinct gs"
"DirProds (λg. G⦇carrier := generate G {g}⦈) (set gs) ≅ G"
"successively (dvd) (map ord gs)" "card (set gs) ≤ card gen"
"compl_fam (λg. generate G {g}) (set gs)" "𝟭 ∉ set gs" by blast
let ?gen = "(λg. generate G {g})"
let ?Hs = "map (λg. ?gen g) gs"
have "subgroup H G" if "H ∈ set ?Hs" for H using that gs by (auto intro: generate_is_subgroup)
moreover have "distinct ?Hs"
using compl_fam_imp_generate_inj[OF gs(1)] gs distinct_map by blast
moreover have "DirProds (λH. G⦇carrier := H⦈) (set ?Hs) ≅ G"
proof -
have gg: "group (G⦇carrier := ?gen g⦈)" if "g ∈ set gs" for g
by (use gs that in ‹auto intro: subgroup.subgroup_is_group generate_is_subgroup›)
then interpret og: group "DirProds (λg. G⦇carrier := ?gen g⦈) (set gs)"
using DirProds_group_iff by blast
have "DirProds (λg. G⦇carrier := ?gen g⦈) (set gs) ≅ DirProds (λH. G⦇carrier := H⦈) (set ?Hs)"
proof (intro DirProds_iso[of ?gen])
show "bij_betw ?gen (set gs) (set ?Hs)"
using ‹distinct ?Hs› gs(2) compl_fam_imp_generate_inj[OF gs(1, 6)]
by (simp add: bij_betw_def)
show "G⦇carrier := ?gen g⦈ ≅ G⦇carrier := ?gen g⦈" if "g ∈ set gs" for g by simp
show "group (G⦇carrier := ?gen g⦈)" if "g ∈ set gs" for g using that by fact
show "Group.group (G⦇carrier := H⦈)" if "H ∈ set ?Hs" for H
by (use gs that in ‹auto intro: subgroup.subgroup_is_group generate_is_subgroup›)
qed
from group.iso_sym[OF og.is_group this] show ?thesis using gs iso_trans by blast
qed
moreover have "successively (dvd) (map card ?Hs)"
proof -
have "card (generate G {g}) = ord g" if "g ∈ set gs" for g
using generate_pow_card that gs(1) by auto
hence "map card ?Hs = map ord gs" by simp
thus ?thesis using gs(4) by argo
qed
moreover have "card (set ?Hs) ≤ card gen" using gs
by (metis ‹distinct ?Hs› distinct_card length_map)
moreover have "compl_fam id (set ?Hs)"
using compl_fam_cong[OF _ compl_fam_imp_generate_inj[OF gs(1, 6)], of id] using gs by auto
moreover have "{𝟭} ∉ set ?Hs" using generate_singleton_one gs by auto
ultimately show ?thesis using that by blast
qed
text ‹Here, the invariant factor decomposition in its classical form.›
corollary (in fin_gen_comm_group) invariant_factor_decomposition_Zn:
obtains ns where
"DirProds (λn. Z (ns!n)) {..<length ns} ≅ G" "successively (dvd) ns" "length ns ≤ card gen"
proof -
from invariant_factor_decomposition_dirprod obtain gs where
gs: "set gs ⊆ carrier G" "distinct gs"
"DirProds (λg. G⦇carrier := generate G {g}⦈) (set gs) ≅ G"
"successively (dvd) (map ord gs)" "card (set gs) ≤ card gen"
"compl_fam (λg. generate G {g}) (set gs)" "𝟭 ∉ set gs" by blast
let ?DP = "DirProds (λg. G⦇carrier := generate G {g}⦈) (set gs)"
have "∃ns. DirProds (λn. Z (ns!n)) {..<length ns} ≅ G
∧ successively (dvd) ns ∧ length ns ≤ card gen"
proof (cases gs, rule)
case Nil
from gs(3) Nil have co: "carrier ?DP = {𝟭⇘?DP⇙}" unfolding DirProds_def by auto
let ?ns = "[]"
have "DirProds (λn. Z ([] ! n)) {} ≅ ?DP"
proof(intro triv_iso DirProds_is_group)
show "carrier (DirProds (λn. Z ([] ! n)) {}) = {𝟭⇘DirProds (λn. Z ([] ! n)) {}⇙}"
using DirProds_empty by blast
qed (use co group_integer_mod_group Nil in auto)
from that[of ?ns] gs co iso_trans[OF this gs(3)]
show "DirProds (λn. Z (?ns ! n)) {..<length ?ns} ≅ G
∧ successively (dvd) ?ns ∧ length ?ns ≤ card gen"
unfolding lessThan_def by simp
next
case c: (Cons a list)
let ?l = "map ord gs"
from c have l: "length ?l > 0" by auto
have "DirProds (λn. Z (?l ! n)) {..<length ?l} ≅ G"
proof -
have "DirProds (λn. Z (?l ! n)) {..<length ?l} ≅ ?DP"
proof(intro DirProds_iso[where ?f = "λn. gs!n"])
show "bij_betw ((!) gs) {..<length ?l} (set gs)" using gs
by (simp add: bij_betw_nth)
show "Z (map ord gs ! i) ≅ G⦇carrier := generate G {gs ! i}⦈" if "i ∈ {..<length ?l}" for i
proof(rule group.iso_sym[OF subgroup.subgroup_is_group[OF generate_is_subgroup]
cyclic_group.Zn_iso[OF cyclic_groupI2]])
show "order (G⦇carrier := generate G {gs ! i}⦈) = map ord gs ! i"
unfolding order_def using that generate_pow_card[of "gs ! i"] gs(1) by force
qed (use gs(1) that in auto)
show "Group.group (Z (map ord gs ! i))" if "i ∈ {..<length (map ord gs)}" for i
using group_integer_mod_group by blast
show "Group.group (G⦇carrier := generate G {g}⦈)" if "g ∈ set gs" for g
using that gs(1) subgroup.subgroup_is_group[OF generate_is_subgroup] by auto
qed
from iso_trans[OF this gs(3)] show ?thesis .
qed
moreover have "length ?l ≤ card gen" using gs by (metis distinct_card length_map)
ultimately show ?thesis using gs c by fastforce
qed
thus ?thesis using that by blast
qed
text ‹As every ‹integer_mod_group› can be decomposed into a product of prime power groups,
we obtain (by using the fact that the direct product does not care about nestedness)
the primary decomposition.›
lemma Zn_iso_DirProds_prime_powers:
assumes "n ≠ 0"
shows "Z n ≅ DirProds (λp. Z (p ^ multiplicity p n)) (prime_factors n)" (is "Z n ≅ ?DP")
proof (cases "n = 1")
case True
show ?thesis by (intro triv_iso[OF group_integer_mod_group DirProds_is_group],
use DirProds_empty carrier_integer_mod_group True in auto)
next
case nno: False
interpret DP: group ?DP by (intro DirProds_is_group, use group_integer_mod_group in blast)
have "order ?DP = prod (order ∘ (λp. Z (p ^ multiplicity p n))) (prime_factors n)"
by (intro DirProds_order, blast)
also have "… = prod (λp. p ^ multiplicity p n) (prime_factors n)" using Zn_order by simp
also have n: "… = n" using prod_prime_factors[OF assms] by simp
finally have oDP: "order ?DP = n" .
then interpret DP: finite_group ?DP
by (unfold_locales, unfold order_def, metis assms card.infinite)
let ?f = "λp∈(prime_factors n). 1"
have fc: "?f ∈ carrier ?DP"
proof -
have p: "0 < multiplicity p n" if "p ∈ prime_factors n" for p
using prime_factors_multiplicity that by auto
have pk: "1 < p ^ k" if "Factorial_Ring.prime p" "0 < k" for p k::nat
using that one_less_power prime_gt_1_nat by blast
show ?thesis unfolding DirProds_def PiE_def
by(use carrier_integer_mod_group assms nno pk p in auto,
metis in_prime_factors_iff nat_int of_nat_power one_less_nat_eq)
qed
have of: "DP.ord ?f = n"
proof -
have "n dvd j" if j: "?f [^]⇘?DP⇙ j = 𝟭⇘?DP⇙" for j
proof (intro pairwise_coprime_dvd'[OF _ _ n[symmetric]])
show "finite (prime_factors n)" by simp
show "∀a∈#prime_factorization n. a ^ multiplicity a n dvd j"
proof
show "p ^ multiplicity p n dvd j" if "p ∈ prime_factors n" for p
proof -
from j have "(?f [^]⇘?DP⇙ j) p = 0"
using that unfolding DirProds_def one_integer_mod_group by auto
hence "?f p [^]⇘Z (p ^ multiplicity p n)⇙ j = 0" using comp_exp_nat[OF that] by metis
hence "group.ord (Z (p ^ multiplicity p n)) (?f p) dvd j" using comp_in_carr[OF fc that]
by (metis group.pow_eq_id group_integer_mod_group one_integer_mod_group)
moreover have "group.ord (Z (p ^ multiplicity p n)) (?f p) = p ^ multiplicity p n"
by (metis (no_types, lifting) Zn_neq1_cyclic_group Zn_order comp_in_carr
cyclic_group.ord_gen_is_group_order fc integer_mod_group_1
restrict_apply' that)
ultimately show ?thesis by simp
qed
qed
show "coprime (i ^ multiplicity i n) (j ^ multiplicity j n)"
if "i ∈# prime_factorization n" "j ∈# prime_factorization n" "i ≠ j" for i j
using that diff_prime_power_imp_coprime by blast
qed
thus ?thesis using fc DP.ord_dvd_group_order gcd_nat.asym oDP by force
qed
interpret DP: cyclic_group ?DP ?f by (intro DP.element_ord_generates_cyclic, use of oDP fc in auto)
show ?thesis using DP.iso_sym[OF DP.Zn_iso[OF oDP]] .
qed
lemma Zn_iso_DirProds_prime_powers':
assumes "n ≠ 0"
shows "Z n ≅ DirProds (λp. Z p) ((λp. p ^ multiplicity p n) ` (prime_factors n))" (is "Z n ≅ ?DP")
proof -
have cp: "(λp. Z (p ^ multiplicity p n)) = (λp. Z p) ∘ (λp. p ^ multiplicity p n)" by auto
have "DirProds (λp. Z (p ^ multiplicity p n)) (prime_factors n) ≅ ?DP"
proof(subst cp, intro DirProds_iso2)
show "inj_on (λp. p ^ multiplicity p n) (prime_factors n)"
by (intro inj_onI; simp add: prime_factors_multiplicity prime_power_inj'')
show "group (DirProds Z ((λp. p ^ multiplicity p n) ` prime_factors n))"
by (intro DirProds_is_group, use group_integer_mod_group in auto)
qed
with Zn_iso_DirProds_prime_powers[OF assms] show ?thesis using Group.iso_trans by blast
qed
corollary (in fin_gen_comm_group) primary_decomposition_Zn:
obtains ns where
"DirProds (λn. Z (ns!n)) {..<length ns} ≅ G"
"∀n∈set ns. n = 0 ∨ (∃p k. Factorial_Ring.prime p ∧ k > 0 ∧ n = p ^ k)"
proof -
from invariant_factor_decomposition_Zn obtain ms where
ms: "DirProds (λm. Z (ms!m)) {..<length ms} ≅ G" "successively (dvd) ms" "length ms ≤ card gen"
by blast
let ?I = "{..<length ms}"
let ?J = "λi. if ms!i = 0 then {0} else (λp. p ^ multiplicity p (ms!i)) ` (prime_factors (ms!i))"
let ?G = "λi. Z"
let ?f = "λi. DirProds (?G i) (?J i)"
have "DirProds (λm. Z (ms!m)) {..<length ms} ≅ DirProds ?f {..<length ms}"
proof (intro DirProds_iso[of id])
show "bij_betw id {..<length ms} {..<length ms}" by blast
show "Z (ms ! i) ≅ ?f (id i)" if "i ∈ {..<length ms}" for i
by (cases "ms!i = 0",
simp add: DirProds_one_cong_sym,
auto intro: Zn_iso_DirProds_prime_powers')
show "⋀i. i ∈ {..<length ms} ⟹ group (Z (ms ! i))" by auto
show "group (?f j)" if "j ∈ {..<length ms}" for j by (auto intro: DirProds_is_group)
qed
also have "… ≅ DirProds (λ(i,j). ?G i j) (Sigma ?I ?J)"
by(rule DirProds_Sigma)
finally have G1: "G ≅ DirProds (λ(i,j). ?G i j) (Sigma ?I ?J)" using ms(1)
by (metis (no_types, lifting) DirProds_is_group Group.iso_trans group.iso_sym group_integer_mod_group)
have "∃ps. set ps = Sigma ?I ?J ∧ distinct ps" by(intro finite_distinct_list, auto)
then obtain ps where ps: "set ps = Sigma ?I ?J" "distinct ps" by blast
define ns where ns: "ns = map snd ps"
have "DirProds (λn. Z (ns!n)) {..<length ns} ≅ DirProds (λ(i,j). ?G i j) (Sigma ?I ?J)"
proof -
obtain b::"nat ⇒ (nat × nat)"
where b: "∀i<length ns. ns!i = snd (b i)" "bij_betw b {..<length ns} (Sigma ?I ?J)"
using ns ps bij_betw_nth by fastforce
moreover have "Z (ns ! i) ≅ (case b i of (i, x) ⇒ Z x)" if "i ∈ {..<length ns}" for i
proof -
have "ns ! i = snd (b i)" using b that by blast
thus ?thesis by (simp add: case_prod_beta)
qed
ultimately show ?thesis by (auto intro: DirProds_iso)
qed
with G1 have "DirProds (λn. Z (ns!n)) {..<length ns} ≅ G" using Group.iso_trans iso_sym by blast
moreover have "n = 0 ∨ (∃p k. Factorial_Ring.prime p ∧ k > 0 ∧ n = p ^ k)" if "n∈set ns" for n
proof -
have "k = 0 ∨ (∃p∈prime_factors (ms!i). k = p ^ multiplicity p (ms!i))" if "k ∈ ?J i" for k i
by (cases "ms!i = 0", use that in auto)
with that ns ps show ?thesis
by (auto, metis (no_types, lifting) mem_Collect_eq neq0_conv prime_factors_multiplicity)
qed
ultimately show
"(⋀ns. ⟦DirProds (λn. Z (ns ! n)) {..<length ns} ≅ G;
∀n∈set ns. n = 0 ∨ (∃p k. Factorial_Ring.prime p ∧ k > 0 ∧ n = p ^ k)⟧ ⟹ thesis)
⟹ thesis" by blast
qed
text ‹As every finite group is also finitely generated, it follows that a finite group can be
decomposed in a product of finite cyclic groups.›
lemma (in finite_comm_group) cyclic_product:
obtains ns where "DirProds (λn. Z (ns!n)) {..<length ns} ≅ G" "∀n∈set ns. n≠0"
proof -
from primary_decomposition_Zn obtain ns where
ns: "DirProds (λn. Z (ns ! n)) {..<length ns} ≅ G"
"∀n∈set ns. n = 0 ∨ (∃p k. normalization_semidom_class.prime p ∧ 0 < k ∧ n = p ^ k)"
by blast
have "False" if "n ∈ {..<length ns}" "ns!n = 0" for n
proof -
from that have "order (DirProds (λn. Z (ns ! n)) {..<length ns}) = 0"
using DirProds_order[of "{..<length ns}" "λn. Z (ns!n)"] Zn_order by auto
with fin iso_same_card[OF ns(1)] show False unfolding order_def by auto
qed
hence "∀n∈set ns. n≠0"
by (metis in_set_conv_nth lessThan_iff)
with ns show ?thesis using that by blast
qed
no_notation integer_mod_group ("Z")
end