Theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend

(*
    File:     Finite_Product_Extend.thy
    Author:   Joseph Thommes, TU München; Manuel Eberl, TU München
*)
section ‹Finite Product›

theory Finite_Product_Extend
  imports IDirProds
begin

text ‹In this section, some general facts about finprod› as well as some tailored for the rest of
this entry are proven.›

text ‹It is often needed to split a product in a single factor and the rest. Thus these two lemmas.›

lemma (in comm_group) finprod_minus:
  assumes "a  A" "f  A  carrier G" "finite A"
  shows "finprod G f A = f a  finprod G f (A - {a})"
proof -
  from assms have "A = insert a (A - {a})" by blast
  then have "finprod G f A = finprod G f (insert a (A - {a}))" by simp
  also have " = f a  finprod G f (A - {a})" using assms by (intro finprod_insert, auto)
  finally show ?thesis .
qed

lemma (in comm_group) finprod_minus_symm:
  assumes "a  A" "f  A  carrier G" "finite A"
  shows "finprod G f A = finprod G f (A - {a})  f a"
proof -
  from assms have "A = insert a (A - {a})" by blast
  then have "finprod G f A = finprod G f (insert a (A - {a}))" by simp
  also have " = f a  finprod G f (A - {a})" using assms by (intro finprod_insert, auto)
  also have " = finprod G f (A - {a})  f a"
    by (intro m_comm, use assms in blast, intro finprod_closed, use assms in blast)
  finally show ?thesis .
qed

text ‹This makes it very easy to show the following trivial fact.›

lemma (in comm_group) finprod_singleton:
  assumes "f x  carrier G" "finprod G f {x} = a"
  shows "f x = a"
proof -
  have "finprod G f {x} = f x  finprod G f {}" using finprod_minus[of x "{x}" f] assms by auto
  thus ?thesis using assms by simp
qed

text ‹The finite product is consistent and closed concerning subgroups.›

lemma (in comm_group) finprod_subgroup:
  assumes "f  S  H" "subgroup H G"
  shows "finprod G f S = finprod (Gcarrier := H) f S"
proof (cases "finite S")
  case True
  interpret H: comm_group "Gcarrier := H" using subgroup_is_comm_group[OF assms(2)] .
  show ?thesis using True assms
  proof (induction S rule: finite_induct)
    case empty
    then show ?case using finprod_empty H.finprod_empty by simp
  next
    case i: (insert x F)
    then have "finprod G f F = finprod (Gcarrier := H) f F" by blast
    moreover have "finprod G f (insert x F) = f x  finprod G f F"
    proof(intro finprod_insert[OF i(1, 2), of f])
      show "f  F  carrier G" "f x  carrier G" using i(4) subgroup.subset[OF i(5)] by blast+
    qed
    ultimately have "finprod G f (insert x F) = f x Gcarrier := Hfinprod (Gcarrier := H) f F"
      by auto
    moreover have "finprod (Gcarrier := H) f (insert x F) = "
    proof(intro H.finprod_insert[OF i(1, 2)])
      show "f  F  carrier (Gcarrier := H)" "f x  carrier (Gcarrier := H)" using i(4) by auto
    qed
    ultimately show ?case by simp
  qed
next
  case False
  then show ?thesis unfolding finprod_def by simp
qed

lemma (in comm_group) finprod_closed_subgroup:
  assumes "subgroup H G" "f  A  H"
  shows "finprod G f A  H"
  using assms(2)
proof (induct A rule: infinite_finite_induct)
case (infinite A)
then show ?case using subgroup.one_closed[OF assms(1)] by auto
next
  case empty
  then show ?case using subgroup.one_closed[OF assms(1)] by auto
next
  case i: (insert x F)
  from finprod_insert[OF i(1, 2), of f] i have fi: "finprod G f (insert x F) = f x  finprod G f F"
    using subgroup.subset[OF assms(1)] by blast
  from i have "finprod G f F  H" "f x  H" by blast+
  with fi show ?case using subgroup.m_closed[OF assms(1)] by presburger 
qed

text ‹It also does not matter if we exponentiate all elements taking part in the product or the
result of the product.›

lemma (in comm_group) finprod_exp:
  assumes "A  carrier G" "f  A  carrier G"
  shows "(finprod G f A) [^] (k::int) = finprod G ((λa. a [^] k)  f) A"
  using assms
proof(induction A rule: infinite_finite_induct)
  case i: (insert x F)
  hence ih: "finprod G f F [^] k = finprod G ((λa. a [^] k)  f) F" by blast
  have fpc: "finprod G f F  carrier G" by (intro finprod_closed, use i in auto)
  have fxc: "f x  carrier G" using i by auto
  have "finprod G f (insert x F) = f x  finprod G f F" by (intro finprod_insert, use i in auto)
  hence "finprod G f (insert x F) [^] k = (f x  finprod G f F) [^] k" by simp
  also have " = f x [^] k  finprod G f F [^] k" using fpc fxc int_pow_distrib by blast
  also have " = ((λa. a [^] k)  f) x  finprod G ((λa. a [^] k)  f) F" using ih by simp
  also have " = finprod G ((λa. a [^] k)  f) (insert x F)"
    by (intro finprod_insert[symmetric], use i in auto)
  finally show ?case .
