Theory Finitely_Generated_Abelian_Groups.Group_Relations

(*
    File:     Group_Relations.thy
    Author:   Joseph Thommes, TU München
*)
section ‹Group relations›

theory Group_Relations
  imports Finite_Product_Extend
begin

text ‹We introduce the notion of a relation of a set of elements: a way to express the neutral
element by using only powers of said elements. The following predicate describes the set of all the
relations that one can construct from a set of elements.›

definition (in comm_group) relations :: "'a set  ('a  int) set" where
  "relations A = {f. finprod G (λa. a [^] f a) A = 𝟭}  extensional A"

text ‹Now some basic lemmas about relations.›

lemma (in comm_group) in_relationsI[intro]:
  assumes "finprod G (λa. a [^] f a) A = 𝟭" "f  extensional A"
  shows "f  relations A"
  unfolding relations_def using assms by blast

lemma (in comm_group) triv_rel:
  "restrict (λ_. 0::int) A  relations A"
proof
  show "(aA. a [^] (λ_A. 0::int) a) = 𝟭" by (intro finprod_one_eqI, simp)
qed simp

lemma (in comm_group) not_triv_relI:
  assumes "a  A" "f a  (0::int)"
  shows "f  (λ_A. 0::int)"
  using assms by auto

lemma (in comm_group) rel_in_carr:
  assumes "A  carrier G" "r  relations A"
  shows "(λa. a [^] r a)  A  carrier G"
  by (meson Pi_I assms(1) int_pow_closed subsetD)

text ‹The following lemmas are of importance when proving the fundamental theorem of finitely
generated abelian groups in the case that there is just the trivial relation between a set of
generators. They all build up to the last lemma that then is actually used in the proof.›

lemma (in comm_group) relations_zero_imp_pow_not_one:
  assumes "a  A" "f(relations A). f a = 0"
  shows "z::int  0. a [^] z  𝟭"
proof (rule ccontr; safe)
  fix z::int
  assume z: "z  0" "a [^] z = 𝟭"
  have "restrict ((λx. 0)(a := z)) A  relations A"
    by (intro in_relationsI finprod_one_eqI, use z in auto)
  thus False using z assms by auto
qed

lemma (in comm_group) relations_zero_imp_ord_zero:
  assumes "a  A" "f(relations A). f a = 0"
  and "a  carrier G"
  shows "ord a = 0"
  using assms relations_zero_imp_pow_not_one[OF assms(1, 2)]
  by (meson finite_cyclic_subgroup_int infinite_cyclic_subgroup_order)

lemma (in comm_group) finprod_relations_triv_harder_better_stronger:
  assumes "A  carrier G" "relations A = {(λ_A. 0::int)}"
  shows "f  PiE A (λa. generate G {a}). finprod G f A = 𝟭  (aA. f a = 𝟭)"
proof(rule, rule)
  fix f
  assume f: "f  (ΠE aA. generate G {a})" "finprod G f A = 𝟭"
  with generate_pow assms(1) have "aA. k::int. f a = a [^] k" by blast
  then obtain r::"'a  int" where r: "aA. f a = a [^] r a" by metis
  have "restrict r A  relations A"
  proof(intro in_relationsI)
    have "(aA. a [^] restrict r A a) = finprod G f A"
      by (intro finprod_cong, use assms r in auto)
    thus "(aA. a [^] restrict r A a) = 𝟭" using f by simp
  qed simp
  with assms(2) have z: "restrict r A = (λ_A. 0)" by blast
  have "(restrict r A) a = r a" if "a  A" for a using that by auto
  with r z show "aA. f a = 𝟭" by auto
qed

lemma (in comm_group) stronger_PiE_finprod_imp:
  assumes "A  carrier G" "f  PiE A (λa. generate G {a}). finprod G f A = 𝟭  (aA. f a = 𝟭)"
  shows "f  PiE ((λa. generate G {a}) ` A) id.
         finprod G f ((λa. generate G {a}) ` A) = 𝟭  (H (λa. generate G {a}) ` A. f H = 𝟭)"
