Theory HomGroupsCompletion

(*  Title:      inst_locales/HomGroupsCompletion.thy
    ID:         $Id: HomGroupsCompletion.thy $
    Author:     Jesus Aransay
    Comments:   We prove that completion homomorphisms between two commutative groups form a commutative group
                with the given product
*)

theory HomGroupsCompletion 
  imports 
  HomGroupCompletion
  begin

subsection{*Homomorphisms seen as algebraic structures*}

text{*Homomorphisms with the underlying operation are closed*}

lemma hom_mult_completion_is_hom:
  includes comm_group G + comm_group G'
  shows "[|f : hom G G'; g : hom G G' |] ==> (%x. if x ∈  carrier G then f x ⊗2 g x else \<one>2) : hom G G'"
  apply (unfold hom_def, simp add: prems, auto simp add: Pi_def m_closed)
  apply (simp add: m_ac hom_completion_closed)
  done

lemma hom_completion_mult_is_hom_completion:
  includes comm_group G + comm_group G'
  assumes "f ∈ hom_completion G G'" and "g ∈ hom_completion G G'"
  shows "(λx. if x ∈ carrier G then f x ⊗G'  g x else \<one>G') ∈ hom_completion G G'"
proof (unfold hom_completion_def completion_fun2_def completion_def, simp, intro conjI)
  show " ∃ga. (λx. if x ∈ carrier G then f x ⊗G' g x else \<one>G') = (λx. if x ∈ carrier G then ga x else \<one>G')"
    by (rule exI [of _ "(λx. f x ⊗G' g x)"])(simp)
next
  from prems show "(λx. if x ∈ carrier G then f x ⊗G' g x else \<one>G') ∈ hom G G'"
    by (intro hom_mult_completion_is_hom, unfold comm_group_def hom_completion_def)(simp_all)
qed

text{*Proof of the existence of an inverse homomorphism*}

lemma hom_completions_mult_inv_is_hom_completion:
  includes comm_group G + comm_group G'
  assumes "f ∈ hom_completion G G'"
  shows "∃g∈hom_completion G G'. (λx. if x ∈ carrier G then g x ⊗G' f x else \<one>G') = (λx. \<one>G')"
proof (intro bexI [of _ "(λx. if x ∈ carrier G then invG' (f x) else \<one>G')"])
  show "(λg. if g ∈ carrier G then invG' f g else \<one>G') ∈ hom_completion G G'"
  proof (unfold hom_completion_def completion_fun2_def completion_def, simp, intro conjI)
    show "∃g. (λg. if g ∈ carrier G then invG' f g else \<one>G') = (λx. if x ∈ carrier G then g x else \<one>G')"
      by (rule exI [of _ "λx. invG' (f x)"], simp)
  next
    show "(λx. if x ∈ carrier G then invG' f x else \<one>G') ∈ hom G G'"
    proof (unfold hom_def, simp, intro conjI)
      from prems show "(λx. if x ∈ carrier G then invG' f x else \<one>G') ∈ carrier G -> carrier G'"
        by (unfold Pi_def hom_completion_def completion_fun2_def completion_def hom_def Pi_def, auto)
    next
      show "∀x∈carrier G. ∀y∈carrier G. invG' f (x ⊗ y) = invG' f x ⊗G' invG' f y"
      proof (intro ballI)
        fix x y
        assume "x ∈ carrier G" and "y ∈ carrier G"
        show "invG' f (x ⊗ y) = invG' f x ⊗G' invG' f y"
        proof -
          from prems have "f (x ⊗ y) = f x ⊗G' f y" by (intro hom_mult, unfold hom_completion_def, simp_all)
          then have "invG' f (x ⊗ y) = invG' (f x ⊗G' f y)" by simp
          also from prems have "… = invG' (f y) ⊗G' invG' (f x)"
            by (intro inv_mult_group) (unfold hom_completion_def hom_def Pi_def, simp_all)
          also from prems have "… = invG' (f x) ⊗G' invG' (f y)"
            by (intro m_comm)(unfold hom_completion_def hom_def Pi_def, simp_all)
          finally show ?thesis by simp
        qed
      qed
    qed
  qed
next
  from prems
  show "(λx. if x ∈ carrier G then (if x ∈ carrier G then invG' f x else \<one>G') ⊗G' f x else \<one>G') = (λx. \<one>G')"
    by (unfold hom_completion_def hom_def Pi_def, auto simp add: expand_fun_eq) 
