Theory IsomorphismClass

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

section "Isomorphism Classes"

text ‹
  The following is a small theory that facilitates working with isomorphism classes of objects
  in a category.
›

theory IsomorphismClass
imports Category3.EpiMonoIso Category3.NaturalTransformation
begin

  context category
  begin

    notation isomorphic (infix "" 50)

    definition iso_class ("_")
    where "iso_class f  {f'. f  f'}"

    definition is_iso_class
    where "is_iso_class F  f. f  F  F = iso_class f"

    definition iso_class_rep
    where "iso_class_rep F  SOME f. f  F"

    lemmas isomorphic_transitive [trans]
    lemmas naturally_isomorphic_transitive [trans]

    lemma inv_in_homI [intro]:
    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 iso_class_is_nonempty:
    assumes "is_iso_class F"
    shows "F  {}"
      using assms is_iso_class_def iso_class_def by auto

    lemma iso_class_memb_is_ide:
    assumes "is_iso_class F" and "f  F"
    shows "ide f"
      using assms is_iso_class_def iso_class_def isomorphic_def by auto

    lemma ide_in_iso_class:
    assumes "ide f"
    shows "f  f"
      using assms iso_class_def is_iso_class_def isomorphic_reflexive by simp

    lemma rep_in_iso_class:
    assumes "is_iso_class F"
    shows "iso_class_rep F  F"
      using assms is_iso_class_def iso_class_rep_def someI_ex [of "λf. f  F"]
            ide_in_iso_class
      by metis

    lemma is_iso_classI:
    assumes "ide f"
    shows "is_iso_class f"
      using assms iso_class_def is_iso_class_def isomorphic_reflexive by blast

    lemma rep_iso_class:
    assumes "ide f"
    shows "iso_class_rep f  f"
      using assms is_iso_classI rep_in_iso_class iso_class_def isomorphic_symmetric
      by blast

    lemma iso_class_elems_isomorphic:
    assumes "is_iso_class F" and "f  F" and "f'  F"
    shows "f  f'"
      using assms iso_class_def
      by (metis is_iso_class_def isomorphic_symmetric isomorphic_transitive mem_Collect_eq)

    lemma iso_class_eqI [intro]:
    assumes "f  g"
    shows "f = g"
    proof -
      have f: "ide f"
        using assms isomorphic_def by auto
      have g: "ide g"
        using assms isomorphic_def by auto
      have "f  g"
        using assms iso_class_def isomorphic_symmetric by simp
      moreover have "g  g"
        using assms g iso_class_def isomorphic_reflexive isomorphic_def by simp
      ultimately have "h. (h  f) = (h  g)"
        using assms g iso_class_def [of f] iso_class_def [of g]
              isomorphic_reflexive isomorphic_symmetric isomorphic_transitive
        by blast
      thus ?thesis by auto
    qed

    lemma iso_class_eq:
    assumes "is_iso_class F" and "is_iso_class G" and "F  G  {}"
    shows "F = G"
    proof -
      obtain h where h: "h  F  h  G"
        using assms by auto
      show ?thesis
        using assms h
        by (metis is_iso_class_def iso_class_elems_isomorphic iso_class_eqI)
    qed

    lemma iso_class_rep [simp]:
    assumes "is_iso_class F"
    shows "iso_class_rep F = F"
    proof (intro iso_class_eq)
      show "is_iso_class iso_class_rep F"
        using assms is_iso_classI iso_class_memb_is_ide rep_in_iso_class by blast
      show "is_iso_class F"
        using assms by simp
      show "iso_class_rep F  F  {}"
        using assms rep_in_iso_class
        by (meson disjoint_iff_not_equal ide_in_iso_class iso_class_memb_is_ide)
    qed

  end

end