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

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

theory lemma_2_2_19_local_nilpot 
  imports 
  lemma_2_2_18_local_nilpot
begin

text{*@{text "Lemma 2.2.19"}, as well as @{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 definition of reduction is used*}

lemma (in diff_group) diff_group_is_group: shows "group D" using prems unfolding diff_group_def comm_group_def by simp

  (*lemma hom_diffs_comp_closed: assumes A: "diff_group A" and B: "diff_group B" and C: "diff_group C"
  and f: "f \<in> hom_diff A B" and g: "g \<in> hom_diff B C"
  shows "g \<circ> f \<in> hom_diff A C"
  proof (unfold hom_diff_def hom_completion_def, auto)
  from f and g have f_compl: "f \<in> completion_fun2 A B" and g_compl: "g \<in> completion_fun2 B C"  
  by (unfold hom_diff_def hom_completion_def, auto)
  with A B C f and hom_diff_is_hom_completion [OF g] and hom_completion_one [of B C g] and completion_closed2 [OF f_compl]
  show "g \<circ> f \<in> completion_fun2 A C"
  by (unfold completion_fun2_def completion_def expand_fun_eq group_def comm_group_def diff_group_def hom_diff_def, 
  simp, intro exI [of _ "g \<circ> f"], auto)
  next
  show "g \<circ> f \<in> hom A C"
  proof (intro homI)
  fix x
  assume x: "x \<in> carrier A" from hom_diff_closed [OF f x] and hom_diff_closed [OF g, of "f x"] show "(g \<circ> f) x \<in> carrier C" by simp
  next
  fix x y
  assume x: "x \<in> carrier A" and y: "y \<in> carrier A" from f g and hom_diff_mult [OF f x y] and hom_diff_mult [OF g, of "f x" "f y"]  
  and hom_diff_closed [OF f x] hom_diff_closed [OF f y] show "(g \<circ> f) (x \<otimes>\<^bsub>A\<^esub> y) = (g \<circ> f) x \<otimes>\<^bsub>C\<^esub> (g \<circ> f) y" by (unfold hom_diff_def, simp)
  qed
  next
  from hom_diff_coherent [OF f] and hom_diff_coherent [OF g] and o_assoc [of g f "differ\<^bsub>A\<^esub>"] and o_assoc [of g "differ\<^bsub>B\<^esub>" f] 
  and o_assoc [of "differ\<^bsub>C\<^esub>" g f] show "g \<circ> f \<circ> differ\<^bsub>A\<^esub> = differ\<^bsub>C\<^esub> \<circ> (g \<circ> f)" by simp
  qed
  *)
  
lemma hom_diffs_comp_closed: includes diff_group A includes diff_group B includes diff_group C
  assumes f: "f \<in> hom_diff A B" and g: "g \<in> hom_diff B C"
  shows "g \<circ> f \<in> hom_diff A C"
proof (unfold hom_diff_def hom_completion_def, auto)
  from f and g have f_compl: "f \<in> completion_fun2 A B" and g_compl: "g \<in> completion_fun2 B C"  
    unfolding hom_diff_def hom_completion_def by auto
  with A.diff_group_is_group B.diff_group_is_group C.diff_group_is_group hom_diff_is_hom_completion [OF f] 
    and hom_diff_is_hom_completion [OF g] and hom_completion_one [of B C g] and completion_closed2 [OF f_compl]
  show "g \<circ> f \<in> completion_fun2 A C"
    unfolding completion_fun2_def completion_def expand_fun_eq apply simp apply (intro exI [of _ "g \<circ> f"]) by auto
next
  show "g \<circ> f \<in> hom A C"
  proof (intro homI)
    fix x
    assume x: "x \<in> carrier A" from hom_diff_closed [OF f x] and hom_diff_closed [OF g, of "f x"] show "(g \<circ> f) x \<in> carrier C" by simp
  next
    fix x y
    assume x: "x \<in> carrier A" and y: "y \<in> carrier A" from f g and hom_diff_mult [OF f x y] and hom_diff_mult [OF g, of "f x" "f y"]  
      and hom_diff_closed [OF f x] hom_diff_closed [OF f y] show "(g \<circ> f) (x \<otimes>\<^bsub>A\<^esub> y) = (g \<circ> f) x \<otimes>\<^bsub>C\<^esub> (g \<circ> f) y" by (unfold hom_diff_def, simp)
  qed
next
  from hom_diff_coherent [OF f] and hom_diff_coherent [OF g] and o_assoc [of g f "differ\<^bsub>A\<^esub>"] and o_assoc [of g "differ\<^bsub>B\<^esub>" f] 
    and o_assoc [of "differ\<^bsub>C\<^esub>" g f] show "g \<circ> f \<circ> differ\<^bsub>A\<^esub> = differ\<^bsub>C\<^esub> \<circ> (g \<circ> f)" by simp
qed

subsection{*Lemma 2.2.19*}

text{*The following lemma corresponds to @{text "Lemma 2.2.19"} as stated in Aransay's memoir*}

lemma (in reduction) lemma_2_2_19: assumes B: "diff_group B" and F_F'_isom: "(F, F') \<in> (C \<cong>\<^bsub>invdiff\<^esub> B)"
  shows "reduction D B (F \<circ> f) (g \<circ> F') h"
proof (intro reductionI)
  from prems show "diff_group D" by (unfold reduction_def, simp)
  from B show "diff_group B" by simp
next
  from hom_diffs_comp_closed [OF D_diff_group C_diff_group B f_hom_diff, of F] and iso_diff_hom_diff [of F C B] 
    and iso_inv_diff_iso_diff [OF F_F'_isom] show "F \<circ> f \<in> hom_diff D B" by simp
next
  from hom_diffs_comp_closed [OF B C_diff_group D_diff_group _ g_hom_diff, of F'] and iso_diff_hom_diff [of F' B C] 
    and iso_inv_diff_iso_diff2 [OF F_F'_isom] show "g \<circ> F' \<in> hom_diff B D" by simp
next
  from h_hom_compl show "h \<in> hom_completion D D" by simp
next
  from sym [OF o_assoc [of F f "(g \<circ> F')"]] and o_assoc [of f g F'] and fg
  have "F \<circ> f \<circ> (g \<circ> F') = F \<circ> ((\<lambda>x. if x \<in> carrier C then id x else \<one>\<^bsub>C\<^esub>) \<circ> F')" by simp
  also from iso_inv_diff_iso_diff2 [OF F_F'_isom] and iso_diff_hom_diff [of F' B C] have "\<dots> = F \<circ> F'"
    unfolding hom_diff_def hom_completion_def completion_fun2_def completion_def hom_def Pi_def expand_fun_eq by auto
  also from iso_inv_diff_id2 [OF F_F'_isom] have "\<dots> = (\<lambda>x. if x \<in> carrier B then id x else \<one>\<^bsub>B\<^esub>)" unfolding completion_def by simp
  finally show "F \<circ> f \<circ> (g \<circ> F') = (\<lambda>x. if x \<in> carrier B then id x else \<one>\<^bsub>B\<^esub>)" by simp
next
  from sym [OF o_assoc [of g F' "(F \<circ> f)"]] and o_assoc [of F' F f] and iso_inv_diff_id [OF F_F'_isom]
  have "g \<circ> F' \<circ> (F \<circ> f) = g \<circ> ((\<lambda>x. if x \<in> carrier C then id x else \<one>\<^bsub>C\<^esub>) \<circ> f)" unfolding completion_def by simp
  also from f_hom_diff have "\<dots> = g \<circ> f" 
    unfolding hom_diff_def hom_completion_def completion_fun2_def completion_def hom_def Pi_def expand_fun_eq by auto
  finally have "g \<circ> F' \<circ> (F \<circ> f) = g \<circ> f" by simp
  with gf_dh_hd show "(\<lambda>x. if x \<in> carrier D then (g \<circ> F' \<circ> (F \<circ> f)) x 
    \<otimes> (if x \<in> carrier D then (differ \<circ> h) x \<otimes> (h \<circ> differ) x else \<one>) else \<one>) =
    (\<lambda>x. if x \<in> carrier D then id x else \<one>)" by (simp only: expand_fun_eq) simp
next
  from fh and sym [OF o_assoc [of F f h]] have "F \<circ> f \<circ> h = F \<circ> (\<lambda>x. if x \<in> carrier D then \<one>\<^bsub>C\<^esub> else \<one>\<^bsub>C\<^esub>)" by simp
  also from B and iso_diff_hom_diff [of F C B] and iso_inv_diff_iso_diff [OF F_F'_isom] and C_diff_group
  have "\<dots> = (\<lambda>x. if x \<in> carrier D then \<one>\<^bsub>B\<^esub> else \<one>\<^bsub>B\<^esub>)"
    by (unfold expand_fun_eq, simp) (intro hom_completion_one, unfold hom_diff_def diff_group_def comm_group_def group_def, auto)
  finally show "F \<circ> f \<circ> h = (\<lambda>x. if x \<in> carrier D then \<one>\<^bsub>B\<^esub> else \<one>\<^bsub>B\<^esub>)" by simp
next
  from hg and o_assoc [of h g F'] have "h \<circ> (g \<circ> F') = (\<lambda>x. if x \<in> carrier C then \<one> else \<one>) \<circ> F'" by simp
  also have "\<dots> = (\<lambda>x. if x \<in> carrier B then \<one> else \<one>)" by (unfold expand_fun_eq, simp)
  finally show "h \<circ> (g \<circ> F') = (\<lambda>x. if x \<in> carrier B then \<one> else \<one>)" by simp
next
  from hh show "h \<circ> h = (\<lambda>x. if x \<in> carrier D then \<one> else \<one>)" by simp
qed

end