# 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
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
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
qed

theorem is_category:
shows
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