(*  Title:      bpl/lemma_2_2_18_local_nilpot.thy
    ID:         $Id: lemma_2_2_18.thy $
    Author:     Jesus Aransay
    Comments:   The set of lemmas proving the equational part of the BPL
*)

header{*Lemma 2.2.18 in Aransay's memoir*}

theory lemma_2_2_18_local_nilpot 
  imports 
  lemma_2_2_17_local_nilpot
  begin

text{*Lemma 2.2.18 is generic, in the sense that the previous definitions and premises from locales @{text lemma_2_2_11} to 
  @{text lemma_2_2_17} are not needed. Only the notion of differential groups and isomorphism of abelian groups are introduced.*}
text{*As far as we are in a generic setting, with homomorphisms instead of endomorphisms, 
  the automation of the ring of endomorphisms is lost, and proofs become a bit more obscure*}

text{*Composition of completions is again a completion*}

lemma hom_completion_comp_closed: includes group A + group B + group C 
  assumes f: "f \<in> hom_completion A B" and g: "g \<in> hom_completion B C" 
  shows "g \<circ> f \<in> hom_completion A C"
  using f g
  unfolding hom_completion_def hom_def Pi_def apply auto
  unfolding completion_fun2_def completion_def apply simp
  apply (intro exI [of _ "g \<circ> f"], auto simp add: expand_fun_eq)
  apply (rule group_hom.hom_one)
  unfolding group_hom_def group_hom_axioms_def hom_def Pi_def by (simp add: prems)

lemma iso_inv_compl_coherent_iso_inv_diff: assumes fg: "(f, g) \<in> (F \<cong>\<^bsub>invcompl\<^esub> G)" and f_coherent: "f \<circ> diff F = diff G \<circ> f" 
  and g_coherent: "g \<circ> diff G = diff F \<circ> g" shows "(f, g) \<in> (F \<cong>\<^bsub>invdiff\<^esub> G)" 
  using fg and f_coherent and g_coherent unfolding iso_inv_diff_def iso_inv_compl_def iso_diff_def iso_compl_def hom_diff_def by simp

subsection{*Lemma 2.2.18*}

text{*The following lemma corresponds to @{text "Lemma 2.2.18"} in the memoir*}
text{*It illustrates quite precisely the difficulties of proving facts about homomorphisms and endomorphisms 
  when we loose the automation supplied in the previous lemmas*}
text{*The difficulties are due to the neccesity of operating with endomorphisms and homomorphisms between different domains, @{term A} and 
  @{term B}*}
text{*A suitable environment would be the one defined by the ring @{text "End (A)"}, the ring @{text "End (B)"}, the commutative group 
  @{text "hom (A, B)"} and the commutative group @{text "hom (A, B)"}, but then the question would be how to supply this structure with any
  automation*}

text{*In my opinion, the definition @{thm [locale=group] "comm_group_def"} should be relaxed; 
  in its actual version, when unfolded, the characterization @{term [locale=group] "group G \<and> comm_monoid G"} is obtained,
  which unfolded again produces @{term [locale=group] "group_axioms G \<and> monoid G \<and> comm_monoid_axioms G \<and> monoid G"}, which is redundant.
  Two possible solutions would be to define @{term [locale=group] "comm_group G = group G \<and> comm_monoid_axioms G"} or also
  @{term [locale=group] "comm_group G = group_axioms G \<and> comm_monoid G"}*}

lemma lemma_2_2_18: assumes A: "diff_group A" and B: "comm_group B" and F_F': "(F, F') \<in> (A \<cong>\<^bsub>invcompl\<^esub> B)"
  shows "diff_group \<lparr>carrier = carrier B, mult = mult B, one = one B, diff = F \<circ> (diff A) \<circ> F'\<rparr>"
  (is "diff_group ?B'")
  and "(F, F') \<in> (A \<cong>\<^bsub>invdiff\<^esub> \<lparr>carrier = carrier B, mult = mult B, one = one B, diff = F \<circ> (diff A) \<circ> F'\<rparr>)"
  (is "_ \<in> A \<cong>\<^bsub>invdiff\<^esub> ?B'")