qed auto

text ‹Some lemmas concerning different combinations of functions in the usage of finprod›.›

lemma (in comm_group) finprod_cong_split:
  assumes "a. a  A  f a  g a = h a"
  and "f  A  carrier G" "g  A  carrier G" "h  A  carrier G"
  shows "finprod G h A = finprod G f A  finprod G g A" using assms
proof(induct A rule: infinite_finite_induct)
  case (infinite A)
  then show ?case by simp
next
  case empty
  then show ?case by simp
next
  case i: (insert x F)
  then have iH: "finprod G h F = finprod G f F  finprod G g F" by fast
  have f: "finprod G f (insert x F) = f x  finprod G f F"
    by (intro finprod_insert[OF i(1, 2), of f]; use i(5) in simp)
  have g: "finprod G g (insert x F) = g x  finprod G g F"
    by (intro finprod_insert[OF i(1, 2), of g]; use i(6) in simp)
  have h: "finprod G h (insert x F) = h x  finprod G h F"
    by (intro finprod_insert[OF i(1, 2), of h]; use i(7) in simp)  
  also have " = h x  (finprod G f F  finprod G g F)" using iH by argo
  also have " = f x  g x  (finprod G f F  finprod G g F)" using i(4) by simp
  also have " = f x  finprod G f F  (g x  finprod G g F)" using m_comm m_assoc i(5-7) by simp
  also have " = finprod G f (insert x F)  finprod G g (insert x F)" using f g by argo
  finally show ?case .
qed

lemma (in comm_group) finprod_comp:
  assumes "inj_on g A" "(f  g) ` A  carrier G"
  shows "finprod G f (g ` A) = finprod G (f  g) A"
  using finprod_reindex[OF _ assms(1), of f] using assms(2) unfolding comp_def by blast

text ‹The subgroup generated by a set of generators (in an abelian group) is exactly the set of
elements that can be written as a finite product using only powers of these elements.›

lemma (in comm_group) generate_eq_finprod_PiE_image:
  assumes "finite gs" "gs  carrier G"
  shows "generate G gs = (λx. finprod G x gs) ` PiE gs (λa. generate G {a})" (is "?g = ?fp")
proof
  show "?g  ?fp"
  proof
    fix x
    assume x: "x  ?g"
    thus "x  ?fp"
    proof (induction rule: generate.induct)
      case one
      show ?case
      proof
        let ?r = "restrict (λ_. 𝟭) gs"
        show "?r  (ΠE ags. generate G {a})" using generate.one by auto
        show "𝟭 = finprod G ?r gs" by(intro finprod_one_eqI[symmetric], simp)
      qed
    next
      case g: (incl g)
      show ?case
      proof
        let ?r = "restrict ((λ_. 𝟭)(g := g)) gs"
        show "?r  (ΠE ags. generate G {a})" using generate.one generate.incl[of g "{g}" G]
          by fastforce
        show "g = finprod G ?r gs"
        proof -
          have "finprod G ?r gs = ?r g  finprod G ?r (gs - {g})"
            by (intro finprod_minus, use assms g in auto)
          moreover have "?r g = g" using g by simp
          moreover have "finprod G ?r (gs - {g}) = 𝟭" by(rule finprod_one_eqI; use g in simp)
          ultimately show ?thesis using assms g by auto
        qed
      qed
    next
      case g: (inv g)
      show ?case
      proof
        let ?r = "restrict ((λ_. 𝟭)(g := inv g)) gs"
        show "?r  (ΠE ags. generate G {a})" using generate.one generate.inv[of g "{g}" G]
          by fastforce
        show "inv g = finprod G ?r gs"
        proof -
          have "finprod G ?r gs = ?r g  finprod G ?r (gs - {g})"
            by (intro finprod_minus, use assms g in auto)
          moreover have "?r g = inv g" using g by simp
          moreover have "finprod G ?r (gs - {g}) = 𝟭" by(rule finprod_one_eqI; use g in simp)
          ultimately show ?thesis using assms g by auto
        qed
      qed
    next
      case gh: (eng g h)
      from gh obtain i where i: "i  (ΠE ags. generate G {a})" "g = finprod G i gs" by blast
      from gh obtain j where j: "j  (ΠE ags. generate G {a})" "h = finprod G j gs" by blast
      from i j have "g  h = finprod G i gs  finprod G j gs" by blast
      also have " = finprod G (λa. i a  j a) gs"
      proof(intro finprod_multf[symmetric]; rule)
        fix x
        assume x: "x  gs"
        have "i x  generate G {x}" "j x  generate G {x}"using i(1) j(1) x by blast+
        thus "i x  carrier G" "j x  carrier G" using generate_incl[of "{x}"] x assms(2) by blast+
      qed
      also have " = finprod G (restrict (λa. i a  j a) gs) gs"
      proof(intro finprod_cong)
        have ip: "i g  generate G {g}" if "g  gs" for g using i that by auto
        have jp: "j g  generate G {g}" if "g  gs" for g using j that by auto
        have "i g  j g  generate G {g}" if "g  gs" for g
          using generate.eng[OF ip[OF that] jp[OF that]] .
        thus "((λa. i a  j a)  gs  carrier G) = True" using generate_incl assms(2) by blast
      qed auto
      finally have "g  h = finprod G (restrict (λa. i a  j a) gs) gs" .
      moreover have "(restrict (λa. i a  j a) gs)  (ΠE ags. generate G {a})"
      proof -
        have ip: "i g  generate G {g}" if "g  gs" for g using i that by auto
        have jp: "j g  generate G {g}" if "g  gs" for g using j that by auto
        have "i g  j g  generate G {g}" if "g  gs" for g
          using generate.eng[OF ip[OF that] jp[OF that]] .
        thus ?thesis by auto
      qed
      ultimately show ?case using i j by blast
    qed
  qed
  show "?fp  ?g"
  proof
    fix x
    assume x: "x  ?fp"
    then obtain f where f: "f  (PiE gs (λa. generate G {a}))" "x = finprod G f gs" by blast
    have sg: "subgroup ?g G" by(intro generate_is_subgroup, fact)
    have "finprod G f gs  ?g"
    proof(intro finprod_closed_subgroup[OF sg])
      have "f g  generate G gs" if "g  gs" for g
      proof -
        have "f g  generate G {g}" using f(1) that by auto
        moreover have "generate G {g}  generate G gs" by(intro mono_generate, use that in simp)
        ultimately show ?thesis by fast
      qed
      thus "f  gs  generate G gs" by simp
    qed
    thus "x  ?g" using f by blast
  qed
