header HomFunctors
theory HomFunctors
imports SetCat Functors
begin
locale into_set = two_cats +
assumes "AA = (AA::('o,'a,'m)category_scheme)"
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: "(op •) : 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: "(op •) 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) \<odot> (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) \<odot> (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) \<odot> (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) \<odot> (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: "(op •) : 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 "(op •) 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) \<odot> (Hom(A,_)\<a> f))
= (λh∈Hom A (Dom f). (g • f) • h)" .
from 4 and 5 and 6
have rhs: "(Hom(A,_)\<a> g) \<odot> (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)
show "two_cats_axioms AA Set"
proof qed rule+
qed
qed
end