Theory Finitely_Generated_Abelian_Groups.DirProds

(*
    File:     DirProds.thy
    Author:   Joseph Thommes, TU München
*)
section ‹Direct group product›

theory DirProds
  imports Finite_Product_Extend Group_Hom Finite_And_Cyclic_Groups
begin

notation integer_mod_group ("Z")

text ‹The direct group product is defined component-wise and provided in an indexed way.›

definition DirProds :: "('a  ('b, 'c) monoid_scheme)  'a set  ('a  'b) monoid" where
  "DirProds G I =  carrier = PiE I (carrier  G),
                   monoid.mult = (λx y. restrict (λi. x i G iy i) I),
                   one = restrict (λi. 𝟭G i) I "

text ‹Basic lemmas about DirProds›.›

lemma DirProds_empty:
  "carrier (DirProds f {}) = {𝟭DirProds f {}}"
  unfolding DirProds_def by auto

lemma DirProds_order:
  assumes "finite I"
  shows "order (DirProds G I) = prod (order  G) I"
  unfolding order_def DirProds_def using assms by (simp add: card_PiE)

lemma DirProds_in_carrI:
  assumes "i. i  I  x i  carrier (G i)" "i. i  I  x i = undefined"
  shows "x  carrier (DirProds G I)"
  unfolding DirProds_def using assms by auto

lemma comp_in_carr:
  assumes "x  carrier (DirProds G I)" "i  I"
  shows "x i  carrier (G i)"
  using assms unfolding DirProds_def by auto

lemma comp_mult:
  assumes "i  I"
  shows "(x DirProds G Iy) i = (x i G iy i)"
  using assms unfolding DirProds_def by simp

lemma comp_exp_nat:
  fixes k::nat
  assumes "i  I"
  shows "(x [^]DirProds G Ik) i = x i [^]G ik"
proof (induction k)
  case 0
  then show ?case using assms unfolding DirProds_def by simp
next
  case i: (Suc k)
  have "(x [^]DirProds G Ik DirProds G Ix) i = (x [^]DirProds G Ik) i G ix i"
    by(rule comp_mult[OF assms])
  also from i have " = x i [^]G ik G ix i" by simp
  also have " = x i [^]G iSuc k" by simp
  finally show ?case by simp
qed

lemma DirProds_m_closed:
  assumes "x  carrier (DirProds G I)" "y  carrier (DirProds G I)" "i. i  I  group (G i)"
  shows "x DirProds G Iy  carrier (DirProds G I)"
  using assms monoid.m_closed[OF group.is_monoid[OF assms(3)]] unfolding DirProds_def by fastforce

lemma partial_restr:
  assumes "a  carrier (DirProds G I)" "J  I"
  shows "restrict a J  carrier (DirProds G J)"
  using assms unfolding DirProds_def by auto 

lemma eq_parts_imp_eq:
  assumes "a  carrier (DirProds G I)" "b  carrier (DirProds G I)" "i. i  I  a i = b i"
  shows "a = b"
  using assms unfolding DirProds_def by fastforce

lemma mult_restr:
  assumes "a  carrier (DirProds G I)" "b  carrier (DirProds G I)" "J  I"
  shows "a DirProds G Jb = restrict (a DirProds G Ib) J"
  using assms unfolding DirProds_def by force

lemma DirProds_one:
  assumes "x  carrier (DirProds G I)"
  shows "(i  I. x i = 𝟭G i)  x = 𝟭DirProds G I⇙"
  using assms unfolding DirProds_def by fastforce

lemma DirProds_one':
  "iI  𝟭DirProds G Ii = 𝟭G i⇙"
  unfolding DirProds_def by simp

lemma DirProds_one'':
  "𝟭DirProds G I= restrict (λi. 𝟭G i) I"
  by (unfold DirProds_def, simp)

lemma DirProds_mult:
  "(⊗DirProds G I) = (λx y. restrict (λi. x i G iy i) I)"
  unfolding DirProds_def by simp

lemma DirProds_one_iso: "(λx. x G)  iso (DirProds f {G}) (f G)"
proof (intro isoI homI)
  show "bij_betw (λx. x G) (carrier (DirProds f {G})) (carrier (f G))"
  proof (unfold bij_betw_def, rule)
    show "inj_on (λx. x G) (carrier (DirProds f {G}))"
      by (intro inj_onI, unfold DirProds_def PiE_def Pi_def extensional_def, fastforce)
    show "(λx. x G) ` carrier (DirProds f {G}) = carrier (f G)"
    proof(intro equalityI subsetI)
      show "x  carrier (f G)" if "x  (λx. x G) ` carrier (DirProds f {G})" for x
        using that unfolding DirProds_def by auto
      show "x  (λx. x G) ` carrier (DirProds f {G})" if xc: "x  carrier (f G)" for x
      proof
        show "(λk{G}. x)  carrier (DirProds f {G})" unfolding DirProds_def using xc by auto
        moreover show "x = (λk{G}. x) G" by simp
      qed
    qed
  qed