qed
    
subsection{*Completion homomorphisms between two algebraic structures form a commutative group*}

lemma hom_completion_groups_mult_comm_group:
  includes comm_group G + comm_group G'                                        
  shows "comm_group (| carrier = hom_completion G G', mult = λf. λg. (λx. if x ∈ carrier G then f x ⊗2 g x else \<one>2),
  one = (λx. if x ∈ carrier G then \<one>2 else \<one>2)|)"
  (is "comm_group ?H_CO")
proof (intro comm_groupI)
  fix f g
  assume "f ∈ carrier ?H_CO" and "g ∈ carrier ?H_CO"
  from prems show "f ⊗?H_CO g ∈ carrier ?H_CO"
    by simp (intro hom_completion_mult_is_hom_completion, unfold comm_group_def, simp_all)
next
  show "\<one>?H_CO ∈ carrier ?H_CO"
  proof (unfold hom_completion_def completion_fun2_def completion_def, auto)
    show "∃g. (λx. \<one>G') = (λx. if x ∈ carrier G then g x else \<one>G')" by (intro exI [of _ "λx. \<one>G'"], simp)
  next
    show "(λx. \<one>G') ∈ hom G G'" by (unfold hom_def Pi_def, simp)
  qed
next
  fix x y z
  assume "x ∈ carrier ?H_CO" and "y ∈ carrier ?H_CO" and "z ∈ carrier ?H_CO"
  from prems show "x ⊗?H_CO y ⊗?H_CO z = x ⊗?H_CO (y ⊗?H_CO z)"
    by (auto simp add: expand_fun_eq hom_completion_def hom_def Pi_def) (rule m_assoc, simp_all)
next
  fix x y
  assume "x ∈ carrier ?H_CO" and "y ∈ carrier ?H_CO"
  from prems show "x ⊗?H_CO y = y ⊗?H_CO x"
    by (auto simp add: expand_fun_eq hom_completion_def hom_def Pi_def) (rule m_comm, simp_all)
next
  fix x
  assume "x ∈ carrier ?H_CO"
  from prems show "\<one>?H_CO⊗?H_CO x = x"
    by (auto simp add: expand_fun_eq hom_completion_def completion_fun2_def completion_def hom_def Pi_def)
next
  fix x
  assume "x ∈ carrier ?H_CO"
  from prems and hom_completions_mult_inv_is_hom_completion [of G G' x] show "∃y∈carrier ?H_CO. y ⊗?H_CO x = \<one>?H_CO"
    by (unfold comm_group_def, simp)
qed

subsection{*Previous facts about homomorphisms of differential structures*}

lemma hom_diff_mult_is_hom_diff:
  includes diff_group D + diff_group D'
  assumes "f ∈ hom_diff D D'" and "g ∈ hom_diff D D'"
  shows "(λx. if x ∈ carrier D then f x ⊗D'  g x else \<one>D') ∈ hom_diff D D'"
proof (unfold hom_diff_def hom_completion_def completion_fun2_def completion_def, simp, intro conjI)
  show " ∃ga. (λx. if x ∈ carrier D then f x ⊗D' g x else \<one>D') = (λx. if x ∈ carrier D then ga x else \<one>D')"
    by (rule exI [of _ "(λx. f x ⊗D' g x)"])(simp)
next
  from prems show "(λx. if x ∈ carrier D then f x ⊗D' g x else \<one>D') ∈ hom D D'"
    by (unfold hom_diff_def hom_completion_def hom_def Pi_def, auto simp add: m_ac)
next
  show "(λx. if x ∈ carrier D then f x ⊗D' g x else \<one>D') o differ = differD' o (λx. if x ∈ carrier D then f x ⊗D' g x else \<one>D')"
  proof (rule ext)
    fix x
    show "((λx. if x ∈ carrier D then f x ⊗D' g x else \<one>D') o differ) x = (differD' o (λx. if x ∈ carrier D then f x ⊗D' g x else \<one>D')) x"
    proof (cases "x ∈ carrier D")
      case True
      from prems show ?thesis
        by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def 
          completion_fun2_def completion_def hom_def Pi_def) (auto simp add: expand_fun_eq)
    next
      case False
      then show ?thesis
      proof (auto simp add: expand_fun_eq)
        show "f ((differ) x) ⊗D' g ((differ) x) = (differD') \<one>D'"
        proof -
          from prems have l_h_s_1: "f ((differ) x) = \<one>D'"
            by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def completion_fun2_def completion_def, 
              auto) (intro group_hom.hom_one, unfold comm_group_def group_hom_def group_hom_axioms_def hom_def Pi_def, simp)
          moreover from prems have l_h_s_2: "g ((differ) x) = \<one>D'" 
            by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def completion_fun2_def completion_def, 
              auto) (intro group_hom.hom_one, unfold comm_group_def group_hom_def group_hom_axioms_def hom_def Pi_def, simp)
          moreover from prems have r_h_s: "(differD') \<one>D' =  \<one>D'"
            by (intro group_hom.hom_one)(unfold diff_group_def comm_group_def group_hom_def group_hom_axioms_def diff_group_axioms_def 
            hom_diff_def hom_completion_def, simp)
          ultimately show ?thesis by simp
        qed
      next
        show "\<one>D' = (differD') \<one>D'"
        proof (rule sym, intro group_hom.hom_one)
          from prems show "group_hom D' D' (differD')"
            by (unfold diff_group_def comm_group_def group_hom_def group_hom_axioms_def diff_group_axioms_def hom_diff_def 
              hom_completion_def, simp)
        qed
      qed
    qed
  qed
