Theory HomFunctors
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,_)⇘𝖺⇙ : Ar → ar Set"
proof (rule funcsetI)
fix f
assume f: "f ∈ Ar"
thus "Hom(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,_)⇘𝗈⇙ : Ob → ob Set"
proof (rule funcsetI)
fix B
assume B: "B ∈ Ob"
have "Hom(A,_)⇘𝗈⇙ 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,_)⇘𝗈⇙ B ∈ ob Set" by simp
qed
lemma (in into_set) homf_preserves_dom:
assumes f: "f ∈ Ar"
shows "Hom(A,_)⇘𝗈⇙ (Dom f) = dom Set (Hom(A,_)⇘𝖺⇙ f)"
proof-
have "Dom f ∈ Ob" using f ..
hence 1: "Hom(A,_)⇘𝗈⇙ (Dom f) = Hom A (Dom f)"
using f by (simp add: homf_def)
have 2: "dom Set (Hom(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,_)⇘𝗈⇙ (Cod f) = cod Set (Hom(A,_)⇘𝖺⇙ f)"
proof-
have "Cod f ∈ Ob" using f ..
hence 1: "Hom(A,_)⇘𝗈⇙ (Cod f) = Hom A (Cod f)"
using f by (simp add: homf_def)
have 2: "cod Set (Hom(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,_)⇘𝖺⇙ (Id B) = id Set (Hom(A,_)⇘𝗈⇙ 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,_)⇘𝖺⇙ (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,_)⇘𝗈⇙ 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,_)⇘𝖺⇙ (g ∙ f) = (Hom(A,_)⇘𝖺⇙ g) ⊙ (Hom(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,_)⇘𝖺⇙ (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,_)⇘𝖺⇙ g) ⊙ (Hom(A,_)⇘𝖺⇙ f)) = Hom A (Dom f)"
using f by (simp add: set_comp_def homf_def)
have 5: "set_cod ((Hom(A,_)⇘𝖺⇙ g) ⊙ (Hom(A,_)⇘𝖺⇙ f)) = Hom A (Cod g)"
using g by (simp add: set_comp_def homf_def)
have "set_func ((Hom(A,_)⇘𝖺⇙ g) ⊙ (Hom(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,_)⇘𝖺⇙ g) ⊙ (Hom(A,_)⇘𝖺⇙ f))
= (λh∈Hom A (Dom f). (g ∙ f) ∙ h)" .
from 4 and 5 and 6
have rhs: "(Hom(A,_)⇘𝖺⇙ g) ⊙ (Hom(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,_)⇘𝖺⇙ : Ar → ar Set"
by (rule homf_preserves_arrows)
show "Hom(A,_)⇘𝗈⇙ : Ob → ob Set"
by (rule homf_preserves_objects)
show "∀f∈Ar. Hom(A,_)⇘𝗈⇙ (Dom f) = dom Set (Hom(A,_)⇘𝖺⇙ f)"
by (intro ballI) (rule homf_preserves_dom)
show "∀f∈Ar. Hom(A,_)⇘𝗈⇙ (Cod f) = cod Set (Hom(A,_)⇘𝖺⇙ f)"
by (intro ballI) (rule homf_preserves_cod)
show "∀B∈Ob. Hom(A,_)⇘𝖺⇙ (Id B) = id Set (Hom(A,_)⇘𝗈⇙ B)"
by (intro ballI) (rule homf_preserves_id)
show "∀f∈Ar. ∀g∈Ar.
Cod f = Dom g ⟶
Hom(A,_)⇘𝖺⇙ (g ∙ f) = comp Set (Hom(A,_)⇘𝖺⇙ g) (Hom(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