qed (unfold DirProds_def PiE_def Pi_def extensional_def, auto)

lemma DirProds_one_cong: "(DirProds f {G})  (f G)"
  using DirProds_one_iso is_isoI by fast

lemma DirProds_one_iso_sym: "(λx. (λ_{G}. x))  iso (f G) (DirProds f {G})"
proof (intro isoI homI)
  show "bij_betw (λx. λ_{G}. x) (carrier (f G)) (carrier (DirProds f {G}))"
  proof (unfold bij_betw_def, rule)
    show "inj_on (λx. (λ_{G}. x)) (carrier (f G))"
      by (intro inj_onI, metis imageI image_constant image_restrict_eq member_remove remove_def)
    show "(λx. (λ_{G}. x)) ` carrier (f G) = carrier (DirProds f {G})"
      unfolding DirProds_def by fastforce
  qed
qed (unfold DirProds_def, auto)

lemma DirProds_one_cong_sym: "(f G)  (DirProds f {G})"
  using DirProds_one_iso_sym is_isoI by fast

text ‹The direct product is a group iff all factors are groups.›

lemma DirProds_is_group:
  assumes "i. i  I  group (G i)"
  shows "group (DirProds G I)"
proof(rule groupI)
  show one_closed: "𝟭DirProds G I carrier (DirProds G I)" unfolding DirProds_def
    by (simp add: assms group.is_monoid)
  fix x
  assume x: "x  carrier (DirProds G I)"
  have one_: "i. i  I  𝟭G i= 𝟭DirProds G Ii" unfolding DirProds_def by simp
  have "i. i  I  𝟭DirProds G Ii G ix i = x i"
  proof -
    fix i
    assume i: "i  I"
    interpret group "G i" using assms[OF i] .
    have "x i  carrier (G i)" using x i comp_in_carr by fast
    thus "𝟭DirProds G Ii G ix i = x i" by(subst one_[OF i, symmetric]; simp)
  qed
  with one_ x show "𝟭DirProds G IDirProds G Ix = x" unfolding DirProds_def by force
  have "restrict (λi. invG i(x i)) I  carrier (DirProds G I)" using x group.inv_closed[OF assms]
    unfolding DirProds_def by fastforce 
  moreover have "restrict (λi. invG i(x i)) I DirProds G Ix = 𝟭DirProds G I⇙"
    using x group.l_inv[OF assms] unfolding DirProds_def by fastforce
  ultimately show "ycarrier (DirProds G I). y DirProds G Ix = 𝟭DirProds G I⇙" by blast
  fix y
  assume y: "y  carrier (DirProds G I)"
  from DirProds_m_closed[OF x y assms] show m_closed: "x DirProds G Iy  carrier (DirProds G I)"
    by blast
  fix z
  assume z: "z  carrier (DirProds G I)"
  have "i. i  I  (x DirProds G Iy DirProds G Iz) i
                    = (x DirProds G I(y DirProds G Iz)) i"
  proof -
    fix i
    assume i: "i  I"
    have "(x DirProds G Iy DirProds G Iz) i = (x DirProds G Iy) i G iz i"
      using assms by (simp add: comp_mult i m_closed z)
    also have " = x i G iy i G iz i" by (simp add: assms comp_mult i x y)
    also have " = x i G i(y i G iz i)" using i assms x y z
      by (meson Group.group_def comp_in_carr monoid.m_assoc)
    also have " = (x DirProds G I(y DirProds G Iz)) i" by (simp add: DirProds_def i)
    finally show "(x DirProds G Iy DirProds G Iz) i
                = (x DirProds G I(y DirProds G Iz)) i" .
  qed
  thus "x DirProds G Iy DirProds G Iz = x DirProds G I(y DirProds G Iz)"
    unfolding DirProds_def by auto
qed

lemma DirProds_obtain_elem_carr:
  assumes "group (DirProds G I)" "i  I" "x  carrier (G i)"
  obtains k where "k  carrier (DirProds G I)" "k i = x"
proof -
  interpret DP: group "DirProds G I" by fact
  from comp_in_carr[OF DP.one_closed] DirProds_one' have ao: "jI. 𝟭G j carrier (G j)" by metis
  let ?r = "restrict ((λj. 𝟭G j)(i := x)) I"
  have "?r  carrier (DirProds G I)"
    unfolding DirProds_def PiE_def Pi_def using assms(2, 3) ao by auto
  moreover have "?r i = x" using assms(2) by simp
  ultimately show "(k. k  carrier (DirProds G I); k i = x  thesis)  thesis" by blast
