Quelle  HomFunctors.thy

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

Define homfunctors, prove that they are functors.
*)

section HomFunctors

theory HomFunctors
imports SetCat Functors
begin

locale into_set = two_cats AA BB
    for AA :: "('o,'a,'m)category_scheme" (structure)
    and BB (structure) +
  fixes U and Set 
  defines "U ≡ (UNIV::'a set)"
  defines "Set ≡ set_cat U"
  assumes BB_Set: "BB = Set"
  fixes homf (‹Hom'(_,'_')›)
  defines "homf A ≡ (
  om = (λB∈Ob. Hom A B),
  am = (λf∈Ar. (set_dom=Hom A (Dom f),set_func=(λg∈Hom A (Dom f). f ∙ g),set_cod=Hom A (Cod f)))
  )"


lemma (in into_set) homf_preserves_arrows:
 "Hom(A,_)_<a> : Ar → ar Set"
proof (rule funcsetI)
  fix f
  assume f: "f ∈ Ar"
  thus "Hom(A,_)_<a> f ∈ ar Set"
  proof (simp add: homf_def Set_def set_cat_def set_arrow_def U_def)
    have 1: "(∙) : Hom (Dom f) (Cod f) → Hom A (Dom f) → Hom A (Cod f)" ..
    have 2: "f ∈ Hom (Dom f) (Cod f)" using f by (simp add: hom_def)
    from 1 and 2 have 3: "(∙) f : Hom A (Dom f) → Hom A (Cod f)" 
      by (rule funcset_mem)
    show "(λg∈Hom A (Dom f). f ∙ g) : Hom A (Dom f) → Hom A (Cod f)"
    proof (rule funcsetI)
      fix g'
      assume "g' ∈ Hom A (Dom f)"
      from 3 and this show "(λg∈Hom A (Dom f). f ∙ g) g' ∈ Hom A (Cod f)"
        by simp (rule funcset_mem)
    qed
  qed
qed


lemma (in into_set) homf_preserves_objects:
 "Hom(A,_)_<o> : Ob → ob Set"
proof (rule funcsetI)
  fix B
  assume B: "B ∈ Ob"
  have "Hom(A,_)_<o> B = Hom A B"
    using B by (simp add: homf_def)
  moreover have "… ∈ ob Set"
    by (simp add: U_def Set_def set_cat_def)
  ultimately show "Hom(A,_)_<o> B ∈ ob Set" by simp
qed


lemma (in into_set) homf_preserves_dom:
  assumes f: "f ∈ Ar"
  shows "Hom(A,_)_<o> (Dom f) = dom Set (Hom(A,_)_<a> f)"
proof-
  have "Dom f ∈ Ob" using f ..
  hence 1: "Hom(A,_)_<o> (Dom f) = Hom A (Dom f)"
    using f by (simp add: homf_def)
  have 2: "dom Set (Hom(A,_)_<a> f) = Hom A (Dom f)"
    using f by (simp add: Set_def homf_def)
  from 1 and 2 show ?thesis by simp
qed

lemma (in into_set) homf_preserves_cod:
  assumes f: "f ∈ Ar"
  shows "Hom(A,_)_<o> (Cod f) = cod Set (Hom(A,_)_<a> f)"
proof-
  have "Cod f ∈ Ob" using f ..
  hence 1: "Hom(A,_)_<o> (Cod f) = Hom A (Cod f)"
    using f by (simp add: homf_def)
  have 2: "cod Set (Hom(A,_)_<a> f) = Hom A (Cod f)"
    using f by (simp add: Set_def homf_def)
  from 1 and 2 show ?thesis by simp
qed


lemma (in into_set) homf_preserves_id:
  assumes B: "B ∈ Ob"
  shows "Hom(A,_)_<a> (Id B) = id Set (Hom(A,_)_<o> B)"
proof-
  have 1: "Id B ∈ Ar" using B ..
  have 2: "Dom (Id B) = B"
    using B by (rule AA.id_dom_cod)
  have 3: "Cod (Id B) = B"
    using B by (rule AA.id_dom_cod)
  have 4: "(λg∈Hom A B. (Id B) ∙ g) = (λg∈Hom A B. g)"
    by (rule ext) (auto simp add: hom_def)
  have "Hom(A,_)_<a> (Id B) = (
    set_dom=Hom A B,
    set_func=(λg∈Hom A B. g),
    set_cod=Hom A B)"
    by (simp add: homf_def 1 2 3 4)
  also have "…= id Set (Hom(A,_)_<o> B)"
    using B by (simp add: Set_def U_def set_cat_def set_id_def homf_def)
  finally show ?thesis .
qed
  

lemma (in into_set) homf_preserves_comp:
  assumes f: "f ∈ Ar" 
    and g: "g ∈ Ar"
    and fg: "Cod f = Dom g"
  shows "Hom(A,_)_<a> (g ∙ f) = (Hom(A,_)_<a> g) ⊙ (Hom(A,_)_<a> f)"
