PS

HFPL in string diagrams

圏論 Limit Hom-functor

Limits in string diagrams - PS の記法を(無理やり)使って･･･

Hom functors

f:id:mbps:20160306110044p:plain

命題.1: Hom functors preverse limits

  • \textstyle\lim _ x : {\textstyle\lim} F \to Fx : limiting cone
    • \implies \operatorname{Hom}(d,{\textstyle\lim _ x}) : \operatorname{Hom}(d,{\textstyle\lim} F) \to \operatorname{Hom}(d,Fx) : limiting cone

証明 @error

一般に currying はできない。代わりに String diagram による圏論まとめ - PS を参照。

Currying は naturality(conicality) を preserve することに注意すると

f:id:mbps:20160306110050p:plain

命題.2

  • \operatorname{Hom}(d,l) \cong \textstyle{\lim} _ x \operatorname{Hom}(d,Fx)
    • \implies l \cong \textstyle\lim _ x Fx

証明

f:id:mbps:20160312124416p:plain

とすると

f:id:mbps:20160312125306p:plain

参考文献

  1. Preservation of limits - PS
  2. Generalized Abstract Nonsense.pdf

Yoneda embedding in string diagrams

圏論 Yoneda String diagram

(String diagram による Yoneda lemma の証明 rev.2 - PS の続き･･･)

Variance を？マークの向きで表すことにする。

Contravariant Yoneda bijection

f:id:mbps:20160303095931p:plain

定義: Yoneda embedding

f:id:mbps:20160303095937p:plain

記法

Natural transformation:

  • (\tau _ X : \operatorname{Hom}(X,A) \to \operatorname{Hom}(X,B) ) _ X

を次のように表す:

f:id:mbps:20160303095944p:plain

命題

  • Yoneda embedding は fully-faithful。

証明

Contravariant Yoneda bijection で特に F := \Lambda _ X \operatorname{Hom}(X,B) とすると

f:id:mbps:20160303095952p:plain

となり、 \varphi ^{-1} は Yoneda embedding と一致しているので。

参考文献

String diagram による Yoneda lemma の証明 rev.2

圏論 String diagram Yoneda

完全版(のつもり)。

記法

Functor F : \mathcal{C} \to \mathcal{Set} について natural transformation:

  • (\tau _ X : \operatorname{Hom}(A,X) \to FX) _ X \in \operatorname{Nat} _ X (\operatorname{Hom}(A,X),FX)

を以下のように描く:

f:id:mbps:20160303094416p:plain

Naturality:

f:id:mbps:20160303094421p:plain

を箱が筒抜けになっていることによって表現した。？ノードは無名関数の無名パラメータ。

この時点で証明は終わったも同然になる。

命題: Yoneda lemma

Functor F : \mathcal{C} \to \mathcal{Set} について

  • \operatorname{Nat} _ X (\operatorname{Hom}(A,X),FX) \cong FA
    • natural in A,F

証明

Yoneda bijection

f:id:mbps:20160303094437p:plain

とすると、左下は筒抜けなので確かに natural であることが分かる。

あとは以下を示せばよい･･･がいずれも明らか。

Bijectivity

f:id:mbps:20160303094458p:plain

Naturality in A

f:id:mbps:20160303094504p:plain

Naturality in F

f:id:mbps:20160303094510p:plain

まとめ

では morphism を格上げしてるんだけど逆に natural transformation の方を格下げした方が分かりやすいと思う。

参考文献