qed

lemma (in comm_group) generate_eq_finprod_Pi_image:
  assumes "finite gs" "gs  carrier G"
  shows "generate G gs = (λx. finprod G x gs) ` Pi gs (λa. generate G {a})" (is "?g = ?fp")
proof -
  have "(λx. finprod G x gs) ` PiE gs (λa. generate G {a})
      = (λx. finprod G x gs) ` Pi gs (λa. generate G {a})"
  proof
    have "PiE gs (λa. generate G {a})  Pi gs (λa. generate G {a})" by blast
    thus "(λx. finprod G x gs) ` PiE gs (λa. generate G {a})
         (λx. finprod G x gs) ` Pi gs (λa. generate G {a})" by blast
    show "(λx. finprod G x gs) ` Pi gs (λa. generate G {a})
         (λx. finprod G x gs) ` PiE gs (λa. generate G {a})"
    proof
      fix x
      assume x: "x  (λx. finprod G x gs) ` Pi gs (λa. generate G {a})"
      then obtain f where f: "x = finprod G f gs" "f  Pi gs (λa. generate G {a})" by blast
      moreover have "finprod G f gs = finprod G (restrict f gs) gs"
      proof(intro finprod_cong)
        have "f g  carrier G" if "g  gs" for g
          using that f(2) mono_generate[of "{g}" gs] generate_incl[OF assms(2)] by fast
        thus "(f  gs  carrier G) = True" by blast
      qed auto        
      moreover have "restrict f gs  PiE gs (λa. generate G {a})" using f(2) by simp
      ultimately show "x  (λx. finprod G x gs) ` PiE gs (λa. generate G {a})" by blast
    qed
  qed
  with generate_eq_finprod_PiE_image[OF assms] show ?thesis by auto
qed

lemma (in comm_group) generate_eq_finprod_Pi_int_image:
  assumes "finite gs" "gs  carrier G"
  shows "generate G gs = (λx. finprod G (λg. g [^] x g) gs) ` Pi gs (λ_. (UNIV::int set))"
