圏論と数式の練習 - www.kotha.netの裏

変な議論してたら教えてください！

命題0

$A$ を集合、 $\mathcal{C}$ を圏、 $|-| : \mathcal{C} \to \mathbf{Set}$ を忘却関手、 $F : \mathbf{Set} \to \mathcal{C}$ を自由関手とすると、以下が成り立つ。
$Nat(Hom(A, |-|), |-|) \simeq |F(A)|$

証明

米田の補題から $|F(A)| \simeq Nat(Hom(A, -), |F(-)|)$ なので、 $Nat(Hom(A, |-|), |-|) \simeq Nat(Hom(A, -), |F(-)|)$ を示せば良い。

$F$ は $|-|$ の左随伴だから、単位 $\eta : Id \to |F(-)|$ と余単位 $\epsilon : F(|-|) \to Id$ が存在して以下が成り立つ。

$|\epsilon| \circ \eta = id$
$\epsilon \circ F(\eta) = id$

以下で具体的に同型射を構成する。写像 $f$ と $g$ を次のように定義する。

$f : Nat(Hom(A, |-|), |-|) \to Nat(Hom(A, -), |F(-)|)$
$f(h)_X = h_{F(X)} \circ Hom(A, \eta_X)$
$g : Nat(Hom(A, -), |F(-)|) \to Nat(Hom(A, |-|), |-|)$
$g(r)_Y = |\epsilon_Y| \circ r_{|Y|}$

$f$ と $g$ が互いに逆であることを示せば良い。

$(g \circ f)(h)_X$
$= |\epsilon_X| \circ h_{F(|X|)} \circ Hom(A, \eta_{|X|}) \quad$ (定義から)
$= h_X \circ Hom(A, |\epsilon_X|) \circ Hom(A, \eta_{|X|}) \quad$ (hの自然性)
$= h_X \circ Hom(A, |\epsilon_X| \circ \eta_{|X|})$ ( $Hom(A,-)$ が関手なので)
$= h_X \circ Hom(A, id)$ (単位と余単位の合成)
$= h_X$ ( $Hom(A,-)$ が関手なので)

$(f \circ g)(r)_Y$
$= |\epsilon_{F(Y)}| \circ r_{|F(Y)|} \circ Hom(A, \eta_Y)$ (定義から)
$= |\epsilon_{F(Y)}| \circ |F(\eta_Y)| \circ r_Y$ (rの自然性)
$= |\epsilon_{F(Y)} \circ F(\eta_Y)| \circ r_Y$ (|-|が関手なので)
$= |id| \circ r_Y$ (単位と余単位の合成)
$= r_Y$ (|-|が関手なので)

これで示された。

以下はインフォーマルな(というよりいい加減な)議論。

主張1

forall m. (Monoid m) => (A -> m) -> m
という型は、Vector Aとだいたい同型である。
forall m. (CommutativeIdempotentMonoid m) => (A -> m) -> m
という型は、Set Aとだいたい同型である。

説得

これらの型は多相型なので、パラメトリシティの制約を受ける。Theorems for free!によると、以下の命題が成り立つ

閉じた項tが型Tを持つならば、(t,t) ∈ R(T)である。

ただし、Rは型を値の集合間の関係に写す写像で、以下のように再帰的に定義される。(この説得に関係ありそうなところだけ)

(f0, f1) ∈ R(A -> B) iff
  ∀ (a0, a1) ∈ R(A). (f0 a0, f1 a1) ∈ R(B)
(t0, t1) ∈ R(∀a. F(a)) iff
  ∀ A : A0 <=> A1. (t0[a=A0], t1[a=A1]) ∈ R(F)A
TがInt,Charなどの基本型なら、
(x0, x1) ∈ R(T, T) iff x0 = x1

ただし、X <=> YはXの値の集合とYの値の集合の関係を表す。

これに従って上の型が課す制約を同値変形していく。

(t, t) ∈ R(forall m. (Monoid m) => (A -> m) -> m)
(t, t) ∈ R(forall m. (m -> m -> m) -> m -> (A -> m) -> m) -- Monoidを辞書渡しに
∀M : M0 <=> M1.
  (t, t) ∈ ((M -> M -> M) -> M -> (A -> M) -> M) -- forallを処理