qed

lemma DirProds_group_imp_groups:
  assumes "group (DirProds G I)" and i: "i  I"
  shows "group (G i)"
proof (intro groupI)
  let ?DP = "DirProds G I"
  interpret DP: group ?DP by fact
  show "𝟭G i carrier (G i)" using DirProds_one' comp_in_carr[OF DP.one_closed i] i by metis
  show "x G iy  carrier (G i)" if "x  carrier (G i)" "y  carrier (G i)" for x y
  proof -
    from DirProds_obtain_elem_carr[OF assms that(1)] obtain k where k: "k  carrier ?DP" "k i = x" .
    from DirProds_obtain_elem_carr[OF assms that(2)] obtain l where l: "l  carrier ?DP" "l i = y" .
    have "k ?DPl  carrier ?DP" using k l by fast
    from comp_in_carr[OF this i] comp_mult[OF i] show ?thesis using k l by metis
  qed
  show "x G iy G iz = x G i(y G iz)"
    if x: "x  carrier (G i)" and y: "y  carrier (G i)" and z: "z  carrier (G i)" for x y z
  proof -
    from DirProds_obtain_elem_carr[OF assms x] obtain k where k: "k  carrier ?DP" "k i = x" .
    from DirProds_obtain_elem_carr[OF assms y] obtain l where l: "l  carrier ?DP" "l i = y" .
    from DirProds_obtain_elem_carr[OF assms z] obtain m where m: "m  carrier ?DP" "m i = z" .
    have "x G iy G iz = (k i) G i(l i) G i(m i)" using k l m by argo
    also have " = (k ?DPl ?DPm) i" using comp_mult[OF i] k l m by metis
    also have " = (k ?DP(l ?DPm)) i"
    proof -
      have "k ?DPl ?DPm = k ?DP(l ?DPm)" using DP.m_assoc[OF k(1) l(1) m(1)] .
      thus ?thesis by simp
    qed
    also have " = (k i) G i((l i) G i(m i))" using comp_mult[OF i] k l m by metis
    finally show ?thesis using k l m by blast
  qed
  show "𝟭G iG ix = x" if "x  carrier (G i)" for x
  proof -
    from DirProds_obtain_elem_carr[OF assms that(1)] obtain k where k: "k  carrier ?DP" "k i = x" .
    hence "𝟭?DP?DPk = k" by simp
    with comp_mult k DirProds_one[OF DP.one_closed] that i show ?thesis by metis
  qed
  show "ycarrier (G i). y G ix = 𝟭G i⇙" if "x  carrier (G i)" for x
  proof -
    from DirProds_obtain_elem_carr[OF assms that(1)] obtain k where k: "k  carrier ?DP" "k i = x" .
    hence ic: "inv?DPk  carrier ?DP" by simp
    have "inv?DPk ?DPk = 𝟭?DP⇙" using k by simp
    hence "(inv?DPk) i G ik i= 𝟭G i⇙" using comp_mult[OF i] DirProds_one'[OF i] by metis
    with k(2) comp_in_carr[OF ic i] show ?thesis by blast
  qed
qed

lemma DirProds_group_iff: "group (DirProds G I)  (iI. group (G i))"
  using DirProds_is_group DirProds_group_imp_groups by metis

lemma comp_inv:
  assumes "group (DirProds G I)" and x: "x  carrier (DirProds G I)" and i: "i  I"
  shows "(inv(DirProds G I)x) i = inv(G i)(x i)"
