Theory 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 "(⨂a∈A. 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 = 𝟭 ⟶ (∀a∈A. f a = 𝟭)"
proof(rule, rule)
  fix f
  assume f: "f ∈ (ΠE a∈A. generate G {a})" "finprod G f A = 𝟭"
  with generate_pow assms(1) have "∀a∈A. ∃k::int. f a = a [^] k" by blast
  then obtain r::"'a ⇒ int" where r: "∀a∈A. f a = a [^] r a" by metis
  have "restrict r A ∈ relations A"
  proof(intro in_relationsI)
    have "(⨂a∈A. a [^] restrict r A a) = finprod G f A"
      by (intro finprod_cong, use assms r in auto)
    thus "(⨂a∈A. 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 "∀a∈A. 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 = 𝟭 ⟶ (∀a∈A. 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 a∈B 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 "(λa∈A. if a ∈ B then f (generate G {a}) else 𝟭) ∈ A - B → carrier G" using Bs by simp
      from fBc show "(λa∈A. 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: "∀a∈A. ?r a = 𝟭" using assms(2) by blast
  then have BA: "∀a∈B∩A. ?r a = 𝟭" by blast
  from Bs sI have "∀a∈A. (generate G {a}) ∈ ((λx. generate G {x}) ` B)" by simp
  then have "∀a∈A. ∃b∈B. 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 = 𝟭 ⟶ (∀a∈A. 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 = (⨂a∈A. 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 "∀a∈A. ?r a = 𝟭" by fast
      then have "∀a∈A. 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" "∀g∈gs. 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