Theory EpiMonoIso

(*  Title:       EpiMonoIso
    Author:      Eugene W. Stark <stark@cs.stonybrook.edu>, 2016
    Maintainer:  Eugene W. Stark <stark@cs.stonybrook.edu>
*)

chapter EpiMonoIso

theory EpiMonoIso
imports Category
begin

  text‹
    This theory defines and develops properties of epimorphisms, monomorphisms,
    isomorphisms, sections, and retractions.
›

  context category
  begin

     definition epi
     where "epi f = (arr f ∧ inj_on (λg. g ⋅ f) {g. seq g f})"

     definition mono
     where "mono f = (arr f ∧ inj_on (λg. f ⋅ g) {g. seq f g})"

     lemma epiI [intro]:
     assumes "arr f" and "⋀g g'. ⟦seq g f; seq g' f; g ⋅ f = g' ⋅ f⟧ ⟹ g = g'"
     shows "epi f"
       using assms epi_def inj_on_def by blast

     lemma epi_implies_arr:
     assumes "epi f"
     shows "arr f"
       using assms epi_def by auto

     (*
      * TODO: epiE and monoE don't need both seq hypotheses.
      * Also, they are not stated in the form of elimination rules.
      *)

     lemma epiE [elim]:
     assumes "epi f"
     and "seq g f" and "seq g' f" and "g ⋅ f = g' ⋅ f"
     shows "g = g'"
       using assms unfolding epi_def inj_on_def by blast
       
     lemma monoI [intro]:
     assumes "arr g" and "⋀f f'. ⟦seq g f; seq g f'; g ⋅ f = g ⋅ f'⟧ ⟹ f = f'"
     shows "mono g"
       using assms mono_def inj_on_def by blast

     lemma mono_implies_arr:
     assumes "mono f"
     shows "arr f"
       using assms mono_def by auto
       
     lemma monoE [elim]:
     assumes "mono g"
     and "seq g f" and "seq g f'" and "g ⋅ f = g ⋅ f'"
     shows "f' = f"
       using assms unfolding mono_def inj_on_def by blast

     definition inverse_arrows
     where "inverse_arrows f g ≡ ide (g ⋅ f) ∧ ide (f ⋅ g)"

     lemma inverse_arrowsI [intro]:
     assumes "ide (g ⋅ f)" and "ide (f ⋅ g)"
     shows "inverse_arrows f g"
       using assms inverse_arrows_def by blast

     lemma inverse_arrowsE [elim]:
     assumes "inverse_arrows f g"
     and "⟦ ide (g ⋅ f); ide (f ⋅ g) ⟧ ⟹ T"
     shows "T"
       using assms inverse_arrows_def by blast

     lemma inverse_arrows_sym:
       shows "inverse_arrows f g ⟷ inverse_arrows g f"
       using inverse_arrows_def by auto

     lemma ide_self_inverse:
     assumes "ide a"
     shows "inverse_arrows a a"
       using assms by auto

     lemma inverse_arrow_unique:
     assumes "inverse_arrows f g" and "inverse_arrows f g'"
     shows "g = g'"
       using assms apply (elim inverse_arrowsE)
       by (metis comp_cod_arr ide_compE comp_assoc seqE)

     lemma inverse_arrows_compose:
     assumes "seq g f" and "inverse_arrows f f'" and "inverse_arrows g g'"
     shows "inverse_arrows (g ⋅ f) (f' ⋅ g')"
       using assms apply (elim inverse_arrowsE, intro inverse_arrowsI)
        apply (metis seqE comp_arr_dom ide_compE comp_assoc)
       by (metis seqE comp_arr_dom ide_compE comp_assoc)

     definition "section"
     where "section f ≡ ∃g. ide (g ⋅ f)"

     lemma sectionI [intro]:
     assumes "ide (g ⋅ f)"
     shows "section f"
       using assms section_def by auto

     lemma sectionE [elim]:
     assumes "section f"
     obtains g where "ide (g ⋅ f)"
       using assms section_def by blast

     definition retraction
     where "retraction g ≡ ∃f. ide (g ⋅ f)"

     lemma retractionI [intro]:
     assumes "ide (g ⋅ f)"
     shows "retraction g"
       using assms retraction_def by auto

     lemma retractionE [elim]:
     assumes "retraction g"
     obtains f where "ide (g ⋅ f)"
       using assms retraction_def by blast
       
     lemma section_is_mono:
     assumes "section g"
     shows "mono g"
     proof
       show "arr g" using assms section_def by blast
       from assms obtain h where h: "ide (h ⋅ g)" by blast
       have hg: "seq h g" using h by auto
       thus "⋀f f'. ⟦seq g f; seq g f'; g ⋅ f = g ⋅ f'⟧ ⟹ f = f'"
         using hg h ide_compE seqE comp_assoc comp_cod_arr by metis
     qed

     lemma retraction_is_epi:
     assumes "retraction g"
     shows "epi g"
     proof
       show "arr g" using assms retraction_def by blast
       from assms obtain f where f: "ide (g ⋅ f)" by blast
       have gf: "seq g f" using f by auto
       thus "⋀h h'. ⟦seq h g; seq h' g; h ⋅ g = h' ⋅ g⟧ ⟹ h = h'"
         using gf f ide_compE seqE comp_assoc comp_arr_dom by metis
     qed

     lemma section_retraction_compose:
     assumes "ide (e ⋅ m)" and "ide (e' ⋅ m')" and "seq m' m"
     shows "ide ((e ⋅ e') ⋅ (m' ⋅ m))"
       using assms seqI seqE ide_compE comp_assoc comp_arr_dom by metis

     lemma sections_compose [intro]:
     assumes "section m" and "section m'" and "seq m' m"
     shows "section (m' ⋅ m)"
       using assms section_def section_retraction_compose by metis

     lemma retractions_compose [intro]:
     assumes "retraction e" and "retraction e'" and "seq e' e"
     shows "retraction (e' ⋅ e)"
     proof -
       from assms(1-2) obtain m m'
       where *: "ide (e ⋅ m) ∧ ide (e' ⋅ m')"
         using retraction_def by auto
       hence "seq m m'"
         using assms(3) by (metis seqE seqI ide_compE)
       with * show ?thesis
         using section_retraction_compose retractionI by blast
     qed
       
     lemma monos_compose [intro]:
     assumes "mono m" and "mono m'" and "seq m' m"
     shows "mono (m' ⋅ m)"
     proof -
       have "inj_on (λf. (m' ⋅ m) ⋅ f) {f. seq (m' ⋅ m) f}"
         unfolding inj_on_def
         using assms
         by (metis CollectD seqE monoE comp_assoc)
       thus ?thesis using assms(3) mono_def by force
     qed           

     lemma epis_compose [intro]:
     assumes "epi e" and "epi e'" and "seq e' e"
     shows "epi (e' ⋅ e)"
     proof -
       have "inj_on (λg. g ⋅ (e' ⋅ e)) {g. seq g (e' ⋅ e)}"
         unfolding inj_on_def
         using assms by (metis CollectD epiE match_2 comp_assoc)
       thus ?thesis using assms(3) epi_def by force
     qed           

     definition iso
     where "iso f ≡ ∃g. inverse_arrows f g"

     lemma isoI [intro]:
     assumes "inverse_arrows f g"
     shows "iso f"
       using assms iso_def by auto

     lemma isoE [elim]:
     assumes "iso f"
     obtains g where "inverse_arrows f g"
       using assms iso_def by blast

     lemma ide_is_iso [simp]:
     assumes "ide a"
     shows "iso a"
       using assms ide_self_inverse by auto

     lemma iso_is_arr:
     assumes "iso f"
     shows "arr f"
       using assms by blast

     lemma iso_is_section:
     assumes "iso f"
     shows "section f"
       using assms inverse_arrows_def by blast

     lemma iso_is_retraction:
     assumes "iso f"
     shows "retraction f"
       using assms inverse_arrows_def by blast

    lemma iso_iff_mono_and_retraction:
    shows "iso f ⟷ mono f ∧ retraction f"
    proof
      show "iso f ⟹ mono f ∧ retraction f"
        by (simp add: iso_is_retraction iso_is_section section_is_mono)
      show "mono f ∧ retraction f ⟹ iso f"
      proof -
        assume f: "mono f ∧ retraction f"
        from f obtain g where g: "ide (f ⋅ g)" by blast
        have "inverse_arrows f g"
          using f g comp_arr_dom comp_cod_arr comp_assoc inverse_arrowsI
          by (metis ide_char' ide_compE monoE mono_implies_arr)
        thus "iso f" by auto
      qed
    qed

    lemma iso_iff_section_and_epi:
    shows "iso f ⟷ section f ∧ epi f"
    proof
      show "iso f ⟹ section f ∧ epi f"
        by (simp add: iso_is_retraction iso_is_section retraction_is_epi)
      show "section f ∧ epi f ⟹ iso f"
      proof -
        assume f: "section f ∧ epi f"
        from f obtain g where g: "ide (g ⋅ f)" by blast
        have "inverse_arrows f g"
          using f g comp_arr_dom comp_cod_arr epi_implies_arr
                comp_assoc ide_compE inverse_arrowsI epiE ide_char'
          by metis
        thus "iso f" by auto
      qed
    qed

    lemma iso_iff_section_and_retraction:
    shows "iso f ⟷ section f ∧ retraction f"
      using iso_is_retraction iso_is_section iso_iff_mono_and_retraction section_is_mono
      by auto

    lemma isos_compose [intro]:
    assumes "iso f" and "iso f'" and "seq f' f"
    shows "iso (f' ⋅ f)"
    proof -
      from assms(1) obtain g where g: "inverse_arrows f g" by blast
      from assms(2) obtain g' where g': "inverse_arrows f' g'" by blast
      have "inverse_arrows (f' ⋅ f) (g ⋅ g')"
        using assms g g inverse_arrowsI inverse_arrowsE section_retraction_compose
        by (simp add: g' inverse_arrows_compose)
      thus ?thesis using iso_def by auto
    qed

    lemma iso_cancel_left:
    assumes "iso f" and "f ⋅ g = f ⋅ g'" and "seq f g"
    shows "g = g'"
      using assms iso_is_section section_is_mono monoE by metis

    lemma iso_cancel_right:
    assumes "iso g" and "f ⋅ g = f' ⋅ g" and "seq f g" and "iso g"
    shows "f = f'"
      using assms iso_is_retraction retraction_is_epi epiE by metis

    definition isomorphic
    where "isomorphic a a' = (∃f. «f : a → a'» ∧ iso f)"

    lemma isomorphicI [intro]:
    assumes "iso f"
    shows "isomorphic (dom f) (cod f)"
      using assms isomorphic_def iso_is_arr by blast

    lemma isomorphicE [elim]:
    assumes "isomorphic a a'"
    obtains f where "«f : a → a'» ∧ iso f"
      using assms isomorphic_def by meson

    definition iso_in_hom  (‹«_ : _ ≅ _»›)
    where "iso_in_hom f a b ≡ «f : a → b» ∧ iso f"

    lemma iso_in_homI [intro]:
    assumes "«f : a → b»" and "iso f"
    shows "«f : a ≅ b»"
      using assms iso_in_hom_def by simp

    lemma iso_in_homE [elim]:
    assumes "«f : a ≅ b»"
    and "⟦«f : a → b»; iso f⟧ ⟹ T"
    shows T
      using assms iso_in_hom_def by simp

    lemma isomorphicI':
    assumes "«f : a ≅ b»"
    shows "isomorphic a b"
      using assms iso_in_hom_def isomorphic_def by auto

    lemma ide_iso_in_hom:
    assumes "ide a"
    shows "«a : a ≅ a»"
      using assms by fastforce

    lemma comp_iso_in_hom [intro]:
    assumes "«f : a ≅ b»" and "«g : b ≅ c»"
    shows "«g ⋅ f : a ≅ c»"
      using assms iso_in_hom_def by auto

    definition inv
    where "inv f = (SOME g. inverse_arrows f g)"

    lemma inv_is_inverse:
    assumes "iso f"
    shows "inverse_arrows f (inv f)"
      using assms inv_def someI [of "inverse_arrows f"] by auto

    lemma iso_inv_iso [intro, simp]:
    assumes "iso f"
    shows "iso (inv f)"
      using assms inv_is_inverse inverse_arrows_sym by blast

    lemma inverse_unique:
    assumes "inverse_arrows f g"
    shows "inv f = g"
      using assms inv_is_inverse inverse_arrow_unique isoI by auto

    lemma inv_ide [simp]:
    assumes "ide a"
    shows "inv a = a"
      using assms by (simp add: inverse_arrowsI inverse_unique)

    lemma inv_inv [simp]:
    assumes "iso f"
    shows "inv (inv f) = f"
      using assms inverse_arrows_sym inverse_unique by blast

    lemma comp_arr_inv:
    assumes "inverse_arrows f g"
    shows "f ⋅ g = dom g"
      using assms by auto

    lemma comp_inv_arr:
    assumes "inverse_arrows f g"
    shows "g ⋅ f = dom f"
      using assms by auto

    lemma comp_arr_inv':
    assumes "iso f"
    shows "f ⋅ inv f = cod f"
      using assms inv_is_inverse by blast

    lemma comp_inv_arr':
    assumes "iso f"
    shows "inv f ⋅ f = dom f"
      using assms inv_is_inverse by blast

    lemma inv_in_hom [simp]:
    assumes "iso f" and "«f : a → b»"
    shows "«inv f : b → a»"
      using assms inv_is_inverse seqE inverse_arrowsE
      by (metis ide_compE in_homE in_homI)

    lemma arr_inv [simp]:
    assumes "iso f"
    shows "arr (inv f)"
      using assms inv_in_hom by blast

    lemma dom_inv [simp]:
    assumes "iso f"
    shows "dom (inv f) = cod f"
      using assms inv_in_hom by blast

    lemma cod_inv [simp]:
    assumes "iso f"
    shows "cod (inv f) = dom f"
      using assms inv_in_hom by blast

    lemma inv_comp:
    assumes "iso f" and "iso g" and "seq g f"
    shows "inv (g ⋅ f) = inv f ⋅ inv g"
      using assms inv_is_inverse inverse_unique inverse_arrows_compose inverse_arrows_def
      by meson

    lemma isomorphic_reflexive:
    assumes "ide f"
    shows "isomorphic f f"
      unfolding isomorphic_def
      using assms ide_is_iso ide_in_hom by blast

    lemma isomorphic_symmetric:
    assumes "isomorphic f g"
    shows "isomorphic g f"
      using assms inv_in_hom by blast

    lemma isomorphic_transitive [trans]:
    assumes "isomorphic f g" and "isomorphic g h"
    shows "isomorphic f h"
      using assms isomorphic_def isos_compose by auto

    text ‹
      A section or retraction of an isomorphism is in fact an inverse.
›

    lemma section_retraction_of_iso:
    assumes "iso f"
    shows "ide (g ⋅ f) ⟹ inverse_arrows f g"
    and "ide (f ⋅ g) ⟹ inverse_arrows f g"
    proof -
      show "ide (g ⋅ f) ⟹ inverse_arrows f g"
        using assms
        by (metis comp_inv_arr' epiE ide_compE inv_is_inverse iso_iff_section_and_epi)
      show "ide (f ⋅ g) ⟹ inverse_arrows f g"
        using assms
        by (metis ide_compE comp_arr_inv' inv_is_inverse iso_iff_mono_and_retraction monoE)
    qed

    text ‹
      A situation that occurs frequently is that we have a commuting triangle,
      but we need the triangle obtained by inverting one side that is an isomorphism.
      The following fact streamlines this derivation.
›

    lemma invert_side_of_triangle:
    assumes "arr h" and "f ⋅ g = h"
    shows "iso f ⟹ seq (inv f) h ∧ g = inv f ⋅ h"
    and "iso g ⟹ seq h (inv g) ∧ f = h ⋅ inv g"
    proof -
      show "iso f ⟹ seq (inv f) h ∧ g = inv f ⋅ h"
        by (metis assms seqE inv_is_inverse comp_cod_arr comp_inv_arr comp_assoc)
      show "iso g ⟹ seq h (inv g) ∧ f = h ⋅ inv g"
        by (metis assms seqE inv_is_inverse comp_arr_dom comp_arr_inv dom_inv comp_assoc)
    qed

    text ‹
      A similar situation is where we have a commuting square and we want to
      invert two opposite sides.
›

    lemma invert_opposite_sides_of_square:
    assumes "seq f g" and "f ⋅ g = h ⋅ k"
    shows "⟦ iso f; iso k ⟧ ⟹ seq g (inv k) ∧ seq (inv f) h ∧ g ⋅ inv k = inv f ⋅ h"
      by (metis assms invert_side_of_triangle comp_assoc)

    text ‹
      The following versions of ‹inv_comp› provide information needed for repeated
      application to a composition of more than two arrows and seem often to be more
      useful.
›

    lemma inv_comp_left:
    assumes "iso (g ⋅ f)" and "iso g"
    shows "inv (g ⋅ f) = inv f ⋅ inv g" and "iso f"
    proof -
      have 1: "inv f = inv (g ⋅ f) ⋅ g"
      proof -
        have "inv (g ⋅ f) ⋅ g = inv (g ⋅ f) ⋅ inv (inv g)"
         using assms by simp
        also have "... = inv (inv g ⋅ g ⋅ f)"
          using assms inv_comp iso_is_arr by simp
        also have "... = inv ((inv g ⋅ g) ⋅ f)"
          using comp_assoc by simp
        also have "... = inv f"
          using assms comp_ide_arr invert_side_of_triangle(1) iso_is_arr comp_assoc
          by metis
        finally show ?thesis by simp
      qed
      show "inv (g ⋅ f) = inv f ⋅ inv g"
        using assms 1 comp_arr_dom comp_assoc
        by (metis arr_inv cod_comp dom_inv invert_side_of_triangle(2) iso_is_arr seqI)
      show "iso f"
        using assms 1 comp_assoc inv_is_inverse
        by (metis arr_inv invert_side_of_triangle(1) inv_inv iso_inv_iso isos_compose)
    qed

    lemma inv_comp_right:
    assumes "iso (g ⋅ f)" and "iso f"
    shows "inv (g ⋅ f) = inv f ⋅ inv g" and "iso g"
    proof -
      have 1: "inv g = f ⋅ inv (g ⋅ f)"
      proof -
        have "f ⋅ inv (g ⋅ f) = inv (inv f) ⋅ inv (g ⋅ f)"
          using assms by simp
        also have "... = inv ((g ⋅ f) ⋅ inv f)"
          using assms inv_comp iso_is_arr by simp
        also have "... = inv (g ⋅ f ⋅ inv f)"
          using comp_assoc by simp
        also have "... = inv g"
          using assms comp_arr_dom invert_side_of_triangle(2) iso_is_arr comp_assoc
          by metis
        finally show ?thesis by simp
      qed
      show "inv (g ⋅ f) = inv f ⋅ inv g"
        using assms 1 comp_cod_arr comp_assoc
        by (metis arr_inv cod_inv dom_comp seqI invert_side_of_triangle(1) iso_is_arr)
      show "iso g"
        using assms 1 comp_assoc inv_is_inverse
        by (metis arr_inv invert_side_of_triangle(2) inv_inv iso_inv_iso isos_compose)
    qed

  end

end