Theory ProductCategory
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 arrI⇩P⇩C [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 seqI⇩P⇩C [intro]:
assumes "C1.seq g1 f1 ∧ C2.seq g2 f2"
shows "seq (g1, g2) (f1, f2)"
using assms comp_def by auto
lemma seqE⇩P⇩C [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 seqE⇩P⇩C 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_homI⇩P⇩C [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_homE⇩P⇩C [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_char⇩P⇩C [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_char⇩P⇩C by force
hence "inverse_arrows f (g1, g2)"
using f g1 g2 ide_char⇩P⇩C comp_char by (intro inverse_arrowsI, auto)
thus "iso f" by auto
qed
lemma isoI⇩P⇩C [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_char⇩P⇩C comp_char by auto
show "ide (f ⋅ (C1.inv (fst f), C2.inv (snd f)))"
using 1 2 ide_char⇩P⇩C comp_char by auto
qed
thus ?thesis using inverse_unique by auto
qed
end
end