Theory Yoneda
chapter Yoneda
theory Yoneda
imports DualCategory SetCat FunctorCategory
begin
text‹
This theory defines the notion of a ``hom-functor'' and gives a proof of the Yoneda Lemma.
In traditional developments of category theory based on set theories such as ZFC,
hom-functors are normally defined to be functors into the large category \textbf{Set}
whose objects are of \emph{all} sets and whose arrows are functions between sets.
However, in HOL there does not exist a single ``type of all sets'', so the notion of
the category of \emph{all} sets and functions does not make sense. To work around this,
we consider a more general setting consisting of a category @{term C} together with
a set category @{term S} and a function @{term "φ :: 'c * 'c ⇒ 'c ⇒ 's"} such that
whenever @{term b} and @{term a} are objects of C then @{term "φ (b, a)"} maps
‹C.hom b a› injectively to ‹S.Univ›. We show that these data induce
a binary functor ‹Hom› from ‹Cop×C› to @{term S} in such a way that @{term φ}
is rendered natural in @{term "(b, a)"}. The Yoneda lemma is then proved for the
Yoneda functor determined by ‹Hom›.
›
section "Hom-Functors"
text‹
A hom-functor for a category @{term C} allows us to regard the hom-sets of @{term C}
as objects of a category @{term S} of sets and functions. Any description of a
hom-functor for @{term C} must therefore specify the category @{term S} and provide
some sort of correspondence between arrows of @{term C} and elements of objects of @{term S}.
If we are to think of each hom-set ‹C.hom b a› of ‹C› as corresponding
to an object ‹Hom (b, a)› of @{term S} then at a minimum it ought to be the
case that the correspondence between arrows and elements is bijective between
‹C.hom b a› and ‹Hom (b, a)›. The ‹hom_functor› locale defined
below captures this idea by assuming a set category @{term S} and a function @{term φ}
taking arrows of @{term C} to elements of ‹S.Univ›, such that @{term φ} is injective
on each set ‹C.hom b a›. We show that these data induce a functor ‹Hom›
from ‹Cop×C› to ‹S› in such a way that @{term φ} becomes a natural
bijection between ‹C.hom b a› and ‹Hom (b, a)›.
›
locale hom_functor =
C: category C +
S: set_category S setp
for C :: "'c comp" (infixr "⋅" 55)
and S :: "'s comp" (infixr "⋅⇩S" 55)
and setp :: "'s set ⇒ bool"
and φ :: "'c * 'c ⇒ 'c ⇒ 's" +
assumes maps_arr_to_Univ: "C.arr f ⟹ φ (C.dom f, C.cod f) f ∈ S.Univ"
and local_inj: "⟦ C.ide b; C.ide a ⟧ ⟹ inj_on (φ (b, a)) (C.hom b a)"
and small_homs: "⟦ C.ide b; C.ide a ⟧ ⟹ setp (φ (b, a) ` C.hom b a)"
begin
sublocale Cop: dual_category C ..
sublocale CopxC: product_category Cop.comp C ..
notation S.in_hom ("«_ : _ →⇩S _»")
notation CopxC.comp (infixr "⊙" 55)
notation CopxC.in_hom ("«_ : _ ⇌ _»")
definition set
where "set ba ≡ φ (fst ba, snd ba) ` C.hom (fst ba) (snd ba)"
lemma set_subset_Univ:
assumes "C.ide b" and "C.ide a"
shows "set (b, a) ⊆ S.Univ"
using assms set_def maps_arr_to_Univ CopxC.ide_char by auto
definition ψ :: "'c * 'c ⇒ 's ⇒ 'c"
where "ψ ba = inv_into (C.hom (fst ba) (snd ba)) (φ ba)"
lemma φ_mapsto:
assumes "C.ide b" and "C.ide a"
shows "φ (b, a) ∈ C.hom b a → set (b, a)"
using assms set_def maps_arr_to_Univ by auto
lemma ψ_mapsto:
assumes "C.ide b" and "C.ide a"
shows "ψ (b, a) ∈ set (b, a) → C.hom b a"
using assms set_def ψ_def local_inj by auto
lemma ψ_φ [simp]:
assumes "«f : b → a»"
shows "ψ (b, a) (φ (b, a) f) = f"
using assms local_inj [of b a] ψ_def by fastforce
lemma φ_ψ [simp]:
assumes "C.ide b" and "C.ide a"
and "x ∈ set (b, a)"
shows "φ (b, a) (ψ (b, a) x) = x"
using assms set_def local_inj ψ_def by auto
lemma ψ_img_set:
assumes "C.ide b" and "C.ide a"
shows "ψ (b, a) ` set (b, a) = C.hom b a"
using assms ψ_def set_def local_inj by auto
text‹
A hom-functor maps each arrow @{term "(g, f)"} of @{term "CopxC"}
to the arrow of the set category @{term[source=true] S} corresponding to the function
that takes an arrow @{term h} of @{term C} to the arrow @{term "C f (C h g)"} of @{term C}
obtained by precomposing with @{term g} and postcomposing with @{term f}.
›
definition map
where "map gf =
(if CopxC.arr gf then
S.mkArr (set (CopxC.dom gf)) (set (CopxC.cod gf))
(φ (CopxC.cod gf) o (λh. snd gf ⋅ h ⋅ fst gf) o ψ (CopxC.dom gf))
else S.null)"
lemma arr_map:
assumes "CopxC.arr gf"
shows "S.arr (map gf)"
proof -
have "φ (CopxC.cod gf) o (λh. snd gf ⋅ h ⋅ fst gf) o ψ (CopxC.dom gf)
∈ set (CopxC.dom gf) → set (CopxC.cod gf)"
using assms φ_mapsto [of "fst (CopxC.cod gf)" "snd (CopxC.cod gf)"]
ψ_mapsto [of "fst (CopxC.dom gf)" "snd (CopxC.dom gf)"]
by fastforce
thus ?thesis
using assms map_def set_subset_Univ small_homs
by (simp add: set_def)
qed
lemma map_ide [simp]:
assumes "C.ide b" and "C.ide a"
shows "map (b, a) = S.mkIde (set (b, a))"
proof -
have "map (b, a) = S.mkArr (set (b, a)) (set (b, a))
(φ (b, a) o (λh. a ⋅ h ⋅ b) o ψ (b, a))"
using assms map_def by auto
also have "... = S.mkArr (set (b, a)) (set (b, a)) (λh. h)"
proof -
have "S.mkArr (set (b, a)) (set (b, a)) (λh. h) = ..."
using assms set_subset_Univ set_def C.comp_arr_dom C.comp_cod_arr
S.arr_mkIde small_homs
by (intro S.mkArr_eqI', simp, fastforce)
thus ?thesis by auto
qed
also have "... = S.mkIde (set (b, a))"
using assms S.mkIde_as_mkArr set_subset_Univ small_homs set_def by simp
finally show ?thesis by blast
qed
lemma set_map:
assumes "C.ide a" and "C.ide b"
shows "S.set (map (b, a)) = set (b, a)"
using assms map_ide set_subset_Univ small_homs set_def by simp
text‹
The definition does in fact yield a functor.
›
sublocale "functor" CopxC.comp S map
proof
show "⋀gf. ¬ CopxC.arr gf ⟹ map gf = S.null"
using map_def by auto
fix gf
assume gf: "CopxC.arr gf"
thus arr: "S.arr (map gf)" using gf arr_map by blast
show "S.dom (map gf) = map (CopxC.dom gf)"
using arr gf local.map_def map_ide by auto
show "S.cod (map gf) = map (CopxC.cod gf)"
using gf set_subset_Univ ψ_mapsto map_def set_def S.arr_mkIde arr map_ide by auto
next
fix gf gf'
assume gf': "CopxC.seq gf' gf"
hence seq: "C.arr (fst gf) ∧ C.arr (snd gf) ∧ C.dom (snd gf') = C.cod (snd gf) ∧
C.arr (fst gf') ∧ C.arr (snd gf') ∧ C.dom (fst gf) = C.cod (fst gf')"
by (elim CopxC.seqE C.seqE, auto)
have 0: "S.arr (map (CopxC.comp gf' gf))"
using gf' arr_map by blast
have 1: "map (gf' ⊙ gf) =
S.mkArr (set (CopxC.dom gf)) (set (CopxC.cod gf'))
(φ (CopxC.cod gf') o (λh. snd (gf' ⊙ gf) ⋅ h ⋅ fst (gf' ⊙ gf))
o ψ (CopxC.dom gf))"
using gf' map_def using CopxC.cod_comp CopxC.dom_comp by auto
also have "... = S.mkArr (set (CopxC.dom gf)) (set (CopxC.cod gf'))
(φ (CopxC.cod gf') ∘ (λh. snd gf' ⋅ h ⋅ fst gf') ∘ ψ (CopxC.dom gf')
∘
(φ (CopxC.cod gf) ∘ (λh. snd gf ⋅ h ⋅ fst gf) ∘ ψ (CopxC.dom gf)))"
proof (intro S.mkArr_eqI')
show "S.arr (S.mkArr (set (CopxC.dom gf)) (set (CopxC.cod gf'))
(φ (CopxC.cod gf') ∘ (λh. snd (gf' ⊙ gf) ⋅ h ⋅ fst (gf' ⊙ gf))
∘ ψ (CopxC.dom gf)))"
using 0 1 by simp
show "⋀x. x ∈ set (CopxC.dom gf) ⟹
(φ (CopxC.cod gf') ∘ (λh. snd (gf' ⊙ gf) ⋅ h ⋅ fst (gf' ⊙ gf)) ∘
ψ (CopxC.dom gf)) x =
(φ (CopxC.cod gf') ∘ (λh. snd gf' ⋅ h ⋅ fst gf') ∘ ψ (CopxC.dom gf') ∘
(φ (CopxC.cod gf) ∘ (λh. snd gf ⋅ h ⋅ fst gf) ∘ ψ (CopxC.dom gf))) x"
using gf' ψ_mapsto set_def ψ_φ C.comp_assoc by fastforce
qed
also have "... = map gf' ⋅⇩S map gf"
using seq gf' map_def arr_map [of gf] arr_map [of gf'] S.comp_mkArr by auto
finally show "map (gf' ⊙ gf) = map gf' ⋅⇩S map gf"
using seq gf' by auto
qed
lemma is_functor:
shows "functor CopxC.comp S map" ..
sublocale binary_functor Cop.comp C S map ..
lemma is_binary_functor:
shows "binary_functor Cop.comp C S map" ..
text‹
The map @{term φ} determines a bijection between @{term "C.hom b a"} and
@{term "set (b, a)"} which is natural in @{term "(b, a)"}.
›
lemma φ_local_bij:
assumes "C.ide b" and "C.ide a"
shows "bij_betw (φ (b, a)) (C.hom b a) (set (b, a))"
using assms local_inj inj_on_imp_bij_betw set_def by auto
lemma φ_natural:
assumes "C.arr g" and "C.arr f" and "h ∈ C.hom (C.cod g) (C.dom f)"
shows "φ (C.dom g, C.cod f) (f ⋅ h ⋅ g) = S.Fun (map (g, f)) (φ (C.cod g, C.dom f) h)"
proof -
let ?φh = "φ (C.cod g, C.dom f) h"
have φh: "?φh ∈ set (C.cod g, C.dom f)"
using assms φ_mapsto set_def by simp
have gf: "CopxC.arr (g, f)" using assms by simp
have "S.Fun (map (g, f)) ?φh =
(φ (C.dom g, C.cod f) ∘ (λh. f ⋅ h ⋅ g) ∘ ψ (C.cod g, C.dom f)) ?φh"
proof -
have "S.Fun (map (g, f)) =
restrict (φ (C.dom g, C.cod f) ∘ (λh. f ⋅ h ⋅ g) ∘ ψ (C.cod g, C.dom f))
(set (C.cod g, C.dom f))"
proof -
have "map (g, f) =
S.mkArr (set (C.cod g, C.dom f)) (set (C.dom g, C.cod f))
(φ (C.dom g, C.cod f) ∘ (λh. f ⋅ h ⋅ g) ∘ ψ (C.cod g, C.dom f))"
using assms map_def by simp
moreover have "S.arr (map (g, f))" using gf by simp
ultimately show ?thesis
using S.Fun_mkArr by simp
qed
thus ?thesis
using φh by simp
qed
also have "... = φ (C.dom g, C.cod f) (f ⋅ h ⋅ g)"
using assms(3) by simp
finally show ?thesis by auto
qed
lemma Dom_map:
assumes "C.arr g" and "C.arr f"
shows "S.Dom (map (g, f)) = set (C.cod g, C.dom f)"
using assms map_def preserves_arr by auto
lemma Cod_map:
assumes "C.arr g" and "C.arr f"
shows "S.Cod (map (g, f)) = set (C.dom g, C.cod f)"
using assms map_def preserves_arr by auto
lemma Fun_map:
assumes "C.arr g" and "C.arr f"
shows "S.Fun (map (g, f)) =
restrict (φ (C.dom g, C.cod f) o (λh. f ⋅ h ⋅ g) o ψ (C.cod g, C.dom f))
(set (C.cod g, C.dom f))"
using assms map_def preserves_arr by force
lemma map_simp_1:
assumes "C.arr g" and "C.ide a"
shows "map (g, a) = S.mkArr (set (C.cod g, a)) (set (C.dom g, a))
(φ (C.dom g, a) o Cop.comp g o ψ (C.cod g, a))"
proof -
have 1: "map (g, a) = S.mkArr (set (C.cod g, a)) (set (C.dom g, a))
(φ (C.dom g, a) o (λh. a ⋅ h ⋅ g) o ψ (C.cod g, a))"
using assms map_def by force
also have "... = S.mkArr (set (C.cod g, a)) (set (C.dom g, a))
(φ (C.dom g, a) o Cop.comp g o ψ (C.cod g, a))"
using assms 1 preserves_arr [of "(g, a)"] set_def C.in_homI C.comp_cod_arr
by (intro S.mkArr_eqI) auto
finally show ?thesis by blast
qed
lemma map_simp_2:
assumes "C.ide b" and "C.arr f"
shows "map (b, f) = S.mkArr (set (b, C.dom f)) (set (b, C.cod f))
(φ (b, C.cod f) o C f o ψ (b, C.dom f))"
proof -
have 1: "map (b, f) = S.mkArr (set (b, C.dom f)) (set (b, C.cod f))
(φ (b, C.cod f) o (λh. f ⋅ h ⋅ b) o ψ (b, C.dom f))"
using assms map_def by force
also have "... = S.mkArr (set (b, C.dom f)) (set (b, C.cod f))
(φ (b, C.cod f) o C f o ψ (b, C.dom f))"
using assms 1 preserves_arr [of "(b, f)"] set_def C.in_homI C.comp_arr_dom
by (intro S.mkArr_eqI) auto
finally show ?thesis by blast
qed
end
text‹
Every category @{term C} has a hom-functor: take @{term S} to be the replete set category
generated by the arrow type ‹'a› of @{term C} and take @{term "φ (b, a)"} to be the map
‹S.UP :: 'a ⇒ 'a SC.arr›.
›
context category
begin
interpretation S: replete_setcat ‹TYPE('a)› .
lemma has_hom_functor:
shows "hom_functor C S.comp S.setp (λ_. S.UP)"
using S.UP_mapsto S.inj_UP injD inj_onI
by unfold_locales (auto simp add: inj_def inj_onI)
end
text‹
The locales ‹set_valued_functor› and ‹set_valued_transformation› provide some
abbreviations that are convenient when working with functors and natural transformations
into a set category.
›
locale set_valued_functor =
C: category C +
S: set_category S setp +
"functor" C S F
for C :: "'c comp"
and S :: "'s comp"
and setp :: "'s set ⇒ bool"
and F :: "'c ⇒ 's"
begin
abbreviation SET :: "'c ⇒ 's set"
where "SET a ≡ S.set (F a)"
abbreviation DOM :: "'c ⇒ 's set"
where "DOM f ≡ S.Dom (F f)"
abbreviation COD :: "'c ⇒ 's set"
where "COD f ≡ S.Cod (F f)"
abbreviation FUN :: "'c ⇒ 's ⇒ 's"
where "FUN f ≡ S.Fun (F f)"
end
locale set_valued_transformation =
C: category C +
S: set_category S setp +
F: set_valued_functor C S setp F +
G: set_valued_functor C S setp G +
natural_transformation C S F G τ
for C :: "'c comp"
and S :: "'s comp"
and setp :: "'s set ⇒ bool"
and F :: "'c ⇒ 's"
and G :: "'c ⇒ 's"
and τ :: "'c ⇒ 's"
begin
abbreviation DOM :: "'c ⇒ 's set"
where "DOM f ≡ S.Dom (τ f)"
abbreviation COD :: "'c ⇒ 's set"
where "COD f ≡ S.Cod (τ f)"
abbreviation FUN :: "'c ⇒ 's ⇒ 's"
where "FUN f ≡ S.Fun (τ f)"
end
section "Yoneda Functors"
text‹
A Yoneda functor is the functor from @{term C} to ‹[Cop, S]› obtained by ``currying''
a hom-functor in its first argument.
›
locale yoneda_functor =
C: category C +
Cop: dual_category C +
CopxC: product_category Cop.comp C +
S: set_category S setp +
Hom: hom_functor C S setp φ
for C :: "'c comp" (infixr "⋅" 55)
and S :: "'s comp" (infixr "⋅⇩S" 55)
and setp :: "'s set ⇒ bool"
and φ :: "'c * 'c ⇒ 'c ⇒ 's"
begin
sublocale Cop_S: functor_category Cop.comp S ..
sublocale curried_functor' Cop.comp C S Hom.map ..
notation Cop_S.in_hom ("«_ : _ →⇩[⇩C⇩o⇩p⇩,⇩S⇩] _»")
abbreviation ψ
where "ψ ≡ Hom.ψ"
text‹
An arrow of the functor category ‹[Cop, S]› consists of a natural transformation
bundled together with its domain and codomain functors. However, when considering
a Yoneda functor from @{term[source=true] C} to ‹[Cop, S]› we generally are only
interested in the mapping @{term Y} that takes each arrow @{term f} of @{term[source=true] C}
to the corresponding natural transformation @{term "Y f"}. The domain and codomain functors
are then the identity transformations @{term "Y (C.dom f)"} and @{term "Y (C.cod f)"}.
›
definition Y
where "Y f ≡ Cop_S.Map (map f)"
lemma Y_simp [simp]:
assumes "C.arr f"
shows "Y f = (λg. Hom.map (g, f))"
using assms preserves_arr Y_def by simp
lemma Y_ide_is_functor:
assumes "C.ide a"
shows "functor Cop.comp S (Y a)"
using assms Y_def Hom.fixing_ide_gives_functor_2 by force
lemma Y_arr_is_transformation:
assumes "C.arr f"
shows "natural_transformation Cop.comp S (Y (C.dom f)) (Y (C.cod f)) (Y f)"
using assms Y_def [of f] map_def Hom.fixing_arr_gives_natural_transformation_2
preserves_dom preserves_cod by fastforce
lemma Y_ide_arr [simp]:
assumes a: "C.ide a" and "«g : b' → b»"
shows "«Y a g : Hom.map (b, a) →⇩S Hom.map (b', a)»"
and "Y a g = S.mkArr (Hom.set (b, a)) (Hom.set (b', a)) (φ (b', a) o Cop.comp g o ψ (b, a))"
using assms Hom.map_simp_1 by (fastforce, auto)
lemma Y_arr_ide [simp]:
assumes "C.ide b" and "«f : a → a'»"
shows "«Y f b : Hom.map (b, a) →⇩S Hom.map (b, a')»"
and "Y f b = S.mkArr (Hom.set (b, a)) (Hom.set (b, a')) (φ (b, a') o C f o ψ (b, a))"
using assms apply fastforce
using assms Hom.map_simp_2 by auto
end
locale yoneda_functor_fixed_object =
yoneda_functor +
fixes a
assumes ide_a: "C.ide a"
begin
sublocale "functor" Cop.comp S ‹Y a›
using ide_a Y_ide_is_functor by auto
sublocale set_valued_functor Cop.comp S setp ‹Y a› ..
end
text‹
The Yoneda lemma states that, given a category @{term C} and a functor @{term F}
from @{term Cop} to a set category @{term S}, for each object @{term a} of @{term C},
the set of natural transformations from the contravariant functor @{term "Y a"}
to @{term F} is in bijective correspondence with the set ‹F.SET a›
of elements of @{term "F a"}.
Explicitly, if @{term e} is an arbitrary element of the set ‹F.SET a›,
then the functions ‹λx. F.FUN (ψ (b, a) x) e› are the components of a
natural transformation from @{term "Y a"} to @{term F}.
Conversely, if @{term τ} is a natural transformation from @{term "Y a"} to @{term F},
then the component @{term "τ b"} of @{term τ} at an arbitrary object @{term b}
is completely determined by the single arrow ‹τ.FUN a (φ (a, a) a)))›,
which is the the element of ‹F.SET a› that corresponds to the image of the
identity @{term a} under the function ‹τ.FUN a›.
Then @{term "τ b"} is the arrow from @{term "Y a b"} to @{term "F b"} corresponding
to the function ‹λx. (F.FUN (ψ (b, a) x) (τ.FUN a (φ (a, a) a)))›
from ‹S.set (Y a b)› to ‹F.SET b›.
The above expressions look somewhat more complicated than the usual versions due to the
need to account for the coercions @{term φ} and @{term ψ}.
›
locale yoneda_lemma =
yoneda_functor_fixed_object C S setp φ a +
F: set_valued_functor Cop.comp S setp F
for C :: "'c comp" (infixr "⋅" 55)
and S :: "'s comp" (infixr "⋅⇩S" 55)
and setp :: "'s set ⇒ bool"
and φ :: "'c * 'c ⇒ 'c ⇒ 's"
and F :: "'c ⇒ 's"
and a :: 'c
begin
text‹
The mapping that evaluates the component @{term "τ a"} at @{term a} of a
natural transformation @{term τ} from @{term Y} to @{term F} on the element
@{term "φ (a, a) a"} of @{term "SET a"}, yielding an element of @{term "F.SET a"}.
›
definition ℰ :: "('c ⇒ 's) ⇒ 's"
where "ℰ τ = S.Fun (τ a) (φ (a, a) a)"
text‹
The mapping that takes an element @{term e} of @{term "F.SET a"} and produces
a map on objects of @{term[source=true] C} whose value at @{term b} is the arrow of
@{term[source=true] S} corresponding to the function
@{term "(λx. F.FUN (ψ (b, a) x) e) ∈ Hom.set (b, a) → F.SET b"}.
›
definition 𝒯⇩o :: "'s ⇒ 'c ⇒ 's"
where "𝒯⇩o e b = S.mkArr (Hom.set (b, a)) (F.SET b) (λx. F.FUN (ψ (b, a) x) e)"
lemma 𝒯⇩o_in_hom:
assumes e: "e ∈ S.set (F a)" and b: "C.ide b"
shows "«𝒯⇩o e b : Y a b →⇩S F b»"
proof -
have "(λx. F.FUN (ψ (b, a) x) e) ∈ Hom.set (b, a) → F.SET b"
proof
fix x
assume x: "x ∈ Hom.set (b, a)"
thus "F.FUN (ψ (b, a) x) e ∈ F.SET b"
using assms e ide_a Hom.ψ_mapsto S.Fun_mapsto [of "F (ψ (b, a) x)"] by force
qed
thus ?thesis
using ide_a b S.mkArr_in_hom Hom.set_subset_Univ S.mkIde_set 𝒯⇩o_def
by (metis C.ideD(1) Cop.ide_char F.preserves_ide Hom.set_map S.setp_set_ide
preserves_ide Y_simp)
qed
text‹
For each @{term "e ∈ F.SET a"}, the mapping @{term "𝒯⇩o e"} gives the components
of a natural transformation @{term 𝒯} from @{term "Y a"} to @{term F}.
›
lemma 𝒯⇩o_induces_transformation:
assumes e: "e ∈ S.set (F a)"
shows "transformation_by_components Cop.comp S (Y a) F (𝒯⇩o e)"
proof
show "⋀b. Cop.ide b ⟹ «𝒯⇩o e b : Y a b →⇩S F b»"
using ide_a e 𝒯⇩o_in_hom by simp
fix g :: 'c
assume g: "Cop.arr g"
let ?b = "Cop.dom g"
let ?b' = "Cop.cod g"
show "𝒯⇩o e (Cop.cod g) ⋅⇩S Y a g = F g ⋅⇩S 𝒯⇩o e (Cop.dom g)"
proof -
have 1: "𝒯⇩o e (Cop.cod g) ⋅⇩S Y a g =
S.mkArr (Hom.set (?b, a)) (F.SET ?b')
((λx. F.FUN (ψ (?b', a) x) e) o (φ (?b', a) o Cop.comp g o ψ (?b, a)))"
proof -
have "S.arr (S.mkArr (Hom.set (?b', a)) (F.SET ?b') (λs. F.FUN (ψ (?b', a) s) e)) ∧
S.dom (S.mkArr (Hom.set (?b', a)) (F.SET ?b') (λs. F.FUN (ψ (?b', a) s) e))
= Y a ?b' ∧
S.cod (S.mkArr (Hom.set (?b', a)) (F.SET ?b') (λs. F.FUN (ψ (?b', a) s) e))
= F ?b'"
using Cop.cod_char 𝒯⇩o_def 𝒯⇩o_in_hom e g
by (metis Cop.ide_char Cop.ide_cod S.in_homE)
moreover have "Y a g = S.mkArr (Hom.set (?b, a)) (Hom.set (?b', a))
(φ (?b', a) ∘ Cop.comp g ∘ ψ (?b, a))"
using Y_ide_arr [of a g ?b' ?b] ide_a g by auto
ultimately show ?thesis
using ide_a e g Y_ide_arr Cop.cod_char 𝒯⇩o_def S.comp_mkArr preserves_arr
by metis
qed
also have "... = S.mkArr (Hom.set (?b, a)) (F.SET ?b')
(F.FUN g o (λx. F.FUN (ψ (?b, a) x) e))"
proof (intro S.mkArr_eqI')
show "S.arr (S.mkArr (Hom.set (?b, a)) (F.SET ?b')
((λx. F.FUN (ψ (?b', a) x) e)
o (φ (?b', a) o Cop.comp g o ψ (?b, a))))"
proof (intro S.arr_mkArrI)
show "setp (Hom.set (Cop.dom g, a))"
by (metis C.ideD(1) Cop.arr_dom Cop.ide_char CopxC.arrI⇩P⇩C Hom.arr_map
S.arr_mkIde Cop.ide_dom g Hom.map_ide ide_a)
show "setp (F.SET (Cop.cod g))"
using g by force
show "(λx. F.FUN (ψ (?b', a) x) e) o (φ (?b', a) o Cop.comp g o ψ (?b, a))
∈ Hom.set (?b, a) → F.SET ?b'"
proof -
have "S.arr (S (𝒯⇩o e ?b') (Y a g))"
using ide_a e g 𝒯⇩o_in_hom Y_ide_arr(1) Cop.ide_char Cop.ide_cod by blast
thus ?thesis using 1 by simp
qed
qed
show "⋀x. x ∈ Hom.set (?b, a) ⟹
((λx. F.FUN (ψ (?b', a) x) e) o (φ (?b', a) o Cop.comp g o ψ (?b, a))) x
= (F.FUN g o (λx. F.FUN (ψ (?b, a) x) e)) x"
proof -
fix x
assume x: "x ∈ Hom.set (?b, a)"
have "((λx. (F.FUN o ψ (?b', a)) x e)
o (φ (?b', a) o Cop.comp g o ψ (?b, a))) x
= F.FUN (ψ (?b', a) (φ (?b', a) (C (ψ (?b, a) x) g))) e"
by simp
also have "... = (F.FUN g o (F.FUN o ψ (?b, a)) x) e"
proof -
have "«ψ (?b, a) x : ?b → a»"
using ide_a x g Hom.ψ_mapsto [of ?b a] by auto
thus ?thesis
using assms g Hom.ψ_φ F.preserves_comp by fastforce
qed
also have "... = (F.FUN g o (λx. F.FUN (ψ (?b, a) x) e)) x" by fastforce
finally show "((λx. F.FUN (ψ (?b', a) x) e) o (φ (?b', a) o Cop.comp g o ψ (?b, a))) x
= (F.FUN g o (λx. F.FUN (ψ (?b, a) x) e)) x"
by simp
qed
qed
also have "... = F g ⋅⇩S 𝒯⇩o e ?b"
proof -
have "S.arr (F g) ∧ F g = S.mkArr (F.SET ?b) (F.SET ?b') (F.FUN g)"
using g S.mkArr_Fun [of "F g"] by simp
moreover have
"S.arr (𝒯⇩o e ?b) ∧
𝒯⇩o e ?b = S.mkArr (Hom.set (?b, a)) (F.SET ?b) (λx. F.FUN (ψ (?b, a) x) e)"
using e g 𝒯⇩o_def 𝒯⇩o_in_hom
by (metis C.ide_cod Cop.arr_char Cop.dom_char S.in_homE)
ultimately show ?thesis
using S.comp_mkArr by metis
qed
finally show ?thesis by blast
qed
qed
definition 𝒯 :: "'s ⇒ 'c ⇒ 's"
where "𝒯 e ≡ transformation_by_components.map Cop.comp S (Y a) (𝒯⇩o e)"
end
locale yoneda_lemma_fixed_e =
yoneda_lemma +
fixes e
assumes E: "e ∈ F.SET a"
begin
interpretation 𝒯e: transformation_by_components Cop.comp S ‹Y a› F ‹𝒯⇩o e›
using E 𝒯⇩o_induces_transformation by auto
sublocale 𝒯e: natural_transformation Cop.comp S ‹Y a› F ‹𝒯 e›
unfolding 𝒯_def ..
lemma natural_transformation_𝒯e:
shows "natural_transformation Cop.comp S (Y a) F (𝒯 e)" ..
lemma 𝒯e_ide:
assumes "Cop.ide b"
shows "S.arr (𝒯 e b)"
and "𝒯 e b = S.mkArr (Hom.set (b, a)) (F.SET b) (λx. F.FUN (ψ (b, a) x) e)"
using assms apply auto[1]
using assms 𝒯⇩o_def 𝒯_def by auto
end
locale yoneda_lemma_fixed_τ =
yoneda_lemma +
τ: natural_transformation Cop.comp S ‹Y a› F τ
for τ
begin
sublocale τ: set_valued_transformation Cop.comp S setp ‹Y a› F τ ..
text‹
The key lemma: The component @{term "τ b"} of @{term τ} at an arbitrary object @{term b}
is completely determined by the single element @{term "τ.FUN a (φ (a, a) a) ∈ F.SET a"}.
›
lemma τ_ide:
assumes b: "Cop.ide b"
shows "τ b = S.mkArr (Hom.set (b, a)) (F.SET b)
(λx. (F.FUN (ψ (b, a) x) (τ.FUN a (φ (a, a) a))))"
proof -
let ?φa = "φ (a, a) a"
have φa: "φ (a, a) a ∈ Hom.set (a, a)" using ide_a Hom.φ_mapsto by fastforce
have 1: "τ b = S.mkArr (Hom.set (b, a)) (F.SET b) (τ.FUN b)"
using ide_a b S.mkArr_Fun [of "τ b"] Hom.set_map by auto
also have
"... = S.mkArr (Hom.set (b, a)) (F.SET b) (λx. (F.FUN (ψ (b, a) x) (τ.FUN a ?φa)))"
proof (intro S.mkArr_eqI')
show 2: "S.arr (S.mkArr (Hom.set (b, a)) (F.SET b) (τ.FUN b))"
using ide_a b 1 S.mkArr_Fun [of "τ b"] Hom.set_map by auto
show "⋀x. x ∈ Hom.set (b, a) ⟹ τ.FUN b x = (F.FUN (ψ (b, a) x) (τ.FUN a ?φa))"
proof -
fix x
assume x: "x ∈ Hom.set (b, a)"
let ?ψx = "ψ (b, a) x"
have ψx: "«?ψx : b → a»"
using ide_a b x Hom.ψ_mapsto [of b a] by auto
show "τ.FUN b x = (F.FUN (ψ (b, a) x) (τ.FUN a ?φa))"
proof -
have "τ.FUN b x = S.Fun (τ b ⋅⇩S Y a ?ψx) ?φa"
proof -
have "τ.FUN b x = τ.FUN b ((φ (b, a) o Cop.comp ?ψx) a)"
using ide_a b x ψx Hom.φ_ψ
by (metis C.comp_cod_arr C.in_homE C.ide_dom Cop.comp_def comp_apply)
also have "... = (τ.FUN b o (φ (b, a) o Cop.comp ?ψx o ψ (a, a))) ?φa"
using ide_a b C.ide_in_hom by simp
also have "... = S.Fun (τ b ⋅⇩S Y a ?ψx) ?φa"
proof -
have "S.seq (τ b) (Y a ?ψx) ∧
τ b ⋅⇩S Y a ?ψx =
S.mkArr (Hom.set (a, a)) (F.SET b)
(τ.FUN b o (φ (b, a) ∘ Cop.comp ?ψx ∘ ψ (a, a)))"
proof
show "S.seq (τ b) (Y a ?ψx)"
using ψx τ.is_natural_2 by fastforce
show "τ b ⋅⇩S Y a ?ψx =
S.mkArr (Hom.set (a, a)) (F.SET b)
(τ.FUN b o (φ (b, a) ∘ Cop.comp ?ψx ∘ ψ (a, a)))"
by (metis 1 2 Cop.arrI Cop.hom_char S.comp_mkArr Y_ide_arr(2)
ψx ide_a preserves_arr)
qed
thus ?thesis
using ide_a b x Hom.φ_mapsto S.Fun_mkArr by force
qed
finally show ?thesis by auto
qed
also have "... = S.Fun (F ?ψx ⋅⇩S τ a) ?φa"
using ide_a b ψx τ.naturality by force
also have "... = F.FUN ?ψx (τ.FUN a ?φa)"
proof -
have "restrict (S.Fun (F ?ψx ⋅⇩S τ a)) (Hom.set (a, a))
= restrict (F.FUN (ψ (b, a) x) o τ.FUN a) (Hom.set (a, a))"
proof -
have "S.arr (F ?ψx ⋅⇩S τ a) ∧
F ?ψx ⋅⇩S τ a = S.mkArr (Hom.set (a, a)) (F.SET b) (F.FUN ?ψx o τ.FUN a)"
proof
show 1: "S.seq (F ?ψx) (τ a)"
using ψx ide_a τ.preserves_cod F.preserves_dom
by (elim C.in_homE, auto)
show "F ?ψx ⋅⇩S τ a = S.mkArr (Hom.set (a, a)) (F.SET b) (F.FUN ?ψx o τ.FUN a)"
proof -
have "τ a = S.mkArr (Hom.set (a, a)) (F.SET a) (τ.FUN a)"
using ide_a 1 S.mkArr_Fun [of "τ a"] Hom.set_map by auto
moreover have "F ?ψx = S.mkArr (F.SET a) (F.SET b) (F.FUN ?ψx)"
using x ψx 1 S.mkArr_Fun [of "F ?ψx"] by fastforce
ultimately show ?thesis
using 1 S.comp_mkArr [of "Hom.set (a, a)" "F.SET a" "τ.FUN a"
"F.SET b" "F.FUN ?ψx"]
by (elim S.seqE, auto)
qed
qed
thus ?thesis by force
qed
thus "S.Fun (F (ψ (b, a) x) ⋅⇩S τ a) ?φa = F.FUN ?ψx (τ.FUN a ?φa)"
using ide_a φa restr_eqE [of "S.Fun (F ?ψx ⋅⇩S τ a)"
"Hom.set (a, a)" "F.FUN ?ψx o τ.FUN a"]
by simp
qed
finally show ?thesis by simp
qed
qed
qed
finally show ?thesis by auto
qed
text‹
Consequently, if @{term τ'} is any natural transformation from @{term "Y a"} to @{term F}
that agrees with @{term τ} at @{term a}, then @{term "τ' = τ"}.
›
lemma eqI:
assumes "natural_transformation Cop.comp S (Y a) F τ'" and "τ' a = τ a"
shows "τ' = τ"
proof (intro NaturalTransformation.eqI)
interpret τ': natural_transformation Cop.comp S ‹Y a› F τ' using assms by auto
interpret T': yoneda_lemma_fixed_τ C S setp φ F a τ' ..
show "natural_transformation Cop.comp S (Y a) F τ" ..
show "natural_transformation Cop.comp S (Y a) F τ'" ..
show "⋀b. Cop.ide b ⟹ τ' b = τ b"
using assms(2) τ_ide T'.τ_ide by simp
qed
end
context yoneda_lemma
begin
text‹
One half of the Yoneda lemma:
The mapping @{term 𝒯} is an injection, with left inverse @{term ℰ},
from the set @{term "F.SET a"} to the set of natural transformations from
@{term "Y a"} to @{term F}.
›
lemma 𝒯_is_injection:
assumes "e ∈ F.SET a"
shows "natural_transformation Cop.comp S (Y a) F (𝒯 e)" and "ℰ (𝒯 e) = e"
proof -
interpret yoneda_lemma_fixed_e C S setp φ F a e
using assms by (unfold_locales, auto)
show "natural_transformation Cop.comp S (Y a) F (𝒯 e)" ..
show "ℰ (𝒯 e) = e"
unfolding ℰ_def
using assms 𝒯e_ide S.Fun_mkArr Hom.φ_mapsto Hom.ψ_φ ide_a
F.preserves_ide S.Fun_ide restrict_apply C.ide_in_hom
by (auto simp add: Pi_iff)
qed
lemma ℰτ_mapsto:
assumes "natural_transformation Cop.comp S (Y a) F τ"
shows "ℰ τ ∈ F.SET a"
proof -
interpret τ: natural_transformation Cop.comp S ‹Y a› F τ
using assms by auto
interpret yoneda_lemma_fixed_τ C S setp φ F a τ ..
show ?thesis
proof (unfold ℰ_def)
have "τ.FUN a ∈ Hom.set (a, a) → F.SET a"
proof -
have "S.arr (τ a) ∧ S.Dom (τ a) = Hom.set (a, a) ∧ S.Cod (τ a) = F.SET a"
using ide_a Hom.set_map by auto
thus ?thesis
using S.Fun_mapsto by blast
qed
thus "τ.FUN a (φ (a, a) a) ∈ F.SET a"
using ide_a Hom.φ_mapsto by fastforce
qed
qed
text‹
The other half of the Yoneda lemma:
The mapping @{term 𝒯} is a surjection, with right inverse @{term ℰ},
taking natural transformations from @{term "Y a"} to @{term F}
to elements of @{term "F.SET a"}.
›
lemma 𝒯_is_surjection:
assumes "natural_transformation Cop.comp S (Y a) F τ"
shows "𝒯 (ℰ τ) = τ"
proof -
interpret natural_transformation Cop.comp S ‹Y a› F τ
using assms by auto
interpret yoneda_lemma_fixed_τ C S setp φ F a τ ..
interpret yoneda_lemma_fixed_e C S setp φ F a ‹ℰ τ›
using assms ℰτ_mapsto by unfold_locales auto
show "𝒯 (ℰ τ) = τ"
using ide_a τ_ide [of a] 𝒯e_ide ℰ_def natural_transformation_𝒯e
by (intro eqI) auto
qed
text‹
The main result.
›
theorem yoneda_lemma:
shows "bij_betw 𝒯 (F.SET a) {τ. natural_transformation Cop.comp S (Y a) F τ}"
using ℰτ_mapsto 𝒯_is_injection 𝒯_is_surjection
by (intro bij_betwI) auto
end
text‹
We now consider the special case in which @{term F} is the contravariant
functor @{term "Y a'"}. Then for any @{term e} in ‹Hom.set (a, a')›
we have @{term "𝒯 e = Y (ψ (a, a') e)"}, and @{term 𝒯} is a bijection from
‹Hom.set (a, a')› to the set of natural transformations from @{term "Y a"}
to @{term "Y a'"}. It then follows that that the Yoneda functor @{term Y}
is a fully faithful functor from @{term C} to the functor category ‹[Cop, S]›.
›
locale yoneda_lemma_for_hom =
yoneda_functor_fixed_object C S setp φ a +
Ya': yoneda_functor_fixed_object C S setp φ a' +
yoneda_lemma C S setp φ "Y a'" a
for C :: "'c comp" (infixr "⋅" 55)
and S :: "'s comp" (infixr "⋅⇩S" 55)
and setp :: "'s set ⇒ bool"
and φ :: "'c * 'c ⇒ 'c ⇒ 's"
and a :: 'c
and a' :: 'c +
assumes ide_a': "C.ide a'"
begin
text‹
In case @{term F} is the functor @{term "Y a'"}, for any @{term "e ∈ Hom.set (a, a')"}
the induced natural transformation @{term "𝒯 e"} from @{term "Y a"} to @{term "Y a'"}
is just @{term "Y (ψ (a, a') e)"}.
›
lemma app_𝒯_equals:
assumes e: "e ∈ Hom.set (a, a')"
shows "𝒯 e = Y (ψ (a, a') e)"
proof -
let ?ψe = "ψ (a, a') e"
have ψe: "«?ψe : a → a'»" using ide_a ide_a' e Hom.ψ_mapsto by auto
interpret Ye: natural_transformation Cop.comp S ‹Y a› ‹Y a'› ‹Y ?ψe›
using Y_arr_is_transformation [of ?ψe] ψe by (elim C.in_homE, auto)
interpret yoneda_lemma_fixed_e C S setp φ ‹Y a'› a e
using ide_a ide_a' e Hom.set_map
by (unfold_locales, simp_all)
interpret yoneda_lemma_fixed_τ C S setp φ ‹Y a'› a ‹𝒯 e› ..
have "natural_transformation Cop.comp S (Y a) (Y a') (Y ?ψe)" ..
moreover have "natural_transformation Cop.comp S (Y a) (Y a') (𝒯 e)" ..
moreover have "𝒯 e a = Y ?ψe a"
proof -
have 1: "𝒯 e a = S.mkArr (Hom.set (a, a)) (Ya'.SET a) (λx. Ya'.FUN (ψ (a, a) x) e)"
using ide_a 𝒯⇩o_def 𝒯e_ide by simp
also have
"... = S.mkArr (Hom.set (a, a)) (Hom.set (a, a')) (φ (a, a') o C ?ψe o ψ (a, a))"
proof (intro S.mkArr_eqI)
show "S.arr (S.mkArr (Hom.set (a, a)) (Ya'.SET a) (λx. Ya'.FUN (ψ (a, a) x) e))"
using ide_a e 1 𝒯e.preserves_reflects_arr
by (metis Cop.ide_char 𝒯e_ide(1))
show "Hom.set (a, a) = Hom.set (a, a)" ..
show 2: "Ya'.SET a = Hom.set (a, a')"
using ide_a ide_a' Y_simp Hom.set_map by simp
show "⋀x. x ∈ Hom.set (a, a) ⟹
Ya'.FUN (ψ (a, a) x) e = (φ (a, a') o C ?ψe o ψ (a, a)) x"
proof -
fix x
assume x: "x ∈ Hom.set (a, a)"
have ψx: "«ψ (a, a) x : a → a»"
using ide_a x Hom.ψ_mapsto [of a a] by auto
have "S.arr (Y a' (ψ (a, a) x)) ∧
Y a' (ψ (a, a) x) = S.mkArr (Hom.set (a, a')) (Hom.set (a, a'))
(φ (a, a') ∘ Cop.comp (ψ (a, a) x) ∘ ψ (a, a'))"
using Y_ide_arr ide_a ide_a' ψx by blast
hence "Ya'.FUN (ψ (a, a) x) e = (φ (a, a') ∘ Cop.comp (ψ (a, a) x) ∘ ψ (a, a')) e"
using e 2 S.Fun_mkArr Ya'.preserves_reflects_arr [of "ψ (a, a) x"] by simp
also have "... = (φ (a, a') o C ?ψe o ψ (a, a)) x" by simp
finally show "Ya'.FUN (ψ (a, a) x) e = (φ (a, a') o C ?ψe o ψ (a, a)) x" by auto
qed
qed
also have "... = Y ?ψe a"
using ide_a ide_a' Y_arr_ide ψe by simp
finally show "𝒯 e a = Y ?ψe a" by auto
qed
ultimately show ?thesis using eqI by auto
qed
lemma is_injective_on_homs:
shows "inj_on map (C.hom a a')"
proof (intro inj_onI)
fix f f'
assume f: "f ∈ C.hom a a'" and f': "f' ∈ C.hom a a'"
assume eq: "map f = map f'"
show "f = f'"
proof -
have "f = ψ (a, a') (ℰ (Y (ψ (a, a') (φ (a, a') f))))"
by (metis (no_types, lifting) C.comp_arr_dom C.ide_in_hom Hom.φ_natural
Hom.ψ_φ ℰ_def category.in_homE f ide_a mem_Collect_eq
Y_simp yoneda_functor_axioms yoneda_functor_def)
also have "... = ψ (a, a') (ℰ (𝒯 (φ (a, a') f')))"
using f f' eq Hom.φ_mapsto [of a a'] ide_a Hom.ψ_φ Y_def
app_𝒯_equals [of "φ (a, a') f'"]
by fastforce
also have "... = f'"
by (metis C.ideD(1) Hom.φ_mapsto Hom.ψ_φ Hom.set_map PiE Y_simp
𝒯_is_injection(2) f' ide_a ide_a' mem_Collect_eq)
finally show ?thesis by auto
qed
qed
end
context yoneda_functor
begin
sublocale faithful_functor C Cop_S.comp map
proof
fix f :: 'c and f' :: 'c
assume par: "C.par f f'" and ff': "map f = map f'"
show "f = f'"
proof -
interpret Ya': yoneda_functor_fixed_object C S setp φ ‹C.cod f›
using par by (unfold_locales, auto)
interpret yoneda_lemma_for_hom C S setp φ ‹C.dom f› ‹C.cod f›
using par by (unfold_locales, auto)
show "f = f'"
using par ff' is_injective_on_homs inj_on_def [of map "C.hom (C.dom f) (C.cod f)"]
by force
qed
qed
lemma is_faithful_functor:
shows "faithful_functor C Cop_S.comp map"
..
sublocale full_functor C Cop_S.comp map
proof
fix a :: 'c and a' :: 'c and t
assume a: "C.ide a" and a': "C.ide a'"
assume t: "«t : map a →⇩[⇩C⇩o⇩p⇩,⇩S⇩] map a'»"
show "∃e. «e : a → a'» ∧ map e = t"
proof
interpret Ya': yoneda_functor_fixed_object C S setp φ a'
using a' by (unfold_locales, auto)
interpret yoneda_lemma_for_hom C S setp φ a a'
using a a' by (unfold_locales, auto)
have NT: "natural_transformation Cop.comp S (Y a) (Y a') (Cop_S.Map t)"
using t a' Y_def Cop_S.Map_dom Cop_S.Map_cod Cop_S.dom_char Cop_S.cod_char
Cop_S.in_homE Cop_S.arrE
by metis
hence 1: "ℰ (Cop_S.Map t) ∈ Hom.set (a, a')"
using ℰτ_mapsto ide_a ide_a' Hom.set_map by simp
moreover have "map (ψ (a, a') (ℰ (Cop_S.Map t))) = t"
proof (intro Cop_S.arr_eqI)
have 2: "«map (ψ (a, a') (ℰ (Cop_S.Map t))) : map a →⇩[⇩C⇩o⇩p⇩,⇩S⇩] map a'»"
using 1 ide_a ide_a' Hom.ψ_mapsto [of a a'] by blast
show "Cop_S.arr t" using t by blast
show "Cop_S.arr (map (ψ (a, a') (ℰ (Cop_S.Map t))))" using 2 by blast
show 3: "Cop_S.Map (map (ψ (a, a') (ℰ (Cop_S.Map t)))) = Cop_S.Map t"
using NT 1 Y_def 𝒯_is_surjection app_𝒯_equals ℰτ_mapsto by metis
show 4: "Cop_S.Dom (map (ψ (a, a') (ℰ (Cop_S.Map t)))) = Cop_S.Dom t"
using t 2 functor_axioms Cop_S.Map_dom by (metis Cop_S.in_homE)
show "Cop_S.Cod (map (ψ (a, a') (ℰ (Cop_S.Map t)))) = Cop_S.Cod t"
using 2 3 4 t Cop_S.Map_cod by (metis Cop_S.in_homE)
qed
ultimately show "«ψ (a, a') (ℰ (Cop_S.Map t)) : a → a'» ∧
map (ψ (a, a') (ℰ (Cop_S.Map t))) = t"
using ide_a ide_a' Hom.ψ_mapsto by auto
qed
qed
lemma is_full_functor:
shows "full_functor C Cop_S.comp map"
..
sublocale fully_faithful_functor C Cop_S.comp map ..
end
end