header {* Yonedas Lemma *}
theory Yoneda
imports HomFunctors NatTrans
begin
subsection {* The Sandwich Natural Transformation *}
locale Yoneda = functor + into_set +
assumes "AA = (AA::('o,'a,'m)category_scheme)"
fixes sandwich :: "['o,'a,'o] => 'a set_arrow" ("σ'(_,_')")
defines "sandwich A a ≡ (λB∈Ob. (|
set_dom=Hom A B,
set_func=(λf∈Hom A B. set_func (F\<a> f) a),
set_cod=F\<o> B
|)),)"
fixes unsandwich :: "['o,'o => 'a set_arrow] => 'a" ("σ\<leftarrow>'(_,_')")
defines "unsandwich A u ≡ set_func (u A) (Id A)"
lemma (in Yoneda) F_into_set:
"Functor F : AA --> Set"
proof-
from F_axioms have "Functor F : AA --> BB" by intro_locales
thus ?thesis
by (simp only: BB_Set)
qed
lemma (in Yoneda) F_comp_func:
assumes 1: "A ∈ Ob" and 2: "B ∈ Ob" and 3: "C ∈ Ob"
and 4: "g ∈ Hom A B" and 5: "f ∈ Hom B C"
shows "set_func (F\<a> (f • g)) = compose (F\<o> A) (set_func (F\<a> f)) (set_func (F\<a> g))"
proof-
from 4 and 5
have 7: "Cod g = Dom f"
and 8: "g ∈ Ar"
and 9: "f ∈ Ar"
and 10: "Dom g = A"
by (simp_all add: hom_def)
from F_preserves_dom and 8 and 10
have 11: "set_dom (F\<a> g) = F\<o> A"
by (simp add: preserves_dom_def BB_Set Set_def) auto
from F_preserves_comp and 7 and 8 and 9
have "F\<a> (f • g) = (F\<a> f) •2 (F\<a> g)"
by (simp add: preserves_comp_def)
hence "set_func (F\<a> (f • g)) = set_func ((F\<a> f) \<odot> (F\<a> g))"
by (simp add: BB_Set Set_def)
also have "… = compose (F\<o> A) (set_func (F\<a> f)) (set_func (F\<a> g))"
by (simp add: set_comp_def 11)
finally show ?thesis .
qed
lemma (in Yoneda) sandwich_funcset:
assumes A: "A ∈ Ob"
and "a ∈ F\<o> A"
shows "σ(A,a) : Ob -> ar Set"
proof (rule funcsetI)
fix B
assume B: "B ∈ Ob"
thus "σ(A,a) B ∈ ar Set"
proof (simp add: Set_def sandwich_def set_cat_def)
show "set_arrow U (|
set_dom = Hom A B,
set_func = λf∈Hom A B. set_func (F \<a> f) a,
set_cod = F \<o> B|)),"
proof (simp add: set_arrow_def, intro conjI)
show "Hom A B ⊆ U" and "F\<o> B ⊆ U"
by (simp_all add: U_def)
show "(λf∈Hom A B. set_func (F\<a> f) a) ∈ Hom A B -> F\<o> B"
proof (rule funcsetI, simp)
fix f
assume f: "f ∈ Hom A B"
with A B have "F\<a> f ∈ Hom2 (F\<o> A) (F\<o> B)"
by (rule functors_preserve_homsets)
hence "F\<a> f ∈ ar Set"
and "set_dom (F\<a> f) = (F\<o> A)"
and "set_cod (F\<a> f) = (F\<o> B)"
by (simp_all add: hom_def BB_Set Set_def)
hence "set_func (F\<a> f) : (F\<o> A) -> (F\<o> B)"
by (simp add: Set_def set_cat_def set_arrow_def)
thus "set_func (F\<a> f) a ∈ F\<o> B"
using `a ∈ F\<o> A`
by (rule funcset_mem)
qed
qed
qed
qed
lemma (in Yoneda) sandwich_type:
assumes A: "A ∈ Ob" and B: "B ∈ Ob"
and "a ∈ F\<o> A"
shows "σ(A,a) B ∈ hom Set (Hom A B) (F\<o> B)"
proof-
have "σ(A,a) ∈ Ob -> ArSet"
using A and `a ∈ F\<o> A` by (rule sandwich_funcset)
hence "σ(A,a) B ∈ ar Set"
using B by (rule funcset_mem)
thus ?thesis
using B by (simp add: sandwich_def hom_def Set_def)
qed
lemma (in Yoneda) sandwich_commutes:
assumes AOb: "A ∈ Ob" and BOb: "B ∈ Ob" and COb: "C ∈ Ob"
and aFa: "a ∈ F\<o> A"
and fBC: "f ∈ Hom B C"
shows "(F \<a> f) \<odot> (σ(A,a) B) = (σ(A,a) C) \<odot> (Hom(A,_) \<a> f)"
proof-
from fBC have 1: "f ∈ Ar" and 2: "Dom f = B" and 3: "Cod f = C"
by (simp_all add: hom_def)
from BOb have "set_dom ((F \<a> f) \<odot> (σ(A,a) B)) = Hom A B"
by (simp add: set_comp_def sandwich_def)
also have "… = set_dom ((σ(A,a) C) \<odot> (Hom(A,_) \<a> f))"
by (simp add: set_comp_def homf_def 1 2)
finally have set_dom_eq:
"set_dom ((F \<a> f) \<odot> (σ(A,a) B))
= set_dom ((σ(A,a) C) \<odot> (Hom(A,_) \<a> f))" .
from BOb COb fBC have "(F\<a> f) ∈ Hom2 (F\<o> B) (F\<o> C)"
by (rule functors_preserve_homsets)
hence "set_cod ((F \<a> f) \<odot> (σ(A,a) B)) = F\<o> C"
by (simp add: set_comp_def BB_Set Set_def set_cat_def hom_def)
also from COb
have "… = set_cod ((σ(A,a) C) \<odot> (Hom(A,_) \<a> f))"
by (simp add: set_comp_def sandwich_def)
finally have set_cod_eq:
"set_cod ((F \<a> f) \<odot> (σ(A,a) B))
= set_cod ((σ(A,a) C) \<odot> (Hom(A,_) \<a> f))" .
from AOb and BOb and COb and fBC and aFa
have set_func_lhs:
"set_func ((F \<a> f) \<odot> (σ(A,a) B)) =
(λg∈Hom A B. set_func (F \<a> (f • g)) a)"
apply (simp add: set_comp_def sandwich_def compose_def)
apply (rule extensionalityI, rule restrict_extensional, rule restrict_extensional)
by (simp add: F_comp_func compose_def)
have "(op •) : Hom B C -> Hom A B -> Hom A C" ..
from this and fBC
have opfType: "(op •) f : Hom A B -> Hom A C"
by (rule funcset_mem)
from 1 and 2
have "set_func ((σ(A,a) C) \<odot> (Hom(A,_) \<a> f)) =
(λg∈Hom A B. set_func (σ(A,a) C) (f • g))"
apply (simp add: set_comp_def homf_def)
apply (simp add: compose_def)
apply (rule extensionalityI, rule restrict_extensional, rule restrict_extensional)
by auto
also from COb and opfType
have " … = (λg∈Hom A B. set_func (F \<a> (f • g)) a)"
apply (simp add: sandwich_def)
apply (rule extensionalityI, rule restrict_extensional, rule restrict_extensional)
by (simp add:Pi_def)
finally have set_func_rhs:
"set_func ((σ(A,a) C) \<odot> (Hom(A,_) \<a> f)) =
(λg∈Hom A B. set_func (F \<a> (f • g)) a)" .
from set_func_lhs and set_func_rhs have
"set_func ((F \<a> f) \<odot> (σ(A,a) B))
= set_func ((σ(A,a) C) \<odot> (Hom(A,_) \<a> f))"
by simp
with set_dom_eq and set_cod_eq show ?thesis
by simp
qed
lemma (in Yoneda) sandwich_natural:
assumes "A ∈ Ob"
and "a ∈ F\<o> A"
shows "σ(A,a) : Hom(A,_) => F in Func(AA,Set)"
proof (intro natural_transformation.intro natural_transformation_axioms.intro two_cats.intro)
show "category AA" ..
show "category Set"
by (simp only: Set_def)(rule set_cat_cat)
show "Functor Hom(A,_) : AA --> Set"
by (rule homf_into_set)
show "Functor F : AA --> Set"
by (rule F_into_set)
show "∀B∈Ob. σ(A,a) B ∈ hom Set (Hom(A,_)\<o> B) (F\<o> B)"
using assms by (auto simp add: homf_def intro: sandwich_type)
show "σ(A,a) : Ob -> ar Set"
using assms by (rule sandwich_funcset)
show "σ(A,a) ∈ extensional (Ob)"
unfolding sandwich_def by (rule restrict_extensional)
show "∀B∈Ob. ∀C∈Ob. ∀f∈Hom B C.
comp Set (F \<a> f) (σ(A,a) B) = comp Set (σ(A,a) C) (Hom(A,_) \<a> f)"
using assms by (auto simp add: Set_def intro: sandwich_commutes)
qed (intro two_cats_axioms.intro, simp_all)
subsection {* Sandwich Components are Bijective *}
lemma (in Yoneda) unsandwich_left_inverse:
assumes 1: "A ∈ Ob"
and 2: "a ∈ F\<o> A"
shows "σ\<leftarrow>(A,σ(A,a)) = a"
proof-
from 1 have "Id A ∈ Hom A A" ..
with 1
have 3: "σ\<leftarrow>(A,σ(A,a)) = set_func (F\<a> (Id A)) a"
by (simp add: sandwich_def homf_def unsandwich_def)
from F_preserves_id and 1
have 4: "F\<a> (Id A) = id Set (F\<o> A)"
by (simp add: preserves_id_def BB_Set)
from F_preserves_objects and 1
have "F\<o> A ∈ Ob2"
by (rule funcset_mem)
hence "F\<o> A ⊆ U"
by (simp add: BB_Set Set_def set_cat_def)
with 2
have 5: "set_func (id Set (F\<o> A)) a = a"
by (simp add: Set_def set_id_def)
show ?thesis
by (simp add: 3 4 5)
qed
lemma (in Yoneda) unsandwich_right_inverse:
assumes 1: "A ∈ Ob"
and 2: "u : Hom(A,_) => F in Func(AA,Set)"
shows "σ(A,σ\<leftarrow>(A,u)) = u"
proof (rule extensionalityI)
show "σ(A,σ\<leftarrow>(A,u)) ∈ extensional (Ob)"
by (unfold sandwich_def, rule restrict_extensional)
from 2 show "u ∈ extensional (Ob)"
by (simp add: natural_transformation_def natural_transformation_axioms_def)
fix B
assume 3: "B ∈ Ob"
with 1
have one: "σ(A,σ\<leftarrow>(A,u)) B = (|
set_dom = Hom A B,
set_func = (λf∈Hom A B. (set_func (F\<a> f)) (set_func (u A) (Id A))),
set_cod = F\<o> B |)),"
by (simp add: sandwich_def unsandwich_def)
from 1 have "Hom(A,_)\<o> A = Hom A A"
by (simp add: homf_def)
with 1 and 2 have "(u A) ∈ hom Set (Hom A A) (F\<o> A)"
by (simp add: natural_transformation_def natural_transformation_axioms_def,
auto)
hence "set_dom (u A) = Hom A A"
by (simp add: hom_def Set_def)
with 1 have applicable: "Id A ∈ set_dom (u A)"
by (simp)(rule)
have two: "(λf∈Hom A B. (set_func (F\<a> f)) (set_func (u A) (Id A)))
= (λf∈Hom A B. (set_func ((F\<a> f) \<odot> (u A)) (Id A)))"
by (rule extensionalityI,
rule restrict_extensional, rule restrict_extensional,
simp add: set_comp_def compose_def applicable)
from 2
have "(∀X∈Ob. ∀Y∈Ob. ∀f∈Hom X Y. (F\<a> f) •2 (u X) = (u Y) •2 (Hom(A,_)\<a> f))"
by (simp add: natural_transformation_def natural_transformation_axioms_def BB_Set)
with 1 and 3
have three: "(λf∈Hom A B. (set_func ((F\<a> f) \<odot> (u A)) (Id A)))
= (λf∈Hom A B. (set_func ((u B) \<odot> (Hom(A,_))\<a> f)) (Id A))"
apply (simp add: BB_Set Set_def)
apply (rule extensionalityI)
apply (rule restrict_extensional, rule restrict_extensional)
by simp
have "∀f ∈ Hom A B. set_dom (Hom(A,_)\<a> f) = Hom A A"
by (intro ballI, simp add: homf_def hom_def)
have roolz: "!!f. f ∈ Hom A B ==> set_dom (Hom(A,_)\<a> f) = Hom A A"
by (simp add: homf_def hom_def)
from 1 have rooly: "Id A ∈ Hom A A" ..
have roolx: "!!f. f ∈ Hom A B ==> f ∈ Ar"
by (simp add: hom_def)
have roolw: "!!f. f ∈ Hom A B ==> Id A ∈ Hom A (Dom f)"
proof-
fix f
assume "f ∈ Hom A B"
hence "Dom f = A" by (simp add: hom_def)
thus "Id A ∈ Hom A (Dom f)"
by (simp add: rooly)
qed
have annoying: "!!f. f ∈ Hom A B ==> Id A = Id (Dom f)"
by (simp add: hom_def)
have "(λf∈Hom A B. (set_func ((u B) \<odot> (Hom(A,_))\<a> f)) (Id A))
= (λf∈Hom A B. (compose (Hom A A) (set_func (u B)) (set_func (Hom(A,_)\<a> f))) (Id A))"
apply (rule extensionalityI)
apply (rule restrict_extensional, rule restrict_extensional)
by (simp add: compose_def set_comp_def roolz rooly)
also have "… = (λf∈Hom A B. (set_func (u B) f))"
apply (rule extensionalityI)
apply (rule restrict_extensional, rule restrict_extensional)
apply (simp add: compose_def homf_def rooly roolx roolw)
apply (simp only: annoying)
apply (simp add: roolx id_right)
done
finally have four:
"(λf∈Hom A B. (set_func ((u B) \<odot> (Hom(A,_))\<a> f)) (Id A))
= (λf∈Hom A B. (set_func (u B) f))" .
from 2 and 3
have uBhom: "u B ∈ hom Set (Hom(A,_)\<o> B) (F\<o> B)"
by (simp add: natural_transformation_def natural_transformation_axioms_def)
with 3
have five: "set_dom (u B) = Hom A B"
by (simp add: hom_def homf_def Set_def set_cat_def)
from uBhom
have six: "set_cod (u B) = F\<o> B"
by (simp add: hom_def homf_def Set_def set_cat_def)
have seven: "restrict (set_func (u B)) (Hom A B) = set_func (u B)"
apply (rule extensionalityI)
apply (rule restrict_extensional)
proof-
from uBhom have "u B ∈ ar Set"
by (simp add: hom_def)
hence almost: "set_func (u B) ∈ extensional (set_dom (u B))"
by (simp add: Set_def set_cat_def set_arrow_def)
from almost and five
show "set_func (u B) ∈ extensional (Hom A B)"
by simp
fix f
assume "f ∈ Hom A B"
thus "restrict (set_func (u B)) (Hom A B) f = set_func (u B) f"
by simp
qed
from one and two and three and four and five and six and seven
show "σ(A,σ\<leftarrow>(A,u)) B = u B"
by simp
qed
text {* In order to state the lemma, we must rectify a curious
omission from the Isabelle/HOL library. They define the idea of
injectivity on a given set, but surjectivity is only defined relative
to the entire universe of the target type. *}
definition
surj_on :: "['a => 'b, 'a set, 'b set] => bool" where
"surj_on f A B <-> (∀y∈B. ∃x∈A. f(x)=y)"
definition
bij_on :: "['a => 'b, 'a set, 'b set] => bool" where
"bij_on f A B <-> inj_on f A & surj_on f A B"
definition
equinumerous :: "['a set, 'b set] => bool" (infix "≅" 40) where
"equinumerous A B <-> (∃f. bij_on f A B)"
theorem (in Yoneda) Yoneda:
assumes 1: "A ∈ Ob"
shows "F\<o> A ≅ {u. u : Hom(A,_) => F in Func(AA,Set)}"
apply (unfold equinumerous_def bij_on_def surj_on_def inj_on_def)
apply (intro exI conjI bexI ballI impI)
proof-
-- "Sandwich is injective"
fix x and y
assume 2: "x ∈ F\<o> A" and 3: "y ∈ F\<o> A"
and 4: "σ(A,x) = σ(A,y)"
hence "σ\<leftarrow>(A,σ(A,x)) = σ\<leftarrow>(A,σ(A,y))"
by simp
with unsandwich_left_inverse
show "x = y"
by (simp add: 1 2 3)
next
-- "Sandwich covers F A"
fix u
assume "u ∈ {y. y : Hom(A,_) => F in Func (AA,Set)}"
hence 2: "u : Hom(A,_) => F in Func (AA,Set)"
by simp
with 1 show "σ(A,σ\<leftarrow>(A,u)) = u"
by (rule unsandwich_right_inverse)
-- "Sandwich is into F A"
from 1 and 2
have "u A ∈ hom Set (Hom A A) (F\<o> A)"
by (simp add: natural_transformation_def natural_transformation_axioms_def homf_def)
hence "u A ∈ ar Set" and "dom Set (u A) = Hom A A" and "cod Set (u A) = F\<o> A"
by (simp_all add: hom_def)
hence uAfuncset: "set_func (u A) : (Hom A A) -> (F\<o> A)"
by (simp add: Set_def set_cat_def set_arrow_def)
from 1 have "Id A ∈ Hom A A" ..
with uAfuncset
show "σ\<leftarrow>(A,u) ∈ F\<o> A"
by (simp add: unsandwich_def, rule funcset_mem)
qed
end