proof -
  from generate_eq_finprod_Pi_image[OF assms]
  have "generate G gs = (λx. finprod G x gs) ` (Π ags. generate G {a})" .
  also have " = (λx. finprod G (λg. g [^] x g) gs) ` Pi gs (λ_. (UNIV::int set))"
  proof(rule; rule)
    fix x
    assume x: "x  (λx. finprod G x gs) ` (Π ags. generate G {a})"
    then obtain f where f: "f  (Π ags. generate G {a})" "x = finprod G f gs" by blast
    hence "k::int. f a = a [^] k" if "a  gs" for a using generate_pow[of a] that assms(2) by blast
    hence "(h::'a  int). ags. f a = a [^] h a" by meson
    then obtain h where h: "ags. f a = a [^] h a" "h  gs  (UNIV :: int set)" by auto
    have "finprod G (λg. g [^] h g) gs = finprod G f gs"
      by (intro finprod_cong, use int_pow_closed h assms(2) in auto)
    with f have "x = finprod G (λg. g [^] h g) gs" by argo
    with h(2) show "x  (λx. finprod G (λg. g [^] x g) gs) ` (gs  (UNIV::int set))" by auto
  next
    fix x
    assume x: "x  (λx. finprod G (λg. g [^] x g) gs) ` (gs  (UNIV::int set))"
    then obtain h where h: "x = finprod G (λg. g [^] h g) gs" "h  gs  (UNIV :: int set)" by blast
    hence "kgenerate G {a}. a [^] h a = k" if "a  gs" for a
      using generate_pow[of a] that assms(2) by blast
    then obtain f where f: "ags. a [^] h a = f a" "f  (Π ags. generate G {a})" by fast
    have "finprod G f gs = finprod G (λg. g [^] h g) gs"
    proof(intro finprod_cong)
      have "f a  carrier G" if "a  gs" for a
        using generate_incl[of "{a}"] assms(2) that f(2) by fast
      thus "(f  gs  carrier G) = True" by blast
    qed (use f in auto)
    with h have "x = finprod G f gs" by argo
    with f(2) show "x  (λx. finprod G x gs) ` (Π ags. generate G {a})" by blast
  qed
  finally show ?thesis .
qed


lemma (in comm_group) IDirProds_eq_finprod_PiE:
  assumes "finite I" "i. i  I  subgroup (S i) G"
  shows "IDirProds G S I = (λx. finprod G x I) ` (PiE I S)" (is "?DP = ?fp")
proof
  show "?fp  ?DP"
  proof
    fix x
    assume x: "x  ?fp"
    then obtain f where f: "f  (PiE I S)" "x = finprod G f I" by blast
    have sDP: "subgroup ?DP G"
      by (intro IDirProds_is_subgroup; use subgroup.subset[OF assms(2)] in blast)
    have "finprod G f I  ?DP"
    proof(intro finprod_closed_subgroup[OF sDP])
      have "f i  IDirProds G S I" if "i  I" for i
      proof
        show "f i  (S i)" using f(1) that by auto
        show "(S i)  IDirProds G S I" by (intro IDirProds_incl[OF that])
      qed
      thus "f  I  IDirProds G S I" by simp
    qed
    thus "x  ?DP" using f by blast
  qed
  show "?DP  ?fp"
  proof(unfold IDirProds_def; rule subsetI)
    fix x
    assume x: "x  generate G ((S ` I))"
    thus "x  ?fp" using assms
    proof (induction rule: generate.induct)
      case one
      define g where g: "g = (λx. if x  I then 𝟭 else undefined)"
      then have "g  PiE I S"
        using subgroup.one_closed[OF one(2)] by auto
      moreover have "finprod G g I = 𝟭" by (intro finprod_one_eqI; use g in simp)
      ultimately show ?case unfolding image_def by (auto; metis)
    next
      case i: (incl h)
      from i obtain j where j: "j  I" "h  (S j)" by blast
      define hf where "hf = (λx. (if x  I then 𝟭 else undefined))(j := h)"
      with j have "hf  PiE I S"
        using subgroup.one_closed[OF i(3)] by force
      moreover have "finprod G hf I = h"
      proof -
        have "finprod G hf I = hf j  finprod G hf (I - {j})"
          by (intro finprod_minus, use assms hf_def subgroup.subset[OF i(3)[OF j(1)]] j in auto)
        moreover have "hf j = h" using hf_def by simp
        moreover have "finprod G hf (I - {j}) = 𝟭" by (rule finprod_one_eqI; use hf_def in simp)
        ultimately show ?thesis using subgroup.subset[OF i(3)[OF j(1)]] j(2) by auto
      qed
      ultimately show ?case unfolding image_def by (auto; metis)
    next
      case i: (inv h)
      from i obtain j where j: "j  I" "h  (S j)" by blast
      have ih: "inv h  (S j)" using subgroup.m_inv_closed[OF i(3)[OF j(1)] j(2)] .
      define hf where "hf = (λx. (if x  I then 𝟭 else undefined))(j := inv h)"
      with j ih have "hf  PiE I S"
        using subgroup.one_closed[OF i(3)] by force
      moreover have "finprod G hf I = inv h"
      proof -
        have "finprod G hf I = hf j  finprod G hf (I - {j})"
          by (intro finprod_minus, use assms hf_def subgroup.subset[OF i(3)[OF j(1)]] j in auto)
        moreover have "hf j = inv h" using hf_def by simp
        moreover have "finprod G hf (I - {j}) = 𝟭" by (rule finprod_one_eqI; use hf_def in simp)
        ultimately show ?thesis using subgroup.subset[OF i(3)[OF j(1)]] j(2) by auto
      qed
      ultimately show ?case unfolding image_def by (auto; metis)
    next
      case e: (eng a b)
      from e obtain f where f: "f  PiE I S" "a = finprod G f I" by blast
      from e obtain g where g: "g  PiE I S" "b = finprod G g I" by blast
      from f g have "a  b = finprod G f I  finprod G g I" by blast
      also have " = finprod G (λa. f a  g a) I"
      proof(intro finprod_multf[symmetric])
        have "(S ` I)  carrier G" using subgroup.subset[OF e(6)] by blast
        thus "f  I  carrier G" "g  I  carrier G"
          using f(1) g(1) unfolding PiE_def Pi_def by auto
      qed
      also have " = finprod G (restrict (λa. f a  g a) I) I"
      proof(intro finprod_cong)
        show "I = I" by simp
        show "i. i  I =simp=> f i  g i = (λaI. f a  g a) i" by simp
        have fp: "f i  (S i)" if "i  I" for i using f that by auto
        have gp: "g i  (S i)" if "i  I" for i using g that by auto
        have "f i  g i  (S i)" if "i  I" for i
          using subgroup.m_closed[OF e(6)[OF that] fp[OF that] gp[OF that]] .
        thus "((λa. f a  g a)  I  carrier G) = True" using subgroup.subset[OF e(6)] by auto
      qed
      finally have "a  b = finprod G (restrict (λa. f a  g a) I) I" .
      moreover have "(restrict (λa. f a  g a) I)  PiE I S"
      proof -
        have fp: "f i  (S i)" if "i  I" for i using f that by auto
        have gp: "g i  (S i)" if "i  I" for i using g that by auto
        have "f i  g i  (S i)" if "i  I" for i
          using subgroup.m_closed[OF e(6)[OF that] fp[OF that] gp[OF that]] .
        thus ?thesis by auto
      qed
      ultimately show ?case using f g by blast
    qed
  qed