proof -
  interpret DP: group "DirProds G I" by fact
  interpret Gi: group "G i" using DirProds_group_imp_groups[OF DP.is_group i] .
  have ixc: "inv(DirProds G I)x  carrier (DirProds G I)" using x by blast
  hence "inv(DirProds G I)x DirProds G Ix = 𝟭DirProds G I⇙" using x by simp
  hence "(inv(DirProds G I)x DirProds G Ix) i = 𝟭G i⇙" by (simp add: DirProds_one' i)
  moreover from comp_mult[OF i]
  have "(inv(DirProds G I)x DirProds G Ix) i = ((inv(DirProds G I)x) i) G i(x i)"
    by blast
  ultimately show ?thesis using x ixc by (simp add: comp_in_carr[OF _ i] group.inv_equality)
qed

text ‹The same is true for abelian groups.›

lemma DirProds_is_comm_group:
  assumes "i. i  I  comm_group (G i)"
  shows "comm_group (DirProds G I)" (is "comm_group ?DP")
proof
  interpret group ?DP using assms DirProds_is_group unfolding comm_group_def by metis
  show "carrier ?DP  Units ?DP" "𝟭?DP carrier ?DP" by simp_all
  fix x
  assume x[simp]: "x  carrier ?DP"
  show "𝟭?DP?DPx = x" "x ?DP𝟭?DP= x" by simp_all
  fix y
  assume y[simp]: "y  carrier ?DP"
  show "x ?DPy  carrier ?DP" by simp
  show "x DirProds G Iy = y DirProds G Ix"
  proof (rule eq_parts_imp_eq[of _ G I])
    show "x ?DPy  carrier ?DP" by simp
    show "y ?DPx  carrier ?DP" by simp
    show "i. iI  (x DirProds G Iy) i = (y DirProds G Ix) i"
    proof -
      fix i
      assume i: "i  I"
      interpret gi: comm_group "(G i)" using assms(1)[OF i] .
      have "(x ?DPy) i = x i G iy i"
        by (intro comp_mult[OF i])
      also have " = y i G ix i" using comp_in_carr[OF _ i] x y gi.m_comm by metis
      also have " = (y ?DPx) i" by (intro comp_mult[symmetric, OF i])
      finally show "(x DirProds G Iy) i = (y DirProds G Ix) i" .
    qed
  qed
  fix z
  assume z[simp]: "z  carrier ?DP"
  show "x ?DPy ?DPz = x ?DP(y ?DPz)" using m_assoc by simp
qed

lemma DirProds_comm_group_imp_comm_groups:
  assumes "comm_group (DirProds G I)" and i: "i  I"
  shows "comm_group (G i)"
proof -
  interpret DP: comm_group "DirProds G I" by fact
  interpret Gi: group "G i" using DirProds_group_imp_groups[OF DP.is_group i] .
  show "comm_group (G i)"
  proof
    show "x G iy = y G ix" if x: "x  carrier (G i)" and y: "y  carrier (G i)" for x y
    proof -
      obtain a where a[simp]: "a  carrier (DirProds G I)" "a i = x"
        using DirProds_obtain_elem_carr[OF DP.is_group i x] .
      obtain b where b[simp]: "b  carrier (DirProds G I)" "b i = y"
        using DirProds_obtain_elem_carr[OF DP.is_group i y] .
      have "a DirProds G Ib = b DirProds G Ia" using DP.m_comm by simp
      hence "(a DirProds G Ib) i = (b DirProds G Ia) i" by argo
      with comp_mult[OF i] have "a i G ib i = b i G ia i" by metis
      with a b show "x G iy = y G ix" by blast
    qed
  qed
qed

lemma DirProds_comm_group_iff: "comm_group (DirProds G I)  (iI. comm_group (G i))"
  using DirProds_is_comm_group DirProds_comm_group_imp_comm_groups by metis

text ‹And also for finite groups.›

lemma DirProds_is_finite_group:
  assumes "i. iI  finite_group (G i)" "finite I"
  shows "finite_group (DirProds G I)"
proof -
  have "group (G i)" if "iI" for i using assms(1)[OF that] unfolding finite_group_def by blast
  from DirProds_is_group[OF this] interpret DP: group "DirProds G I" by fast
  show ?thesis
  proof(unfold_locales)
    have "order (DirProds G I)  0"
    proof(unfold DirProds_order[OF assms(2)])
      have "(order  G) i  0" if "iI" for i
        using assms(1)[OF that] by (simp add: finite_group.order_gt_0)
      thus "prod (order  G) I  0" by (simp add: assms(2))
    qed
    thus "finite (carrier (DirProds G I))" unfolding order_def by (meson card.infinite)
  qed
qed

lemma DirProds_finite_imp_finite_groups:
  assumes "finite_group (DirProds G I)" "finite I"
  shows "i. iI  finite_group (G i)"
proof -
  fix i assume i: "i  I"
  interpret DP: finite_group "DirProds G I" by fact
  interpret group "G i" by (rule DirProds_group_imp_groups[OF DP.is_group i])
  show "finite_group (G i)"
  proof(unfold_locales)
    have oDP: "order (DirProds G I)  0" by blast
    with DirProds_order[OF assms(2), of G] have "order (G i)  0" using i assms(2) by force
    thus "finite (carrier (G i))" unfolding order_def by (meson card_eq_0_iff)
  qed
qed

lemma DirProds_finite_group_iff:
  assumes "finite I"
  shows "finite_group (DirProds G I)  (iI. finite_group (G i))"
  using DirProds_is_finite_group DirProds_finite_imp_finite_groups assms by metis

lemma DirProds_finite_comm_group_iff:
  assumes "finite I"
  shows "finite_comm_group (DirProds G I)  (iI. finite_comm_group (G i))"
  using DirProds_finite_group_iff[OF assms] DirProds_comm_group_iff unfolding finite_comm_group_def by fast

text ‹If a group is an internal direct product of a family of subgroups, it is isomorphic to the
direct product of these subgroups.›

lemma (in comm_group) subgroup_iso_DirProds_IDirProds:
  assumes "subgroup J G" "is_idirprod J S I" "finite I"
  shows "(λx. GiI. x i)  iso (DirProds (λi. Gcarrier := (S i)) I) (Gcarrier := J)"
(is "?fp  iso ?DP ?J")
proof -
  from assms(2) have assm: "J = IDirProds G S I"
                           "compl_fam S I"
    unfolding is_idirprod_def by auto
  from assms(1, 2) have assm': "i. i  I  subgroup (S i) (Gcarrier := J)"
    using normal_imp_subgroup subgroup_incl by (metis IDirProds_incl assms(2) is_idirprod_def)
  interpret J: comm_group ?J using subgroup_is_comm_group[OF assms(1)] .
  interpret DP: comm_group ?DP
    by (intro DirProds_is_comm_group; use J.subgroup_is_comm_group[OF assm'] in simp)
  have inJ: "S i  J" if "i  I" for i using subgroup.subset[OF assm'[OF that]] by simp
  have hom: "?fp  hom ?DP ?J"
  proof (rule homI)
    fix x
    assume x[simp]: "x  carrier ?DP"
    show "finprod G x I  carrier ?J"
    proof (subst finprod_subgroup[OF _ assms(1)])
      show "x  I  J" using inJ comp_in_carr[OF x] by auto
      thus "finprod ?J x I  carrier ?J" by (intro J.finprod_closed; simp)
    qed
    fix y
    assume y[simp]: "y  carrier ?DP"
    show "finprod G (x ?DPy) I = finprod G x I ?Jfinprod G y I"
    proof(subst (1 2 3) finprod_subgroup[of _ _ J])
      show xyJ: "x  I  J" "y  I  J" using x y inJ comp_in_carr[OF x] comp_in_carr[OF y]
        by auto
      show xyJ1: "x ?DPy  I  J" using inJ x y comp_in_carr[of "x ?DPy"] by fastforce
      show "subgroup J G" using assms(1) .
      show "finprod ?J (x ?DPy) I = finprod ?J x I ?Jfinprod ?J y I"
      proof (rule J.finprod_cong_split)
        show "x  I  carrier ?J" "y  I  carrier ?J" using xyJ by simp_all
        show "x ?DPy  I  carrier ?J" using xyJ1 by simp
        fix i
        assume i: "i  I"
        then have "x i Gcarrier := (S i) y i = (x ?DPy) i"
          by (intro comp_mult[symmetric])
        thus "x i ?Jy i = (x ?DPy) i" by simp
      qed
    qed
  qed
  then interpret fp: group_hom ?DP ?J ?fp unfolding group_hom_def group_hom_axioms_def by blast
  have s: "subgroup (S i) G" if "i  I" for i using incl_subgroup[OF assms(1) assm'[OF that]] .
  have "kernel ?DP ?J ?fp = {𝟭?DP}"
  proof -
    have "a = 𝟭?DP⇙" if "a  kernel ?DP ?J ?fp" for a
    proof -
      from that have a: "finprod G a I = 𝟭" "a  carrier ?DP" unfolding kernel_def by simp_all
      from compl_fam_imp_triv_finprod[OF assm(2) assms(3) s a(1)] comp_in_carr[OF a(2)]
      have "iI. a i = 𝟭" by simp
      then show ?thesis using DirProds_one[OF a(2)] by fastforce
    qed
    thus ?thesis using fp.one_in_kernel by blast
  qed
  moreover have "J  ?fp ` carrier ?DP"
    using assm(1) IDirProds_eq_finprod_PiE[OF assms(3) incl_subgroup[OF assms(1) assm']]
    unfolding DirProds_def PiE_def Pi_def by simp
  ultimately show ?thesis using hom fp.iso_iff unfolding kernel_def by auto
qed

lemma (in comm_group) iso_DirProds_IDirProds:
  assumes "is_idirprod (carrier G) S I" "finite I"
  shows "(λx. GiI. x i)  iso (DirProds (λi. Gcarrier := (S i)) I) G"
  using subgroup_iso_DirProds_IDirProds[OF subgroup_self assms(1, 2)] by auto

lemma (in comm_group) cong_DirProds_IDirProds:
  assumes "is_idirprod (carrier G) S I" "finite I"
  shows "DirProds (λi. Gcarrier := (S i)) I  G"
  by (intro is_isoI, use iso_DirProds_IDirProds[OF assms] in blast)

text ‹In order to prove the isomorphism between two direct products, the following lemmas provide
some criterias.›

lemma DirProds_iso:
  assumes "bij_betw f I J" "i. iI  Gs i  Hs (f i)"
          "i. iI  group (Gs i)" "j. jJ  group (Hs j)"
  shows "DirProds Gs I  DirProds Hs J"
proof -
  interpret DG: group "DirProds Gs I" using DirProds_is_group assms(3) by blast
  interpret DH: group "DirProds Hs J" using DirProds_is_group assms(4) by blast
  from assms(1) obtain g where g: "g = inv_into I f" "bij_betw g J I" by (meson bij_betw_inv_into)
  hence fgi: "i. i  I  g (f i) = i" "j. j  J  f (g j) = j"
    using assms(1) bij_betw_inv_into_left[OF assms(1)] bij_betw_inv_into_right[OF assms(1)] by auto
  from assms(2) have "i. i  I  (h. h  iso (Gs i) (Hs (f i)))" unfolding is_iso_def by blast
  then obtain h where h: "i. i  I  h i  iso (Gs i) (Hs (f i))" by metis
  let ?h = "(λx. (λj. if jJ then (h (g j)) (x (g j)) else undefined))"
  have hc: "?h x  carrier (DirProds Hs J)" if "x  carrier (DirProds Gs I)" for x
  proof -
    have xc: "x  carrier (DirProds Gs I)" by fact
    have "h (g j) (x (g j))  carrier (Hs j)" if "j  J" for j
    proof(intro iso_in_carr[OF _ comp_in_carr[OF xc], of "h (g j)" "g j" "Hs j"])
      show "g j  I" using g(2)[unfolded bij_betw_def] that by blast
      from h[OF this] show "h (g j)  Group.iso (Gs (g j)) (Hs j)" using fgi(2)[OF that] by simp
    qed
    thus ?thesis using xc unfolding DirProds_def PiE_def extensional_def by auto
  qed
  moreover have "?h (x DirProds Gs Iy)= ?h x DirProds Hs J?h y"
    if "x  carrier (DirProds Gs I)" "y  carrier (DirProds Gs I)" for x y
  proof(intro eq_parts_imp_eq[OF hc[OF DG.m_closed[OF that]] DH.m_closed[OF hc[OF that(1)] hc[OF that(2)]]])
    fix j
    assume j: "j  J"
    hence gj: "g j  I" using g unfolding bij_betw_def by blast
    from assms(3)[OF gj] assms(4)[OF j] have g: "group (Gs (g j))" "Group.group (Hs j)" .
    from iso_imp_homomorphism[OF h[OF gj]] fgi(2)[OF j] g
    interpret hjh: group_hom "Gs (g j)" "Hs j" "h (g j)"
      unfolding group_hom_def group_hom_axioms_def by simp
    show "(?h (x DirProds Gs Iy)) j = (?h x DirProds Hs J?h y) j"
    proof(subst comp_mult)
      show "(if j  J then h (g j) (x (g j) Gs (g j)y (g j)) else undefined)
          = (?h x DirProds Hs J?h y) j"
      proof(subst comp_mult)
        have "h (g j) (x (g j) Gs (g j)y (g j)) = h (g j) (x (g j)) Hs jh (g j) (y (g j))"
          using comp_in_carr[OF that(1) gj] comp_in_carr[OF that(2) gj] by simp
        thus "(if j  J then h (g j) (x (g j) Gs (g j)y (g j)) else undefined) =
              (if j  J then h (g j) (x (g j)) else undefined)
      Hs j(if j  J then h (g j) (y (g j)) else undefined)"
          using j by simp
      qed (use j g that hc in auto)
    qed (use gj g that in auto)
  qed
  ultimately interpret hgh: group_hom "DirProds Gs I" "DirProds Hs J" ?h
    unfolding group_hom_def group_hom_axioms_def by (auto intro: homI)
  have "carrier (DirProds Hs J)  ?h ` carrier (DirProds Gs I)"
  proof
    show "x  ?h ` carrier (DirProds Gs I)" if xc: "x  carrier (DirProds Hs J)" for x
    proof -
      from h obtain k where k: "i. iI  k i = inv_into (carrier (Gs i)) (h i)" by fast
      hence kiso: "i. iI  k i  iso (Hs (f i)) (Gs i)"
        using h by (simp add: assms(3) group.iso_set_sym)
      hence hk: "y = (h (g j)  (k (g j))) y" if "j  J" "y  carrier (Hs j)" for j y
      proof -
        have gj: "g j  I" using that g[unfolded bij_betw_def] by blast
        thus ?thesis
          using h[OF gj, unfolded iso_def] k[OF gj] that fgi(2)[OF that(1)] bij_betw_inv_into_right
          unfolding comp_def by fastforce
      qed
      let ?k = "(λi. if iI then k i else (λ_. undefined))"
      let ?y = "(λi. (?k i) (x (f i)))"
      have "x j = (λj. if j  J then h (g j) (?y (g j)) else undefined) j" for j
      proof (cases "j  J")
        case True
        thus ?thesis using hk[OF True comp_in_carr[OF that True]]
                           fgi(2)[OF True] g[unfolded bij_betw_def] by auto
      next
        case False
        thus ?thesis using that[unfolded DirProds_def] by auto
      qed
      moreover have "?y  carrier (DirProds Gs I)"
      proof -
        have "?y i  carrier (Gs i)" if i: "i  I" for i
          using k[OF i] h[OF i] comp_in_carr[OF xc] assms(1) bij_betwE iso_in_carr kiso that
          by fastforce
        moreover have "?y i = undefined" if i: "i  I" for i using i by simp
        ultimately show ?thesis unfolding DirProds_def PiE_def Pi_def extensional_def by simp
      qed
      ultimately show ?thesis by fast
    qed
  qed
  moreover have "x = 𝟭DirProds Gs I⇙"
    if "x  carrier (DirProds Gs I)" "?h x = 𝟭DirProds Hs J⇙" for x
  proof -
    have "iI. x i = 𝟭Gs i⇙"
    proof
      fix i
      assume i: "i  I"
      interpret gi: group "Gs i" using assms(3)[OF i] .
      interpret hfi: group "Hs (f i)" using assms(4) i assms(1)[unfolded bij_betw_def] by blast
      from h[OF i] interpret hi: group_hom "(Gs i)" "Hs (f i)" "h i"
        unfolding group_hom_def group_hom_axioms_def iso_def by blast
      from that have hx: "?h x  carrier (DirProds Hs J)" by simp
      from DirProds_one[OF this] that(2)
      have "(if j  J then h (g j) (x (g j)) else undefined) = 𝟭Hs j⇙" if "j  J" for j
        using that by blast
      hence "h (g (f i)) (x (g (f i))) = 𝟭Hs (f i)⇙" using i assms(1)[unfolded bij_betw_def] by auto
      hence "h i (x i) = 𝟭Hs (f i)⇙" using fgi(1)[OF i] by simp
      with hi.iso_iff h[OF i] comp_in_carr[OF that(1) i] show "x i = 𝟭Gs i⇙" by fast
    qed
    with DirProds_one that show ?thesis using assms(3) by blast
  qed
  ultimately show ?thesis unfolding is_iso_def using hgh.iso_iff by blast
qed

lemma DirProds_iso1:
  assumes "i. iI  Gs i  (f  Gs) i" "i. iI  group (Gs i)" "i. iI  group ((f  Gs) i)"
  shows "DirProds Gs I  DirProds (f  Gs) I"
proof -
  interpret DP: group "DirProds Gs I" using DirProds_is_group assms by metis
  interpret fDP: group "DirProds (f  Gs) I" using DirProds_is_group assms by metis
  from assms have "iI. (g. g  iso (Gs i) ((f  Gs) i))" unfolding is_iso_def by blast
  then obtain J where J: "iI. J i  iso (Gs i) ((f  Gs) i)" by metis
  let ?J = "(λi. if iI then J i else (λ_. undefined))"
  from J obtain K where K: "iI. K i = inv_into (carrier (Gs i)) (J i)" by fast
  hence K_iso: "iI. K i  iso ((f  Gs) i) (Gs i)" using group.iso_set_sym assms J by metis
  let ?K = "(λi. if iI then K i else (λ_. undefined))"
  have JKi: "(?J i) ((?K i) (x i)) = x i" if "x  carrier (DirProds (f  Gs) I)" for i x
  proof -
    have "(J i) ((K i) (x i)) = x i" if "x  carrier (DirProds (f  Gs) I)" "i  I" for i x
    proof -
      from J that have "(J i) ` (carrier (Gs i)) = carrier ((f  Gs) i)"
        unfolding iso_def bij_betw_def by blast
      hence "y. y  carrier (Gs i)  (J i) y = x i" using that by (metis comp_in_carr imageE)
      with someI_ex[OF this] that show "(J i) ((K i) (x i)) = x i"
        using K J K_iso unfolding inv_into_def by auto
    qed
    moreover have "(?J i) ((K i) (x i)) = x i" if "x  carrier (DirProds (f  Gs) I)" "i  I" for i x
      using that unfolding DirProds_def PiE_def extensional_def by force
    ultimately show ?thesis using that by simp
  qed
  let ?r = "(λe. restrict (λi. ?J i (e i)) I)"
  have hom: "?r  hom (DirProds Gs I) (DirProds (f  Gs) I)"
  proof (intro homI)
    show "?r x  carrier (DirProds (f  Gs) I)" if "x  carrier (DirProds Gs I)" for x
      using that J comp_in_carr[OF that] unfolding DirProds_def iso_def bij_betw_def by fastforce
    show "?r (x DirProds Gs Iy) = ?r x DirProds (f  Gs) I?r y"
      if "x  carrier (DirProds Gs I)" "y  carrier (DirProds Gs I)" for x y
      using that J comp_in_carr[OF that(1)] comp_in_carr[OF that(2)]
      unfolding DirProds_def iso_def hom_def by force
  qed
  then interpret r: group_hom "(DirProds Gs I)" "(DirProds (f  Gs) I)" ?r
    unfolding group_hom_def group_hom_axioms_def by blast
  have "carrier (DirProds (f  Gs) I)  ?r ` carrier (DirProds Gs I)"
  proof
    show "x  ?r ` carrier (DirProds Gs I)" if "x  carrier (DirProds (f  Gs) I)" for x
    proof
      show "x = (λiI. ?J i ((?K i) (x i)))"
        using JKi[OF that] that unfolding DirProds_def PiE_def by (simp add: extensional_restrict)
      show "(λi. ?K i (x i))  carrier (DirProds Gs I)" using K_iso iso_in_carr that
        unfolding DirProds_def PiE_def Pi_def extensional_def by fastforce
    qed
  qed
  moreover have "x = 𝟭DirProds Gs I⇙"
    if "x  carrier (DirProds Gs I)" "?r x = 𝟭DirProds (f  Gs) I⇙" for x
  proof -
    have "iI. x i = 𝟭Gs i⇙"
    proof
      fix i
      assume i: "i  I"
      with J assms interpret Ji: group_hom "(Gs i)" "(f  Gs) i" "J i"
        unfolding group_hom_def group_hom_axioms_def iso_def by blast
      from that have rx: "?r x  carrier (DirProds (f  Gs) I)" by simp
      from i DirProds_one[OF this] that
      have "(λiI. (if i  I then J i else (λ_. undefined)) (x i)) i = 𝟭(f  Gs) i⇙" by blast
      hence "(J i) (x i) = 𝟭(f  Gs) i⇙" using i by simp
      with Ji.iso_iff mp[OF spec[OF J[unfolded Ball_def]] i] comp_in_carr[OF that(1) i]
      show "x i = 𝟭Gs i⇙" by fast
    qed
    with DirProds_one[OF that(1)] show ?thesis by blast
  qed
  ultimately show ?thesis unfolding is_iso_def using r.iso_iff by blast
qed

lemma DirProds_iso2:
  assumes "inj_on f A" "group (DirProds g (f ` A))"
  shows "DirProds (g  f) A  DirProds g (f ` A)"
proof (intro DirProds_iso[of f])
  show "bij_betw f A (f ` A)" using assms(1) unfolding bij_betw_def by blast
  show "i. i  A  (g  f) i  g (f i)" unfolding comp_def using iso_refl by simp
  from assms(2) show "i. i  (f ` A)  group (g i)" using DirProds_group_imp_groups by fast
  with assms(1) show "i. i  A  group ((g  f) i)" by auto
qed

text ‹The direct group product distributes when nested.›

lemma DirProds_Sigma:
  "DirProds (λi. DirProds (G i) (J i)) I  DirProds (λ(i,j). G i j) (Sigma I J)" (is "?L  ?R")
proof (intro is_isoI isoI)
  let ?f = "λx. restrict (case_prod x) (Sigma I J)"
  show hom: "?f  hom ?L ?R"
  proof(intro homI)
    show "?f a  carrier ?R" if "a  carrier ?L" for a
      using that unfolding DirProds_def PiE_def Pi_def extensional_def by auto
    show "?f (a ?Lb) = ?f a ?R?f b" if "a  carrier ?L" and "b  carrier ?L" for a b
      using that unfolding DirProds_def PiE_def Pi_def extensional_def by auto
  qed
  show "bij_betw ?f (carrier ?L) (carrier ?R)"
  proof (intro bij_betwI)
    let ?g = "λx. (λi. if iI then (λj. if j(J i) then x(i, j) else undefined) else undefined)"
    show "?f  carrier ?L  carrier ?R" unfolding DirProds_def by fastforce
    show "?g  carrier ?R  carrier ?L" unfolding DirProds_def by fastforce
    show "?f (?g x) = x" if "x  carrier ?R" for x
      using that unfolding DirProds_def PiE_def Pi_def extensional_def by auto
    show "?g (?f x) = x" if "x  carrier ?L" for x
      using that unfolding DirProds_def PiE_def Pi_def extensional_def by force
  qed
qed

no_notation integer_mod_group ("Z")

end