Theory lemma_2_2_19_local_nilpot

(*  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 ∈ hom_diff A B" and g: "g ∈ hom_diff B C"
  shows "g o f ∈ hom_diff A C"
  proof (unfold hom_diff_def hom_completion_def, auto)
  from f and g have f_compl: "f ∈ completion_fun2 A B" and g_compl: "g ∈ 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 o f ∈ 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 o f"], auto)
  next
  show "g o f ∈ hom A C"
  proof (intro homI)
  fix x
  assume x: "x ∈ carrier A" from hom_diff_closed [OF f x] and hom_diff_closed [OF g, of "f x"] show "(g o f) x ∈ carrier C" by simp
  next
  fix x y
  assume x: "x ∈ carrier A" and y: "y ∈ 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 o f) (x ⊗A y) = (g o f) x ⊗C (g o 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 "differA"] and o_assoc [of g "differB" f] 
  and o_assoc [of "differC" g f] show "g o f o differA = differC o (g o f)" by simp
  qed
  *)
  
lemma hom_diffs_comp_closed: includes diff_group A includes diff_group B includes diff_group C
  assumes f: "f ∈ hom_diff A B" and g: "g ∈ hom_diff B C"
  shows "g o f ∈ hom_diff A C"
proof (unfold hom_diff_def hom_completion_def, auto)
  from f and g have f_compl: "f ∈ completion_fun2 A B" and g_compl: "g ∈ 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 o f ∈ completion_fun2 A C"
    unfolding completion_fun2_def completion_def expand_fun_eq apply simp apply (intro exI [of _ "g o f"]) by auto
next
  show "g o f ∈ hom A C"
  proof (intro homI)
    fix x
    assume x: "x ∈ carrier A" from hom_diff_closed [OF f x] and hom_diff_closed [OF g, of "f x"] show "(g o f) x ∈ carrier C" by simp
  next
    fix x y
    assume x: "x ∈ carrier A" and y: "y ∈ 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 o f) (x ⊗A y) = (g o f) x ⊗C (g o 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 "differA"] and o_assoc [of g "differB" f] 
    and o_assoc [of "differC" g f] show "g o f o differA = differC o (g o 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') ∈ (C ≅invdiff B)"
  shows "reduction D B (F o f) (g o 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 o f ∈ 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 o F' ∈ hom_diff B D" by simp
next
  from h_hom_compl show "h ∈ hom_completion D D" by simp
next
  from sym [OF o_assoc [of F f "(g o F')"]] and o_assoc [of f g F'] and fg
  have "F o f o (g o F') = F o ((λx. if x ∈ carrier C then id x else \<one>C) o F')" by simp
  also from iso_inv_diff_iso_diff2 [OF F_F'_isom] and iso_diff_hom_diff [of F' B C] have "… = F o 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 "… = (λx. if x ∈ carrier B then id x else \<one>B)" unfolding completion_def by simp
  finally show "F o f o (g o F') = (λx. if x ∈ carrier B then id x else \<one>B)" by simp
next
  from sym [OF o_assoc [of g F' "(F o f)"]] and o_assoc [of F' F f] and iso_inv_diff_id [OF F_F'_isom]
  have "g o F' o (F o f) = g o ((λx. if x ∈ carrier C then id x else \<one>C) o f)" unfolding completion_def by simp
  also from f_hom_diff have "… = g o 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 o F' o (F o f) = g o f" by simp
  with gf_dh_hd show "(λx. if x ∈ carrier D then (g o F' o (F o f)) x 
    ⊗ (if x ∈ carrier D then (differ o h) x ⊗ (h o differ) x else \<one>) else \<one>) =
    (λx. if x ∈ 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 o f o h = F o (λx. if x ∈ carrier D then \<one>C else \<one>C)" 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 "… = (λx. if x ∈ carrier D then \<one>B else \<one>B)"
    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 o f o h = (λx. if x ∈ carrier D then \<one>B else \<one>B)" by simp
next
  from hg and o_assoc [of h g F'] have "h o (g o F') = (λx. if x ∈ carrier C then \<one> else \<one>) o F'" by simp
  also have "… = (λx. if x ∈ carrier B then \<one> else \<one>)" by (unfold expand_fun_eq, simp)
  finally show "h o (g o F') = (λx. if x ∈ carrier B then \<one> else \<one>)" by simp
next
  from hh show "h o h = (λx. if x ∈ carrier D then \<one> else \<one>)" by simp
qed

end