Theory Cat

(*  Title:       Category theory using Isar and Locales
    Author:      Greg O'Keefe, June, July, August 2003
    License: LGPL
*)

section ‹Categories›

theory Cat
imports "HOL-Library.FuncSet"
begin

subsection ‹Definitions›

record ('o, 'a) category =
  ob :: "'o set" ("Obı"  70)
  ar :: "'a set" ("Arı"  70)
  dom :: "'a ⇒ 'o" ("Domı _" [81] 70)
  cod :: "'a ⇒ 'o" ("Codı _" [81] 70)
  id :: "'o ⇒ 'a" ("Idı _" [81] 80)
  comp :: "'a ⇒ 'a ⇒ 'a"  (infixl "∙ı" 60)

definition
  hom :: "[('o,'a,'m) category_scheme, 'o, 'o] ⇒ 'a set"
    ("Homı _ _" [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 "(∙) : Hom (Dom g) (Cod g) → Hom (Dom f) (Dom g) → Hom (Dom f) (Cod g)" ..
  from this and g_homset 
  have "(∙) 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