qed

lemma (in comm_group) IDirProds_eq_finprod_Pi:
  assumes "finite I" "i. i  I  subgroup (S i) G"
  shows "IDirProds G S I = (λx. finprod G x I) ` (Pi I S)" (is "?DP = ?fp")
proof -
  have "(λx. finprod G x I) ` (Pi I S) = (λx. finprod G x I) ` (PiE I S)"
  proof
    have "PiE I S  Pi I S" by blast
    thus "(λx. finprod G x I) ` PiE I S  (λx. finprod G x I) ` Pi I S" by blast
    show "(λx. finprod G x I) ` Pi I S  (λx. finprod G x I) ` PiE I S"
    proof
      fix x
      assume x: "x  (λx. finprod G x I) ` Pi I S"
      then obtain f where f: "x = finprod G f I" "f  Pi I S" by blast
      moreover have "finprod G f I = finprod G (restrict f I) I"
        by (intro finprod_cong; use f(2) subgroup.subset[OF assms(2)] in fastforce)
      moreover have "restrict f I  PiE I S" using f(2) by simp
      ultimately show "x  (λx. finprod G x I) ` PiE I S" by blast
    qed
  qed
  with IDirProds_eq_finprod_PiE[OF assms] show ?thesis by auto
qed

text ‹If we switch one element from a set of generators, the generated set stays the same if both
elements can be generated from the others together with the switched element respectively.›

lemma (in comm_group) generate_one_switched_exp_eqI:
  assumes "A  carrier G" "a  A" "B = (A - {a})  {b}"
  and "f  A  (UNIV::int set)" "g  B  (UNIV::int set)"
  and "a = finprod G (λx. x [^] g x) B" "b = finprod G (λx. x [^] f x) A"
  shows "generate G A = generate G B"
proof(intro generate_one_switched_eqI[OF assms(1, 2, 3)]; cases "finite A")
  case True
  hence fB: "finite B" using assms(3) by blast
  have cB: "B  carrier G"
  proof -
    have "b  carrier G"
      by (subst assms(7), intro finprod_closed, use assms(1, 4) int_pow_closed in fast)
    thus ?thesis using assms(1, 3) by blast
  qed
  show "a  generate G B"
  proof(subst generate_eq_finprod_Pi_image[OF fB cB], rule)
    show "a = finprod G (λx. x [^] g x) B" by fact
    have "x [^] g x  generate G {x}" if "x  B" for x using generate_pow[of x] cB that by blast
    thus "(λx. x [^] g x)  (Π aB. generate G {a})" unfolding Pi_def by blast
  qed
  show "b  generate G A"
  proof(subst generate_eq_finprod_Pi_image[OF True assms(1)], rule)
    show "b = finprod G (λx. x [^] f x) A" by fact
    have "x [^] f x  generate G {x}" if "x  A" for x
      using generate_pow[of x] assms(1) that by blast
    thus "(λx. x [^] f x)  (Π aA. generate G {a})" unfolding Pi_def by blast
  qed