∀M : M0 <=> M1.
  ∀(<>, <>') ∈ R(M -> M -> M).
    (t (<>), t (<>')) ∈ R(M -> (A -> M) -> M) -- ->を処理
∀M : M0 <=> M1.
  ∀(<>, <>') ∈ R(M -> M -> M).
    ∀(e, e') ∈ R(M).
      (t (<>) e, t (<>') e') ∈ R((A -> M) -> M)
∀M : M0 <=> M1.
  ∀(<>, <>') ∈ R(M -> M -> M).
    ∀(e, e') ∈ M.
      ∀(f, f') ∈ R(A -> M).
        (t (<>) e f, t (<>') e' f') ∈ M

さらに、

(<>, <>') ∈ R(M -> M -> M)
∀(a, a') ∈ M.
  (<> a, <>' a') ∈ R(M -> M)
∀(a, a') ∈ M.
  ∀(b, b') ∈ M.
    (<> a b, <>' a' b') ∈ M

(f, f') ∈ R(A -> M)
∀(x, x') ∈ R(A).
  (f x, f' x') ∈ M
∀x :: A.
  (f x, f' x) ∈ M -- Aを基本型として扱う

ここで、Mが(関係の特別な場合としての)関数の場合だけを考える*1。すなわち、この関数をuと書くことにして、

(a, a') ∈ M iff a' = u a

すると、さらに以下のように簡略化できる。

(<>, <>') ∈ R(M -> M -> M)
∀a,b. u (a <> b) = u a <> u b

(f, f') ∈ R(A -> M)
∀x :: A. u (f x) = f' x
u . f = f'

元の条件に代入する。

(t, t) ∈ R(forall m. (Monoid m) => (A -> m) -> m)
∀u :: M0 -> M1.
  ∀(<>, <>').
    (∀a,b. u (a <> b) = u a <> u b) =>
      ∀(e, e').
        (u e = e') =>
          ∀(f, f').
            (u . f = f') =>
              u (t (<>) e f) = t (<>') e' f'
∀u :: M0 -> M1.
  ∀(<>, <>').
    ∀(e, e').
      ∀(f, f').
        (uがモノイド準同型) =>
              u (t (<>) e f) = t (<>') e' (u . f)
∀u :: M0 -> M1.
  ∀f.
    (uがモノイド準同型) =>
      u (t f) = t (u . f) -- 辞書渡しを暗黙に

結局、満たされるべき条件は、fが任意の関数で、uが任意のモノイド準同型のとき、u (t f) = t (u . f)が成り立つことである。

これは要するに、tの要素が $Hom_{\mathbf{Mon}}(A,|-|)$ から $|-|$ への自然変換だということである。命題0より、このような自然変換の集合は $|F(A)|$ と同型である。 $\mathbf{Mon}$ におけるAの自由対象はAの有限列だから、これはVector Aに同型。

制約がMonoidでなくCommutativeIdempotentMonoidの場合も同様の議論。

以上が説得されるべきことであった。

感想と反省

圏論の議論が面倒。全部Haskellの等式推論でやりたい。(実際fとgの構成はHaskellでやった)。たぶん圏論上手い人はもっとうまく証明できるはずなんだけど、どうしていいか分からない。
米田の補題を使わずにやろうとしたらひどいことになった。なぜかは分からない。
パラメトリシティから自然性にもっていく議論があやしい。必要性しか示してない。
seqどころか⊥の存在すら無視している。モノイド則を満たさないMonoidインスタンスの存在も。
Lens' s a (定義は forall f. (Functor f) => (a -> f a) -> s -> f s)が(s -> (a, (a -> s)))と同型であることも似た議論で示せる？
集合としての同型しか示してないけど、実際には命題0の左辺の自然変換の集合には(CがMonなら)モノイド構造が入るはず。本当はこれを主張したかったが、述べる方法すら分からなかった。もしかして同型が存在するだけでなく自然であることを示せばいい？

*1:こうするとなぜかうまくいくらしい