proof-
  have 1: "g ∙ f ∈ Ar" using assms ..
  have 2: "Dom (g ∙ f) = Dom f" using f g fg ..
  have 3: "Cod (g ∙ f) = Cod g" using f g fg ..
  have lhs: "Hom(A,_)_<a> (g ∙ f) = (
    set_dom=Hom A (Dom f),
    set_func=(λh∈Hom A (Dom f). (g ∙ f) ∙ h),
    set_cod=Hom A (Cod g))"
    by (simp add: homf_def 1 2 3)
  have 4: "set_dom ((Hom(A,_)_<a> g) ⊙ (Hom(A,_)_<a> f)) = Hom A (Dom f)"
    using f by (simp add: set_comp_def homf_def)
  have 5: "set_cod ((Hom(A,_)_<a> g) ⊙ (Hom(A,_)_<a> f)) = Hom A (Cod g)"
    using g by (simp add: set_comp_def homf_def)
  have "set_func ((Hom(A,_)_<a> g) ⊙ (Hom(A,_)_<a> f))
      = compose (Hom A (Dom f)) (λy∈Hom A (Dom g). g ∙ y) (λx∈Hom A (Dom f). f ∙ x)"
    using f g by (simp add: set_comp_def homf_def)
  also have "… = (λh∈Hom A (Dom f). (g ∙ f) ∙ h)"
  proof (
      rule extensionalityI, 
      rule compose_extensional,
      rule restrict_extensional,
      simp)
    fix h
    assume 10: "h ∈ Hom A (Dom f)"
    hence 11: "f ∙ h ∈ Hom A (Dom g)"
    proof-
      from 10 have "h ∈ Ar" by (simp add: hom_def)
      have 100: "(∙) : Hom (Dom f) (Dom g) → Hom A (Dom f) → Hom A (Dom g)"
        by (rule AA.comp_types)
      have "f ∈ Hom (Dom f) (Cod f)" using f by (simp add: hom_def)
      hence 101: "f ∈ Hom (Dom f) (Dom g)" using fg by simp
      from 100 and 101
      have "(∙) f : Hom A (Dom f) → Hom A (Dom g)"
        by (rule funcset_mem)
      from this and 10 
      show "f ∙ h ∈ Hom A (Dom g)"
        by (rule funcset_mem)
    qed
    hence "Cod (f ∙ h) = Dom g" 
      and "Dom (f ∙ h) = A"
      and "f ∙ h ∈ Ar"
      by (simp_all add: hom_def)
    thus "compose (Hom A (Dom f)) (λy∈Hom A (Dom g). g ∙ y) (λx∈Hom A (Dom f). f ∙ x) h =
        (g ∙ f) ∙ h"
      using f g fg 10 by (simp add: compose_def 10 11 hom_def)
  qed
  finally have 6: "set_func ((Hom(A,_)_<a> g) ⊙ (Hom(A,_)_<a> f))
    = (λh∈Hom A (Dom f). (g ∙ f) ∙ h)" .
  from 4 and 5 and 6
  have rhs: "(Hom(A,_)_<a> g) ⊙ (Hom(A,_)_<a> f) = (
    set_dom=Hom A (Dom f),
    set_func=(λh∈Hom A (Dom f). (g ∙ f) ∙ h),
    set_cod=Hom A (Cod g))"
    by simp
  show ?thesis
    by (simp add: lhs rhs)
qed


theorem (in into_set) homf_into_set:
  "Functor Hom(A,_) : AA ⟶ Set"
proof (intro functor.intro functor_axioms.intro)
  show "Hom(A,_)_<a> : Ar → ar Set"
    by (rule homf_preserves_arrows)
  show "Hom(A,_)_<o> : Ob → ob Set"
    by (rule homf_preserves_objects)
  show "∀f∈Ar. Hom(A,_)_<o> (Dom f) = dom Set (Hom(A,_)_<a> f)"
    by (intro ballI) (rule homf_preserves_dom)
  show "∀f∈Ar. Hom(A,_)_<o> (Cod f) = cod Set (Hom(A,_)_<a> f)"
    by (intro ballI) (rule homf_preserves_cod)
  show "∀B∈Ob. Hom(A,_)_<a> (Id B) = id Set (Hom(A,_)_<o> B)"
    by (intro ballI) (rule homf_preserves_id)
  show "∀f∈Ar. ∀g∈Ar.
    Cod f = Dom g ⟶
    Hom(A,_)_<a> (g ∙ f) = comp Set (Hom(A,_)_<a> g) (Hom(A,_)_<a> f)"
    by (intro ballI impI, simp add: Set_def set_cat_def) (rule homf_preserves_comp)
  show "two_cats AA Set"
  proof intro_locales
    show "category Set" 
      by (unfold Set_def, rule set_cat_cat)
  qed
qed

end