proof -
  show "diff_group ?B'"
  proof (unfold diff_group_def diff_group_axioms_def comm_group_def group_def comm_monoid_def, intro conjI)
    from B show "monoid ?B'" unfolding comm_group_def group_def monoid_def by simp
    from B show "monoid ?B'" unfolding comm_group_def group_def monoid_def by simp
    from B show "comm_monoid_axioms ?B'" unfolding comm_group_def comm_monoid_def comm_monoid_axioms_def by simp
    from B show "group_axioms ?B'" unfolding comm_group_def group_def group_axioms_def Units_def by simp
  next
    from F_F' have F'_hom: "F' \<in> hom_completion B A" unfolding iso_inv_compl_def iso_compl_def by simp
    from diff_group.diff_hom [OF A] have diff: "differ\<^bsub>A\<^esub> \<in> hom_completion A A" by simp
    from hom_completion_comp_closed [OF _ _ _ F'_hom diff ] and A and B have diff_F': "differ\<^bsub>A\<^esub> \<circ> F' \<in> hom_completion B A"
      unfolding diff_group_def comm_group_def group_def by simp
    from F_F' have F_hom: "F \<in> hom_completion A B" unfolding iso_inv_compl_def iso_compl_def by simp
    from hom_completion_comp_closed [OF _ _ _ diff_F' F_hom] and A and B have "differ\<^bsub>?B'\<^esub> \<in> hom_completion B B"
      unfolding diff_group_def comm_group_def group_def by (simp add: o_assoc)
    then show "differ\<^bsub>?B'\<^esub> \<in> hom_completion ?B' ?B'"
      unfolding hom_completion_def completion_fun2_def completion_def hom_def Pi_def expand_fun_eq by auto
  next
    from sym [OF o_assoc [of " F \<circ> differ\<^bsub>A\<^esub>" F' "F \<circ> differ\<^bsub>A\<^esub> \<circ> F'"]] and sym [OF o_assoc [of F "differ\<^bsub>A\<^esub>" F']] 
      and o_assoc [of F' F "(differ\<^bsub>A\<^esub> \<circ> F')"]
    have "differ\<^bsub>?B'\<^esub> \<circ> differ\<^bsub>?B'\<^esub> = F \<circ> differ\<^bsub>A\<^esub> \<circ> ((F' \<circ> F) \<circ> (differ\<^bsub>A\<^esub> \<circ> F'))" by simp
    also from iso_inv_compl_id [OF F_F'] have "\<dots> = F \<circ> differ\<^bsub>A\<^esub> \<circ> ((\<lambda>x. if x \<in> carrier A then id x else \<one>\<^bsub>A\<^esub>) \<circ> (differ\<^bsub>A\<^esub> \<circ> F'))"
      unfolding iso_inv_compl_def completion_def by simp
    also from o_assoc [of "(\<lambda>x. if x \<in> carrier A then id x else \<one>\<^bsub>A\<^esub>)" "differ\<^bsub>A\<^esub>" "F'"] have "\<dots> =  F \<circ> differ\<^bsub>A\<^esub> \<circ> (differ\<^bsub>A\<^esub> \<circ> F')"
    proof -
      from diff_group.diff_hom [OF A] have "(\<lambda>x. if x \<in> carrier A then id x else \<one>\<^bsub>A\<^esub>) \<circ> (differ\<^bsub>A\<^esub>) = (differ\<^bsub>A\<^esub>)"
	unfolding hom_completion_def completion_fun2_def completion_def hom_def Pi_def expand_fun_eq by auto
      with o_assoc [of "(\<lambda>x. if x \<in> carrier A then id x else \<one>\<^bsub>A\<^esub>)" "differ\<^bsub>A\<^esub>" "F'"] show ?thesis by simp
    qed
    also from sym [OF o_assoc [of F "differ\<^bsub>A\<^esub>" "differ\<^bsub>A\<^esub> \<circ> F'"]] and o_assoc [of "differ\<^bsub>A\<^esub>" "differ\<^bsub>A\<^esub>"  F'] 
    have "\<dots> = F \<circ> ((differ\<^bsub>A\<^esub> \<circ> differ\<^bsub>A\<^esub>) \<circ> F')" by simp
    also from diff_group.diff_nilpot [OF A] have "\<dots> = F \<circ> ((\<lambda>x. \<one>\<^bsub>A\<^esub>) \<circ> F')" by simp
    also have "\<dots> = F \<circ> (\<lambda>x. \<one>\<^bsub>A\<^esub>)" by (simp add: expand_fun_eq)
    also from F_F' A B have "\<dots> = (\<lambda>x. \<one>\<^bsub>B\<^esub>)" by (unfold iso_inv_compl_def iso_compl_def expand_fun_eq, auto) 
    (intro hom_completion_one, unfold group_def diff_group_def comm_group_def, simp_all)
    also have "\<dots> = (\<lambda>x. \<one>\<^bsub>?B'\<^esub>)" by simp
    finally show "differ\<^bsub>?B'\<^esub> \<circ> differ\<^bsub>?B'\<^esub> = (\<lambda>x. \<one>\<^bsub>?B'\<^esub>)" by simp
  qed
next
  from F_F' have F_F'_iso_compl: "(F, F') \<in> A \<cong>\<^bsub>invcompl\<^esub> ?B'"
    unfolding iso_inv_compl_def iso_compl_def completion_def expand_fun_eq hom_completion_def hom_def Pi_def completion_fun2_def by auto
  moreover have F_coherent: "F \<circ> diff A = diff ?B' \<circ> F"
  proof -
    have "diff A = diff A \<circ> completion A A id"
    proof (rule ext)
      fix x
      show "(differ\<^bsub>A\<^esub>) x = (differ\<^bsub>A\<^esub> \<circ> completion A A id) x"
      proof (cases "x \<in> carrier A")
	case True with diff_group.diff_hom [OF A] show "(differ\<^bsub>A\<^esub>) x = (differ\<^bsub>A\<^esub> \<circ> completion A A id) x" 
	  unfolding hom_completion_def completion_fun2_def completion_def by simp
      next
	case False with diff_group.diff_hom [OF A]
	have l_h_s: "(differ\<^bsub>A\<^esub>) x = \<one>\<^bsub>A\<^esub>" unfolding hom_completion_def completion_fun2_def completion_def by auto
	from False have "(completion A A id) x = \<one>\<^bsub>A\<^esub>" by (unfold completion_def, simp)
	with hom_completion_one [OF _ _ diff_group.diff_hom [OF A]] and A have r_h_s: "(differ\<^bsub>A\<^esub> \<circ> completion A A id) x = \<one>\<^bsub>A\<^esub>" 
	  unfolding diff_group_def comm_group_def group_def by simp
	from r_h_s and l_h_s show "(differ\<^bsub>A\<^esub>) x = (differ\<^bsub>A\<^esub> \<circ> completion A A id) x" by simp
      qed
    qed
    also from iso_inv_compl_id [OF F_F'] and o_assoc [of "diff A" F' F] have "\<dots> = diff A \<circ> F' \<circ> F" by simp
    finally have "diff A = diff A \<circ> F' \<circ> F" by simp
    with o_assoc [of F "diff A \<circ> F'" F] and o_assoc [of F "diff A" F'] show ?thesis by simp
  qed
  moreover have F'_coherent: "F' \<circ> diff ?B' = diff A \<circ> F'"
  proof -
    have "diff A = completion A A id \<circ> diff A"
    proof (rule ext)
      fix x
      show "(differ\<^bsub>A\<^esub>) x = (completion A A id \<circ> differ\<^bsub>A\<^esub>) x"
      proof (cases "x \<in> carrier A")
	case True with diff_group.diff_hom [OF A] and diff_group.diff_hom [OF A] 
	  and hom_completion_closed [of "diff A" A A x] show "(differ\<^bsub>A\<^esub>) x = (completion A A id \<circ> differ\<^bsub>A\<^esub>) x"
	  unfolding hom_completion_def completion_fun2_def completion_def by simp
      next
	case False with diff_group.diff_hom [OF A] have l_h_s: "(differ\<^bsub>A\<^esub>) x = \<one>\<^bsub>A\<^esub>" 
	  unfolding hom_completion_def completion_fun2_def completion_def by auto
	with l_h_s have r_h_s: "(completion A A id \<circ> differ\<^bsub>A\<^esub>) x = \<one>\<^bsub>A\<^esub>" unfolding completion_def by simp
	from r_h_s and l_h_s show "(differ\<^bsub>A\<^esub>) x = (completion A A id \<circ> differ\<^bsub>A\<^esub>) x" by simp
      qed
    qed
    also from iso_inv_compl_id [OF F_F'] and sym [OF o_assoc [of F' F "diff A"]] have "\<dots> = F' \<circ> F \<circ> diff A" by simp
    finally have "diff A = F' \<circ> F \<circ> diff A" by simp
    then show ?thesis by (auto simp add: o_assoc)
  qed
  ultimately show "(F, F') \<in> A \<cong>\<^bsub>invdiff\<^esub> ?B'" by (intro iso_inv_compl_coherent_iso_inv_diff)
qed

end