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 :: "('o1,'a1,'m1)category_scheme" (structure)
and BB :: "('o2,'a2,'m2)category_scheme" (structure) +
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∈Ar⇘AA⇙. G⇘\<o>⇙ (Dom⇘AA⇙ f) = Dom⇘BB⇙ (G⇘\<a>⇙ f)"
and "preserves_cod G ≡ ∀f∈Ar⇘AA⇙. G⇘\<o>⇙ (Cod⇘AA⇙ f) = Cod⇘BB⇙ (G⇘\<a>⇙ f)"
and "preserves_id G ≡ ∀A∈Ob⇘AA⇙. G⇘\<a>⇙ (Id⇘AA⇙ A) = Id⇘BB⇙ (G⇘\<o>⇙ A)"
and "preserves_comp G ≡
∀f∈Ar⇘AA⇙. ∀g∈Ar⇘AA⇙. Cod⇘AA⇙ f = Dom⇘AA⇙ g --> G⇘\<a>⇙ (g •⇘AA⇙ f) = (G⇘\<a>⇙ g) •⇘BB⇙ (G⇘\<a>⇙ f)"
locale "functor" = two_cats +
fixes F (structure)
assumes F_preserves_arrows: "F⇘\<a>⇙ : Ar⇘AA⇙ -> Ar⇘BB⇙"
and F_preserves_objects: "F⇘\<o>⇙ : Ob⇘AA⇙ -> Ob⇘BB⇙"
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"
begin
lemmas F_axioms = F_preserves_arrows F_preserves_objects F_preserves_dom
F_preserves_cod F_preserves_id F_preserves_comp
lemmas func_pred_defs = preserves_dom_def preserves_cod_def preserves_id_def preserves_comp_def
end
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 ∈ Ob⇘AA⇙"
and 2: "B ∈ Ob⇘AA⇙"
and 3: "f ∈ Hom⇘AA⇙ A B"
shows "F⇘\<a>⇙ f ∈ Hom⇘BB⇙ (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 ∈ Ar⇘BB⇙"
by (rule funcset_mem)
from 4 and F_preserves_dom
have "Dom⇘BB⇙ (F⇘\<a>⇙ f) = F⇘\<o>⇙ (Dom⇘AA⇙ f)"
by (simp add: preserves_dom_def)
also from 3 have "… = F⇘\<o>⇙ A"
by (simp add: hom_def)
finally have 6: "Dom⇘BB⇙ (F⇘\<a>⇙ f) = F⇘\<o>⇙ A" .
from 4 and F_preserves_cod
have "Cod⇘BB⇙ (F⇘\<a>⇙ f) = F⇘\<o>⇙ (Cod⇘AA⇙ f)"
by (simp add: preserves_cod_def)
also from 3 have "… = F⇘\<o>⇙ B"
by (simp add: hom_def)
finally have 7: "Cod⇘BB⇙ (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