next
  case False
  hence b: "b = 𝟭" using assms(7) unfolding finprod_def by simp
  from False assms(3) have "infinite B" by simp
  hence a: "a = 𝟭" using assms(6) unfolding finprod_def by simp
  show "a  generate G B" using generate.one a by blast
  show "b  generate G A" using generate.one b by blast
qed

text ‹We can characterize a complementary family of subgroups when the only way to form the neutral
element as a product of picked elements from each subgroup is to pick the neutral element from each
subgroup.›

lemma (in comm_group) compl_fam_imp_triv_finprod:
  assumes "compl_fam S I" "finite I" "i. i  I  subgroup (S i) G"
  and "finprod G f I = 𝟭" "f  Pi I S"
  shows "iI. f i = 𝟭"
proof (rule ccontr; clarify)
  from assms(5) have f: "f i  (S i)" if "i  I" for i using that by fastforce
  fix i
  assume i: "i  I"
  have si: "subgroup (S i) G" using assms(3)[OF i] .
  consider (triv) "(S i) = {𝟭}" | (not_triv) "(S i)  {𝟭}" by blast
  thus "f i = 𝟭"
  proof (cases)
    case triv
    then show ?thesis using f[OF i] by blast
  next
    case not_triv
    show ?thesis
    proof (rule ccontr)
      have fc: "f i  carrier G" using f[OF i] subgroup.subset[OF si] by blast
      assume no: "f i  𝟭"
      have fH: "f i  (S i)" using f[OF i] .
      from subgroup.m_inv_closed[OF si this] have ifi: "inv (f i)  (S i)" .
      moreover have "inv (f i)  𝟭" using no fc by simp
      moreover have "inv (f i) = finprod G f (I - {i})"
      proof -
        have "𝟭 = finprod G f I" using assms(4) by simp
        also have " = finprod G f (insert i (I - {i}))"
        proof -
          have "I = insert i (I - {i})" using i by fast
          thus ?thesis by simp
        qed
        also have " = f i  finprod G f (I - {i})"
        proof(intro finprod_insert)
          show "finite (I - {i})" using assms(2) by blast
          show "i  I - {i}" by blast
          show "f  I - {i}  carrier G" using assms(3) f subgroup.subset by blast
          show "f i  carrier G" by fact
        qed
        finally have o: "𝟭 = f i  finprod G f (I - {i})" .
        show ?thesis
        proof(intro inv_equality)
          show "f i  carrier G" by fact
          show "finprod G f (I - {i})  carrier G"
            by (intro finprod_closed; use assms(3) f subgroup.subset in blast)
          from m_comm[OF this fc] o show "finprod G f (I - {i})  f i = 𝟭" by simp
        qed
      qed
      moreover have "finprod G f (I - {i})  IDirProds G S (I - {i})"
      proof (intro finprod_closed_subgroup IDirProds_is_subgroup)
        show " (S ` (I - {i}))  carrier G" using assms(3) subgroup.subset by auto
        have "f j  (IDirProds G S (I - {i}))" if "j  (I - {i})" for j
          using IDirProds_incl[OF that] f that by blast
        thus "f  I - {i}  IDirProds G S (I - {i})" by blast
      qed
      ultimately have "¬complementary (S i) (IDirProds G S (I - {i}))"
        unfolding complementary_def by auto
      thus False using assms(1) i unfolding compl_fam_def by blast
    qed
  qed
qed

lemma (in comm_group) triv_finprod_imp_compl_fam:
  assumes "finite I" "i. i  I  subgroup (S i) G"
  and "f  Pi I S. finprod G f I = 𝟭  (iI. f i = 𝟭)"
  shows "compl_fam S I"
proof (unfold compl_fam_def; rule)
  fix k
  assume k: "k  I"
  let ?DP = "IDirProds G S (I - {k})"
  show "complementary (S k) ?DP"
  proof (rule ccontr; unfold complementary_def)
    have sk: "subgroup (S k) G" using assms(2)[OF k] .
    have sDP: "subgroup ?DP G"
      by (intro IDirProds_is_subgroup; use subgroup.subset[OF assms(2)] in blast)
    assume a: "(S k)  IDirProds G S (I - {k})  {𝟭}"
    then obtain x where x: "x  (S k)" "x  IDirProds G S (I - {k})" "x  𝟭"
      using subgroup.one_closed sk sDP by blast
    then have "x  (λx. finprod G x (I - {k})) ` (Pi (I - {k}) S)"
      using IDirProds_eq_finprod_Pi[of "(I - {k})"] assms(1, 2) by blast
    then obtain ht where ht: "finprod G ht (I - {k}) = x" "ht  Pi (I - {k}) S" by blast
    define h where h: "h = (ht(k := inv x))"
    then have hPi: "h  Pi I S" using ht subgroup.m_inv_closed[OF assms(2)[OF k] x(1)] by auto
    have "finprod G h (I - {k}) = x"
    proof (subst ht(1)[symmetric], intro finprod_cong)
      show "I - {k} = I - {k}" by simp
      show "(h  I - {k}  carrier G) = True" using h ht(2) subgroup.subset[OF assms(2)]
        unfolding Pi_def id_def by auto
      show "i. i  I - {k} =simp=> h i = ht i" using ht(2) h by simp
    qed
    moreover have "finprod G h I = h k  finprod G h (I - {k})"
      by (intro finprod_minus; use k assms hPi subgroup.subset[OF assms(2)] Pi_def in blast)
    ultimately have "finprod G h I = inv x  x" using h by simp
    then have "finprod G h I = 𝟭" using subgroup.subset[OF sk] x(1) by auto
    moreover have "h k  𝟭" using h x(3) subgroup.subset[OF sk] x(1) by force
    ultimately show False using assms(3) k hPi by blast
  qed
