Theory lemma_2_2_18_local_nilpot

Up to index of Isabelle/HOL/HOL-Algebra/BPL

theory lemma_2_2_18_local_nilpot
imports lemma_2_2_17_local_nilpot
begin
(*  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 ∈ hom_completion A B" and g: "g ∈ hom_completion B C"
  shows "g o f ∈ hom_completion A C"
  using f g
  apply (unfold hom_completion_def hom_def Pi_def, auto)
  apply (unfold completion_fun2_def completion_def, simp)
  apply (intro exI [of _ "g o f"], auto simp add: expand_fun_eq)
  apply (rule group_hom.hom_one, unfold group_hom_def group_hom_axioms_def hom_def Pi_def, simp add: prems)
  done

lemma iso_inv_compl_coherent_iso_inv_diff: assumes fg: "(f, g) ∈ (F ≅invcompl G)" and f_coherent: "f o diff F = diff G o f"
  and g_coherent: "g o diff G = diff F o g" shows "(f, g) ∈ (F ≅invdiff G)"
  using fg and f_coherent and g_coherent by (unfold iso_inv_diff_def iso_inv_compl_def iso_diff_def iso_compl_def hom_diff_def, 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 ∧ comm_monoid G"} is obtained,
  which unfolded again produces @{term [locale=group] "group_axioms G ∧ monoid G ∧ comm_monoid_axioms G ∧ monoid G"}, which is redundant.
  Two possible solutions would be to define @{term [locale=group] "comm_group G = group G ∧ comm_monoid_axioms G"} or also
  @{term [locale=group] "comm_group G = group_axioms G ∧ comm_monoid G"}*}

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

end

lemma hom_completion_comp_closed: 

  [| group A; group B; group C; f ∈ hom_completion A B; g ∈ hom_completion B C |]
  ==> g o f ∈ hom_completion A C

lemma iso_inv_compl_coherent_iso_inv_diff: 

  [| (f, g) ∈ F ≅invcompl G; f o differF = differG o f;
     g o differG = differF o g |]
  ==> (f, g) ∈ F ≅invdiff G

Lemma 2.2.18

lemma lemma_2_2_18(1): 

  [| diff_group A; comm_group B; (F, F') ∈ A ≅invcompl B |]
  ==> diff_group
       (| carrier = carrier B, mult = op ⊗B, one = \<one>B,
          diff = F o differA o F', ... = () |)

and lemma_2_2_18(2): 

  [| diff_group A; comm_group B; (F, F') ∈ A ≅invcompl B |]
  ==> (F, F')
      ∈ A ≅invdiff
        (| carrier = carrier B, mult = op ⊗B, one = \<one>B,
           diff = F o differA o F', ... = () |)