qed

lemma hom_diff_mult_inv_is_hom_diff:
  includes diff_group D + diff_group D'
  assumes "f ∈ hom_diff D D'"
  shows "∃g∈hom_diff D D'. (λx. if x ∈ carrier D then g x ⊗D' f x else \<one>D') = (λx. \<one>D')"
proof (intro bexI [of _ "(λx. if x ∈ carrier D then invD' (f x) else \<one>D')"])
  show "(λg. if g ∈ carrier D then invD' f g else \<one>D') ∈ hom_diff D D'"
  proof (unfold hom_diff_def hom_completion_def completion_fun2_def completion_def, simp, intro conjI)
    show "∃g. (λg. if g ∈ carrier D then invD' f g else \<one>D') = (λx. if x ∈ carrier D then g x else \<one>D')"
      by (rule exI [of _ "λx. invD' (f x)"], simp)
  next
    show "(λx. if x ∈ carrier D then invD' f x else \<one>D') ∈ hom D D'"
    proof (unfold hom_def, simp, intro conjI)
      from prems show "(λx. if x ∈ carrier D then invD' f x else \<one>D') ∈ carrier D -> carrier D'"
        by (unfold hom_diff_def hom_completion_def completion_fun2_def completion_def hom_def Pi_def, auto)
    next
      show "∀x∈carrier D. ∀y∈carrier D. invD' f (x ⊗ y) = invD' f x ⊗D' invD' f y"
      proof (intro ballI)
        fix x y
        assume "x ∈ carrier D" and "y ∈ carrier D"
        show "invD' f (x ⊗ y) = invD' f x ⊗D' invD' f y"
        proof -
          from prems have "f (x ⊗ y) = f x ⊗D' f y" by (intro hom_mult, unfold hom_diff_def hom_completion_def, simp_all)
          then have "invD' f (x ⊗ y) = invD' (f x ⊗D' f y)" by simp
          also from prems have "… = invD' (f y) ⊗D' invD' (f x)"
            by (intro inv_mult_group) (unfold hom_diff_def hom_completion_def hom_def Pi_def, simp_all)
          also from prems have "… = invD' (f x) ⊗D' invD' (f y)"
            by (intro m_comm)(unfold hom_diff_def hom_completion_def hom_def Pi_def, simp_all)
          finally show ?thesis by simp
        qed
      qed
    qed
  next
    show "(λg. if g ∈ carrier D then invD' f g else \<one>D') o differ = differD' o (λg. if g ∈ carrier D then invD' f g else \<one>D')"
    proof (simp add: expand_fun_eq, intro allI impI conjI)
      fix x
      assume "x ∈ carrier D"
      show "invD' f ((differ) x) = (differD') (invD' f x)"
      proof -
          (*We prove that f ((differ) x) is the opposite of both inv f ((differ) x) and (differ) (inv f x)*)
        have "(invD' f ((differ) x) = (differD') (invD' f x)) = (invD' f ((differ) x) ⊗D' f ((differ) x) = (differD') (invD' f x) 
          ⊗D' f ((differ) x))"
        proof (rule sym, rule r_cancel)
          from prems show "f ((differ) x) ∈ carrier D'"
            by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def hom_def Pi_def, simp)
        next
          from prems show "invD' f ((differ) x) ∈ carrier D'"
            by (intro inv_closed)(unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def hom_def Pi_def, simp)
        next
          from prems show "(differD') (invD' f x) ∈ carrier D'"
            by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def hom_def Pi_def, simp)
        qed
        also have "(invD' f ((differ) x) ⊗D' f ((differ) x) = (differD') (invD' f x) ⊗D' f ((differ) x))"
        proof -
          have l_h: "invD' f ((differ) x) ⊗D'  f ((differ) x) = \<one>D'"
          proof (rule l_inv)
            from prems show "f ((differ) x) ∈ carrier D'"
              by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def hom_def Pi_def, simp)
          qed
          moreover have r_h: "(differD') (invD' f x) ⊗D' f ((differ) x) = \<one>D'"
          proof -
            have "(differD') (invD' f x) ⊗D' f ((differ) x) = (differD') (invD' f x) ⊗D' (differD') (f x)"
            proof -
              from prems have "f ((differ) x) = (differD') (f x)"
                by (unfold diff_group_axioms_def hom_diff_def hom_completion_def hom_def Pi_def, simp add: expand_fun_eq)
              then show ?thesis by simp
            qed
            also have "… = (differD') (invD' f x ⊗D' f x)"
            proof (rule sym, rule hom_mult)
              from prems show "differD' ∈ hom D' D'"
                by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def, simp)
            next
              from prems show "invD' f x ∈ carrier D'"
                by (intro inv_closed, unfold hom_diff_def hom_completion_def hom_def Pi_def, simp)
            next
              from prems show "f x ∈ carrier D'"
                by (unfold hom_diff_def hom_completion_def hom_def Pi_def, simp)
            qed
            also have "… = (differD') (\<one>D')"
            proof -
              from prems have "invD' f x ⊗D' f x = \<one>D'"
                by (intro l_inv, unfold hom_diff_def hom_completion_def hom_def Pi_def, simp)
              then show ?thesis by simp
            qed
            also from prems have "… = \<one>D'"
            proof (intro group_hom.hom_one, unfold diff_group_def comm_group_def group_hom_def group_hom_axioms_def, intro conjI, simp_all)
              from prems show "differD' ∈ hom D' D'"
                by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def, simp)
            qed
            finally show ?thesis by simp
          qed
          ultimately show ?thesis by simp
        qed
        finally show ?thesis by simp
      qed
    next
        (*The following cases are the non meaningful ones, for instance, when x ∉ carrier D and so*)
      fix x
      assume "x ∈ carrier D" and "(differ) x ∉ carrier D"
        (*From these premises a contradiction follows*)
      from prems show "\<one>D' = (differD') (invD' f x)"
        by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def hom_def Pi_def, simp)
    next
      fix x
      assume "x ∉ carrier D"
      from prems show "invD' f ((differ) x) = (differD') \<one>D'"
      proof - 
        have l_h: "invD' f ((differ) x) = \<one>D'"
        proof -
          from prems have "invD' f ((differ) x) = invD' f (\<one>)"
            by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def completion_fun2_def completion_def Pi_def, auto)
          also have "… = invD' \<one>D'"
          proof -
            from prems have "f \<one> = \<one>D'"
              by (intro group_hom.hom_one) (unfold diff_group_def comm_group_def group_hom_def group_hom_axioms_def hom_diff_def hom_completion_def, auto)
            then show ?thesis by simp
          qed
          also have "… = \<one>D'"
            by (rule inv_one)
          finally show ?thesis by simp
        qed
        moreover from prems have r_h: "(differD') \<one>D' = \<one>D'"
          by (intro group_hom.hom_one)
        (unfold diff_group_def diff_group_axioms_def comm_group_def group_hom_def group_hom_axioms_def hom_diff_def hom_completion_def, auto)
        ultimately show ?thesis by simp
      qed
    next
      show "\<one>D' = (differD') \<one>D'"
      proof (rule sym, intro group_hom.hom_one)
        from prems show "group_hom D' D' (differD')"
          by (unfold diff_group_def comm_group_def diff_group_axioms_def group_hom_def group_hom_axioms_def hom_diff_def hom_completion_def, auto)
      qed
    qed
  qed
