Theory HOL-Algebra.Free_Abelian_Groups

section‹Free Abelian Groups›

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‹Generalised finite product›

definition
  gfinprod :: "[('b, 'm) monoid_scheme, 'a  'b, 'a set]  'b"
  where "gfinprod G f A =
   (if finite {x  A. f x  𝟭G} then finprod G f {x  A. f x  𝟭G} else 𝟭G)"

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;
    i. i  B =simp=> f i = g i  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  𝟭G}" "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  𝟭G}" "finite {x  A. g x  𝟭G}"
     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  𝟭G}  {i  A. g i  𝟭G})"
    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  𝟭G}  {i  A. g i  𝟭G}) = gfinprod G f A"
      "finprod G g ({i  A. f i  𝟭G}  {i  A. g i  𝟭G}) = 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 A  B 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  𝟭A i}" and finy: "finite {i  I. y i  𝟭A i}"
    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 A iy 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 A iy i else undefined))  I  carrier G"
    by (simp add: lam Pi_cong)
  with lam x y assms
  show "gfinprod G (λi. f i ((x sum_group I Ay) i)) I
      = gfinprod G (λi. f i (x i)) I  gfinprod G (λ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‹Free Abelian groups on a set, using the "frag" type constructor.          ›

definition free_Abelian_group :: "'a set  ('a 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]: "𝟭free_Abelian_group S= 0"
  by (auto simp: free_Abelian_group_def)

lemma mult_free_Abelian_group [simp]: "x free_Abelian_group Sy = x + y"
  by (auto simp: free_Abelian_group_def)

lemma inv_free_Abelian_group [simp]: "Poly_Mapping.keys x  S  invfree_Abelian_group Sx = -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 [^]free_Abelian_group S- int (Suc n)
     = invfree_Abelian_group S(x [^]free_Abelian_group Sint (Suc n))"
    by (rule group.int_pow_neg [OF group_free_Abelian_group]) (use assms in simp add: free_Abelian_group_def)
  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 0 int"
    apply (rule finite_subset [OF _ finite_keys [of u]])
    unfolding keys.rep_eq by force
  define h :: "('c 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 free_Abelian_group Sy) = 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 force simp: free_Abelian_group_def h_def intro: gfinprod_closed)
  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::'aint. 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}
     (S E carrier G)"  (is "?lhs  ?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  extensional (carrier (free_Abelian_group S)). f  hom (free_Abelian_group S) G}"
    if f: "f  S 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 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 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 E ?Two"
    using G2.eqpoll_homomorphisms_from_free_Abelian_group by (simp add: carrier_integer_mod_group)
  finally have *: "S E ?Two  T E ?Two" .
  then have "finite (S E ?Two)  finite (T 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 0 int. Poly_Mapping.keys c  S  Poly_Mapping.keys c  T" and "x  S" for x
    using ST [of "frag_of x"] x  S 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 ?Gy) = ?h x ?H?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  S i then poly_mapping.lookup x k else 0)" if "i  I" for i k and x :: "'b 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
      (c  S i. poly_mapping.lookup x c = 0)" if "i  I" for i and x :: "'b 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  ΠE iI. {c. Poly_Mapping.keys c  S i}. finite {i  I. x i  0}}"
      if x: "Poly_Mapping.keys x   (S ` I)" for x :: "'b 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. cS 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 (λiI. 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: c  S i 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 i  I J_def eq in auto simp: in_keys_iff)
          with i  I have "?h (λjI. Abs_poly_mapping (?f j)) = Abs_poly_mapping (?f i) + sum' (λ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 (λiI. Abs_poly_mapping (?f i))"
          by (rule poly_mapping_eqI)
        have "(λi. Abs_poly_mapping (?f i))  (Π iI. {c. Poly_Mapping.keys c  S i})"
          by (auto simp: PiE_def Pi_def in_keys_iff)
        then show "(λiI. Abs_poly_mapping (?f i))
                  {x  ΠE iI. {c. Poly_Mapping.keys c  S i}. finite {i  I. x i  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 = 𝟭?H⇙"
      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 i  I
            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 = 𝟭sum_group I (λi. free_Abelian_group (S i))⇙"
        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