Quelle 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, opaque_lifting) 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 (force 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

quality100%

¤ Dauer der Verarbeitung: 0.5 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.