next
  from prems show "(λx. if x ∈ carrier D then (if x ∈ carrier D then invD' f x else \<one>D') ⊗D' f x else \<one>D') = (λx. \<one>D')"
    by (unfold hom_diff_def hom_completion_def hom_def Pi_def, auto simp add: expand_fun_eq) 
qed

text{*The set of completion differential homomorphisms between two differential groups are a commutative group*}

lemma hom_diff_groups_mult_comm_group:
  includes diff_group D + diff_group D'                                        
  shows "comm_group (| carrier = hom_diff D D', mult = λf. λg. (λx. if x ∈ carrier D then f x ⊗2 g x else \<one>2),
  one = (λx. if x ∈ carrier D then \<one>2 else \<one>2)|)"
  (is "comm_group ?H_DI")
proof (intro comm_groupI)
  fix f g
  assume "f ∈ carrier ?H_DI" and "g ∈ carrier ?H_DI"
  from prems and hom_diff_mult_is_hom_diff [of D D' f g] show "f ⊗?H_DI g ∈ carrier ?H_DI"
    by (unfold diff_group_def, simp)
next
  show "\<one>?H_DI ∈ carrier ?H_DI"
  proof (unfold hom_diff_def hom_completion_def completion_fun2_def completion_def, auto)
    show "∃g. (λx. \<one>D') = (λx. if x ∈ carrier D then g x else \<one>D')"
      by (intro exI [of _ "λx. \<one>D'"], simp)
  next
    show "(λx. \<one>D') ∈ hom D D'"
      by (unfold hom_def Pi_def, simp)
  next
    from prems show "(λx. \<one>D') o differ = differD' o (λx. \<one>D')"
      by (auto simp add: expand_fun_eq) (rule sym, intro group_hom.hom_one,
        unfold diff_group_def comm_group_def group_hom_def group_hom_axioms_def diff_group_axioms_def hom_diff_def hom_completion_def, simp)
  qed
next
  fix x y z
  assume "x ∈ carrier ?H_DI" and "y ∈ carrier ?H_DI" and "z ∈ carrier ?H_DI"
  from prems show "x ⊗?H_DI y ⊗?H_DI z = x ⊗?H_DI (y ⊗?H_DI z)"
    by (auto simp add: expand_fun_eq hom_diff_def hom_completion_def hom_def Pi_def) (rule m_assoc, simp_all)
next
  fix x y
  assume "x ∈ carrier ?H_DI" and "y ∈ carrier ?H_DI"
  from prems show "x ⊗?H_DI y = y ⊗?H_DI x"
    by (auto simp add: expand_fun_eq hom_diff_def hom_completion_def hom_def Pi_def) (rule m_comm, simp_all)
next
  fix x
  assume "x ∈ carrier ?H_DI"
  from prems show "\<one> ?H_DI ⊗?H_DI x = x"
    by (auto simp add: expand_fun_eq hom_diff_def hom_completion_def completion_fun2_def completion_def hom_def Pi_def)
next
  fix x
  assume "x ∈ carrier ?H_DI"
    (*When we omit the G G' in the instantiation, the premises monoid G monoid G' are lost. Why?*)
  from prems and hom_diff_mult_inv_is_hom_diff [of D D' x] show "∃y∈carrier ?H_DI. y ⊗?H_DI x = \<one> ?H_DI "
    by (unfold diff_group_def, simp)
qed

text{*The following result has been already proved in @{thm [locale=diff_group] hom_diff_mult_comm_group};
    now that we have provided a proof of a similar result but for two different differential groups, @{term D} and @{term D'}, 
    it can be trivially proved for the case @{term "D = D'"}*}

lemma (in diff_group) hom_diff_group_mult_comm_group_inst:
  shows "comm_group (| carrier = hom_diff D D, mult = λf. λg. (λx. if x ∈ carrier D then f x ⊗ g x else \<one>),
  one = (λx. if x ∈ carrier D then \<one> else \<one>)|)"
  using prems hom_diff_groups_mult_comm_group [of D D] by simp

end