Theory SetCat

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

section ‹{{\sf Set}} is a Category›

theory SetCat
imports Cat
begin

subsection‹Definitions›

record 'c set_arrow =
  set_dom :: "'c set"
  set_func :: "'c ⇒ 'c"
  set_cod :: "'c set"

definition
  set_arrow :: "['c set, 'c set_arrow] ⇒ bool" where
  "set_arrow U f ⟷ set_dom f ⊆ U & set_cod f ⊆ U
    & (set_func f): (set_dom f) → (set_cod f) 
    & set_func f ∈ extensional (set_dom f)"

definition
  set_id :: "['c set, 'c set] ⇒ 'c set_arrow" where
  "set_id U = (λs∈Pow U. ⦇set_dom=s, set_func=λx∈s. x, set_cod=s⦈)"

definition
  set_comp :: "['c set_arrow, 'c set_arrow] ⇒ 'c set_arrow"  (infix "⊙" 70) where
  "set_comp g f =
  ⦇
    set_dom = set_dom f, 
    set_func = compose (set_dom f) (set_func g) (set_func f), 
    set_cod = set_cod g
  ⦈"

definition
  set_cat :: "'c set ⇒ ('c set, 'c set_arrow) category" where
  "set_cat U =
  ⦇ 
    ob = Pow U,
    ar = {f. set_arrow U f},
    dom = set_dom,
    cod = set_cod,
    id = set_id U, 
    comp = set_comp
  ⦈"


subsection ‹Simple Rules and Lemmas›

lemma set_objectI [intro]: "A ⊆ U ⟹ A ∈ ob (set_cat U)"
  by (simp add: set_cat_def)

lemma set_objectE [intro]: "A ∈ ob (set_cat U) ⟹ A ⊆ U"
  by (simp add: set_cat_def)

lemma set_homI [intro]:
  assumes "A ⊆ U"
  and "B ⊆ U"
  and "f : A→B"
  and "f ∈ extensional A"
  shows "⦇set_dom=A, set_func=f, set_cod=B⦈ ∈ hom (set_cat U) A B"
  using assms by (simp add: set_cat_def hom_def set_arrow_def)

lemma set_dom [simp]: "dom (set_cat U) f = set_dom f"
  by (simp add: set_cat_def)

lemma set_cod [simp]: "cod (set_cat U) f = set_cod f"
  by (simp add: set_cat_def)

lemma set_id [simp]: "id (set_cat U) A = set_id U A"
  by (simp add: set_cat_def)

lemma set_comp [simp]: "comp (set_cat U) g f = g ⊙ f"
  by (simp add: set_cat_def)
  

lemma set_dom_cod_object_subset [intro]:
  assumes f: "f ∈ ar (set_cat U)"
  shows "dom (set_cat U) f ∈ ob (set_cat U)"
    and "cod (set_cat U) f ∈ ob (set_cat U)"
    and "set_cod f ⊆ U"
    and "set_dom f ⊆ U"
proof-
  note [simp] = set_cat_def set_arrow_def
  have "dom (set_cat U) f = set_dom f" using f by simp
  also show "… ⊆ U" using f by simp
  finally show "dom (set_cat U) f ∈ ob (set_cat U)" ..
  have "cod (set_cat U) f = set_cod f" using f by simp
  also show "… ⊆ U" using f by simp
  finally show "cod (set_cat U) f ∈ ob (set_cat U)" ..
qed


text ‹In this context, ‹f ∈ hom A B› is quite a strong claim.›

lemma set_homE [intro]:
  assumes f: "f ∈ hom (set_cat U) A B"
  shows "A ⊆ U"
    and "B ⊆ U"
    and "set_dom f = A"
    and "set_func f : A → B"
    and "set_cod f = B"
proof-
  have 1: "f ∈ ar (set_cat U)" 
    using f by (simp add: hom_def set_cat_def)
  show 2: "set_dom f = A"
    using f by (simp add: set_cat_def hom_def set_arrow_def)
  from 1 have "set_dom f ⊆ U" ..
  thus "A ⊆ U" by (simp add: 2)
  show 3: "set_cod f = B"
    using f by (simp add: set_cat_def hom_def set_arrow_def)
  from 1 have "set_cod f ⊆ U" ..
  thus "B ⊆ U" by (simp add: 3)
  have "set_func f ∈ (set_dom f) → (set_cod f)"
    using f by (auto simp add: set_cat_def hom_def set_arrow_def)
  thus "set_func f ∈ A → B"
    by (simp add: 2 3)