qed

lemma (in comm_group) triv_finprod_iff_compl_fam_Pi:
  assumes "finite I" "i. i  I  subgroup (S i) G"
  shows "compl_fam S I  (f  Pi I S. finprod G f I = 𝟭  (iI. f i = 𝟭))"
  using compl_fam_imp_triv_finprod triv_finprod_imp_compl_fam assms by blast

lemma (in comm_group) triv_finprod_iff_compl_fam_PiE:
  assumes "finite I" "i. i  I  subgroup (S i) G"
  shows "compl_fam S I  (f  PiE I S. finprod G f I = 𝟭  (iI. f i = 𝟭))"
proof
  show "compl_fam S I  fPiE I S. finprod G f I = 𝟭  (iI. f i = 𝟭)"
    using triv_finprod_iff_compl_fam_Pi[OF assms] by auto
  have "fPiE I S. finprod G f I = 𝟭  (iI. f i = 𝟭)
     fPi I S. finprod G f I = 𝟭  (iI. f i = 𝟭)"
  proof(rule+)
    fix f i
    assume f: "f  Pi I S" "finprod G f I = 𝟭" and i: "i  I"
    assume allf: "fPiE I S. finprod G f I = 𝟭  (iI. f i = 𝟭)"
    have "f i = restrict f I i" using i by simp
    moreover have "finprod G (restrict f I) I = finprod G f I"
      using f subgroup.subset[OF assms(2)] unfolding Pi_def by (intro finprod_cong; auto)
    moreover have "restrict f I  PiE I S" using f by simp
    ultimately show "f i = 𝟭" using allf f i by metis
  qed
  thus "fPiE I S. finprod G f I = 𝟭  (iI. f i = 𝟭)  compl_fam S I"
    using triv_finprod_iff_compl_fam_Pi[OF assms] by presburger
qed

text ‹The finite product also distributes when nested.›

(* Manuel Eberl, TODO: move to library *)
lemma (in comm_monoid) finprod_Sigma:
  assumes "finite A" "x. x  A  finite (B x)"
  assumes "x y. x  A  y  B x  g x y  carrier G"
  shows   "(xA. yB x. g x y) = (zSigma A B. case z of (x, y)  g x y)"
  using assms
proof (induction A rule: finite_induct)
  case (insert x A)
  have "(zSigma (insert x A) B. case z of (x, y)  g x y) =
          (zPair x ` B x. case z of (x, y)  g x y)  (zSigma A B. case z of (x, y)  g x y)"
    unfolding Sigma_insert using insert.prems insert.hyps
    by (subst finprod_Un_disjoint) auto
  also have "(zSigma A B. case z of (x, y)  g x y) = (xA. yB x. g x y)"
    using insert.prems insert.hyps by (subst insert.IH [symmetric]) auto
  also have "(zPair x ` B x. case z of (x, y)  g x y) = (yB x. g x y)"
    using insert.prems insert.hyps by (subst finprod_reindex) (auto intro: inj_onI)
  finally show ?case
    using insert.hyps insert.prems by simp
qed auto

text ‹With the now proven facts, we are able to provide criterias to inductively construct a
group that is the internal direct product of a set of generators.›

(* belongs to IDirProd, but uses finprod stuff *)
lemma (in comm_group) idirprod_generate_ind:
  assumes "finite gs" "gs  carrier G" "g  carrier G"
          "is_idirprod (generate G gs) (λg. generate G {g}) gs"
          "complementary (generate G {g}) (generate G gs)"
  shows "is_idirprod (generate G (gs  {g})) (λg. generate G {g}) (gs  {g})"
proof(cases "g  gs")
  case True
  hence "gs = (gs  {g})" by blast
  thus ?thesis using assms(4) by auto 