proof(rule, rule)
  fix f
  assume f: "f  PiE ((λa. generate G {a}) ` A) id" "finprod G f ((λa. generate G {a}) ` A) = 𝟭"
  define B where "B = inv_into A (λa. generate G {a}) ` ((λa. generate G {a}) ` A)"
  have Bs: "B  A"
  proof
    fix x
    assume x: "x  B"
    then obtain C where C: "C  ((λa. generate G {a}) ` A)" "x = inv_into A (λa. generate G {a}) C"
      unfolding B_def by blast
    then obtain c where c: "C = generate G {c}" "c  A" by blast
    with C someI_ex[of "λy. y  A  generate G {y} = C"] show "x  A"
      unfolding inv_into_def by blast
  qed
  have sI: "(λx. generate G {x}) ` B = (λx. generate G {x}) ` A"
  proof
    show "(λx. generate G {x}) ` B  (λx. generate G {x}) ` A" using Bs by blast
    show "(λx. generate G {x}) ` A  (λx. generate G {x}) ` B"
    proof
      fix C
      assume C: "C  (λx. generate G {x}) ` A"
      then obtain x where x: "x = inv_into A (λa. generate G {a}) C" unfolding B_def by blast
      then obtain c where c: "C = generate G {c}" "c  A" using C by blast
      with C x someI_ex[of "λy. y  A  generate G {y} = C"] have "generate G {x} = C"
        unfolding inv_into_def by blast
      with x C show "C  (λx. generate G {x}) ` B" unfolding B_def by blast
    qed
  qed
  have fBc: "f (generate G {b})  carrier G" if "b  B" for b
  proof -
    have "f (generate G {b})  generate G {b}" using f(1)
      by (subst (asm) sI[symmetric], use that in fastforce)
    moreover have "generate G {b}  carrier G" using assms(1) that Bs generate_incl by blast
    ultimately show ?thesis by blast
  qed
  let ?r = "restrict (λa. if aB then f (generate G {a}) else 𝟭) A"
  have "?r  PiE A (λa. generate G {a})"
  proof
    show "?r x = undefined" if "x  A" for x using that by simp
    show "?r x  generate G {x}" if "x  A" for x using that generate.one B_def f(1) by auto
  qed
  moreover have "finprod G ?r A = 𝟭"
  proof (cases "finite A")
    case True
    have "A = B  (A - B)" using Bs by auto
    then have "finprod G ?r A = finprod G ?r (B(A-B))" by auto
    moreover have " = finprod G ?r B  finprod G ?r (A - B)"
    proof(intro finprod_Un_disjoint)
      from True Bs finite_subset show "finite B" "finite (A - B)" "B  (A - B) = {}" by auto
      show "(λaA. if a  B then f (generate G {a}) else 𝟭)  A - B  carrier G" using Bs by simp
      from fBc show "(λaA. if a  B then f (generate G {a}) else 𝟭)  B  carrier G"
        using Bs by auto
    qed
    moreover have "finprod G ?r B = 𝟭"
    proof -
      have "finprod G ?r B = finprod G (f  (λa. generate G {a})) B"
      proof(intro finprod_cong')
        show "?r b = (f  (λa. generate G {a})) b" if "b  B" for b using that Bs by auto
        show "f  (λa. generate G {a})  B  carrier G" using fBc by simp
      qed simp
      also have " = finprod G f ((λa. generate G {a}) ` B)"
      proof(intro finprod_comp[symmetric])
        show "(f  (λa. generate G {a})) ` B  carrier G" using fBc by auto
        show "inj_on (λa. generate G {a}) B"
          by (intro inj_onI, unfold B_def, metis (no_types, lifting) f_inv_into_f inv_into_into)
      qed
      also have " = finprod G f ((λa. generate G {a}) ` A)" using sI by argo
      finally show ?thesis using f(2) by argo
    qed
    moreover have "finprod G ?r (A - B) = 𝟭" by(intro finprod_one_eqI, simp)
    ultimately show ?thesis by fastforce
  next
    case False
    then show ?thesis unfolding finprod_def by simp
  qed
  ultimately have a: "aA. ?r a = 𝟭" using assms(2) by blast
  then have BA: "aBA. ?r a = 𝟭" by blast
  from Bs sI have "aA. (generate G {a})  ((λx. generate G {x}) ` B)" by simp
  then have "aA. bB. f (generate G {a}) = f (generate G {b})" by force
  thus "H(λa. generate G {a}) ` A. f H = 𝟭" using a BA Bs by fastforce
qed

lemma (in comm_group) finprod_relations_triv:
  assumes "A  carrier G" "relations A = {(λ_A. 0::int)}"
  shows "f  PiE ((λa. generate G {a}) ` A) id.
         finprod G f ((λa. generate G {a}) ` A) = 𝟭  (H (λa. generate G {a}) ` A. f H = 𝟭)"
  using assms finprod_relations_triv_harder_better_stronger stronger_PiE_finprod_imp by presburger

lemma (in comm_group) ord_zero_strong_imp_rel_triv:
  assumes "A  carrier G" "a  A. ord a = 0"
  and "f  PiE A (λa. generate G {a}). finprod G f A = 𝟭  (aA. f a = 𝟭)"
  shows "relations A = {(λ_A. 0::int)}"
proof -
  have "r. r  relations A  r = (λ_A. 0::int)"
  proof
    fix r x
    assume r: "r  relations A"
    show "r x = (λ_A. 0::int) x"
    proof (cases "x  A")
      case True
      let ?r = "restrict (λa. a [^] r a) A"
      have rp: "?r  PiE A (λa. generate G {a})"
      proof -
        have "?r  extensional A" by blast
        moreover have "?r  Pi A (λa. generate G {a})"
        proof
          fix a
          assume a: "a  A"
          then have sga: "subgroup (generate G {a}) G" using generate_is_subgroup assms(1) by auto
          show "a [^] r a  generate G {a}"
            using generate.incl[of a "{a}" G] subgroup_int_pow_closed[OF sga] by simp
        qed
        ultimately show ?thesis unfolding PiE_def by blast
      qed
      have "finprod G ?r A = (aA. a [^] r a)" by(intro finprod_cong, use assms(1) in auto)
      with r have "finprod G ?r A = 𝟭" unfolding relations_def by simp
      with assms(3) rp have "aA. ?r a = 𝟭" by fast
      then have "aA. a [^] r a = 𝟭" by simp
      with assms(1, 2) True have "r x = 0"
        using finite_cyclic_subgroup_int infinite_cyclic_subgroup_order by blast
      thus ?thesis using True by simp
    next
      case False
      thus ?thesis using r unfolding relations_def extensional_def by simp
    qed
  qed
  thus ?thesis using triv_rel by blast
qed

lemma (in comm_group) compl_fam_iff_relations_triv:
  assumes "finite gs" "gs  carrier G" "ggs. ord g = 0"
  shows "relations gs = {(λ_gs. 0::int)}  compl_fam (λg. generate G {g}) gs"
  using triv_finprod_iff_compl_fam_PiE[of _ "λg. generate G {g}", OF assms(1) generate_is_subgroup]
        ord_zero_strong_imp_rel_triv[OF assms(2, 3)]
        finprod_relations_triv_harder_better_stronger[OF assms(2)] assms by blast

end