header {* Categories *}
theory Cat
imports "~~/src/HOL/Library/FuncSet"
begin
subsection {* Definitions *}
record ('o, 'a) category =
ob :: "'o set" ("Ob\<index>" 70)
ar :: "'a set" ("Ar\<index>" 70)
dom :: "'a => 'o" ("Dom\<index> _" [81] 70)
cod :: "'a => 'o" ("Cod\<index> _" [81] 70)
id :: "'o => 'a" ("Id\<index> _" [81] 80)
comp :: "'a => 'a => 'a" (infixl "•\<index>" 60)
definition
hom :: "[('o,'a,'m) category_scheme, 'o, 'o] => 'a set"
("Hom\<index> _ _" [81,81] 80) where
"hom CC A B = { f. f∈ar CC & dom CC f = A & cod CC f = B }"
locale category =
fixes CC (structure)
assumes dom_object [intro]:
"f ∈ Ar ==> Dom f ∈ Ob"
and cod_object [intro]:
"f ∈ Ar ==> Cod f ∈ Ob"
and id_left [simp]:
"f ∈ Ar ==> Id (Cod f) • f = f"
and id_right [simp]:
"f ∈ Ar ==> f • Id (Dom f) = f"
and id_hom [intro]:
"A ∈ Ob ==> Id A ∈ Hom A A"
and comp_types [intro]:
"!!A B C. (comp CC) : (Hom B C) -> (Hom A B) -> (Hom A C)"
and comp_associative [simp]:
"f ∈ Ar ==> g ∈ Ar ==> h ∈ Ar
==> Cod h = Dom g ==> Cod g = Dom f
==> f • (g • h) = (f • g) • h"
subsection {* Lemmas *}
lemma (in category) homI:
assumes "f ∈ Ar" and "Dom f = A" and "Cod f = B"
shows "f ∈ Hom A B"
using assms by (auto simp add: hom_def)
lemma (in category) homE:
assumes "A ∈ Ob" and "B ∈ Ob" and "f ∈ Hom A B"
shows "Dom f = A" and "Cod f = B"
proof-
show "Dom f = A" using assms by (simp add: hom_def)
show "Cod f = B" using assms by (simp add: hom_def)
qed
lemma (in category) id_arrow [intro]:
assumes "A ∈ Ob"
shows "Id A ∈ Ar"
proof-
from `A ∈ Ob` have "Id A ∈ Hom A A" by (rule id_hom)
thus "Id A ∈ Ar" by (simp add: hom_def)
qed
lemma (in category) id_dom_cod:
assumes "A ∈ Ob"
shows "Dom (Id A) = A" and "Cod (Id A) = A"
proof-
from `A ∈ Ob` have 1: "Id A ∈ Hom A A" ..
then show "Dom (Id A) = A" and "Cod (Id A) = A"
by (simp_all add: hom_def)
qed
lemma (in category) compI [intro]:
assumes f: "f ∈ Ar" and g: "g ∈ Ar" and "Cod f = Dom g"
shows "g • f ∈ Ar"
and "Dom (g • f) = Dom f"
and "Cod (g • f) = Cod g"
proof-
have "f ∈ Hom (Dom f) (Cod f)" using f by (simp add: hom_def)
with `Cod f = Dom g` have f_homset: "f ∈ Hom (Dom f) (Dom g)" by simp
have g_homset: "g ∈ Hom (Dom g) (Cod g)" using g by (simp add: hom_def)
have "(op •) : Hom (Dom g) (Cod g) -> Hom (Dom f) (Dom g) -> Hom (Dom f) (Cod g)" ..
from this and g_homset
have "(op •) g ∈ Hom (Dom f) (Dom g) -> Hom (Dom f) (Cod g)"
by (rule funcset_mem)
from this and f_homset
have gf_homset: "g • f ∈ Hom (Dom f) (Cod g)"
by (rule funcset_mem)
thus "g • f ∈ Ar"
by (simp add: hom_def)
from gf_homset show "Dom (g • f) = Dom f" and "Cod (g • f) = Cod g"
by (simp_all add: hom_def)
qed
end