next
  case gngs: False
  show ?thesis
  proof (intro is_idirprod_subgroup_suffices)
    have gsgc: "gs  {g}  carrier G" using assms(2, 3) by blast
    thus "generate G (gs  {g}) = IDirProds G (λg. generate G {g}) (gs  {g})"
      unfolding IDirProds_def using generate_idem_Un by presburger
    show "igs  {g}. subgroup (generate G {i}) G" using generate_is_subgroup gsgc by auto
    have sg: "subgroup (generate G {g}) G" by (intro generate_is_subgroup, use assms(3) in blast)
    from assms(4) is_idirprod_def have ih: "x. x  gs  generate G {x}  G"
                                           "compl_fam (λg. generate G {g}) gs"
      by fastforce+
    hence ca: "complementary (generate G {a}) (generate G (gs - {a}))" if "a  gs" for a
      unfolding compl_fam_def IDirProds_def
      using gsgc generate_idem_Un[of "gs - {a}"] that by fastforce
    have aux: "gs  {g} - {i}  carrier G" for i using gsgc by blast
    show "compl_fam (λg. generate G {g}) (gs  {g})"
    proof(unfold compl_fam_def IDirProds_def, subst generate_idem_Un[OF aux],
          rule, rule ccontr)
      fix h
      assume h: "h  gs  {g}"
      assume c: "¬ complementary (generate G {h}) (generate G (gs  {g} - {h}))"
      show "False"
      proof (cases "h = g")
        case True
        with c have "¬ complementary (generate G {g}) (generate G (gs - {g}))" by auto
        moreover have "complementary (generate G {g}) (generate G (gs - {g}))"
          by (rule subgroup_subset_complementary[OF generate_is_subgroup generate_is_subgroup[of gs]
                   generate_is_subgroup mono_generate], use assms(2, 3, 5) in auto)
        ultimately show False by blast
      next
        case hng: False
        hence h: "h  gs" "h  g" using h by blast+
        hence "gs  {g} - {h} = gs - {h}  {g}" by blast
        with c have c: "¬ complementary (generate G {h}) (generate G (gs - {h}  {g}))" by argo
        then obtain k where k: "k  generate G {h}" "k  generate G (gs - {h}  {g})" "k  𝟭"
          unfolding complementary_def using generate.one by blast 
        with ca have kngh: "k  generate G (gs - {h})" using h unfolding complementary_def by blast
        from k(2) generate_eq_finprod_PiE_image[of "gs - {h}  {g}"] assms(1) gsgc
        obtain f where f:
          "k = finprod G f (gs - {h}  {g})" "f  (ΠE ags - {h}  {g}. generate G {a})"
          by blast
        have fg: "f a  generate G {a}" if "a  (gs - {h}  {g})" for a using that f(2) by blast
        have fc: "f a  carrier G" if "a  (gs - {h}  {g})" for a
        proof -
          have "generate G {a}  carrier G" if "a  (gs - {h}  {g})" for a
            using that generate_incl[of "{a}"] gsgc by blast
          thus "f a  carrier G" using that fg by auto
        qed
        have kp: "k = f g  finprod G f (gs - {h})"
        proof -
          have "(gs - {h}  {g}) = insert g (gs - {h})" by fast
          moreover have "finprod G f (insert g (gs - {h})) = f g  finprod G f (gs - {h})"
            by (intro finprod_insert, use fc assms(1) gngs in auto)
          ultimately show ?thesis using f(1) by argo
        qed
        have fgsh: "finprod G f (gs - {h})  generate G (gs - {h})"
        proof(intro finprod_closed_subgroup[OF generate_is_subgroup])
          show "gs - {h}  carrier G" using gsgc by blast
          have "f a  generate G (gs - {h})" if "a  (gs - {h})" for a
            using mono_generate[of "{a}" "gs - {h}"] fg that by blast
          thus "f  gs - {h}  generate G (gs - {h})" by blast
        qed
        have "f g  finprod G f (gs - {h})  generate G gs"
        proof
          assume fpgs: "f g  finprod G f (gs - {h})  generate G gs"
          from fgsh have fgsgs: "finprod G f (gs - {h})  generate G gs"
            using mono_generate[of "gs - {h}" gs] by blast
          have fPi: "f  (Π a(gs - {h}). generate G {a})" using f by blast
          have gI: "generate G (gs - {h})
                  = (λx. finprod G x (gs - {h})) ` (Π ags - {h}. generate G {a})"
            using generate_eq_finprod_Pi_image[of "gs - {h}"] assms(1, 2) by blast
          have fgno: "f g  𝟭"
          proof (rule ccontr)
            assume o: "¬ f g  𝟭"
            hence kf: "k = finprod G f (gs - {h})" using kp finprod_closed fc by auto
            hence "k  generate G (gs - {h})" using fPi gI by blast
            thus False using k ca h unfolding complementary_def by blast
          qed
          from fpgs have "f g  generate G gs"
            using subgroup.mult_in_cancel_right[OF generate_is_subgroup[OF assms(2)] fc[of g] fgsgs]
            by blast
          with fgno assms(5) fg[of g] show "False" unfolding complementary_def by blast
        qed
        moreover have "k  generate G gs" using k(1) mono_generate[of "{h}" gs] h(1) by blast
        ultimately show False using kp by blast
      qed
    qed
  qed
qed

end