|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Free_Abelian_Groups.thy
Sprache: Isabelle
|
|
section\<open>Free Abelian Groups\<close>
theory Free_Abelian_Groups
imports
Product_Groups FiniteProduct "HOL-Cardinals.Cardinal_Arithmetic"
"HOL-Library.Countable_Set" "HOL-Library.Poly_Mapping" "HOL-Library.Equipollence"
begin
(*Move? But where?*)
lemma eqpoll_Fpow:
assumes "infinite A" shows "Fpow A \ A"
unfolding eqpoll_iff_card_of_ordIso
by (metis assms card_of_Fpow_infinite)
lemma infinite_iff_card_of_countable: "\countable B; infinite B\ \ infinite A \ ( |B| \o |A| )"
unfolding infinite_iff_countable_subset card_of_ordLeq countable_def
by (force intro: card_of_ordLeqI ordLeq_transitive)
lemma iso_imp_eqpoll_carrier: "G \ H \ carrier G \ carrier H"
by (auto simp: is_iso_def iso_def eqpoll_def)
subsection\<open>Generalised finite product\<close>
definition
gfinprod :: "[('b, 'm) monoid_scheme, 'a \ 'b, 'a set] \ 'b"
where "gfinprod G f A =
(if finite {x \<in> A. f x \<noteq> \<one>\<^bsub>G\<^esub>} then finprod G f {x \<in> A. f x \<noteq> \<one>\<^bsub>G\<^esub>} else \<one>\<^bsub>G\<^esub>)"
context comm_monoid begin
lemma gfinprod_closed [simp]:
"f \ A \ carrier G \ gfinprod G f A \ carrier G"
unfolding gfinprod_def
by (auto simp: image_subset_iff_funcset intro: finprod_closed)
lemma gfinprod_cong:
"\A = B; f \ B \ carrier G;
\<And>i. i \<in> B =simp=> f i = g i\<rbrakk> \<Longrightarrow> gfinprod G f A = gfinprod G g B"
unfolding gfinprod_def
by (auto simp: simp_implies_def cong: conj_cong intro: finprod_cong)
lemma gfinprod_eq_finprod [simp]: "\finite A; f \ A \ carrier G\ \ gfinprod G f A = finprod G f A"
by (auto simp: gfinprod_def intro: finprod_mono_neutral_cong_left)
lemma gfinprod_insert [simp]:
assumes "finite {x \ A. f x \ \\<^bsub>G\<^esub>}" "f \ A \ carrier G" "f i \ carrier G"
shows "gfinprod G f (insert i A) = (if i \ A then gfinprod G f A else f i \ gfinprod G f A)"
proof -
have f: "f \ {x \ A. f x \ \} \ carrier G"
using assms by (auto simp: image_subset_iff_funcset)
have "{x. x = i \ f x \ \ \ x \ A \ f x \ \} = (if f i = \ then {x \ A. f x \ \} else insert i {x \ A. f x \ \})"
by auto
then show ?thesis
using assms
unfolding gfinprod_def by (simp add: conj_disj_distribR insert_absorb f split: if_split_asm)
qed
lemma gfinprod_distrib:
assumes fin: "finite {x \ A. f x \ \\<^bsub>G\<^esub>}" "finite {x \ A. g x \ \\<^bsub>G\<^esub>}"
and "f \ A \ carrier G" "g \ A \ carrier G"
shows "gfinprod G (\i. f i \ g i) A = gfinprod G f A \ gfinprod G g A"
proof -
have "finite {x \ A. f x \ g x \ \}"
by (auto intro: finite_subset [OF _ finite_UnI [OF fin]])
then have "gfinprod G (\i. f i \ g i) A = gfinprod G (\i. f i \ g i) ({i \ A. f i \ \\<^bsub>G\<^esub>} \ {i \ A. g i \ \\<^bsub>G\<^esub>})"
unfolding gfinprod_def
using assms by (force intro: finprod_mono_neutral_cong)
also have "\ = gfinprod G f A \ gfinprod G g A"
proof -
have "finprod G f ({i \ A. f i \ \\<^bsub>G\<^esub>} \ {i \ A. g i \ \\<^bsub>G\<^esub>}) = gfinprod G f A"
"finprod G g ({i \ A. f i \ \\<^bsub>G\<^esub>} \ {i \ A. g i \ \\<^bsub>G\<^esub>}) = gfinprod G g A"
using assms by (auto simp: gfinprod_def intro: finprod_mono_neutral_cong_right)
moreover have "(\i. f i \ g i) \ {i \ A. f i \ \} \ {i \ A. g i \ \} \ carrier G"
using assms by (force simp: image_subset_iff_funcset)
ultimately show ?thesis
using assms
apply simp
apply (subst finprod_multf, auto)
done
qed
finally show ?thesis .
qed
lemma gfinprod_mono_neutral_cong_left:
assumes "A \ B"
and 1: "\i. i \ B - A \ h i = \"
and gh: "\x. x \ A \ g x = h x"
and h: "h \ B \ carrier G"
shows "gfinprod G g A = gfinprod G h B"
proof (cases "finite {x \ B. h x \ \}")
case True
then have "finite {x \ A. h x \ \}"
apply (rule rev_finite_subset)
using \<open>A \<subseteq> B\<close> by auto
with True assms show ?thesis
apply (simp add: gfinprod_def cong: conj_cong)
apply (auto intro!: finprod_mono_neutral_cong_left)
done
next
case False
have "{x \ B. h x \ \} \ {x \ A. h x \ \}"
using 1 by auto
with False have "infinite {x \ A. h x \ \}"
using infinite_super by blast
with False assms show ?thesis
by (simp add: gfinprod_def cong: conj_cong)
qed
lemma gfinprod_mono_neutral_cong_right:
assumes "A \ B" "\i. i \ B - A \ g i = \" "\x. x \ A \ g x = h x" "g \ B \ carrier G"
shows "gfinprod G g B = gfinprod G h A"
using assms by (auto intro!: gfinprod_mono_neutral_cong_left [symmetric])
lemma gfinprod_mono_neutral_cong:
assumes [simp]: "finite B" "finite A"
and *: "\i. i \ B - A \ h i = \" "\i. i \ A - B \ g i = \"
and gh: "\x. x \ A \ B \ g x = h x"
and g: "g \ A \ carrier G"
and h: "h \ B \ carrier G"
shows "gfinprod G g A = gfinprod G h B"
proof-
have "gfinprod G g A = gfinprod G g (A \ B)"
by (rule gfinprod_mono_neutral_cong_right) (use assms in auto)
also have "\ = gfinprod G h (A \ B)"
by (rule gfinprod_cong) (use assms in auto)
also have "\ = gfinprod G h B"
by (rule gfinprod_mono_neutral_cong_left) (use assms in auto)
finally show ?thesis .
qed
end
lemma (in comm_group) hom_group_sum:
assumes hom: "\i. i \ I \ f i \ hom (A i) G" and grp: "\i. i \ I \ group (A i)"
shows "(\x. gfinprod G (\i. (f i) (x i)) I) \ hom (sum_group I A) G"
unfolding hom_def
proof (intro CollectI conjI ballI)
show "(\x. gfinprod G (\i. f i (x i)) I) \ carrier (sum_group I A) \ carrier G"
using assms
by (force simp: hom_def carrier_sum_group intro: gfinprod_closed simp flip: image_subset_iff_funcset)
next
fix x y
assume x: "x \ carrier (sum_group I A)" and y: "y \ carrier (sum_group I A)"
then have finx: "finite {i \ I. x i \ \\<^bsub>A i\<^esub>}" and finy: "finite {i \ I. y i \ \\<^bsub>A i\<^esub>}"
using assms by (auto simp: carrier_sum_group)
have finfx: "finite {i \ I. f i (x i) \ \}"
using assms by (auto simp: is_group hom_one [OF hom] intro: finite_subset [OF _ finx])
have finfy: "finite {i \ I. f i (y i) \ \}"
using assms by (auto simp: is_group hom_one [OF hom] intro: finite_subset [OF _ finy])
have carr: "f i (x i) \ carrier G" "f i (y i) \ carrier G" if "i \ I" for i
using hom_carrier [OF hom] that x y assms
by (fastforce simp add: carrier_sum_group)+
have lam: "(\i. f i ( x i \\<^bsub>A i\<^esub> y i)) \ I \ carrier G"
using x y assms by (auto simp: hom_def carrier_sum_group PiE_def Pi_def)
have lam': "(\i. f i (if i \ I then x i \\<^bsub>A i\<^esub> y i else undefined)) \ I \ carrier G"
by (simp add: lam Pi_cong)
with lam x y assms
show "gfinprod G (\i. f i ((x \\<^bsub>sum_group I A\<^esub> y) i)) I
= gfinprod G (\<lambda>i. f i (x i)) I \<otimes> gfinprod G (\<lambda>i. f i (y i)) I"
by (simp add: carrier_sum_group PiE_def Pi_def hom_mult [OF hom]
gfinprod_distrib finfx finfy carr cong: gfinprod_cong)
qed
subsection\<open>Free Abelian groups on a set, using the "frag" type constructor. \<close>
definition free_Abelian_group :: "'a set \ ('a \\<^sub>0 int) monoid"
where "free_Abelian_group S = \carrier = {c. Poly_Mapping.keys c \ S}, monoid.mult = (+), one = 0\"
lemma group_free_Abelian_group [simp]: "group (free_Abelian_group S)"
proof -
have "\x. Poly_Mapping.keys x \ S \ x \ Units (free_Abelian_group S)"
unfolding free_Abelian_group_def Units_def
by clarsimp (metis eq_neg_iff_add_eq_0 neg_eq_iff_add_eq_0 keys_minus)
then show ?thesis
unfolding free_Abelian_group_def
by unfold_locales (auto simp: dest: subsetD [OF keys_add])
qed
lemma carrier_free_Abelian_group_iff [simp]:
shows "x \ carrier (free_Abelian_group S) \ Poly_Mapping.keys x \ S"
by (auto simp: free_Abelian_group_def)
lemma one_free_Abelian_group [simp]: "\\<^bsub>free_Abelian_group S\<^esub> = 0"
by (auto simp: free_Abelian_group_def)
lemma mult_free_Abelian_group [simp]: "x \\<^bsub>free_Abelian_group S\<^esub> y = x + y"
by (auto simp: free_Abelian_group_def)
lemma inv_free_Abelian_group [simp]: "Poly_Mapping.keys x \ S \ inv\<^bsub>free_Abelian_group S\<^esub> x = -x"
by (rule group.inv_equality [OF group_free_Abelian_group]) auto
lemma abelian_free_Abelian_group: "comm_group(free_Abelian_group S)"
apply (rule group.group_comm_groupI [OF group_free_Abelian_group])
by (simp add: free_Abelian_group_def)
lemma pow_free_Abelian_group [simp]:
fixes n::nat
shows "Group.pow (free_Abelian_group S) x n = frag_cmul (int n) x"
by (induction n) (auto simp: nat_pow_def free_Abelian_group_def frag_cmul_distrib)
lemma int_pow_free_Abelian_group [simp]:
fixes n::int
assumes "Poly_Mapping.keys x \ S"
shows "Group.pow (free_Abelian_group S) x n = frag_cmul n x"
proof (induction n)
case (nonneg n)
then show ?case
by (simp add: int_pow_int)
next
case (neg n)
have "x [^]\<^bsub>free_Abelian_group S\<^esub> - int (Suc n)
= inv\<^bsub>free_Abelian_group S\<^esub> (x [^]\<^bsub>free_Abelian_group S\<^esub> int (Suc n))"
by (rule group.int_pow_neg [OF group_free_Abelian_group]) (use assms in \<open>simp add: free_Abelian_group_def\<close>)
also have "\ = frag_cmul (- int (Suc n)) x"
by (metis assms inv_free_Abelian_group pow_free_Abelian_group int_pow_int minus_frag_cmul
order_trans keys_cmul)
finally show ?case .
qed
lemma frag_of_in_free_Abelian_group [simp]:
"frag_of x \ carrier(free_Abelian_group S) \ x \ S"
by simp
lemma free_Abelian_group_induct:
assumes major: "Poly_Mapping.keys x \ S"
and minor: "P(0)"
"\x y. \Poly_Mapping.keys x \ S; Poly_Mapping.keys y \ S; P x; P y\ \ P(x-y)"
"\a. a \ S \ P(frag_of a)"
shows "P x"
proof -
have "Poly_Mapping.keys x \ S \ P x"
using major
proof (induction x rule: frag_induction)
case (diff a b)
then show ?case
by (meson Un_least minor(2) order.trans keys_diff)
qed (auto intro: minor)
then show ?thesis ..
qed
lemma sum_closed_free_Abelian_group:
"(\i. i \ I \ x i \ carrier (free_Abelian_group S)) \ sum x I \ carrier (free_Abelian_group S)"
apply (induction I rule: infinite_finite_induct, auto)
by (metis (no_types, hide_lams) UnE subsetCE keys_add)
lemma (in comm_group) free_Abelian_group_universal:
fixes f :: "'c \ 'a"
assumes "f ` S \ carrier G"
obtains h where "h \ hom (free_Abelian_group S) G" "\x. x \ S \ h(frag_of x) = f x"
proof
have fin: "Poly_Mapping.keys u \ S \ finite {x \ S. f x [^] poly_mapping.lookup u x \ \}" for u :: "'c \\<^sub>0 int"
apply (rule finite_subset [OF _ finite_keys [of u]])
unfolding keys.rep_eq by force
define h :: "('c \\<^sub>0 int) \ 'a"
where "h \ \x. gfinprod G (\a. f a [^] poly_mapping.lookup x a) S"
show "h \ hom (free_Abelian_group S) G"
proof (rule homI)
fix x y
assume xy: "x \ carrier (free_Abelian_group S)" "y \ carrier (free_Abelian_group S)"
then show "h (x \\<^bsub>free_Abelian_group S\<^esub> y) = h x \ h y"
using assms unfolding h_def free_Abelian_group_def
by (simp add: fin gfinprod_distrib image_subset_iff Poly_Mapping.lookup_add int_pow_mult cong: gfinprod_cong)
qed (use assms in \<open>force simp: free_Abelian_group_def h_def intro: gfinprod_closed\<close>)
show "h(frag_of x) = f x" if "x \ S" for x
proof -
have fin: "(\a. f x [^] (1::int)) \ {x} \ carrier G" "f x [^] (1::int) \ carrier G"
using assms that by force+
show ?thesis
by (cases " f x [^] (1::int) = \") (use assms that in \auto simp: h_def gfinprod_def finprod_singleton\)
qed
qed
lemma eqpoll_free_Abelian_group_infinite:
assumes "infinite A" shows "carrier(free_Abelian_group A) \ A"
proof (rule lepoll_antisym)
have "carrier (free_Abelian_group A) \ {f::'a\int. f ` A \ UNIV \ {x. f x \ 0} \ A \ finite {x. f x \ 0}}"
unfolding lepoll_def
by (rule_tac x="Poly_Mapping.lookup" in exI) (auto simp: poly_mapping_eqI lookup_not_eq_zero_eq_in_keys inj_onI)
also have "\ \ Fpow (A \ (UNIV::int set))"
by (rule lepoll_restricted_funspace)
also have "\ \ A \ (UNIV::int set)"
proof (rule eqpoll_Fpow)
show "infinite (A \ (UNIV::int set))"
using assms finite_cartesian_productD1 by fastforce
qed
also have "\ \ A"
unfolding eqpoll_iff_card_of_ordIso
proof -
have "|A \ (UNIV::int set)| <=o |A|"
by (simp add: assms card_of_Times_ordLeq_infinite flip: infinite_iff_card_of_countable)
moreover have "|A| \o |A \ (UNIV::int set)|"
by simp
ultimately have "|A| *c |(UNIV::int set)| =o |A|"
by (simp add: cprod_def ordIso_iff_ordLeq)
then show "|A \ (UNIV::int set)| =o |A|"
by (metis Times_cprod ordIso_transitive)
qed
finally show "carrier (free_Abelian_group A) \ A" .
have "inj_on frag_of A"
by (simp add: frag_of_eq inj_on_def)
moreover have "frag_of ` A \ carrier (free_Abelian_group A)"
by (simp add: image_subsetI)
ultimately show "A \ carrier (free_Abelian_group A)"
by (force simp: lepoll_def)
qed
proposition (in comm_group) eqpoll_homomorphisms_from_free_Abelian_group:
"{f. f \ extensional (carrier(free_Abelian_group S)) \ f \ hom (free_Abelian_group S) G}
\<approx> (S \<rightarrow>\<^sub>E carrier G)" (is "?lhs \<approx> ?rhs")
unfolding eqpoll_def bij_betw_def
proof (intro exI conjI)
let ?f = "\f. restrict (f \ frag_of) S"
show "inj_on ?f ?lhs"
proof (clarsimp simp: inj_on_def)
fix g h
assume
g: "g \ extensional (carrier (free_Abelian_group S))" "g \ hom (free_Abelian_group S) G"
and h: "h \ extensional (carrier (free_Abelian_group S))" "h \ hom (free_Abelian_group S) G"
and eq: "restrict (g \ frag_of) S = restrict (h \ frag_of) S"
have 0: "0 \ carrier (free_Abelian_group S)"
by simp
interpret hom_g: group_hom "free_Abelian_group S" G g
using g by (auto simp: group_hom_def group_hom_axioms_def is_group)
interpret hom_h: group_hom "free_Abelian_group S" G h
using h by (auto simp: group_hom_def group_hom_axioms_def is_group)
have "Poly_Mapping.keys c \ S \ Poly_Mapping.keys c \ S \ g c = h c" for c
proof (induction c rule: frag_induction)
case zero
show ?case
using hom_g.hom_one hom_h.hom_one by auto
next
case (one x)
then show ?case
using eq by (simp add: fun_eq_iff) (metis comp_def)
next
case (diff a b)
then show ?case
using hom_g.hom_mult hom_h.hom_mult hom_g.hom_inv hom_h.hom_inv
apply (auto simp: dest: subsetD [OF keys_diff])
by (metis keys_minus uminus_add_conv_diff)
qed
then show "g = h"
by (meson g h carrier_free_Abelian_group_iff extensionalityI)
qed
have "f \ (\f. restrict (f \ frag_of) S) `
{f \<in> extensional (carrier (free_Abelian_group S)). f \<in> hom (free_Abelian_group S) G}"
if f: "f \ S \\<^sub>E carrier G"
for f :: "'c \ 'a"
proof -
obtain h where h: "h \ hom (free_Abelian_group S) G" "\x. x \ S \ h(frag_of x) = f x"
proof (rule free_Abelian_group_universal)
show "f ` S \ carrier G"
using f by blast
qed auto
let ?h = "restrict h (carrier (free_Abelian_group S))"
show ?thesis
proof
show "f = restrict (?h \ frag_of) S"
using f by (force simp: h)
show "?h \ {f \ extensional (carrier (free_Abelian_group S)). f \ hom (free_Abelian_group S) G}"
using h by (auto simp: hom_def dest!: subsetD [OF keys_add])
qed
qed
then show "?f ` ?lhs = S \\<^sub>E carrier G"
by (auto simp: hom_def Ball_def Pi_def)
qed
lemma hom_frag_minus:
assumes "h \ hom (free_Abelian_group S) (free_Abelian_group T)" "Poly_Mapping.keys a \ S"
shows "h (-a) = - (h a)"
proof -
have "Poly_Mapping.keys (h a) \ T"
by (meson assms carrier_free_Abelian_group_iff hom_in_carrier)
then show ?thesis
by (metis (no_types) assms carrier_free_Abelian_group_iff group_free_Abelian_group group_hom.hom_inv group_hom_axioms_def group_hom_def inv_free_Abelian_group)
qed
lemma hom_frag_add:
assumes "h \ hom (free_Abelian_group S) (free_Abelian_group T)" "Poly_Mapping.keys a \ S" "Poly_Mapping.keys b \ S"
shows "h (a+b) = h a + h b"
proof -
have "Poly_Mapping.keys (h a) \ T"
by (meson assms carrier_free_Abelian_group_iff hom_in_carrier)
moreover
have "Poly_Mapping.keys (h b) \ T"
by (meson assms carrier_free_Abelian_group_iff hom_in_carrier)
ultimately show ?thesis
using assms hom_mult by fastforce
qed
lemma hom_frag_diff:
assumes "h \ hom (free_Abelian_group S) (free_Abelian_group T)" "Poly_Mapping.keys a \ S" "Poly_Mapping.keys b \ S"
shows "h (a-b) = h a - h b"
by (metis (no_types, lifting) assms diff_conv_add_uminus hom_frag_add hom_frag_minus keys_minus)
proposition isomorphic_free_Abelian_groups:
"free_Abelian_group S \ free_Abelian_group T \ S \ T" (is "(?FS \ ?FT) = ?rhs")
proof
interpret S: group "?FS"
by simp
interpret T: group "?FT"
by simp
interpret G2: comm_group "integer_mod_group 2"
by (rule abelian_integer_mod_group)
let ?Two = "{0..<2::int}"
have [simp]: "\ ?Two \ {a}" for a
by (simp add: subset_iff) presburger
assume L: "?FS \ ?FT"
let ?HS = "{h \ extensional (carrier ?FS). h \ hom ?FS (integer_mod_group 2)}"
let ?HT = "{h \ extensional (carrier ?FT). h \ hom ?FT (integer_mod_group 2)}"
have "S \\<^sub>E ?Two \ ?HS"
apply (rule eqpoll_sym)
using G2.eqpoll_homomorphisms_from_free_Abelian_group by (simp add: carrier_integer_mod_group)
also have "\ \ ?HT"
proof -
obtain f g where "group_isomorphisms ?FS ?FT f g"
using L S.iso_iff_group_isomorphisms by (force simp: is_iso_def)
then have f: "f \ hom ?FS ?FT"
and g: "g \ hom ?FT ?FS"
and gf: "\x \ carrier ?FS. g(f x) = x"
and fg: "\y \ carrier ?FT. f(g y) = y"
by (auto simp: group_isomorphisms_def)
let ?f = "\h. restrict (h \ g) (carrier ?FT)"
let ?g = "\h. restrict (h \ f) (carrier ?FS)"
show ?thesis
proof (rule lepoll_antisym)
show "?HS \ ?HT"
unfolding lepoll_def
proof (intro exI conjI)
show "inj_on ?f ?HS"
apply (rule inj_on_inverseI [where g = ?g])
using hom_in_carrier [OF f]
by (auto simp: gf fun_eq_iff carrier_integer_mod_group Ball_def Pi_def extensional_def)
show "?f ` ?HS \ ?HT"
proof clarsimp
fix h
assume h: "h \ hom ?FS (integer_mod_group 2)"
have "h \ g \ hom ?FT (integer_mod_group 2)"
by (rule hom_compose [OF g h])
moreover have "restrict (h \ g) (carrier ?FT) x = (h \ g) x" if "x \ carrier ?FT" for x
using g that by (simp add: hom_def)
ultimately show "restrict (h \ g) (carrier ?FT) \ hom ?FT (integer_mod_group 2)"
using T.hom_restrict by fastforce
qed
qed
next
show "?HT \ ?HS"
unfolding lepoll_def
proof (intro exI conjI)
show "inj_on ?g ?HT"
apply (rule inj_on_inverseI [where g = ?f])
using hom_in_carrier [OF g]
by (auto simp: fg fun_eq_iff carrier_integer_mod_group Ball_def Pi_def extensional_def)
show "?g ` ?HT \ ?HS"
proof clarsimp
fix k
assume k: "k \ hom ?FT (integer_mod_group 2)"
have "k \ f \ hom ?FS (integer_mod_group 2)"
by (rule hom_compose [OF f k])
moreover have "restrict (k \ f) (carrier ?FS) x = (k \ f) x" if "x \ carrier ?FS" for x
using f that by (simp add: hom_def)
ultimately show "restrict (k \ f) (carrier ?FS) \ hom ?FS (integer_mod_group 2)"
using S.hom_restrict by fastforce
qed
qed
qed
qed
also have "\ \ T \\<^sub>E ?Two"
using G2.eqpoll_homomorphisms_from_free_Abelian_group by (simp add: carrier_integer_mod_group)
finally have *: "S \\<^sub>E ?Two \ T \\<^sub>E ?Two" .
then have "finite (S \\<^sub>E ?Two) \ finite (T \\<^sub>E ?Two)"
by (rule eqpoll_finite_iff)
then have "finite S \ finite T"
by (auto simp: finite_funcset_iff)
then consider "finite S" "finite T" | "~ finite S" "~ finite T"
by blast
then show ?rhs
proof cases
case 1
with * have "2 ^ card S = (2::nat) ^ card T"
by (simp add: card_PiE finite_PiE eqpoll_iff_card)
then have "card S = card T"
by auto
then show ?thesis
using eqpoll_iff_card 1 by blast
next
case 2
have "carrier (free_Abelian_group S) \ carrier (free_Abelian_group T)"
using L by (simp add: iso_imp_eqpoll_carrier)
then show ?thesis
using 2 eqpoll_free_Abelian_group_infinite eqpoll_sym eqpoll_trans by metis
qed
next
assume ?rhs
then obtain f g where f: "\x. x \ S \ f x \ T \ g(f x) = x"
and g: "\y. y \ T \ g y \ S \ f(g y) = y"
using eqpoll_iff_bijections by metis
interpret S: comm_group "?FS"
by (simp add: abelian_free_Abelian_group)
interpret T: comm_group "?FT"
by (simp add: abelian_free_Abelian_group)
have "(frag_of \ f) ` S \ carrier (free_Abelian_group T)"
using f by auto
then obtain h where h: "h \ hom (free_Abelian_group S) (free_Abelian_group T)"
and h_frag: "\x. x \ S \ h (frag_of x) = (frag_of \ f) x"
using T.free_Abelian_group_universal [of "frag_of \ f" S] by blast
interpret hhom: group_hom "free_Abelian_group S" "free_Abelian_group T" h
by (simp add: h group_hom_axioms_def group_hom_def)
have "(frag_of \ g) ` T \ carrier (free_Abelian_group S)"
using g by auto
then obtain k where k: "k \ hom (free_Abelian_group T) (free_Abelian_group S)"
and k_frag: "\x. x \ T \ k (frag_of x) = (frag_of \ g) x"
using S.free_Abelian_group_universal [of "frag_of \ g" T] by blast
interpret khom: group_hom "free_Abelian_group T" "free_Abelian_group S" k
by (simp add: k group_hom_axioms_def group_hom_def)
have kh: "Poly_Mapping.keys x \ S \ Poly_Mapping.keys x \ S \ k (h x) = x" for x
proof (induction rule: frag_induction)
case zero
then show ?case
apply auto
by (metis group_free_Abelian_group h hom_one k one_free_Abelian_group)
next
case (one x)
then show ?case
by (auto simp: h_frag k_frag f)
next
case (diff a b)
with keys_diff have "Poly_Mapping.keys (a - b) \ S"
by (metis Un_least order_trans)
with diff hhom.hom_closed show ?case
by (simp add: hom_frag_diff [OF h] hom_frag_diff [OF k])
qed
have hk: "Poly_Mapping.keys y \ T \ Poly_Mapping.keys y \ T \ h (k y) = y" for y
proof (induction rule: frag_induction)
case zero
then show ?case
apply auto
by (metis group_free_Abelian_group h hom_one k one_free_Abelian_group)
next
case (one y)
then show ?case
by (auto simp: h_frag k_frag g)
next
case (diff a b)
with keys_diff have "Poly_Mapping.keys (a - b) \ T"
by (metis Un_least order_trans)
with diff khom.hom_closed show ?case
by (simp add: hom_frag_diff [OF h] hom_frag_diff [OF k])
qed
have "h \ iso ?FS ?FT"
unfolding iso_def bij_betw_iff_bijections mem_Collect_eq
proof (intro conjI exI ballI h)
fix x
assume x: "x \ carrier (free_Abelian_group S)"
show "h x \ carrier (free_Abelian_group T)"
by (meson x h hom_in_carrier)
show "k (h x) = x"
using x by (simp add: kh)
next
fix y
assume y: "y \ carrier (free_Abelian_group T)"
show "k y \ carrier (free_Abelian_group S)"
by (meson y k hom_in_carrier)
show "h (k y) = y"
using y by (simp add: hk)
qed
then show "?FS \ ?FT"
by (auto simp: is_iso_def)
qed
lemma isomorphic_group_integer_free_Abelian_group_singleton:
"integer_group \ free_Abelian_group {x}"
proof -
have "(\n. frag_cmul n (frag_of x)) \ iso integer_group (free_Abelian_group {x})"
proof (rule isoI [OF homI])
show "bij_betw (\n. frag_cmul n (frag_of x)) (carrier integer_group) (carrier (free_Abelian_group {x}))"
apply (rule bij_betwI [where g = "\y. Poly_Mapping.lookup y x"])
by (auto simp: integer_group_def in_keys_iff intro!: poly_mapping_eqI)
qed (auto simp: frag_cmul_distrib)
then show ?thesis
unfolding is_iso_def
by blast
qed
lemma group_hom_free_Abelian_groups_id:
"id \ hom (free_Abelian_group S) (free_Abelian_group T) \ S \ T"
proof -
have "x \ T" if ST: "\c:: 'a \\<^sub>0 int. Poly_Mapping.keys c \ S \ Poly_Mapping.keys c \ T" and "x \ S" for x
using ST [of "frag_of x"] \<open>x \<in> S\<close> by simp
then show ?thesis
by (auto simp: hom_def free_Abelian_group_def Pi_def)
qed
proposition iso_free_Abelian_group_sum:
assumes "pairwise (\i j. disjnt (S i) (S j)) I"
shows "(\f. sum' f I) \ iso (sum_group I (\i. free_Abelian_group(S i))) (free_Abelian_group (\(S ` I)))"
(is "?h \ iso ?G ?H")
proof (rule isoI)
show hom: "?h \ hom ?G ?H"
proof (rule homI)
show "?h c \ carrier ?H" if "c \ carrier ?G" for c
using that
apply (simp add: sum.G_def carrier_sum_group)
apply (rule order_trans [OF keys_sum])
apply (auto simp: free_Abelian_group_def)
done
show "?h (x \\<^bsub>?G\<^esub> y) = ?h x \\<^bsub>?H\<^esub> ?h y"
if "x \ carrier ?G" "y \ carrier ?G" for x y
using that by (simp add: sum.finite_Collect_op carrier_sum_group sum.distrib')
qed
interpret GH: group_hom "?G" "?H" "?h"
using hom by (simp add: group_hom_def group_hom_axioms_def)
show "bij_betw ?h (carrier ?G) (carrier ?H)"
unfolding bij_betw_def
proof (intro conjI subset_antisym)
show "?h ` carrier ?G \ carrier ?H"
apply (clarsimp simp: sum.G_def carrier_sum_group simp del: carrier_free_Abelian_group_iff)
by (force simp: PiE_def Pi_iff intro!: sum_closed_free_Abelian_group)
have *: "poly_mapping.lookup (Abs_poly_mapping (\j. if j \ S i then poly_mapping.lookup x j else 0)) k
= (if k \<in> S i then poly_mapping.lookup x k else 0)" if "i \<in> I" for i k and x :: "'b \<Rightarrow>\<^sub>0 int"
using that by (auto simp: conj_commute cong: conj_cong)
have eq: "Abs_poly_mapping (\j. if j \ S i then poly_mapping.lookup x j else 0) = 0
\<longleftrightarrow> (\<forall>c \<in> S i. poly_mapping.lookup x c = 0)" if "i \<in> I" for i and x :: "'b \<Rightarrow>\<^sub>0 int"
apply (auto simp: poly_mapping_eq_iff fun_eq_iff)
apply (simp add: * Abs_poly_mapping_inverse conj_commute cong: conj_cong)
apply (force dest!: spec split: if_split_asm)
done
have "x \ ?h ` {x \ \\<^sub>E i\I. {c. Poly_Mapping.keys c \ S i}. finite {i \ I. x i \ 0}}"
if x: "Poly_Mapping.keys x \ \ (S ` I)" for x :: "'b \\<^sub>0 int"
proof -
let ?f = "(\i c. if c \ S i then Poly_Mapping.lookup x c else 0)"
define J where "J \ {i \ I. \c\S i. c \ Poly_Mapping.keys x}"
have "J \ (\c. THE i. i \ I \ c \ S i) ` Poly_Mapping.keys x"
proof (clarsimp simp: J_def)
show "i \ (\c. THE i. i \ I \ c \ S i) ` Poly_Mapping.keys x"
if "i \ I" "c \ S i" "c \ Poly_Mapping.keys x" for i c
proof
show "i = (THE i. i \ I \ c \ S i)"
using assms that by (auto simp: pairwise_def disjnt_def intro: the_equality [symmetric])
qed (simp add: that)
qed
then have fin: "finite J"
using finite_subset finite_keys by blast
have [simp]: "Poly_Mapping.keys (Abs_poly_mapping (?f i)) = {k. ?f i k \ 0}" if "i \ I" for i
by (simp add: eq_onp_def keys.abs_eq conj_commute cong: conj_cong)
have [simp]: "Poly_Mapping.lookup (Abs_poly_mapping (?f i)) c = ?f i c" if "i \ I" for i c
by (auto simp: Abs_poly_mapping_inverse conj_commute cong: conj_cong)
show ?thesis
proof
have "poly_mapping.lookup x c = poly_mapping.lookup (?h (\i\I. Abs_poly_mapping (?f i))) c"
for c
proof (cases "c \ Poly_Mapping.keys x")
case True
then obtain i where "i \ I" "c \ S i" "?f i c \ 0"
using x by (auto simp: in_keys_iff)
then have 1: "poly_mapping.lookup (sum' (\j. Abs_poly_mapping (?f j)) (I - {i})) c = 0"
using assms
apply (simp add: sum.G_def Poly_Mapping.lookup_sum pairwise_def disjnt_def)
apply (force simp: eq split: if_split_asm intro!: comm_monoid_add_class.sum.neutral)
done
have 2: "poly_mapping.lookup x c = poly_mapping.lookup (Abs_poly_mapping (?f i)) c"
by (auto simp: \<open>c \<in> S i\<close> Abs_poly_mapping_inverse conj_commute cong: conj_cong)
have "finite {i \ I. Abs_poly_mapping (?f i) \ 0}"
by (rule finite_subset [OF _ fin]) (use \<open>i \<in> I\<close> J_def eq in \<open>auto simp: in_keys_iff\<close>)
with \<open>i \<in> I\<close> have "?h (\<lambda>j\<in>I. Abs_poly_mapping (?f j)) = Abs_poly_mapping (?f i) + sum' (\<lambda>j. Abs_poly_mapping (?f j)) (I - {i})"
by (simp add: sum_diff1')
then show ?thesis
by (simp add: 1 2 Poly_Mapping.lookup_add)
next
case False
then have "poly_mapping.lookup x c = 0"
using keys.rep_eq by force
then show ?thesis
unfolding sum.G_def by (simp add: lookup_sum * comm_monoid_add_class.sum.neutral)
qed
then show "x = ?h (\i\I. Abs_poly_mapping (?f i))"
by (rule poly_mapping_eqI)
have "(\i. Abs_poly_mapping (?f i)) \ (\ i\I. {c. Poly_Mapping.keys c \ S i})"
by (auto simp: PiE_def Pi_def in_keys_iff)
then show "(\i\I. Abs_poly_mapping (?f i))
\<in> {x \<in> \<Pi>\<^sub>E i\<in>I. {c. Poly_Mapping.keys c \<subseteq> S i}. finite {i \<in> I. x i \<noteq> 0}}"
using fin unfolding J_def by (simp add: eq in_keys_iff cong: conj_cong)
qed
qed
then show "carrier ?H \ ?h ` carrier ?G"
by (simp add: carrier_sum_group) (auto simp: free_Abelian_group_def)
show "inj_on ?h (carrier (sum_group I (\i. free_Abelian_group (S i))))"
unfolding GH.inj_on_one_iff
proof clarify
fix x
assume "x \ carrier ?G" "?h x = \\<^bsub>?H\<^esub>"
then have eq0: "sum' x I = 0"
and xs: "\i. i \ I \ Poly_Mapping.keys (x i) \ S i" and xext: "x \ extensional I"
and fin: "finite {i \ I. x i \ 0}"
by (simp_all add: carrier_sum_group PiE_def Pi_def)
have "x i = 0" if "i \ I" for i
proof -
have "sum' x (insert i (I - {i})) = 0"
using eq0 that by (simp add: insert_absorb)
moreover have "Poly_Mapping.keys (sum' x (I - {i})) = {}"
proof -
have "x i = - sum' x (I - {i})"
by (metis (mono_tags, lifting) diff_zero eq0 fin sum_diff1' minus_diff_eq that)
then have "Poly_Mapping.keys (x i) = Poly_Mapping.keys (sum' x (I - {i}))"
by simp
then have "Poly_Mapping.keys (sum' x (I - {i})) \ S i"
using that xs by metis
moreover
have "Poly_Mapping.keys (sum' x (I - {i})) \ (\j \ I - {i}. S j)"
proof -
have "Poly_Mapping.keys (sum' x (I - {i})) \ (\i\{j \ I. j \ i \ x j \ 0}. Poly_Mapping.keys (x i))"
using keys_sum [of x "{j \ I. j \ i \ x j \ 0}"] by (simp add: sum.G_def)
also have "\ \ \ (S ` (I - {i}))"
using xs by force
finally show ?thesis .
qed
moreover have "A = {}" if "A \ S i" "A \ \ (S ` (I - {i}))" for A
using assms that \<open>i \<in> I\<close>
by (force simp: pairwise_def disjnt_def image_def subset_iff)
ultimately show ?thesis
by metis
qed
then have [simp]: "sum' x (I - {i}) = 0"
by (auto simp: sum.G_def)
have "sum' x (insert i (I - {i})) = x i"
by (subst sum.insert' [OF finite_subset [OF _ fin]]) auto
ultimately show ?thesis
by metis
qed
with xext [unfolded extensional_def]
show "x = \\<^bsub>sum_group I (\i. free_Abelian_group (S i))\<^esub>"
by (force simp: free_Abelian_group_def)
qed
qed
qed
lemma isomorphic_free_Abelian_group_Union:
"pairwise disjnt I \ free_Abelian_group(\ I) \ sum_group I free_Abelian_group"
using iso_free_Abelian_group_sum [of "\X. X" I]
by (metis SUP_identity_eq empty_iff group.iso_sym group_free_Abelian_group is_iso_def sum_group)
lemma isomorphic_sum_integer_group:
"sum_group I (\i. integer_group) \ free_Abelian_group I"
proof -
have "sum_group I (\i. integer_group) \ sum_group I (\i. free_Abelian_group {i})"
by (rule iso_sum_groupI) (auto simp: isomorphic_group_integer_free_Abelian_group_singleton)
also have "\ \ free_Abelian_group I"
using iso_free_Abelian_group_sum [of "\x. {x}" I] by (auto simp: is_iso_def)
finally show ?thesis .
qed
end
¤ Dauer der Verarbeitung: 0.28 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
|
|
|
|
|
