HFPL in string diagrams
Limits in string diagrams - PS の記法を(無理やり)使って・・・
Hom functors
命題.1: Hom functors preverse limits
- : limiting cone
- : limiting cone
証明 @error
一般に currying はできない。代わりに String diagram による圏論まとめ - PS を参照。
Currying は naturality(conicality) を preserve することに注意すると
命題.2
証明
とすると
参考文献
Universal morphisms in string diagrams
Yoneda embedding in string diagrams
(String diagram による Yoneda lemma の証明 rev.2 - PS の続き・・・)
Variance を?マークの向きで表すことにする。
Contravariant Yoneda bijection
定義: Yoneda embedding
記法
Natural transformation:
を次のように表す:
命題
- Yoneda embedding は fully-faithful。
証明
Contravariant Yoneda bijection で特に とすると
となり、 は Yoneda embedding と一致しているので。
参考文献
String diagram による Yoneda lemma の証明 rev.2
完全版(のつもり)。
記法
Functor について natural transformation:
を以下のように描く:
Naturality:
を箱が筒抜けになっていることによって表現した。?ノードは無名関数の無名パラメータ。
この時点で証明は終わったも同然になる。
命題: Yoneda lemma
Functor について
-
- natural in
証明
Yoneda bijection
とすると、左下は筒抜けなので確かに natural であることが分かる。
あとは以下を示せばよい・・・がいずれも明らか。
Bijectivity
Naturality in
Naturality in
まとめ
では morphism を格上げしてるんだけど逆に natural transformation の方を格下げした方が分かりやすいと思う。