header {* Functors *}
theory Functors
imports Cat
begin
subsection {* Definitions *}
record ('o1,'a1,'o2,'a2) functor =
om :: "'o1 => 'o2"
am :: "'a1 => 'a2"
abbreviation
om_syn ("_ \<o>" [81]) where
"F\<o> ≡ om F"
abbreviation
am_syn ("_ \<a>" [81]) where
"F\<a> ≡ am F"
locale two_cats = AA: category AA + BB: category BB
for AA (structure) and BB (structure) +
assumes "AA = (AA :: ('o1,'a1,'m1)category_scheme)"
assumes "BB = (BB :: ('o2,'a2,'m2)category_scheme)"
fixes preserves_dom :: "('o1,'a1,'o2,'a2)functor => bool"
and preserves_cod :: "('o1,'a1,'o2,'a2)functor => bool"
and preserves_id :: "('o1,'a1,'o2,'a2)functor => bool"
and preserves_comp :: "('o1,'a1,'o2,'a2)functor => bool"
defines "preserves_dom G ≡
∀f∈Ar1. G\<o> (Dom1 f) = Dom2 (G\<a> f)"
and "preserves_cod G ≡
∀f∈Ar1. G\<o> (Cod1 f) = Cod2 (G\<a> f)"
and "preserves_id G ≡
∀A∈Ob1. G\<a> (Id1 A) = Id2 (G\<o> A)"
and "preserves_comp G ≡
∀f∈Ar1. ∀g∈Ar1. Cod1 f = Dom1 g --> G\<a> (g •1 f) = (G\<a> g) •2 (G\<a> f)"
locale functor = two_cats +
fixes F (structure)
assumes F_preserves_arrows: "F\<a> : Ar1 -> Ar2"
and F_preserves_objects: "F\<o> : Ob1 -> Ob2"
and F_preserves_dom: "preserves_dom F"
and F_preserves_cod: "preserves_cod F"
and F_preserves_id: "preserves_id F"
and F_preserves_comp: "preserves_comp F"
notes F_axioms = F_preserves_arrows F_preserves_objects F_preserves_dom
F_preserves_cod F_preserves_id F_preserves_comp
notes func_pred_defs = preserves_dom_def preserves_cod_def preserves_id_def preserves_comp_def
text {* This gives us nicer notation for asserting that things are functors. *}
abbreviation
Functor ("Functor _ : _ --> _" [81]) where
"Functor F : AA --> BB ≡ functor AA BB F"
subsection {* Simple Lemmas *}
text {* For example: *}
lemma (in functor) "Functor F : AA --> BB" ..
lemma functors_preserve_arrows [intro]:
assumes "Functor F : AA --> BB"
and "f ∈ ar AA"
shows "F\<a> f ∈ ar BB"
proof-
from `Functor F : AA --> BB`
have "F\<a> : ar AA -> ar BB"
by (simp add: functor_def functor_axioms_def)
from this and `f ∈ ar AA`
show ?thesis by (rule funcset_mem)
qed
lemma (in functor) functors_preserve_homsets:
assumes 1: "A ∈ Ob1"
and 2: "B ∈ Ob1"
and 3: "f ∈ Hom1 A B"
shows "F\<a> f ∈ Hom2 (F\<o> A) (F\<o> B)"
proof-
from 3
have 4: "f ∈ Ar"
by (simp add: hom_def)
with F_preserves_arrows
have 5: "F\<a> f ∈ Ar2"
by (rule funcset_mem)
from 4 and F_preserves_dom
have "Dom2 (F\<a> f) = F\<o> (Dom1 f)"
by (simp add: preserves_dom_def)
also from 3 have "… = F\<o> A"
by (simp add: hom_def)
finally have 6: "Dom2 (F\<a> f) = F\<o> A" .
from 4 and F_preserves_cod
have "Cod2 (F\<a> f) = F\<o> (Cod1 f)"
by (simp add: preserves_cod_def)
also from 3 have "… = F\<o> B"
by (simp add: hom_def)
finally have 7: "Cod2 (F\<a> f) = F\<o> B" .
from 5 and 6 and 7
show ?thesis
by (simp add: hom_def)
qed
lemma functors_preserve_objects [intro]:
assumes "Functor F : AA --> BB"
and "A ∈ ob AA"
shows "F\<o> A ∈ ob BB"
proof-
from `Functor F : AA --> BB`
have "F\<o> : ob AA -> ob BB"
by (simp add: functor_def functor_axioms_def)
from this and `A ∈ ob AA`
show ?thesis by (rule funcset_mem)
qed
subsection {* Identity Functor *}
definition
id_func :: "('o,'a,'m) category_scheme => ('o,'a,'o,'a) functor" where
"id_func CC = (|om=(λA∈ob CC. A), am=(λf∈ar CC. f)|)),"
locale one_cat = two_cats +
assumes endo: "BB = AA"
lemma (in one_cat) id_func_preserves_arrows:
shows "(id_func AA)\<a> : Ar -> Ar"
by (unfold id_func_def, rule funcsetI, simp)
lemma (in one_cat) id_func_preserves_objects:
shows "(id_func AA)\<o> : Ob -> Ob"
by (unfold id_func_def, rule funcsetI, simp)
lemma (in one_cat) id_func_preserves_dom:
shows "preserves_dom (id_func AA)"
unfolding preserves_dom_def endo
proof
fix f
assume f: "f ∈ Ar"
hence lhs: "(id_func AA)\<o> (Dom f) = Dom f"
by (simp add: id_func_def) auto
have "(id_func AA)\<a> f = f"
using f by (simp add: id_func_def)
hence rhs: "Dom (id_func AA)\<a> f = Dom f"
by simp
from lhs and rhs show "(id_func AA)\<o> (Dom f) = Dom (id_func AA)\<a> f"
by simp
qed
lemma (in one_cat) id_func_preserves_cod:
"preserves_cod (id_func AA)"
apply (unfold preserves_cod_def, simp only: endo)
proof
fix f
assume f: "f ∈ Ar"
hence lhs: "(id_func AA)\<o> (Cod f) = Cod f"
by (simp add: id_func_def) auto
have "(id_func AA)\<a> f = f"
using f by (simp add: id_func_def)
hence rhs: "Cod (id_func AA)\<a> f = Cod f"
by simp
from lhs and rhs show "(id_func AA)\<o> (Cod f) = Cod (id_func AA)\<a> f"
by simp
qed
lemma (in one_cat) id_func_preserves_id:
"preserves_id (id_func AA)"
unfolding preserves_id_def endo
proof
fix A
assume A: "A ∈ Ob"
hence lhs: "(id_func AA)\<a> (Id A) = Id A"
by (simp add: id_func_def) auto
have "(id_func AA)\<o> A = A"
using A by (simp add: id_func_def)
hence rhs: "Id ((id_func AA)\<o> A) = Id A"
by simp
from lhs and rhs show "(id_func AA)\<a> (Id A) = Id ((id_func AA)\<o> A)"
by simp
qed
lemma (in one_cat) id_func_preserves_comp:
"preserves_comp (id_func AA)"
unfolding preserves_comp_def endo
proof (intro ballI impI)
fix f and g
assume f: "f ∈ Ar" and g: "g ∈ Ar" and "Cod f = Dom g"
then have "g • f ∈ Ar" ..
hence lhs: "(id_func AA)\<a> (g • f) = g • f"
by (simp add: id_func_def)
have id_f: "(id_func AA)\<a> f = f"
using f by (simp add: id_func_def)
have id_g: "(id_func AA)\<a> g = g"
using g by (simp add: id_func_def)
hence rhs: "(id_func AA)\<a> g • (id_func AA)\<a> f = g • f"
by (simp add: id_f id_g)
from lhs and rhs
show "(id_func AA)\<a> (g • f) = (id_func AA)\<a> g • (id_func AA)\<a> f"
by simp
qed
theorem (in one_cat) id_func_functor:
"Functor (id_func AA) : AA --> AA"
proof-
from id_func_preserves_arrows
and id_func_preserves_objects
and id_func_preserves_dom
and id_func_preserves_cod
and id_func_preserves_id
and id_func_preserves_comp
show ?thesis
by unfold_locales (simp_all add: endo preserves_dom_def
preserves_cod_def preserves_id_def preserves_comp_def)
qed
end