qed


subsection ‹Set is a Category›
lemma set_id_left:
  assumes f: "f ∈ ar (set_cat U)"
  shows "set_id U (set_cod f) ⊙ f = f"
proof-
  from ‹f ∈ ar (set_cat U)› have "set_cod f ⊆ U" ..
  hence 1: "set_id U (set_cod f) ⊙ f = 
    ⦇
    set_dom=set_dom f, 
    set_func=compose (set_dom f) (λx∈set_cod f. x) (set_func f),
    set_cod=set_cod f
    ⦈"
    using f by (simp add: set_comp_def set_id_def)
  have 2: "compose (set_dom f)  (λx∈set_cod f. x) (set_func f) = set_func f"
  proof (rule extensionalityI)
    show "compose (set_dom f) (λx∈set_cod f. x) (set_func f) ∈ extensional (set_dom f)"
      by (rule compose_extensional)
    show "set_func f ∈ extensional (set_dom f)"
      using f by (simp add: set_cat_def set_arrow_def)
    fix x
    assume x_in_dom: "x ∈ set_dom f"
    have f_into_cod: "set_func f : (set_dom f) → (set_cod f)" 
      using f by (simp add: set_cat_def set_arrow_def)
    from f_into_cod and x_in_dom
    have f_x_in_cod: "set_func f x ∈ set_cod f"
      by (rule funcset_mem)
    show "compose (set_dom f) (λx∈set_cod f. x) (set_func f) x = set_func f x"
      by (simp add: x_in_dom f_x_in_cod compose_def)
  qed
  from 1 have "set_id U (set_cod f) ⊙ f = 
    ⦇
    set_dom=set_dom f, 
    set_func=set_func f,
    set_cod=set_cod f
    ⦈"
    by (simp only: 2)
  also have "… = f"
    by simp
  finally show ?thesis .
qed

lemma set_id_right:
  assumes f: "f ∈ ar (set_cat U)"
  shows "f ⊙ (set_id U (set_dom f)) = f"
proof-
  from ‹f ∈ ar (set_cat U)› have "set_dom f ⊆ U" ..
  hence 1: "f ⊙ (set_id U (set_dom f)) = 
    ⦇
    set_dom=set_dom f, 
    set_func=compose (set_dom f) (set_func f) (λx∈set_dom f. x),
    set_cod=set_cod f
    ⦈"
    using f by (simp add: set_comp_def set_id_def)
  have 2: "compose (set_dom f) (set_func f) (λx∈set_dom f. x) = set_func f"
  proof (rule extensionalityI)
    show "compose (set_dom f) (set_func f) (λx∈set_dom f. x) ∈ extensional (set_dom f)"
      by (rule compose_extensional)
    show "set_func f ∈ extensional (set_dom f)"
      using f by (simp add: set_cat_def set_arrow_def)
    fix x
    assume x_in_dom: "x ∈ set_dom f"
    thus "compose (set_dom f) (set_func f) (λx∈set_dom f. x) x = set_func f x"
      by (simp add: compose_def)
  qed
  from 1 have "f ⊙ (set_id U (set_dom f)) = 
    ⦇
    set_dom=set_dom f, 
    set_func=set_func f,
    set_cod=set_cod f
    ⦈"
    by (simp only: 2)
  also have "… = f"
    by simp
  finally show ?thesis .
qed

lemma set_id_hom:
  assumes "A ∈ ob (set_cat U)"
  shows "id (set_cat U) A ∈ hom (set_cat U) A A"
proof-
  from ‹A ∈ ob (set_cat U)› have 1: "A ⊆ U" ..
  hence "id (set_cat U) A = ⦇set_dom=A, set_func=λx∈A. x, set_cod=A⦈"
    by (simp add: set_cat_def set_id_def)
  also have "… ∈ hom (set_cat U) A A"
  proof (rule set_homI)
    show "(λx∈A. x) ∈ A → A"
      by (rule funcsetI, auto)
    show "(λx∈A. x) ∈ extensional A"
      by (rule restrict_extensional)
  qed (rule 1, rule 1)
  finally show ?thesis .
