Theory Functors
section ‹Functors›
theory Functors
imports Cat
begin
subsection ‹Definitions›
record ('o1,'a1,'o2,'a2) "functor" =
om :: "'o1 ⇒ 'o2"
am :: "'a1 ⇒ 'a2"
abbreviation
om_syn ("_ ⇘𝗈⇙" [81]) where
"F⇘𝗈⇙ ≡ om F"
abbreviation
am_syn ("_ ⇘𝖺⇙" [81]) where
"F⇘𝖺⇙ ≡ 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⇘𝗈⇙ (Dom⇘AA⇙ f) = Dom⇘BB⇙ (G⇘𝖺⇙ f)"
and "preserves_cod G ≡ ∀f∈Ar⇘AA⇙. G⇘𝗈⇙ (Cod⇘AA⇙ f) = Cod⇘BB⇙ (G⇘𝖺⇙ f)"
and "preserves_id G ≡ ∀A∈Ob⇘AA⇙. G⇘𝖺⇙ (Id⇘AA⇙ A) = Id⇘BB⇙ (G⇘𝗈⇙ A)"
and "preserves_comp G ≡
∀f∈Ar⇘AA⇙. ∀g∈Ar⇘AA⇙. Cod⇘AA⇙ f = Dom⇘AA⇙ g ⟶ G⇘𝖺⇙ (g ∙⇘AA⇙ f) = (G⇘𝖺⇙ g) ∙⇘BB⇙ (G⇘𝖺⇙ f)"
locale "functor" = two_cats +
fixes F (structure)
assumes F_preserves_arrows: "F⇘𝖺⇙ : Ar⇘AA⇙ → Ar⇘BB⇙"
and F_preserves_objects: "F⇘𝗈⇙ : 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⇘𝖺⇙ f ∈ ar BB"
proof-
from ‹Functor F : AA ⟶ BB›
have "F⇘𝖺⇙ : 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⇘𝖺⇙ f ∈ Hom⇘BB⇙ (F⇘𝗈⇙ A) (F⇘𝗈⇙ B)"
proof-
from 3
have 4: "f ∈ Ar"
by (simp add: hom_def)
with F_preserves_arrows
have 5: "F⇘𝖺⇙ f ∈ Ar⇘BB⇙"
by (rule funcset_mem)
from 4 and F_preserves_dom
have "Dom⇘BB⇙ (F⇘𝖺⇙ f) = F⇘𝗈⇙ (Dom⇘AA⇙ f)"
by (simp add: preserves_dom_def)
also from 3 have "… = F⇘𝗈⇙ A"
by (simp add: hom_def)
finally have 6: "Dom⇘BB⇙ (F⇘𝖺⇙ f) = F⇘𝗈⇙ A" .
from 4 and F_preserves_cod
have "Cod⇘BB⇙ (F⇘𝖺⇙ f) = F⇘𝗈⇙ (Cod⇘AA⇙ f)"
by (simp add: preserves_cod_def)
also from 3 have "… = F⇘𝗈⇙ B"
by (simp add: hom_def)
finally have 7: "Cod⇘BB⇙ (F⇘𝖺⇙ f) = F⇘𝗈⇙ 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⇘𝗈⇙ A ∈ ob BB"
proof-
from ‹Functor F : AA ⟶ BB›
have "F⇘𝗈⇙ : 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)⇘𝖺⇙ : Ar → Ar"
by (unfold id_func_def, rule funcsetI, simp)
lemma (in one_cat) id_func_preserves_objects:
shows "(id_func AA)⇘𝗈⇙ : 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)⇘𝗈⇙ (Dom f) = Dom f"
by (simp add: id_func_def) auto
have "(id_func AA)⇘𝖺⇙ f = f"
using f by (simp add: id_func_def)
hence rhs: "Dom (id_func AA)⇘𝖺⇙ f = Dom f"
by simp
from lhs and rhs show "(id_func AA)⇘𝗈⇙ (Dom f) = Dom (id_func AA)⇘𝖺⇙ 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)⇘𝗈⇙ (Cod f) = Cod f"
by (simp add: id_func_def) auto
have "(id_func AA)⇘𝖺⇙ f = f"
using f by (simp add: id_func_def)
hence rhs: "Cod (id_func AA)⇘𝖺⇙ f = Cod f"
by simp
from lhs and rhs show "(id_func AA)⇘𝗈⇙ (Cod f) = Cod (id_func AA)⇘𝖺⇙ 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)⇘𝖺⇙ (Id A) = Id A"
by (simp add: id_func_def) auto
have "(id_func AA)⇘𝗈⇙ A = A"
using A by (simp add: id_func_def)
hence rhs: "Id ((id_func AA)⇘𝗈⇙ A) = Id A"
by simp
from lhs and rhs show "(id_func AA)⇘𝖺⇙ (Id A) = Id ((id_func AA)⇘𝗈⇙ 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)⇘𝖺⇙ (g ∙ f) = g ∙ f"
by (simp add: id_func_def)
have id_f: "(id_func AA)⇘𝖺⇙ f = f"
using f by (simp add: id_func_def)
have id_g: "(id_func AA)⇘𝖺⇙ g = g"
using g by (simp add: id_func_def)
hence rhs: "(id_func AA)⇘𝖺⇙ g ∙ (id_func AA)⇘𝖺⇙ f = g ∙ f"
by (simp add: id_f id_g)
from lhs and rhs
show "(id_func AA)⇘𝖺⇙ (g ∙ f) = (id_func AA)⇘𝖺⇙ g ∙ (id_func AA)⇘𝖺⇙ 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