Theory ProductCategory

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

chapter ProductCategory

theory ProductCategory
imports Category EpiMonoIso
begin

  text‹
    This theory defines the product of two categories @{term C1} and @{term C2},
    which is the category @{term C} whose arrows are ordered pairs consisting of an
    arrow of @{term C1} and an arrow of @{term C2}, with composition defined
    componentwise.  As the ordered pair (C1.null, C2.null)› is available
    to serve as C.null›, we may directly identify the arrows of the product
    category @{term C} with ordered pairs, leaving the type of arrows of @{term C}
    transparent.
›

  locale product_category =
    C1: category C1 +
    C2: category C2
  for C1 :: "'a1 comp"      (infixr 1 55)
  and C2 :: "'a2 comp"      (infixr 2 55)
  begin

    type_synonym ('aa1, 'aa2) arr = "'aa1 * 'aa2"

    notation C1.in_hom      («_ : _ 1 _»)
    notation C2.in_hom      («_ : _ 2 _»)

    abbreviation (input) Null :: "('a1, 'a2) arr"
    where "Null  (C1.null, C2.null)"

    abbreviation (input) Arr :: "('a1, 'a2) arr  bool"
    where "Arr f  C1.arr (fst f)  C2.arr (snd f)"

    abbreviation (input) Ide :: "('a1, 'a2) arr  bool"
    where "Ide f  C1.ide (fst f)  C2.ide (snd f)"

    abbreviation (input) Dom :: "('a1, 'a2) arr  ('a1, 'a2) arr"
    where "Dom f  (if Arr f then (C1.dom (fst f), C2.dom (snd f)) else Null)"

    abbreviation (input) Cod :: "('a1, 'a2) arr  ('a1, 'a2) arr"
    where "Cod f  (if Arr f then (C1.cod (fst f), C2.cod (snd f)) else Null)"

    definition comp :: "('a1, 'a2) arr  ('a1, 'a2) arr  ('a1, 'a2) arr"
    where "comp g f = (if Arr f  Arr g  Cod f = Dom g then
                         (C1 (fst g) (fst f), C2 (snd g) (snd f))
                       else Null)"

    notation comp      (infixr  55)

    lemma not_Arr_Null:
    shows "¬Arr Null"
      by simp

    interpretation partial_composition comp
    proof
      show "∃!n. f. n  f = n  f  n = n"
      proof
        let ?P = "λn. f. n  f = n  f  n = n"
        show 1: "?P Null" using comp_def not_Arr_Null by metis
        thus "n. f. n  f = n  f  n = n  n = Null" by metis
      qed
    qed

    notation in_hom  («_ : _  _»)

    lemma null_char [simp]:
    shows "null = Null"
    proof -
      let ?P = "λn. f. n  f = n  f  n = n"
      have "?P Null" using comp_def not_Arr_Null by metis
      thus ?thesis
        unfolding null_def using the1_equality [of ?P Null] ex_un_null by blast
    qed

    lemma ide_Ide:
    assumes "Ide a"
    shows "ide a"
      unfolding ide_def comp_def null_char
      using assms C1.not_arr_null C1.ide_in_hom C1.comp_arr_dom C1.comp_cod_arr
            C2.comp_arr_dom C2.comp_cod_arr
      by auto

    lemma has_domain_char:
    shows "domains f  {}  Arr f"
    proof
      show "domains f  {}  Arr f"
        unfolding domains_def comp_def null_char by (auto; metis)
      assume f: "Arr f"
      show "domains f  {}"
      proof -
        have "ide (Dom f)  comp f (Dom f)  null"
          using f comp_def ide_Ide C1.comp_arr_dom C1.arr_dom_iff_arr C2.arr_dom_iff_arr
          by auto
        thus ?thesis using domains_def by blast
      qed
    qed

    lemma has_codomain_char:
    shows "codomains f  {}  Arr f"
    proof
      show "codomains f  {}  Arr f"
        unfolding codomains_def comp_def null_char by (auto; metis)
      assume f: "Arr f"
      show "codomains f  {}"
      proof -
        have "ide (Cod f)  comp (Cod f) f  null"
          using f comp_def ide_Ide C1.comp_cod_arr C1.arr_cod_iff_arr C2.arr_cod_iff_arr
          by auto
        thus ?thesis using codomains_def by blast
      qed
    qed

    lemma arr_char [iff]:
    shows "arr f  Arr f"
      using has_domain_char has_codomain_char arr_def by simp

    lemma arrIPC [intro]:
    assumes "C1.arr f1" and "C2.arr f2"
    shows "arr (f1, f2)"
      using assms by simp

    lemma arrE:
    assumes "arr f"
    and "C1.arr (fst f)  C2.arr (snd f)  T"
    shows "T"
      using assms by auto

    lemma seqIPC [intro]:
    assumes "C1.seq g1 f1  C2.seq g2 f2"
    shows "seq (g1, g2) (f1, f2)"
      using assms comp_def by auto

    lemma seqEPC [elim]:
    assumes "seq g f"
    and "C1.seq (fst g) (fst f)  C2.seq (snd g) (snd f)  T"
    shows "T"
      using assms comp_def
      by (metis (no_types, lifting) C1.seqI C2.seqI Pair_inject not_arr_null null_char)

    lemma seq_char [iff]:
    shows "seq g f  C1.seq (fst g) (fst f)  C2.seq (snd g) (snd f)"
      using comp_def by auto

    lemma Dom_comp:
    assumes "seq g f"
    shows "Dom (g  f) = Dom f"
    proof -
      have "C1.arr (fst f)  C1.arr (fst g)  C1.dom (fst g) = C1.cod (fst f)"
        using assms by blast
      moreover have "C2.arr (snd f)  C2.arr (snd g)  C2.dom (snd g) = C2.cod (snd f)"
        using assms by blast
      ultimately show ?thesis
        by (simp add: comp_def)
    qed

    lemma Cod_comp:
    assumes "seq g f"
    shows "Cod (g  f) = Cod g"
    proof -
      have "C1.arr (fst f)  C1.arr (fst g)  C1.dom (fst g) = C1.cod (fst f)"
        using assms by blast
      moreover have "C2.arr (snd f)  C2.arr (snd g)  C2.dom (snd g) = C2.cod (snd f)"
        using assms by blast
      ultimately show ?thesis
        by (simp add: comp_def)
    qed

    theorem is_category:
    shows "category comp"
    proof
      fix f
      show "(domains f  {}) = (codomains f  {})"
        using has_domain_char has_codomain_char by simp
      fix g
      show "g  f  null  seq g f"
        using comp_def seq_char by (metis C1.seqI C2.seqI Pair_inject null_char)
      fix h
      show "seq h g  seq (h  g) f  seq g f"
        using seq_char
        by (metis category.seqE category.seqI Dom_comp
            product_category_axioms product_category_def fst_conv snd_conv)
      show "seq h (g  f)  seq g f  seq h g"
        using seq_char
        by (metis category.seqE category.seqI Cod_comp
            product_category_axioms product_category_def fst_conv snd_conv)
      show "seq g f  seq h g  seq (h  g) f"
        using seq_char
        by (metis arrE category.seqE category.seqI Dom_comp
            product_category_axioms product_category_def fst_conv snd_conv)
      show "seq g f  seq h g  (h  g)  f = h  g  f"
        using comp_def null_char seq_char C1.comp_assoc C2.comp_assoc
        by (elim seqEPC C1.seqE C2.seqE, simp)
    qed

    sublocale category comp
      using is_category comp_def by auto

    lemma dom_char:
    shows "dom f = Dom f"
    proof (cases "Arr f")
      show "¬Arr f  dom f = Dom f"
        unfolding dom_def using has_domain_char by auto
      show "Arr f  dom f = Dom f"
        using ide_Ide apply (intro dom_eqI, simp)
        using seq_char comp_def C1.arr_dom_iff_arr C2.arr_dom_iff_arr by auto
    qed

    lemma dom_simp [simp]:
    assumes "arr f"
    shows "dom f = (C1.dom (fst f), C2.dom (snd f))"
      using assms dom_char by auto

    lemma cod_char:
    shows "cod f = Cod f"
    proof (cases "Arr f")
      show "¬Arr f  cod f = Cod f"
        unfolding cod_def using has_codomain_char by auto
      show "Arr f  cod f = Cod f"
        using ide_Ide seqI apply (intro cod_eqI, simp)
        using seq_char comp_def C1.arr_cod_iff_arr C2.arr_cod_iff_arr by auto
    qed

    lemma cod_simp [simp]:
    assumes "arr f"
    shows "cod f = (C1.cod (fst f), C2.cod (snd f))"
      using assms cod_char by auto

    lemma in_homIPC [intro, simp]:
    assumes "«fst f: fst a 1 fst b»" and "«snd f: snd a 2 snd b»"
    shows "«f: a  b»"
      using assms by fastforce

    lemma in_homEPC [elim]:
    assumes "«f: a  b»"
    and "«fst f: fst a 1 fst b»  «snd f: snd a 2 snd b»  T"
    shows "T"
      using assms
      by (metis C1.in_homI C2.in_homI arr_char cod_simp dom_simp fst_conv in_homE snd_conv)

    lemma ide_charPC [iff]:
    shows "ide f  Ide f"
      using ide_in_hom C1.ide_in_hom C2.ide_in_hom by blast

    lemma comp_char:
    shows "g  f = (if C1.arr (C1 (fst g) (fst f))  C2.arr (C2 (snd g) (snd f)) then
                       (C1 (fst g) (fst f), C2 (snd g) (snd f))
                    else Null)"
      using comp_def by auto

    lemma comp_simp [simp]:
    assumes "C1.seq (fst g) (fst f)" and "C2.seq (snd g) (snd f)"
    shows "g  f = (fst g 1 fst f, snd g 2 snd f)"
      using assms comp_char by simp

    lemma iso_char [iff]:
    shows "iso f  C1.iso (fst f)  C2.iso (snd f)"
    proof
      assume f: "iso f"
      obtain g where g: "inverse_arrows f g" using f by auto
      have 1: "ide (g  f)  ide (f  g)"
        using f g by (simp add: inverse_arrows_def)
      have "g  f = (fst g 1 fst f, snd g 2 snd f)  f  g = (fst f 1 fst g, snd f 2 snd g)"
        using 1 comp_char arr_char by (meson ideD(1) seq_char)
      hence "C1.ide (fst g 1 fst f)  C2.ide (snd g 2 snd f) 
             C1.ide (fst f 1 fst g)  C2.ide (snd f 2 snd g)"
        using 1 ide_char by simp
      hence "C1.inverse_arrows (fst f) (fst g)  C2.inverse_arrows (snd f) (snd g)"
        by auto
      thus "C1.iso (fst f)  C2.iso (snd f)" by auto
      next
      assume f: "C1.iso (fst f)  C2.iso (snd f)"
      obtain g1 where g1: "C1.inverse_arrows (fst f) g1" using f by blast
      obtain g2 where g2: "C2.inverse_arrows (snd f) g2" using f by blast
      have "C1.ide (g1 1 fst f)  C2.ide (g2 2 snd f) 
            C1.ide (fst f 1 g1)  C2.ide (snd f 2 g2)"
        using g1 g2 ide_charPC by force
      hence "inverse_arrows f (g1, g2)"
        using f g1 g2 ide_charPC comp_char by (intro inverse_arrowsI, auto)
      thus "iso f" by auto
    qed

    lemma isoIPC [intro, simp]:
    assumes "C1.iso (fst f)" and "C2.iso (snd f)"
    shows "iso f"
      using assms by simp

    lemma isoD:
    assumes "iso f"
    shows "C1.iso (fst f)" and "C2.iso (snd f)"
      using assms by auto

    lemma inv_simp [simp]:
    assumes "iso f"
    shows "inv f = (C1.inv (fst f), C2.inv (snd f))"
    proof -
      have "inverse_arrows f (C1.inv (fst f), C2.inv (snd f))"
      proof
        have 1: "C1.inverse_arrows (fst f) (C1.inv (fst f))"
          using assms iso_char C1.inv_is_inverse by simp
        have 2: "C2.inverse_arrows (snd f) (C2.inv (snd f))"
          using assms iso_char C2.inv_is_inverse by simp
        show "ide ((C1.inv (fst f), C2.inv (snd f))  f)"
          using 1 2 ide_charPC comp_char by auto
        show "ide (f  (C1.inv (fst f), C2.inv (snd f)))"
          using 1 2 ide_charPC comp_char by auto
      qed
      thus ?thesis using inverse_unique by auto
    qed

  end

end