qed


lemma set_comp_types:
"comp (set_cat U) ∈ hom (set_cat U) B C → hom (set_cat U) A B → hom (set_cat U) A C"
proof (rule funcsetI)
  fix g
  assume g_BC: "g ∈ hom (set_cat U) B C"
  hence comp_cod: "set_cod g = C" ..
  show "comp (set_cat U) g ∈ hom (set_cat U) A B → hom (set_cat U) A C"
  proof (rule funcsetI)
    fix f
    assume f_AB: "f ∈ hom (set_cat U) A B"
    hence comp_dom: "set_dom f = A" ..
    show "comp (set_cat U) g f ∈ hom (set_cat U) A C"
    proof-
      have "comp (set_cat U) g f = 
        ⦇
        set_dom = A, 
        set_func = compose (set_dom f) (set_func g) (set_func f),
        set_cod = C
        ⦈"
        by (simp add: set_cat_def set_comp_def comp_cod comp_dom)
      also have "… ∈ hom (set_cat U) A C"
      proof (rule set_homI)
        from f_AB show "A ⊆ U" ..
        from g_BC show "C ⊆ U" ..
        from f_AB have fs_f: "set_func f: A → B" ..
        from g_BC have fs_g: "set_func g: B → C" ..
        from fs_g and fs_f
        show " compose (set_dom f) (set_func g) (set_func f) : A → C"
          by (simp only: comp_dom) (rule funcset_compose)
        show "compose (set_dom f) (set_func g) (set_func f) ∈ extensional A"
          by (simp only: comp_dom) (rule compose_extensional)
      qed
      finally show ?thesis .
    qed
  qed
qed

text ‹We reason explicitly about the function component of the
composite arrow, leaving the rest to the simplifier.›

lemma set_comp_associative:
  fixes f and g and h
  assumes f: "f ∈ ar (set_cat U)" 
    and g: "g ∈ ar (set_cat U)" 
    and h: "h ∈ ar (set_cat U)" 
    and hg: "cod (set_cat U) h = dom (set_cat U) g" 
    and gf: "cod (set_cat U) g = dom (set_cat U) f"
  shows "comp (set_cat U) f (comp (set_cat U) g h) =
  comp (set_cat U) (comp (set_cat U) f g) h"
proof (simp add: set_cat_def set_comp_def)
  show "compose (set_dom h) (set_func f) (compose (set_dom h) (set_func g) (set_func h)) =
    compose (set_dom h) (compose (set_dom g) (set_func f) (set_func g)) (set_func h)"
  proof (rule compose_assoc)
    show "set_func h ∈ set_dom h → set_dom g" 
      using h hg by (simp add: set_cat_def set_arrow_def)
  qed
qed


theorem set_cat_cat:  "category (set_cat U)"
proof (rule category.intro)
  fix f
  assume f: "f ∈ ar (set_cat U)"
  show "dom (set_cat U) f ∈ ob (set_cat U)" using f ..
  show "cod (set_cat U) f ∈ ob (set_cat U)" using f ..
  show "comp (set_cat U) (id (set_cat U) (cod (set_cat U) f)) f = f"
    using f by (simp add: set_id_left)
  show "comp (set_cat U) f (id (set_cat U) (dom (set_cat U) f)) = f"
    using f by (simp add: set_id_right)
next
  fix A
  assume "A ∈ ob (set_cat U)"
  then show "id (set_cat U) A ∈ hom (set_cat U) A A"
    by (rule set_id_hom)
next
  fix A and B and C
  show "comp (set_cat U) ∈ hom (set_cat U) B C → hom (set_cat U) A B → hom (set_cat U) A C"
    by (rule set_comp_types)
next
  fix f and g and h
  assume "f ∈ ar (set_cat U)" 
    and  "g ∈ ar (set_cat U)" 
    and  "h ∈ ar (set_cat U)" 
    and "cod (set_cat U) h = dom (set_cat U) g" 
    and "cod (set_cat U) g = dom (set_cat U) f"
  then show "comp (set_cat U) f (comp (set_cat U) g h) =
    comp (set_cat U) (comp (set_cat U) f g) h"
    by (rule set_comp_associative)
qed

end