分散合意アルゴリズム Raft を TLA+ で検証する

はじめに

この記事では分散合意アルゴリズム Raft を 形式仕様記述 + モデル検査ツールの TLA+ を用いて実際に検証を行う手順を示します。Raft の作者が公開している TLA+ のコードは Raft のアルゴリズムのみが実装されていて検証の部分のコードがないためこの記事で補います。Raft や TLA+ に関する詳細は解説しませんが、詳細を知るためのリンクを集めたので、詳しく知りたい方はそちらを参照してください。

分散合意アルゴリズム Raft とは

分散合意アルゴリズムとは

分散合意アルゴリズムの合意とはアルゴリズムに参加する複数のサーバーの有する状態が共通の状態に収束することです。分散合意アルゴリズムは参加するサーバーに障害が発生しても一貫した状態を保持します。
この性質は多くの高可用性と高信頼性を必要とする分散アルゴリズムが必要とする性質で、分散合意アルゴリズムは多くの分散アルゴリズムが必要とする共通の機能を抽象化し取り出したアルゴリズムと考えられます。
今後何かしらの分散処理システムを実装する場合は、分散合意アルゴリズムの上に必要とする特有の機能を追加する形で実装できないか検討するといいでしょう。

Raft の特徴

Raft の大雑把な動作イメージを理解するには以下のサイトが役に立ちます。

Raft は次の特徴を持つアルゴリズムとして Diego Ongaro によって考案されました

  • アルゴリズムの理解のしやすさに重点が置かれている
  • サーバー間の協調動作に使用するのは RequestVote RPC と AppendEntries RPC の 2 つの RPC のみ
  • 実装可能な程度にアルゴリズムの詳細が説明されている
  • LogCabin という実装が公開されている
  • TLA+ による検証が行われている

この記事で注目するのはTLA+ による検証が行われている点です。
Diego Ongaro による TLA+ のソースコードは GitHub で公開されているのですが、アルゴリズムのコアの部分についての実装だけで検証に関するコードが抜け落ちています。彼自身は検証に必要なコードも書いて検証したと思いますが、その部分は公開されていないのでこの記事で補います。

Raft についてはすでに日本語で書かれた記事や資料がいくつかあるのでリンクを以下にリストします。

論文の 3 章の内容をほぼすべて日本語翻訳した内容です。英語の論文を読む前にざっと目を通しておくと理解が深まると思います。

  • PFI の勉強会のスライド資料

www.slideshare.net
アルゴリズムのコアの部分だけでなく実システムに必要なメンバーシップ管理や、ログのコンパクション、Client との Interaction の内容まで解説されています。

  • 分散合意アルゴリズム Raft を理解する

qiita.com
Raft は Crash-Recovery 障害に対して耐性を持つことに言及しています。

Raft に関するクイズを記事の最後に載せていますので、理解度の確認に使用してください。

Raft が満たす性質

Raft は以下の 5 つの性質が常に満たされることを保証します。
Raft に参加するサーバーの再起動や、サーバー間メッセージの重複やドロップなどが任意のタイミングで任意の回数発生する状況下であっても、これらの性質が満たされ続けることを TLA+ を用いて検証します。

Election Safety

1 つの term には多くとも 1 つの Leader が選出される。

正確を期すために補足すると、1 つの term に Leader が存在しない場合もあります。また、同時に複数の Leader が存在する場合もあります。複数の Leader が存在する場合は、Leader の term が異なっている必要があります。古い term を持つ Leader が新しい Leader からのメッセージを受け取ると Follower に戻ります。

Leader Append-Only

Leader は自分自身の log に対して追記のみをして、書き換えや削除をしない。

Leader は自身が作成した entry については log に追記しかしません。よって、Leader が Leader になった時点で保持していた log が不変であることを検証します。
Leader である期間を通して、Leader になった時点で保持していた log が不変であることと、Leader が作成した entry は追記のみという 2 つの事実を合わせて Leader Append-Only が成り立つことを検証できます。

Log Matching

2 つの log が同じ index に同じ term の entry を持つなら、その index までの entry は全て一致する。

Raft アルゴリズムの中核の AppendEntries RPC は Leader の log を Follower にコピーする際、 Follower の log とどの index まで一致しているか判断する際にこの性質に大きく依存しています。つまり、この性質が成り立つことは Raft にとって非常に重要です。
具体的には Leader は log の末尾から先頭方向に向かって、Follower の log の entry の term を順に比較します。ある index で、entry の term が一致したら、先頭からその index までの entry は全て一致しているとみなして(Log Matching が成り立つとみなして)entry も転送しないし、本当に一致しているかのチェックもしません。
Log Matching を検証することは難しくありません。一方で、なぜこの性質が成り立つのか?は説明するのがとても難しいです。この性質が成り立つことを検証するのではなく証明をして理解しようと私が奮闘した記録が次の記事にあるので興味のある人は参考にしてください。
www.orecoli.com

Leader Completeness

もしある entry がある term に commit されたなら、その term 以降の全ての Leader はその entry を log の中に含む。

Raft アルゴリズムの生涯を通して、一度 commit された entry は Leader が変わっても存続します。Raft が合意するのは、Leader の log の先頭から commit index までの内容です。

State Machine Safety

ある server の log の特定の index の entry を自身の state machine に適用するとき、他の全ての server の log のその index には同じ entry が存在する。

各 server は Leader から AppendEntires RPC により、自身の log のどこまでが commit されているか通知されます。commit された entry は Leader Completeness より Leader が変わっても log の同じ index に存在し、各 server の log は Leader の log と一致するように AppendEntries RPC により複製されます。
つまり、各 server の commit index までの log はリーダーの log と一致するので、各 server が自身の state machine に適用する entry は必ずこの commit index 以下であるという制約を満たす限り全ての server は同じ entry を同じ順序で自身の state machine に適用します。
今回検証するコードでは state machine に entry を適用する部分は記述されていないので上の制約を満たすのは実装者の責任です。

TLA+ とは

TLA+ は分散合意アルゴリズムの Paxos や LaTeX の開発者として知られる
Leslie Lamport によって開発された形式仕様記述言語 + モデル検査ツールです。数学的な記述を用いてシステムやプログラムの仕様を厳密に記述することにより仕様上の間違いや修正が困難なバグの発見を補助します。特に分散システムの検証に威力を発揮します

以下の記事では TLA+ のような形式手法が必要とされる動機について非常によく説明されています。
orgachem.hatenablog.com

TLA+ は Amazon が自社のクラウドで提供されているサービスの検証に用いたことで話題になりました。
masateruk.hatenablog.com
sakaia.hatenadiary.org

国内企業でも TLA+ について調査したり、実際に使用している例が出てきています。
swet.dena.com
dev.classmethod.jp
tkh86.hateblo.jp
FINAL FANTASY XV POCKET EDITION を支える AWS サーバレス技術

TLA+ による Raft の形式的仕様

以下のコードが Raft の検証コードです。Diego Ongaro によるオリジナルのコードのコメントを日本語に翻訳しています。また検証に必要な変数やコードを追加しています。
コードの最後に上で挙げた Raft が満たす性質を新たに追加した変数等を使用して論理式として表現しています。それぞれの性質の説明と論理式の対応を確認してください。

-------------------------------- MODULE main --------------------------------
EXTENDS Naturals, FiniteSets, Sequences, TLC

\* Server ID の集合
CONSTANTS Server

\* Client のリクエストに含まれる値の集合
CONSTANTS Value

\* Server の取りうる状態
CONSTANTS Follower, Candidate, Leader

\* 予約された定数
CONSTANTS Nil

\* メッセージタイプ:
CONSTANTS RequestVoteRequest, RequestVoteResponse,
          AppendEntriesRequest, AppendEntriesResponse

----
\* 大域変数

\* Server 間のリクエストとリスポンスを記録する重複を許す集合(Bag)
\* TLA+ は重複を許す集合をサポートしないので、Message から Nat への集合で代替する
VARIABLE messages

\* 証明で使用する記録用の変数で実装には現れない
\* leader の最初の log と投票者の log を含む、成功した選挙を記録する
\* 成功した選挙に関する様々な情報を含む関数の集合(BecomeLeader を参照)
\* 本記事の検証では使用しない
VARIABLE elections

\* 証明で使用する記録用の変数で実装には現れない
\* system 内のすべての log を記録する
\* 本記事の検証では使用しないためコメントアウト
\* VARIABLE allLogs

----
\* 以下の変数は Server ごとに個別の変数 (ドメインが Server の関数)

\* 各 Server の term
VARIABLE currentTerm

\* 各 Server の state で次のいずれか (Follower, Candidate, or Leader)
VARIABLE state

\* 各 Server が現在の term で投票した Candidate か
\* もしくは誰にも投票していない場合は Nil
VARIABLE votedFor
serverVars == <<currentTerm, state, votedFor>>

\* log の entry の Sequence。
VARIABLE log

\* state machine が適用する可能性のある log の最新 entry の index
VARIABLE commitIndex
logVars == <<log, commitIndex>>

\* 以下の変数は Candidate の場合にのみ使用される:
\* 現在の term で RequestVote に対する返信を受け取った Server の集合
VARIABLE votesResponded

\* 現在の term で Candidate に対する投票を受け取った Server の集合
VARIABLE votesGranted

\* 証明で使用する記録用の変数で実装には現れない
\* Candidate に対して現在の term で投票した Server の log を記録する
\* 本記事の検証では使用しない
VARIABLE voterLog
candidateVars == <<votesResponded, votesGranted, voterLog>>

\* 以下の変数は Leader の場合にのみ使用される:
\* それぞれの Follower に次に送る entry の index を記録する
VARIABLE nextIndex

\* それぞれの Follower の log と Leader の log が一致することが確認されている index を記録する
\* この変数は Leader が commitIndex を計算するのに使用する
VARIABLE matchIndex

\* 証明で使用する記録用の変数で実装には現れない
\* リーダーに選出された時点での log を保持する
\* LeaderAppendOnly の検証に使用する
VARIABLE leaderStartLog

\* 証明で使用する記録用の変数で実装には現れない
\* リーダーが commit したエントリーのリスト
\* Leader Completeness の検証に使用する
VARIABLE commitedEntries
leaderVars == <<nextIndex, matchIndex, elections, leaderStartLog, commitedEntries>>

\* Server ごとの変数は以上
----

\* 全ての変数。stuttering のために使用
vars == <<messages, serverVars, candidateVars, leaderVars, logVars>>
----
\* Helpers

\* 定足数以上の Server が含まれる集合の集合
\* この集合の要素は過半数以上の Server を含むが、唯一重要な性質は、
\* この集合の要素は他のどの要素との間にも共通の Server を含むことである
Quorum == {i \in SUBSET(Server) : Cardinality(i) * 2 > Cardinality(Server)}

\* log の最後の entry の term。log が空の場合は 0 を返す
LastTerm(xlog) == IF Len(xlog) = 0 THEN 0 ELSE xlog[Len(xlog)].term

\* Send と Reply オペレーターのための Helper
\* message m と message の Bag を渡すと m を追加した新しい Bag を返す
WithMessage(m, msgs) ==
    IF m \in DOMAIN msgs THEN
        [msgs EXCEPT ![m] = msgs[m] + 1]
    ELSE
        msgs @@ (m :> 1)

\* Discard と Reply オペレーターのための Helper
\* message m と message の Bag を渡すと m を削除した新しい Bag を返す
\* msgs[m] が 0 になった後に WithMessages で再度 msgs[m] = 1 となるのを防ぐため、
\* オリジナルの実装から修正済み
WithoutMessage(m, msgs) ==
    IF m \in DOMAIN msgs THEN
      IF msgs[m] = 1 THEN
        [d \in DOMAIN msgs \ {m} |-> msgs[d]]
      ELSE
        [msgs EXCEPT ![m] = msgs[m] - 1]
    ELSE
      msgs

\* message m を messages に追加する
Send(m) == messages' = WithMessage(m, messages)

\* message m を messages から削除する
Discard(m) == messages' = WithoutMessage(m, messages)

\* Send と Discard の組み合わせ
Reply(response, request) ==
    messages' = WithoutMessage(request, WithMessage(response, messages))

\* 集合から最小の値を返す。集合が空集合の場合は undefined を返す
Min(s) == CHOOSE x \in s : \A y \in s : x <= y

\* 集合から最大の値を返す。集合が空集合の場合は undefined を返す
Max(s) == CHOOSE x \in s : \A y \in s : x >= y

\* 2 つの log の term が一致する最大の index を返す
MaxMatchTermIndex(log1, log2) == 
  LET indexes == {i \in 1..Min({Len(log1), Len(log2)}) : log1[i].term = log2[i].term}
  IN IF indexes = {} THEN 0 ELSE Max(indexes)

----
\* 全ての変数の初期値を定義する

\* Leader は自分自身に message を送信しないため、nextIndex[i][i] と matchIndex[i][i] の値は
\* 参照されることはないが、定義が簡単になるので含んだ状態で定義する
InitHistoryVars   == /\ elections       = {}
                     /\ voterLog        = [i \in Server |-> [j \in {} |-> <<>>]]
InitServerVars    == /\ currentTerm     = [i \in Server |-> 1]
                     /\ state           = [i \in Server |-> Follower]
                     /\ votedFor        = [i \in Server |-> Nil]
InitCandidateVars == /\ votesResponded  = [i \in Server |-> {}]
                     /\ votesGranted    = [i \in Server |-> {}]
InitLeaderVars    == /\ nextIndex       = [i \in Server |-> [j \in Server |-> 1]]
                     /\ matchIndex      = [i \in Server |-> [j \in Server |-> 0]]
                     /\ leaderStartLog  = [i \in Server |-> <<>>]
                     /\ commitedEntries = <<>>
InitLogVars       == /\ log             = [i \in Server |-> << >>]
                     /\ commitIndex     = [i \in Server |-> 0]
Init              == /\ messages        = [m \in {} |-> 0]
                     /\ InitHistoryVars
                     /\ InitServerVars
                     /\ InitCandidateVars
                     /\ InitLeaderVars
                     /\ InitLogVars

----
\* 状態遷移の定義

\* Server i は永続化ストレージに保存した情報(currentTerm, votedFor, log)を使用してリスタートする
\* currentTerm, votedFor, log 以外の情報は全て失う
Restart(i) ==
    /\ state'          = [state EXCEPT ![i] = Follower]
    /\ votesResponded' = [votesResponded EXCEPT ![i] = {}]
    /\ votesGranted'   = [votesGranted EXCEPT ![i] = {}]
    /\ voterLog'       = [voterLog EXCEPT ![i] = [j \in {} |-> <<>>]]
    /\ nextIndex'      = [nextIndex EXCEPT ![i] = [j \in Server |-> 1]]
    /\ matchIndex'     = [matchIndex EXCEPT ![i] = [j \in Server |-> 0]]
    /\ commitIndex'    = [commitIndex EXCEPT ![i] = 0]
    /\ UNCHANGED <<messages, currentTerm, votedFor, log, elections, leaderStartLog, commitedEntries>>

\* Server i は Timeout して新しい選挙を開始する
Timeout(i) == /\ state[i] \in {Follower, Candidate}
              /\ state'          = [state EXCEPT ![i] = Candidate]
              /\ currentTerm'    = [currentTerm EXCEPT ![i] = currentTerm[i] + 1]
              \* ほとんどの実装では自分自身への投票を atomic な操作として実装するだろうが、
              \* ここではより弱い localhost へのメッセージとして形式化する
              /\ votedFor'       = [votedFor EXCEPT ![i] = Nil]
              /\ votesResponded' = [votesResponded EXCEPT ![i] = {}]
              /\ votesGranted'   = [votesGranted EXCEPT ![i] = {}]
              /\ voterLog'       = [voterLog EXCEPT ![i] = [j \in {} |-> <<>>]]
              /\ UNCHANGED <<messages, leaderVars, logVars>>

\* Candidate i は Server j に対して RequestVote request を送信する
RequestVote(i, j) ==
    /\ state[i] = Candidate
    /\ j \notin votesResponded[i]
    /\ Send([mtype         |-> RequestVoteRequest,
             mterm         |-> currentTerm[i],
             mlastLogTerm  |-> LastTerm(log[i]),
             mlastLogIndex |-> Len(log[i]),
             msource       |-> i,
             mdest         |-> j])
    /\ UNCHANGED <<serverVars, candidateVars, leaderVars, logVars>>

\* Leader i は Server j に対して最大で 1 つの entry を含む AppendEntries request を送信する
\* 実際の実装では複数の entry を一度に送信したいと思うが、一般性を失うことなく atomic な領域を最小化するために
\* ここでは 1 つの entry に限定する
AppendEntries(i, j) ==
    /\ i /= j
    /\ state[i] = Leader
    /\ LET prevLogIndex == nextIndex[i][j] - 1
           prevLogTerm  == IF prevLogIndex > 0 THEN
                               log[i][prevLogIndex].term
                           ELSE
                               0
           \* log の最後に到達するまで最大で 1 つの entry を送信する
           lastEntry    == Min({Len(log[i]), nextIndex[i][j]})
           entries      == SubSeq(log[i], nextIndex[i][j], lastEntry)
       IN Send([mtype          |-> AppendEntriesRequest,
                mterm          |-> currentTerm[i],
                mprevLogIndex  |-> prevLogIndex,
                mprevLogTerm   |-> prevLogTerm,
                mentries       |-> entries,
                \* mlog は証明で使用する記録用の変数で実装には現れない
                mlog           |-> log[i],
                mcommitIndex   |-> Min({commitIndex[i], lastEntry}),
                msource        |-> i,
                mdest          |-> j])
    /\ UNCHANGED <<serverVars, candidateVars, leaderVars, logVars>>

\* Candidate i が Leader に遷移する
BecomeLeader(i) ==
    /\ state[i]        = Candidate
    /\ votesGranted[i] \in Quorum
    /\ state'          = [state EXCEPT ![i] = Leader]
    /\ nextIndex'      = [nextIndex EXCEPT ![i] =
                             [j \in Server |-> Len(log[i]) + 1]]
    /\ matchIndex'     = [matchIndex EXCEPT ![i] =
                             [j \in Server |-> 0]]
    /\ elections'      = elections \cup
                             {[eterm     |-> currentTerm[i],
                               eleader   |-> i,
                               elog      |-> log[i],
                               evotes    |-> votesGranted[i],
                               evoterLog |-> voterLog[i]]}
    /\ leaderStartLog' = [leaderStartLog EXCEPT ![i] = log[i]]
    /\ UNCHANGED <<messages, currentTerm, votedFor, candidateVars, logVars, commitedEntries>>

\* Leader i は値 v を log に追加する client の要求を受け付ける
ClientRequest(i, v) ==
    /\ state[i] = Leader
    /\ LET entry == [term  |-> currentTerm[i],
                     value |-> v]
           newLog == Append(log[i], entry)
       IN  log' = [log EXCEPT ![i] = newLog]
    /\ UNCHANGED <<messages, serverVars, candidateVars,
                   leaderVars, commitIndex>>

\* Leader i は commitIndex を進める
\* この処理は AppendEntries response の処理とは別のステップとして行われます。
\* 理由は、atomic な領域を最小化するためと、
\* 単一サーバのクラスタであっても Leader が entry を commit できるようにするためです。
AdvanceCommitIndex(i) ==
    /\ state[i] = Leader
    /\ LET \* index まで同じ log を保持している Server の集合
           Agree(index)   == {i} \cup {k \in Server :
                                          matchIndex[i][k] >= index}
           \* 過半数の Server が一致した entry を持っている index の集合
           agreeIndexes   == {index \in 1..Len(log[i]) :
                                 Agree(index) \in Quorum}
           \* commitIndex'[i] の新しい値
           \* log の Max(agreeIndexes) の entry の term が Leader の currentTerm と一致する場合にのみ
           \* commitIndex が更新されることに注意
           newCommitIndex ==
               IF /\ agreeIndexes /= {}
                  /\ log[i][Max(agreeIndexes)].term = currentTerm[i]
               THEN
                   Max(agreeIndexes)
               ELSE
                   commitIndex[i]
       IN
         /\ commitIndex'     = [commitIndex EXCEPT ![i] = newCommitIndex]
         /\ commitedEntries' = commitedEntries \o SubSeq(log[i], Len(commitedEntries)+1, newCommitIndex)
    /\ UNCHANGED <<messages, serverVars, candidateVars, nextIndex, matchIndex, elections, leaderStartLog, log>>

----
\* Message handlers
\* i = 受信 Server, j = 送信 Server, m = message

\* m.mterm <= currentTerm[i] が成り立つ場合に
\* Server i は Server j からの RequestVote request を受信する
HandleRequestVoteRequest(i, j, m) ==
    LET logOk == \/ m.mlastLogTerm > LastTerm(log[i])
                 \/ /\ m.mlastLogTerm = LastTerm(log[i])
                    /\ m.mlastLogIndex >= Len(log[i])
        grant == /\ m.mterm = currentTerm[i]
                 /\ logOk
                 /\ votedFor[i] \in {Nil, j}
    IN /\ m.mterm <= currentTerm[i]
       /\ \/ grant  /\ votedFor' = [votedFor EXCEPT ![i] = j]
          \/ ~grant /\ UNCHANGED votedFor
       /\ Reply([mtype        |-> RequestVoteResponse,
                 mterm        |-> currentTerm[i],
                 mvoteGranted |-> grant,
                 \* mlog は証明で使用する記録用の変数で実装には現れない
                 mlog         |-> log[i],
                 msource      |-> i,
                 mdest        |-> j],
                 m)
       /\ UNCHANGED <<state, currentTerm, candidateVars, leaderVars, logVars>>

\* m.mterm = currentTerm[i] が成り立つ場合に
\* Server i は Server j からの RequestVote response を受信する
HandleRequestVoteResponse(i, j, m) ==
    \* 現在の状態が Candidate でない場合でも票を集計しますが、単に無視されるので問題ありません。
    /\ m.mterm = currentTerm[i]
    /\ votesResponded' = [votesResponded EXCEPT ![i] =
                              votesResponded[i] \cup {j}]
    /\ \/ /\ m.mvoteGranted
          /\ votesGranted' = [votesGranted EXCEPT ![i] =
                                  votesGranted[i] \cup {j}]
          /\ voterLog' = [voterLog EXCEPT ![i] =
                              voterLog[i] @@ (j :> m.mlog)]
       \/ /\ ~m.mvoteGranted
          /\ UNCHANGED <<votesGranted, voterLog>>
    /\ Discard(m)
    /\ UNCHANGED <<serverVars, votedFor, leaderVars, logVars>>

\* m.mterm <= currentTerm[i] が成り立つ場合に
\* Server i は Server j から AppendEntries request を受信する
\* ここでは、長さが 0 か 1 の m.entries のみを処理するが、複数回の独立した 1 entry の request
\* を処理する場合と同様に扱うことで実際の実装では複数の entry を含む m.entries を受信して処理してよい
HandleAppendEntriesRequest(i, j, m) ==
    LET logOk == \/ m.mprevLogIndex = 0
                 \/ /\ m.mprevLogIndex > 0
                    /\ m.mprevLogIndex <= Len(log[i])
                    /\ m.mprevLogTerm = log[i][m.mprevLogIndex].term
    IN /\ m.mterm <= currentTerm[i]
       /\ \/ /\ \* request を拒否する
                \/ m.mterm < currentTerm[i]
                \/ /\ m.mterm = currentTerm[i]
                   /\ state[i] = Follower
                   /\ \lnot logOk
             /\ Reply([mtype           |-> AppendEntriesResponse,
                       mterm           |-> currentTerm[i],
                       msuccess        |-> FALSE,
                       mmatchIndex     |-> 0,
                       msource         |-> i,
                       mdest           |-> j],
                       m)
             /\ UNCHANGED <<serverVars, logVars>>
          \/ \* Follower 状態に戻る
             /\ m.mterm = currentTerm[i]
             /\ state[i] = Candidate
             /\ state' = [state EXCEPT ![i] = Follower]
             /\ UNCHANGED <<currentTerm, votedFor, logVars, messages>>
          \/ \* request を受け入れる
             /\ m.mterm = currentTerm[i]
             /\ state[i] = Follower
             /\ logOk
             /\ LET index == m.mprevLogIndex + 1
                IN \/ \* すでに request の内容を処理済み
                       /\ \/ m.mentries = << >>
                          \/ /\ Len(log[i]) >= index
                             /\ log[i][index].term = m.mentries[1].term
                       \* 次の処理は古い request や重複した request を受信した場合
                       \* commitIndex を減らす可能性があるが実際にはほとんど何の影響も及ぼさない 
                       /\ commitIndex' = [commitIndex EXCEPT ![i] =
                                              m.mcommitIndex]
                       /\ Reply([mtype           |-> AppendEntriesResponse,
                                 mterm           |-> currentTerm[i],
                                 msuccess        |-> TRUE,
                                 mmatchIndex     |-> m.mprevLogIndex +
                                                     Len(m.mentries),
                                 msource         |-> i,
                                 mdest           |-> j],
                                 m)
                       /\ UNCHANGED <<serverVars, logVars>>
                   \/ \* conflict: 1 entry を削除
                       /\ m.mentries /= << >>
                       /\ Len(log[i]) >= index
                       /\ log[i][index].term /= m.mentries[1].term
                       /\ LET new == [index2 \in 1..(Len(log[i]) - 1) |->
                                          log[i][index2]]
                          IN log' = [log EXCEPT ![i] = new]
                       /\ UNCHANGED <<serverVars, commitIndex, messages>>
                   \/ \* no conflict: entry を追加
                       /\ m.mentries /= << >>
                       /\ Len(log[i]) = m.mprevLogIndex
                       /\ log' = [log EXCEPT ![i] =
                                      Append(log[i], m.mentries[1])]
                       /\ UNCHANGED <<serverVars, commitIndex, messages>>
       /\ UNCHANGED <<candidateVars, leaderVars>>

\* m.mterm = currentTerm[i] が成り立つ場合に
\* Server i は Server j からの AppendEntries response を受信する
HandleAppendEntriesResponse(i, j, m) ==
    /\ m.mterm = currentTerm[i]
    /\ \/ /\ m.msuccess \* 成功した場合
          /\ nextIndex'  = [nextIndex  EXCEPT ![i][j] = m.mmatchIndex + 1]
          /\ matchIndex' = [matchIndex EXCEPT ![i][j] = m.mmatchIndex]
       \/ /\ \lnot m.msuccess \* 失敗した場合
          /\ nextIndex'  = [nextIndex EXCEPT ![i][j] =
                               Max({nextIndex[i][j] - 1, 1})]
          /\ UNCHANGED <<matchIndex>>
    /\ Discard(m)
    /\ UNCHANGED <<serverVars, candidateVars, logVars, elections, leaderStartLog, commitedEntries>>

\* 受信者の currentTerm よりも新しい term を持つ任意の RPC message は受信者の currentTerm を初めに更新する
UpdateTerm(i, j, m) ==
    /\ m.mterm > currentTerm[i]
    /\ currentTerm'    = [currentTerm EXCEPT ![i] = m.mterm]
    /\ state'          = [state       EXCEPT ![i] = Follower]
    /\ votedFor'       = [votedFor    EXCEPT ![i] = Nil]
    \* message m はさらに処理する必要があるので messages に変更はない
    /\ UNCHANGED <<messages, candidateVars, leaderVars, logVars>>

\* 古い term を持つ reponse は破棄する
DropStaleResponse(i, j, m) ==
    /\ m.mterm < currentTerm[i]
    /\ Discard(m)
    /\ UNCHANGED <<serverVars, candidateVars, leaderVars, logVars>>

\* message を受信する
Receive(m) ==
    LET i == m.mdest
        j == m.msource
    IN \* 任意の新しい term を持つ RPC は受信者の term を先に更新する
       \* 古い term を持つ response は破棄される
       \/ UpdateTerm(i, j, m)
       \/ /\ m.mtype = RequestVoteRequest
          /\ HandleRequestVoteRequest(i, j, m)
       \/ /\ m.mtype = RequestVoteResponse
          /\ \/ DropStaleResponse(i, j, m)
             \/ HandleRequestVoteResponse(i, j, m)
       \/ /\ m.mtype = AppendEntriesRequest
          /\ HandleAppendEntriesRequest(i, j, m)
       \/ /\ m.mtype = AppendEntriesResponse
          /\ \/ DropStaleResponse(i, j, m)
             \/ HandleAppendEntriesResponse(i, j, m)

\* End of message handlers.
----
\* Network 状態の遷移

\* network は message を複製する
DuplicateMessage(m) ==
    /\ Send(m)
    /\ UNCHANGED <<serverVars, candidateVars, leaderVars, logVars>>

\* network は message を落とす
DropMessage(m) ==
    /\ Discard(m)
    /\ UNCHANGED <<serverVars, candidateVars, leaderVars, logVars>>

----
\* 変数の遷移の仕方の定義
Next ==  \/ \E i \in Server : Restart(i)
         \/ \E i \in Server : Timeout(i)
         \/ \E i,j \in Server : RequestVote(i, j)
         \/ \E i \in Server : BecomeLeader(i)
         \/ \E i \in Server, v \in Value : ClientRequest(i, v)
         \/ \E i \in Server : AdvanceCommitIndex(i)
         \/ \E i,j \in Server : AppendEntries(i, j)
         \/ \E m \in DOMAIN messages : Receive(m)
         \/ \E m \in DOMAIN messages : DuplicateMessage(m)
         \/ \E m \in DOMAIN messages : DropMessage(m)
         \* 全ての log を追跡する History 変数:
         \* 今回の検証では使用しないのでコメントアウト
\*       /\ allLogs' = allLogs \cup {log[i] : i \in Server}

\* Raft の状態遷移は初期状態から始まって Next の定義にしたがって遷移する
Spec == Init /\ [][Next]_vars

----
\* Raft は常に以下の性質が成り立つことを保証します
\* 以下の Operator を Invariant として TLA model checker に設定してください

\* 1 つの term には多くとも 1 つの Leader が存在する
ElectionSafety == \A s1,s2 \in Server: s1 /= s2 /\ currentTerm[s1] = currentTerm[s2] => state[s1] /= Leader \/ state[s2] /= Leader

\* Leader は自分自身の log に対して追記のみをして、書き換えや削除をしない
LeaderAppendOnly == \A i \in Server : state[i] = Leader => SubSeq(log[i], 1, Len(leaderStartLog[i])) = leaderStartLog[i]

\* 2 つの log が同じ index に同じ term の entry を持つなら、その index までの entry は全て一致する
LogMatching == \A i,j \in Server: i /= j => LET k == MaxMatchTermIndex(log[i], log[j]) IN SubSeq(log[i], 1, k) = SubSeq(log[j], 1, k)

\* もしある entry がある term に commit されたなら、その term 以降の全ての Leader はその entry を log の中に含む
LeaderCompleteness == \A i \in Server : state[i] = Leader => commitedEntries = SubSeq(log[i], 1, Len(commitedEntries))

\* ある Server の log の特定の index の entry を自身の state machine に適用するとき
\* 他の全ての Server の log のその index には同じ entry が存在する
\* 各 Server が自身の state machine に適用する entry は必ず commitIndex 以下である必要がある
StateMachineSafety == LET
                        minCommitIndex == Min({ commitIndex[i] : i \in Server})
                      IN
                        \A i,j \in Server: SubSeq(log[i], 1, minCommitIndex) = SubSeq(log[j], 1, minCommitIndex)

=============================================================================

TLA+ による Raft の検証方法

TLA+ Toolbox のインストール

以下の GitHub のページにアクセスして、自身の環境に応じた TLA+ Toolbox の zip ファイルをダウンロードしてインストールします。
github.com

TLA+ Toolbox のインストール
TLA+ Toolbox のインストール

新規 Spec の作成

TLA+ Toolbox を起動したら、メニューの 「File」->「Open Spec」->「Add New Spec」を選択します。適当なディレクトリに main.tla という名前でファイルを作成します。

新規 Spec の作成
新規 Spec の作成

ファイルを作成したら上のコードを貼り付けます。

検証用コードの貼り付け
検証用コードの貼り付け

検証コードの 1 行目の MODULE 名とファイル名は一致する必要があります。もし、上の操作で別の名前をつけた場合は MODULE main の箇所を MODULE *fileName* に修正してください。

Model の作成と実行

次に Model を作成します。メニューの 「TLC Model Checker」->「New Model」を選択します。モデルの名前はデフォルトの Model_1 で構いません。

新規モデルを作成
新規モデルを作成

すると 10 errors detected というエラーが表示されます。これは main.tla で使用している定数に値が割り当てられていないという意味なので値を割り当てていきます。

モデル作成時のエラー
モデル作成時のエラー

画面中央右の What is the model? という欄の AppendEntriesResponse の行をダブルクリックするとダイアログが表示されます。

定数への値の割り当て
定数への値の割り当て

AppendEntriesResponse に対しては Model value を選択して Finish ボタンをクリックします。同様に Value と Server 以外の定数に Model Value を割り当てます。

残りの定数への値の割り当て
残りの定数への値の割り当て

Value は Client が Raft に対して書き込む内容です。アプリケーションによって幾つの値を取りうるかは変化します。一方で、Value の種類を増やしても Raft の性質の検証にはあまり役に立たない上に、探索する必要のある状態空間が増えるのでここでは 2 つの値を割り当てます。
Value に集合を割り当てるには Set of model value を選択して値をフォームに入力します。ここでは {op1, op2} を Value に割り当てます。

定数 Value に値を割り当て
定数 Value に値を割り当て

最後に Server に値を割り当てます。Raft において各 Server の役割は対称的です。つまりそれぞれに区別をつける必要がありません。例えば 3 つの Server {s1, s2, s3} がある場合に s1 がはじめに Leader になるパターンと s2, s3 がそれぞれはじめに Leader になるパターン全部を検証する必要はありません。s1 が Leader になるパターンだけを検証すれば十分です。このように区別をつけないようにすることで探索する必要のある空間を大幅に減らすことができます。
Server に区別をつけない値の集合を割り当てるには Set of model value を選択した後に、Symmetry set にチェックを入れます。ここでは Server に {s1, s2, s3} を割り当てます。

定数 Server に値を割り当て
定数 Server に値を割り当て

ここでは Server が 3 台の場合を検証する手順を示しましたが、1 台や 2 台 の場合も同様です(1 台の場合は Symmetry set のチェックボックスを外す)。4 台以上でも構いません。次に、下の What to check? の Invariant をクリックしてフォームを開きます。ここに検証する必要のある性質を指定していきます。

Invariant を指定するフォーム
Invariant を指定するフォーム

右の Add をクリックするとダイアログが表示されるので、フォームに ElectionSafety と入力して Finish をクリックします。

Invariant に ElectionSafety を指定
Invariant に ElectionSafety を指定

同様に LeaderAppendOnly、LogMatching、LeaderCompleteness、StateMachineSafety を追加します。

全ての Invariant を指定
全ての Invariant を指定

Invariant に指定することで、Raft が探索して発見した全ての状態において、Invariant に指定した論理式が True になるかチェックされます。もし、False になるような状態が見つかればエラーと共に、その状態に至る過程と全ての変数の値が表示されるので原因を特定します。

検証を始めるには、左上の緑の Run TLC ボタンをクリックします。

モデルチェックの開始ボタン
モデルチェックの開始ボタン

自動的に Model Check Results ページがオープンして Model Check の進行状況を表示します。

Model Check Results ページ
Model Check Results ページ

ちなみに、この Raft の検証コードは問題がないはずなのでモデルチェックはいつまでたっても終わりません。Leader の log は延々と伸び続けるだけだからです。
モデルチェックに対して何かしらの制約をかけて終わらせたい場合は、Additional Spec Options のページの State Constraint に適切な制約を記述することで終わらせることもできます。

Model Check を実行し続けるとすぐにチェックした状態数が数千万単位になります。それだけの状態数において上の Invariant が満たされ続けるということが確認できたので、Raft のアルゴリズムの健全性を高い確度で確信できます。この網羅性の高さと、チェックする状態数の多さがテストと比較した場合の形式仕様記述 + モデル検査ツールの優位性です。

補足: コマンドラインでの検証

手元のマシンではなく、クラウド上により強力なマシンを用意して、より高速に検証をしたいという方向けに TLC Model Checker をコマンドラインで動かす方法もあります。
medium.com

Java は OpenJDK ではなくて OracleJDK を使用します。OpenJDK ではエラーがでます。OracleJDK をインストールしたら以下のツールを git clone してインストールします。
github.com

コマンドラインでの検証用に上の main.tla と同じディレクトリに以下の 2 つのファイルを MC.tla、MC.cfg という名前で保存します。このファイルの内容は、main.tla を保存したディレクトリに TLC Model Checker によって生成される main.toolbox 内からコピーしたものです。

---- MODULE MC ----
EXTENDS main, TLC

\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
op1, op2
----

\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
s1, s2, s3
----

\* MV CONSTANT definitions Value
const_1593089061951878000 ==
{op1, op2}
----

\* MV CONSTANT definitions Server
const_1593089061951879000 ==
{s1, s2, s3}
----

\* SYMMETRY definition
symm_1593089061951880000 ==
Permutations(const_1593089061951879000)
----

=============================================================================
\* MV CONSTANT declarations
CONSTANTS
op1 = op1
op2 = op2
\* MV CONSTANT declarations
CONSTANTS
s1 = s1
s2 = s2
s3 = s3
\* CONSTANT declarations
CONSTANT AppendEntriesResponse = AppendEntriesResponse
\* CONSTANT declarations
CONSTANT Follower = Follower
\* CONSTANT declarations
CONSTANT Leader = Leader
\* CONSTANT declarations
CONSTANT Nil = Nil
\* CONSTANT declarations
CONSTANT RequestVoteResponse = RequestVoteResponse
\* CONSTANT declarations
CONSTANT Candidate = Candidate
\* CONSTANT declarations
CONSTANT RequestVoteRequest = RequestVoteRequest
\* CONSTANT declarations
CONSTANT AppendEntriesRequest = AppendEntriesRequest
\* MV CONSTANT definitions
CONSTANT
Value <- const_1593089061951878000
\* MV CONSTANT definitions
CONSTANT
Server <- const_1593089061951879000
\* SYMMETRY definition
SYMMETRY symm_1593089061951880000
\* SPECIFICATION definition
SPECIFICATION
Spec
\* INVARIANT definition
INVARIANT
ElectionSafety
LeaderAppendOnly
LogMatching
LeaderCompleteness
StateMachineSafety

最後に以下のコマンドを実行します。

tlc MC.tla -config MC.cfg -workers auto

Raft の拡張について

上で検証した TLA+ のコードは Raft のコアアルゴリズムに関する記述です。一方で、実際に Raft を運用する場合はさらにいくつかの機能を追加する必要があります。論文では以下の 4 つの拡張機能について検討されています。

  • Leadership Transfer (Chapter 3)
  • Membership Change (Chapter 4)
  • Log Compaction (Chapter 5)
  • Client Interaction (Chapter 6)

各機能の詳細は論文を参照してください。ここでは、拡張機能の検証コードを追加する視点でこれらの機能を見ていきます。今後コードを書いて検証する予定のない方は飛ばしてください。私はこれらの機能を全て追加した検証コードを実装し検証済みです。公開はしないので興味のある方はご連絡ください。

Leadership Transfer

Leadership Transfer は Leader が意図的に Leadership を他の Server に移譲する機能です。例えば、メンテナンスのために Leader の Server をクラスターから外す場合や、Leader が動く Server が高負荷状態にある場合やネットワークレイテンシーが大きい場合に意図的に他の Server に Leadership を移譲したい場合に使用します。
Leader を単に停止すれば他の Server が Election Timeout 後に自動的に選挙を開始しますが、Leadership Transfer を使用すれば Election Timeout を待たずに選挙のプロセスをすぐに開始でき、ダウンタイムを最小にできます。

Leadership Transfer を検証コードに追加するのは簡単です。新しい Message Type として TimeoutNow を追加します。Leader は自身が保有する log と十分に多くの entry を共有している Server に対して TimeoutNow メッセージを送信します。TimeoutNow メッセージを受信した Follower はすぐに Candidate に遷移し新しい選挙を開始します。

Leadership Transfer は拡張機能の中で検証コードの実装が一番簡単なので練習問題として実装して検証してみるといいでしょう。

Membership Change

実運用環境では Raft クラスターを運用しながら落ちた Server をクラスターから外したり、replication 数を増やすために Server を追加する必要があります。Raft ではクラスターに 1 台ずつ Server を追加または削除するという操作を繰り返すことで任意回数のクラスターメンバーの入れ替えを実現します。ここまでは定数 Server に指定した Server の集合は全て Raft のクラスターに参加していると想定していました。この拡張機能では Server の集合のうち Raft のクラスターに参加している Server が動的に変化する状況で Invariant が成り立つことを検証します。

追加する RPC は AddServer、RemoveServer の 2 つです。さらに Server の状態として NonVoting、Waiting を追加します。この 2 つの状態はクラスターに参加していない状態を表現します。さらに Configuration(クラスター構成情報) を log の entry として共有するので、entry にも ETValue、ETConfig の 2 つの型を導入します。

Waiting 状態にある Server をすぐに Follower としてクラスターに参加させると、新しい Follower の log が Leader の log に追いつくまで entry が中々 commit できずに可用性が低下する場合があります。その状況を避けるために、クラスターに参加させる前に log が追いつくまで待機するのが NonVoting 状態です。NonVoting 状態の Server は Leader から AppendEntriesRequest を受信しますが、選挙には関わりません。また、NonVoting 状態の Server が存在する状態で Leader の変更があった場合にどうするか、など取り扱いが複雑です。
Configuration についても、ETConfig 型の entry はcommit されていなくても有効なものと判断して参照しますが、新しい AddServer RPC、RemoveServer RPC を受け付けるのは最新の ETConfig 型の entry が commit 済みの場合のみでタイミングにズレがあります。

Log Compaction

Raft の log は動作期間を通して伸びる一方です。log が大きくなると、より多くのディスクを占有し、再起動時の state machine の再構築により多くの時間がかかるようになります。そして、最終的には可用性の問題が発生します。従って、実用的なシステムでは何らかの形での log を圧縮する必要があります。

TLA+ で検証する際には Memory Base か Disk Base かは関係ありません。Incremental Approach は Raft の検証よりも log-structured merge trees のアルゴリズムの検証になりそうなので私は検証していません。Leader Base Snapshot も実装はしていませんがそれほど複雑にはならないと思います。ここでは Memory Base Snapshot を実装する場合を想定します。
state machine が Snapshot を取得すると、Snapshot を作成した時点で state machine に適用している log の index までは破棄することができます。そこで、破棄した index を記憶するために prevIndex、prevTerm を新たに Server ごとの変数として追加します。さらに、Invariant を検証するために snapshot という変数を追加して、そこに削除した log を記録しておくといいでしょう。
log を削除すると log の長さが変わるので、今まで Len(log[i]) のように log の長さを直接使用していた箇所を全て書き換える必要があります。さらに、Follower が必要とする log の entry をすでに削除していた場合に Snapshot を転送する InstallSnapshot RPC を実装します。InstallSnapshot RPC も 1 回の実行で Snapshot を全て転送するのではなく徐々に転送するようにすると実際のシステムの検証により近づくでしょう。

Client Interaction

論文では、Client Interaction は Membership Change や Log Compaction と比較すると簡潔に述べられていますが実装は一番大変です。Client Interaction を考慮する必要がある理由としては Raft をベースに構築した分散ロックシステムを利用する、論文の Figure 6.2 の状況が一番わかりやすいと思います。

f:id:hitotakuchan:20200627213119p:plain
Figure 6.2: 重複したコマンドによる誤った結果の例。クライアントがロックを取得するためにコマンドを送信したとします。クライアントの最初のコマンドはロックを取得しましたが、クライアントは確認応答を受け取りませんでした。クライアントがリクエストを再試行すると、ロックは獲得済みのためリクエストは失敗します。

Figure 6.2 の状況でも正しく動作するために、各 Server は Client のセッション情報と Client の request を処理した結果の Cache をそれぞれ保持する必要があります。Leader は Client からの request を管理する Queue と処理結果の Cache を使用して Client の request を適切に処理します。Client は自身に割り当てられた Client ID とメッセージの index を管理してメッセージにユニークな ID を割り当てる必要があります。また、論文では ClientRequest RPC と ClientQuery RPC を別の処理として説明していますが、entry の型だけが違う同じ処理としていいと思います。

Client Interaction では Raft の 5 つの性質に加えて「同じ ID を持つ Client の request が Raft によって 2 度処理されることはない」という Invariant を加えて検証するといいでしょう。

おわりに

形式仕様記述の道を極めていきたいと思った人はまずこの記事のコードに上で説明した拡張機能を実装して検証するといいでしょう。プログラミングの経験がある方は TLA+ の記述法にはじめは違和感を感じるかもしれませんがすぐに意図したアルゴリズムを実装できるようになると思います。
次の段階として、この記事では Raft の満たす 5 つの性質を私が論理式に直しましたが、自分自身で論理式として表現できるか確認してください。あるいは、他に満たすべき性質はないか?拡張機能について満たす必要のある性質は何か?を考えてそれを論理式として追加し検証してください。ただし、多くの人はこの段階で躓くと思います。

上で引用した記事にも同様のことに言及している箇所があるので引用します。

このような事情も相まって、形式手法を上手に扱うのにはかなりの知識が必要です。実際に取り組んでみるとわかるのですが、まず人間は意図通りの論理式やモデルを書けません(必要な条件を忘れていたりそもそも意図が間違ってたりする)。当たり前の話ですが、従来のコードでさえ正しく書けないのに、より抽象度の高い論理式やモデルを最初から正しく書けるはずがないのです

正確に意図を論理式として表現する能力はプログラミングというよりも数学の領域の能力だと思います。この能力は、大学で数学を先行する初学者も身につけるのに大いに苦労する能力だと思います。この能力をどうやって身につけるか?という問いに明確な回答を私は持ち合わせてはいませんが、場数を踏む必要があるのは間違いありません。今後このブログで TLA+ を用いてプログラムの検証を行う内容の記事を書く予定です。

最後に、Raft を TLA+ を用いて検証する手順を通して形式仕様記述やモデル検査とはどういうものなのか?検証とテストの違いは何か?といったことを大雑把に把握して今後の学習のためのエントリーポイントとしてこの記事を利用してもらえると嬉しいです。

Raft 理解度を調べるクイズ

  • Client からの接続が Timeout までに commit が成功しなかった entry はその後 commit されるか?
  • Leader は Client からの書き込み entry を log に保存すると同時に state machine を更新してもよいか?
  • Leader は Leader になった時点で自身の log に存在する entry を全て commit してもよいか?
  • commit index は Leader だけが保持しているのか?それとも全ての server がそれぞれ保持しているか?
  • 各 server が保持する currentTerm を更新するのは正確にいつといつか?

参考資料

Raft に関する資料

TAL+ の仕様を理解する上では 3 章と 8 章を読むといいです。
4,5,6 章は Raft をより実用的なシステムにする上で必要な追加機能の解説です。論文中でも、このブログでも検証しているのは Raft のコアアルゴリズムの部分だけで、これらの機能を追加した場合の検証はされていません。Raft を実装しプロダクション用途で使用する場合にはこれらの機能も合わせて検証する必要があるでしょう。
9, 10 章は Raft の実装の性能評価などが書かれているので自身で Raft を実装する人は読むといいと思います。また、Raft に依存した分散システムを運用している人が、適切な設定値を決める際の根拠として参照するといいでしょう。

  • Raft の考案者 Diego Ongaro による TLA+ 実装

github.com

  • LogCabin – Diego Ongaro による Raft の実装

github.com

  • Raft の動作する様子

Raft
Raft Consensus Algorithm

  • Raft に関して日本語で読める資料

PFI の勉強会のスライド資料
Raft(分散合意アルゴリズム)について · GitHub
分散合意アルゴリズム Raft を理解する - Qiita

TLA+ に関する資料

  • TLA+ のホームページ

lamport.azurewebsites.net

  • 形式手法についての記事

自動テストに限界を感じた私がなぜ形式手法に魅了されたのか - 若くない何かの悩み
AWSにおける形式手法 - masateruk’s blog
形式手法 (Formal Methods) についての調査 - つれづれ日記
ゼロから学んだ形式手法 - DeNA Testing Blog
TLA+の社内勉強会スライド公開します - takaha.siの技術メモ
[TLA+] TLA+と形式仕様言語 [目的と準備] | Developers.IO
FINAL FANTASY XV POCKET EDITION を支える AWS サーバレス技術

  • TLA+ の設計者 Leslie Lamport による TLA+ を用いた形式検証の教科書

これから TLA+ を使用して形式検証を行いたいと思う人はこの本を読みましょう。

  • TLA+ をプログラマフレンドリーな構文にした PlusCal を用いた形式検証の教科書

Practical TLA+: Planning Driven Development

Practical TLA+: Planning Driven Development

  • 作者:Wayne, Hillel
  • 発売日: 2018/10/12
  • メディア: ペーパーバック
PlusCal を用いて仕様を記述すると TLA+ と比較して簡略になる部分はあります。
一方で、私はこの記事を書くにあたって Raft の仕様を PlusCal で書き換えるという作業を行いました。その経験で言うと、簡単な小さい仕様であれば PlusCal で記述する方が簡潔になりますが、Raft のようにアルゴリズムが複雑で大きい仕様になると PlusCal の表現力の弱さが足かせになります。
この本を読むこと自体は有益なのでお勧めしますが、PlusCal を実際に仕事で使うかと言われれば、私は使いません。

A Proof for Log Matching Property of Raft

背景

分散合意アルゴリズム Raft は kubernetes のクラスターの構成情報を保存する etcd の内部で使われておりお世話になっている方も多いアルゴリズムだと思います。
この記事では Raft の満たす重要な性質である Log Matching Property について証明します。


元々、『Raft を TLA+ で検証する』というタイトルの記事を書こうと考えて Raft の考案者 Diego Ongaro の博士論文を読み始めました(その記事は後日公開予定です)。
アルゴリズムは論文の 3 章に書かれているのですが、そこで Raft が常に成り立つことを保証する 5 つの性質の 1 つとして Log Matching Property を挙げています。
Log Matching Property は次のような性質です。

  • 異なるログの 2 つの entry が同じインデックスと term を持つ場合、それらは同じコマンドを格納する。
  • 異なるログの 2 つの entry が同じインデックスと term を持つ場合、ログは先行するすべての entry で一致する。

Diego Ongaro はこれらの性質を証明するのではなく TLA+ という形式仕様記述言語を使用して検証しています。
実用上はそれで十分なのですが、論文中で Log Matching Property の証明について次のように言及しています。

1 つ目の特性は、leader が与えられた term の与えられたログインデックスを持つ entry を最大 1 つ作成し、entry はログ内での位置を決して変更しないという事実からきています。2 つ目の特性は、AppendEntries によって実行される一貫性チェックによって保証されます。

私は、形式的な証明を沢山してきているので、この内容を元に Log Matching Property を脳内で証明しようと試みたのですが全くできる気配がありませんでした。
例えば、「entry はログ内での位置を決して変更しない」ことも証明しないといけない性質なのに証明せずに使用しています。
また、「AppendEntries によって実行される一貫性チェック」に関しても、AppendEntries は実用上の理由により、 follower のログの最後の entry の term が leader のログの同じインデックスの entry の term と一致すると、それ以下のログは一致しているとみなして再帰的な処理をやめてしまいます。
再帰的な処理をやめるというのが証明をする上でとても厄介で、寧ろこのような最適化はせずに leader のログを丸々 follower にコピーするというアルゴリズムになっている方が性質の証明はずっと簡単です。


結局納得できる証明を構成するのに Stay Home 期間の 2 週間を費やしました。
証明をするためのポイントは、一見無関係に見える leader のログの間の関係性をどのように論理式で表現し公理として採用するかという点でした。
この公理が強すぎると、今証明しようとしている Log Matching Property 自体を公理に誤って入れ込んでしまう可能性があります。
実際私も 1 週間くらい考えた末に証明できたと思い記事を書いていたのですが、証明を見直してみると Log Matching Property を仮定するような公理を元に証明していることに気付きやり直しました。
公理の最終案は以下になります。


 Axiom
\begin{equation}
\forall (i\colon Index)(t \colon Term),\, t \neq L_{t}[i].term \Rightarrow \\
\forall (l \colon Log),\ \exists (l' \colon Log)(t' \colon Term),\, L_{t}[i].term \le t' \lt t \land AppendEntries(i, t, l) = AppendEntries(i, t', l')
\end{equation}


この公理が以下の 3 つの気持ちを表現していることを感じ取ってもらえるでしょうか。

  • Raft では leader は自身のログに自身の term の entry しか追加しないこと
  • term  t の leader のログに term  t’ の entry があったとしてもその entry が term  t’ の leader によって term  t の leader のログに書き込まれたとは限らないこと
  • leader 同士のログはこの関係を通して互いに関連していること


十分に形式的に証明をしたつもりではいますが、Coq 等で実際に証明したわけではないので 100% 正しいとは言えません。
もし、誤りを見つけた方がいたらコメント欄で教えていただけると幸いです。

Log Matching Property の証明

データ構造と述語の定義

Log Matching Property を証明するためにまずデータ構造と述語を定義します。記述は特定の言語を想定していません。

// Index, Term は Nat の別名
type Index = Nat
type Term = Nat

// Entry は Term を指定して作成
Inductive Entry = makeEntry : Term -> Entry

// Log は Entry の List
type Log = List Entry

log の index は 1 から始まるとし index 0 へのアクセスは undefined とします。また、log  l の部分リスト  l[i..0] は空リストであると定義します。

次に AppendEntries 関数を定義します。

Function AppendEntries(i: Index)(t: Term)(l: Log) : Log =
  if i = 0 then
    []
  else
    // AppendEntries で i-1 の log を作成して末尾に Lt[i] を追加
    if i > length(l) + 1 then
      AppendEntries(i-1, t, l)::Lt[i]
    elseif i = length(l) + 1 then
      // l の末尾の entry の term と Lt[i-1] の term が等しい場合は、l の後に Lt[i] を追加
      // そうでない場合は AppndEntries で i-1 の log を作成して末尾に Lt[i] を追加
      if l[i-1].term = Lt[i-1].term then
        l::Lt[i]
      else
        AppendEntries(i-1, t, l)::Lt[i]
      end
    else
      // i が length(l) + 1 より短い場合は l の末尾の entry を削除して AppendEntries を呼び出す
      AppendEntries(i, t, l[1..length(l)-1])
    end
  end

AppendEntries 関数は任意の index と term と log を受け取って長さが  i の log を返します。 Lt は term  t における leader の log を表します。Raft では leader の log は時間とともに成長しますがここでは定数とし、 i を変更することで模倣します。

log は entry のリストですが、Raft で扱う log は AppendEntries 関数を通して作成された log のみです。これを述語として表現します。

Inductive RaftLog : Term -> Log -> Prop :=
  | rlnil : ∀ (t: Term), RaftLog(t, [])
  | rlAppend:  ∀(t, t': Term)(l: Log)(i: Index), RaftLog(t', l) -> t' <= t -> RaftLog(t, AppendEntries(i, t, l)).

rlnil は任意の空リストは任意の term で RaftLog であるという意味です。
rlAppend は log  l が term  t' \le t で RaftLog( t',  l) であるなら AppendEntries( i,  t,  l) は RaftLog であるという意味です。
任意の log を取り扱うのではなく、RaftLog(t, l) という述語が真になる log のみを考察の対象にします。

AppendEntries 関数の性質

AppendEntries 関数の性質について 4 つの Lemma(補題) を証明します。

Lemma AppendEntries 1 はアルゴリズム中の  i \lt length(l) + 1 の場合に関する補題です。
log の長さが最終的な長さよりも長い場合は再帰的に末尾の entry が削除されます。AppendEntries に log をそのまま渡しても、log を先に短くしてから渡しても結果は変わりません。


 Lemma\ AppendEntries\ 1
\begin{equation}
\forall (l\colon Log)(i\colon Index)(t \colon Term),\, i \le length(l) \Rightarrow AppendEntries(i, t, l) = AppendEntries(i, t, l[1..(i\!-\!1)])
\end{equation} Proof
log  l に関する帰納法を用いる。

  •  l = [] の場合

 i \le length(l) より  i = 0 であるから  AppendEntries(0, t, []) = AppendEntries(0, t, []) が成り立つ。

  •  l = l'::e の場合

帰納法の仮定より次のことが成り立つ。
\begin{equation}
\forall (i\colon Index)(t\colon Term),\, i \le length(l') \Rightarrow AppendEntries(i, t, l') = AppendEntries(i, t, l'[1..(i\!-\!1)])
\end{equation}
 i \le length(l'::e) より  i = length(l'::e) の場合と  i \lt length(l'::e) の場合を考える。

  •  i = length(l'::e) の場合

 i \lt length(l'::e)+1 であるから
\begin{align*}
AppendEntries(i, t, l'::e) &= AppendEntries(i, t, l') \\
&= AppendEntries(i, t, (l'::e)[1..(i\!-\!1)])
\end{align*}

  •  i \lt length(l'::e) の場合

 i \lt length(l'::e) であるから
\begin{align*}
AppendEntries(i, t, l'::e) &= AppendEntries(i, t, l')
\end{align*}
が成り立つ。一方で、 i \le length(l') であるから仮定より次のことが成り立つ。
\begin{align*}
AppendEntries(i, t, l') &= AppendEntries(i, t, l'[1..(i\!-\!1)]) \\
&= AppendEntries(i, t, (l'::e)[1..(i\!-\!1)])
\end{align*}

 \square

Lemma AppendEntries 2 は空リストに対して term  t において AppendEntries を実行すると term  t の leader の log と一致することを意味します。


 Lemma\ AppendEntries\ 2
\begin{equation}
\forall (i\colon Index)(t \colon Term),\, AppendEntries(i, t, [ ]) = L_{t}[1..i]
\end{equation} Proof
index  i に関する帰納法を用いる。

  •  i = 0 の場合

\begin{equation}
AppendEntries(0, t, [ ]) = [] = L_{t}[1..0]
\end{equation}

  •  i = k の場合

 i \lt k のとき次式が成り立つと仮定する。
\begin{equation}
\forall (t \colon Term),\, AppendEntries(i, t, [ ]) = L_{t}[1..i]
\end{equation}
 i = k \gt 0 とすると、

  •  k \gt 1 の場合

\begin{align*}
AppendEntries(k, t, [ ]) &= AppendEntries(k-1, t, [ ])::L_{t}[k] \\
&= L_{t}[1..(k\!-\!1)]::L_{t}[k] \ (\because \rm{帰納法の仮定}) \\
&= L_{t}[1..k]
\end{align*}

  •  k = 1 の場合

\begin{align*}
AppendEntries(1, t, [ ]) &= AppendEntries([ ], t, [ ])::L_{t}[1] \\
&= L_{t}[1]
\end{align*}

 \square

証明は省略しますが Lemma AppendEntries 2 より term  t の leader の log の部分 log  L_{t}[1..i] は RaftLog であることが示せます。


 Lemma\ RaftLog\ 1
\begin{equation}
\forall (i \colon Index)(t\colon Term),\, RaftLog(t, L_{t}[1..i])
\end{equation}

Lemma AppendEntries 3 は任意の log  l から term  t において長さ  i の log を AppendEntries で作成すると、末尾は term  t の leader の  i 番目の entry と一致することを意味します。


 Lemma\ AppendEntries\ 3
\begin{equation}
\forall (i\colon Index)(t \colon Term)(l\colon Log),\, AppendEntries(i, t, l)[i] = L_{t}[i]
\end{equation} Proof

  •  i = 0 の場合

\begin{equation}
AppendEntries(0, t, l)[0] = undefined = L_{t}[0]
\end{equation}

  •  i \gt length(l)+1 の場合

\begin{align*}
AppendEntries(i, t, l)[i] &= (AppendEntries(i\!-\!1,t,l)::Lt[i])[i] \\
&= Lt[i]
\end{align*}

  •  i = length(l)+1 の場合
  •  l[i\!-\!1].term = L_{t}[i\!-\!1].term の場合

\begin{align*}
AppendEntries(i, t, l)[i] &= (l::Lt[i])[i] \\
&= Lt[i]
\end{align*}

  •  l[i\!-\!1].term \neq L_{t}[i\!-\!1].term の場合

\begin{align*}
AppendEntries(i, t, l)[i] &= (AppendEntries(i\!-\!1,t,l)::Lt[i])[i] \\
&= Lt[i]
\end{align*}

  •  i \lt length(l)+1 の場合

\begin{align*}
AppendEntries(i, t, l)[i] &= AppendEntries(i,t,l[1..(length(l)\!-\!1)])[i] \\
&= AppendEntries(i,t,l[1..(i\!-\!1)])[i] \ (\because Lemma\ AppendEntries\ 1) \\
&= Lt[i] \ (\because i = length(l)+1 \rm{の場合と同様の議論により})
\end{align*}

 \square

Lemma AppendEntries 4 は任意の log  l から term  t において長さ  i の log を AppendEntries で作成すると、 i\!-\!1 番目の entry の term は term  t の leader の  i\!-\!1 番目の entry の term と一致することを意味します。


 Lemma\ AppendEntries\ 4
\begin{equation}
\forall (i\colon Index)(t \colon Term)(l\colon Log),\, i \gt 1 \Rightarrow AppendEntries(i, t, l)[i\!-\!1].term = L_{t}[i\!-\!1].term
\end{equation} Proof

  •  i \gt length(l)+1 の場合

\begin{align*}
AppendEntries(i, t, l)[i\!-\!1].term &= (AppendEntries(i\!-\!1,t,l)::L_{t}[i])[i\!-\!1].term \\
&= AppendEntries(i\!-\!1,t,l)[i\!-\!1].term \\
&= Lt[i\!-\!1].term \ (\because Lemma\ AppendEntries\ 3)
\end{align*}

  •  i = length(l)+1 の場合
  •  l[i\!-\!1].term = L_{t}[i\!-\!1].term の場合

\begin{align*}
AppendEntries(i, t, l)[i\!-\!1].term &= (l::L_{t}[i])[i\!-\!1].term \\
&= l[i\!-\!1].term \\
&= Lt[i\!-\!1].term
\end{align*}

  •  l[i\!-\!1].term \neq L_{t}[i\!-\!1].term の場合

\begin{align*}
AppendEntries(i, t, l)[i\!-\!1].term &= (AppendEntries(i\!-\!1,t,l)::L_{t}[i])[i\!-\!1].term \\
&= AppendEntries(i\!-\!1,t,l)[i\!-\!1].term \\
&= Lt[i\!-\!1].term \ (\because Lemma\ AppendEntries\ 3)
\end{align*}

  •  i \lt length(l)+1 の場合

\begin{align*}
AppendEntries(i, t, l)[i\!-\!1].term &= AppendEntries(i,t,l[1..(i\!-\!1)])[i\!-\!1].term\ (\because Lemma\ AppendEntries\ 1) \\
&= Lt[i\!-\!1].term\ (\because i = length(l)+1 \rm{の場合と同様の議論により})
\end{align*}

 \square

leader の log に関する性質

leader の log に関する性質でここまでで定義したデータ型や述語では表現できていない性質があります。それは、leader は現在の term を持つ entry を自身の log に追記し、自身の log から以前の term の entry を修正、削除しないことです。
現在の term を  t とすると、leader の log  L_{t} に含まれる term  t' \lt t の entry は leader 自身が  L_{t} に書き込むことはありません。一方で、term  t' の leader が書き込んだとも限りません。
この Raft の性質を表現するために以下の論理式を公理として追加します。


 Axiom
\begin{equation}
\forall (i\colon Index)(t \colon Term),\, t \neq L_{t}[i].term \Rightarrow \\
\forall (l \colon Log),\ \exists (l' \colon Log)(t' \colon Term),\, L_{t}[i].term \le t' \lt t \land AppendEntries(i, t, l) = AppendEntries(i, t', l')
\end{equation}

この公理を用いて 6 つの補題を証明します。
Lemma leader 1 は leader の log が index  i に term  t の entry を持つなら、その entry は term  t の leader の index  i の entry と一致することを意味します。


 Lemma\ leader\ 1
\begin{equation}
\forall (i\colon Index)(t \colon Term),\, L_{t}[i] = L_{L_{t}[i].term}[i]
\end{equation} Proof
二項関係  R \colon Term \to Term \to Prop R\,y\,x = y \lt x \land L_{t}[i].term \le y と定義する。また  P \colon Term \to Prop P\,x = L_{x}[i] = L_{L_{t}[i].term}[i] と定義する。
二項関係  R が well founded relation であることを利用して well founded induction を用いて次を証明する。
\begin{equation}
\forall (x\colon Term),\, \left( \forall (y \colon Term),\, y \lt x \land L_{t}[i].term \le y \Rightarrow L_{y}[i] = L_{L_{t}[i].term}[i] \right) \Rightarrow L_{x}[i] = L_{L_{t}[i].term}[i]
\end{equation}
 x = L_{t}[i].term なら  L_{x}[i] = L_{L_{t}[i].term}[i] が成り立つので、 x \neq L_{t}[i].term とする。すると公理より次が成り立つ。
\begin{equation}
\exists (l' \colon Log)(y \colon Term),\, L_{t}[i].term \le y \lt x \land AppendEntries(i, x, [ ]) = AppendEntries(i, y, l')
\end{equation}
Lemma AppendEntries 2, 3 より  AppendEntries(i, x, [])[i] = L_{x}[i] が成り立つ。よって
\begin{align*}
L_{x}[i] &= AppendEntries(i, x, [ ])[i] \\
&= AppendEntries(i, y, l')[i] \\
&= L_{y}[i] \ (\because Lemma\ AppendEntries\ 3) \\
&= L_{L_{t}[i].term}[i]\ (\because \rm{帰納法の仮定})
\end{align*}

 \square

Lemma leader 2 は term を跨いだ AppendEntries 関数の一貫性に関する補題です。
任意の log  l に対して term  t で長さが  i の log を AppendEntries 関数で作成すると、その log は、ある log  l' が存在して、term  L_{t}[i] において AppendEntries 関数で作成した log と一致します。


 Lemma\ leader\ 2
\begin{equation}
\forall (i\colon Index)(t \colon Term),\, \forall (l \colon Log),\ \exists (l' \colon Log),\, AppendEntries(i, t, l) = AppendEntries(i, L_{t}[i].term, l')
\end{equation} Proof
Lemma leader 1 と同様に二項関係  R \colon Term \to Term \to Prop R\,y\,x = y \lt x \land L_{t}[i].term \le y と定義する。また  P \colon Term \to Prop P\,x = \forall (l\colon Log),\, \exists (l' \colon Log),\, AppendEntries(i, x, l) = AppendEntries(i, L_{t}[i].term, l') と定義する。
公理より
\begin{equation}
\exists (l' \colon Log)(y \colon Term),\, L_{t}[i].term \le y \lt x \land AppendEntries(i, x, l) = AppendEntries(i, y, l')
\end{equation}
帰納法の仮定より次が成り立つ。
\begin{equation}
\exists (l'' \colon Log),\, AppendEntries(i, y, l') = AppendEntries(i, L_{t}[i].term, l'')
\end{equation}
以上より
\begin{align*}
AppendEntries(i, x, l) &= AppendEntries(i, y, l') \\
&= AppendEntries(i, L_{t}[i].term, l'')
\end{align*}

 \square

Lemma leader 3 は Lemma leader 1 と似ていますが index が  i\!-\!1 になっています。
 t' = L_{t}[i].term なら、Lemma leader 1 より  L_{t}[i] = L_{t'}[i] が成り立ちますが  L_{t}[i\!-\!1] と  L_{t'}[i\!-\!1] の関係については term の一致が証明できます。
 i\!-\!1 の term が一致していることから、Lemma leader 1 を使えば entry が一致していることが言えますが Lemma leader 3 は Lemma leader 4 を証明するための準備なのでこれで十分です。


 Lemma\ leader\ 3
\begin{equation}
\forall (i\colon Index)(t,t' \colon Term),\, i \gt 1 \Rightarrow t' = L_{t}[i].term \Rightarrow L_{t}[i\!-\!1].term = L_{t'}[i\!-\!1].term
\end{equation} Proof
\begin{align*}
L_{t}[i\!-\!1].term &= L_{t}[1..i][i\!-\!1].term \\
&= AppendEntries(i, t, [ ])[i\!-\!1].term \ (\because\ Lemma\ AppendEntries\ 2) \\
&= AppendEntries(i, t', l')[i\!-\!1].term \ (\because\ Lemma\ leader\ 2) \\
&= L_{t'}[i\!-\!1].term \ (\because Lemma\ AppendEntries\ 4) \\
\end{align*}

 \square

 t' = L_{t}[i].term のとき、index  i の entry が  L_{t'}[i] と一致することは Lemma leader 1 で証明しました。
Lemma leader 4 は index  i の entry だけではなく index  1 から  i までの全ての entry が一致することを意味します。


 Lemma\ leader\ 4
\begin{equation}
\forall (i\colon Index)(t,t' \colon Term),\, t' = L_{t}[i].term \Rightarrow L_{t}[1..i] = L_{t'}[1..i]
\end{equation} Proof
 i に関する帰納法で示す。

  •  i = 1 の場合

Lemma leader 1 より  L_{t}[1] = L_{t'}[1] が成り立つ。

  •  i = k の場合

Lemma leader 3 より  L_{t}[i\!-\!1].term = L_{t'}[i\!-\!1].term が成り立つ。 L_{t}[i\!-\!1].term = t'' とすると次が成り立つ。
\begin{align*}
L_{t}[1..(i\!-\!1)] &= L_{t''}[1..(i\!-\!1)]\ (\because \rm{帰納法の仮定}) \\
&= L_{t'}[1..(i\!-\!1)]
\end{align*}
よって、
\begin{align*}
L_{t}[1..i] &= L_{t}[1..(i\!-\!1)]::L_{t}[i] \\
&= L_{t'}[1..(i\!-\!1)]::L_{t}[i] \\
&= L_{t'}[1..(i\!-\!1)]::L_{t'}[i]\ (\because Lemma\ leader\ 1) \\
&= L_{t'}[1..i]
\end{align*}

 \square

Lemma leader 5 は AppendEntries 関数は leader の log のコピー関数であることを意味します。


 Lemma\ leader\ 5
\begin{equation}
\forall (t' \colon Term)(l \colon Log),\, RaftLog(t', l) \Rightarrow \forall (i \colon Index)(t \colon Term),\, AppendEntries(i, t, l) = L_{t}[1..i]
\end{equation} Proof
 RaftLog(t', l) に関する帰納法で示す。

  •  l = [] の場合

Lemma AppendEntries 2 より  AppendEntries(i, t, []) = L_{t}[1..i] が成り立つ。

  •  l = AppendEntries(length(l), t', l') の場合

帰納法の仮定より  l = AppendEntries(length(l), t', l') = L_{t'}[1..length(l)] が成り立つ。
つまり、今証明すべきことは次の論理式である。
\begin{equation}
\forall (i \colon Index)(t \colon Term),\, AppendEntries(i, t, L_{t'}[1..length(l)]) = L_{t}[1..i]
\end{equation}
index  i に関する帰納法で示す。

  •  i = 0 の場合

 AppendEntries(0, t, L_{t'}[1..length(l)]) = [] = L_{t}[1..0] が成り立つ。

  •  i = k の場合
  •  k \gt length(l)+1 の場合

\begin{align*}
AppendEntries(k, t, L_{t'}[1..length(l)]) &= AppendEntries(k\!-\!1, t, L_{t'}[1..length(l)])::L_{t}[k] \\
&= L_{t}[1..(k\!-\!1)]::L_{t}[k]\ (\because \text{帰納法の仮定}) \\
&= L_{t}[1..k]
\end{align*}

  •  k = length(l)+1 の場合
  •  L_{t'}[1..(k\!-\!1)][k\!-\!1].term = L_{t}[k\!-\!1].term の場合

 L_{t'}[1..(k\!-\!1)][k\!-\!1].term = L_{t}[k\!-\!1].term = t''' とすると Lemma leader 4 より次が成り立つ。
\begin{align*}
L_{t'}[1..(k\!-\!1)] &= L_{t'''}[1..(k\!-\!1)] \\
&= L_{t}[1..(k\!-\!1)]
\end{align*}
よって
\begin{align*}
AppendEntries(k, t, L_{t'}[1..(k\!-\!1)]) &= L_{t'}[1..(k\!-\!1)]::L_{t}[k] \\
&= L_{t}[1..(k\!-\!1)]::L_{t}[k] \\
&= L_{t}[1..k]
\end{align*}

  •  L_{t'}[1..(k\!-\!1)][k\!-\!1].term \neq L_{t}[k\!-\!1.term] の場合

\begin{align*}
AppendEntries(k, t, L_{t'}[1..(k\!-\!1)]) &= AppendEntries(k\!-\!1, t, L_{t'}[1..(k\!-\!1)])::L_{t}[k] \\
&= L_{t}[1..(k\!-\!1)]::L_{t}[k]\ (\because \text{帰納法の仮定}) \\
&= L_{t}[1..k]
\end{align*}

  •  k \lt length(l)+1 の場合

\begin{align*}
AppendEntries(k, t, L_{t'}[1..length(l)]) &= AppendEntries(k, t, L_{t'}[1..(length(l)\!-\!1)]) \\
&= AppendEntries(k, t, L_{t'}[1..(k\!-\!1)])\ (\because Lemma\ AppendEntries\ 1) \\
&= L_{t}[1..k]\ (\because k = length(l)+1 \rm{の場合と同様}\ Lemma\ RaftLog\ 1) \\
\end{align*}

 \square

Lemma leader 6 は Log Matching Property を証明するための最後の補題です。
log  l が RaftLog で  t = l[i].term なら  l の部分 log  l[1..i] L_{t}[1..i] と一致することを意味します。


 Lemma\ leader\ 6
\begin{equation}
\forall (i \colon Index)(t, t' \colon Term)(l \colon Log),\, RaftLog(t', l) \Rightarrow t = l[i].term \Rightarrow l[1..i] = L_{t}[1..i]
\end{equation} Proof
RaftLog に関する帰納法で示す。

  •  l = [] の場合

 [] に対する term が定義されないので trivial に成り立つものとする。

  •  l = AppendEntries(length(l), t', l') の場合

Lemma leader 5 より次が成り立つ。
\begin{align*}
l[1..i] &= AppendEntries(length(l), t', l')[1..i] \\
&= L_{t'}[1..length(l)][1..i] \ (\because Lemma\ leader\ 5) \\
&= L_{t'}[1..i]
\end{align*}
 t = l[i].term = L_{t'}[i].term が成り立つから、Lemma leader 4 より  l[1..i] = L_{t'}[1..i] = L_{t}[1..i] が成り立つ。

 \square

Log Matching Property の証明

以上の準備を元に Log Matching Property を証明します。


 Theorem\ Log\ Matching\ Property
\begin{equation}
\forall (l_{1}, l_{2}\colon Log)(t_{1},t_{2}\colon Term)(i: Index),\, RaftLog(t_{1}, l_{1}) \Rightarrow RaftLog(t_{2}, l_{2}) \Rightarrow l_{1}[i].term = l_{2}[i].term \Rightarrow l_{1}[1..i] = l_{2}[1..i]
\end{equation} Proof
 l_{1}[i].term = l_{2}[i].term = t とすると Lemma leader 6 より  l_{1}[1..i] = L_{t}[1..i] = l_{2}[1..i] が成り立つ。

 \square

参考資料

Raft のアルゴリズムは 3 章で説明されています。

  • TLA+ の標準的な教科書

ナンプレ(数独)は難しさを定義するのが難しい

はじめに

私は先日、最新技術にキャッチアップするためにレベル別ナンプレ(数独) – 無料問題集 | パズル製作研究所(以下 puzzle.dev)というナンプレのサイトを構築しました。サイトでは自動生成した大量の問題の中から毎日難易度順に 13 問をランダムに出題しています。

以前、 CalcBlocks というサイトで計算ブロック・数字ブロック・ビルディングパズルなどのナンプレよりも自動生成が難しいパズルの自動生成をしていたのでナンプレサービスも簡単に作れるだろうと思ってました。

確かに、ナンプレの問題の自動生成はすぐにできました。でも、難易度別に問題を出し分けようとした時、問題に直面しました。

ナンプレの難しさって何で決まるんだ?

サイトを作り始めた頃は初期のヒントの数が少ないほど難しいと思っていましたが、これは間違いです。私はあまりにもナンプレのことを知らなさ過ぎました。

この記事は、以前の私と同様にナンプレというパズルの存在やルール位は知っているけど、解き方のテクニックなどについては詳しく知らない人向けにナンプレの奥深さを知ってもらいたくて書きました。
まず、初心者の多くが使う仮置きという解き方テクニックについて説明します。次に、世界一難しいナンプレの問題を作ろうとして失敗した話を紹介します。最後に、私がナンプレを解くテクニックを 13 個に整理してそれを使って難易度を定義した話をします。

仮置きは最強のテクニックだけど邪道です

puzzle.dev を作る前の私はナンプレについて

電車やバスでおじさんが解いてる時間をかけさえすれば簡単に解けるパズル

程度の認識でした。時間をかけさえすれば解くことができるというのは正しいです。仮置きと呼ばれるテクニックをひたすら繰り返せば原理的には解けます。
仮置きは以下のようなテクニックです。

  1. 数字が確定できるセルに数字をすべて入れる
  2. 数字が確定していないセルに入る可能性がある数字の中から適当に数字を入れる
  3. 1 と 2 をナンプレのルールと矛盾する、もしくは答えにたどり着くまで繰り返す
  4. ナンプレのルールと矛盾したら、2 に戻って別の数字を試す

仮置きはどんなナンプレの問題もこのテクニックだけで解くことができる最強で汎用性の高いテクニックです。ナンプレを解くプログラムを作成しろと言われたらほとんどのプログラマーはこのアルゴリズムを実装しようとするのではないでしょうか?
一方で、このアルゴリズムは、矛盾にたどり着いた場合にはさかのぼって別の数字を試すという BackTrack(引き戻し)が何度も発生するので紙の上で人が実行するのはほとんど不可能です。アプリ等で補助を受けても難しいし単なる運ゲーになってしまって楽しくありません。
これらの理由からナンプレ愛好家の間では仮置きは邪道と見なされています。

世界一難しいナンプレの問題の作成に失敗

10 年ほど前、世界一難しいナンプレの問題を作ったと数学者が発表したのち、その問題がすぐに基本的なテクニックのみを用いて解かれたことがありました。当時の様子は以下の記事で伺い知ることができます。

ここは推測なのですが、おそらく仮置きのアルゴリズムをベースに難しさを定義していたのではないかと思います。しかし、すでに述べたようにナンプレ愛好家は仮置きを使いません。特定のアルゴリズムを使ってコンピューターで解くのが難しくても、人間が簡単に解けるならその問題は難しいと言えるでしょうか。

私は当初、初期のヒントの数が少なければ少ないほど難しいのではないかと考えていましたが、初期のヒントの数が少なくても基本的なテクニックのみで解ける問題はたくさんあります。初期のヒントが少ない問題を作るのはとても難しいです。でも、人間が簡単に解けるならやはり難しい問題とは言えないと思います。
ちなみに、ナンプレの問題の初期のヒントの最小個数は 17個 であることが知られています。

大切なのは人間にとっての難しさです。

ナンプレを解くための 13 個のテクニック

人間にとっての難しさを定義するためには、ナンプレ愛好家の人たちがナンプレを解く時に使用しているテクニックについて十分によく理解する必要があります。
ナンプレを解くテクニックには大きく分けて 2 つの種類があります。

  • この空白のセルにはこの数字しか入らないと決めるテクニック
  • この空白のセルにはこの数字は入らないと決めるテクニック

ほとんどのナンプレ初心者の方は空白のセルに入る数字の候補を減らしていく 2 つ目の種類のテクニックを知らないために難しい問題を解くことができないと思います。
ナンバープレース(ナンプレ、数独)の解き方テクニック集 | パズル製作研究所 では下の 13 個のテクニックについて図を使いながら詳しく解説しました。

  1. ボードの領域で独り
  2. 数字別ボードの枠で独り
  3. 残り 2 席
  4. 3 人寄ればもんじゅの知恵
  5. 候補は独り
  6. 数字別ボードの行・列で独り
  7. 隠しレーザー
  8. 隠しコレーザー
  9. 2 国同盟
  10. n 国同盟
  11. 井形レーザー
  12. XY チェイン
  13. シンプルチェイン

13 個のテクニックは、私が書籍やネットで公開されているテクニックを調べて、それぞれについてそれは一体どういうテクニックなのか、他のテクニックとどう関係しているのか、新しいテクニックはないかなどを検討して整理した結果です(名前は適当です)。
例えばテクニック4 の 3 人寄ればもんじゅの知恵は私のオリジナルのテクニックです(私が知らないだけでどこかで解説されているかもしれません)。
他にもテクニック7 の隠しレーザーはよく知られたテクニックですが、そのテクニックを少し変更したテクニック8 の隠しコレーザーを説明しているサイトはほとんどありません。
テクニック 1 から 6 がこの数字しか入らないと決めるテクニックで、テクニック 7 以降がこの数字は入らないと決めるテクニックです。

AWS 上でランダムに作成した 4000 万問のナンプレの問題を実際に 13 個のテクニックを使用して解いたところ 99.5% の問題を解くことができました。逆に言うと、0.5% の問題は解くことができませんでした。
この結果から、私が解説したテクニックの集合は完全ではないにせよ十分に強力だと考えています。

ナンプレの難しさを定義する

人間にとっての難しさを定義する準備が整いました。
puzzle.dev では 13 個のテクニックを上で紹介した順で簡単なテクニックから難しいテクニックの順に並べています。その上で、より難しいテクニックを多く使わないと解けない問題の方が難しいと定義しています。

もう少し正確に定義します。
問題を解く場合には必ず簡単なテクニックから試します。もし、使えるテクニックが見つかればそのテクニックを使って、セルに入る数字を決めるか、セルに入る数字の候補を減らします。次は、再度最初のテクニックに戻って使えるテクニックを探します。これを繰り返します。
この手順にしたがって問題を解くと、それぞれのテクニックを使った回数が得られます。例えばテクニック 1 からテクニック 13 の順に使った回数を並べると次のようになります。
\begin{align*}
[21,24,0,0,1,0,0,0,0,0,0,0,0]
\end{align*}
これはある問題を解くのに、テクニック 1 を 21 回、テクニック 2 を 24 回、テクニック 5 を 1 回使ったことを表しています。どの順でテクニックを使ったかはわかりません。
難易度を決める際には先ほどのテクニックの使用回数を逆順に並べ替えた後で辞書式順序で比較します。例えば問題を解くのに使ったテクニックの回数が以下の 2 つの問題があったとします。
\begin{align*}
\text{問題} 1: [21,24,0,0,1,0,0,0,0,0,0,0,0] \\
\text{問題} 2: [21,22,1,1,0,1,0,0,0,0,0,0,0]
\end{align*}
この二つの問題の難しさを比較するためにこの数字の並び順をそれぞれ逆順に並べ替えます。
\begin{align*}
[0,0,0,0,0,0,0,0,1,0,0,24,21] \\
[0,0,0,0,0,0,0,1,0,1,1,22,21]
\end{align*}
この二つを辞書式順序で比較します。すると、
\begin{align*}
[0,0,0,0,0,0,0,0,1,0,0,24,21] \lt [0,0,0,0,0,0,0,1,0,1,1,22,21]
\end{align*}
となるので、この順序で大きい問題 2 が問題 1 より難しい問題であると判断します。
この難易度の決め方によって 「より難しいテクニックをより多く使っている問題の方が難しい問題である」 という気持ちを順序として表現することができます。

まだ発展・改良の余地はあるか?

puzzle.dev では、ナンプレの難易度の定義をより難しいテクニックを使わないと解けない問題の方が難しいと定義しましたが、これは唯一絶対正しい難易度の定義ではありません。例えば XY チェインやシンプルチェインの長さは現状一切考慮していませんが、チェインの長さが長い方が難しい問題になると思います。より人間の感覚に合うように難しさの定義も修正していく必要があります。

自動生成した問題のうち 0.5% の問題は 13 個のテクニックを利用しても解けません。13 個のテクニックを適用できない状況を詳しく分析することで新しいテクニックを発見できる可能性があります。新しいテクニックが見つかれば、難しさの定義も変える必要があります。

私が思いもつかないようなテクニックや、難易度の定義をみなさんが思いついてくれることを楽しみにしています。

おわりに

この記事を読んでナンプレの奥深さを知って楽しんでくれる人が増えると嬉しいです。

補足: 技術的な話

補足としてナンプレの問題の自動生成に用いた技術について簡単に解説します。

サイトを支える技術

サイトの構成には以下のフレームワークやサービスを使用しました。

サーバー側は AWS 上で APIGateway + Lambda のサーバーレスで構築しています。
ナンプレの問題の自動生成も Lambda 関数の組み合わせで実現し構成は全て Terraform で管理しています。

Sat Solver を利用した問題の自動生成

ここでは初期のヒントからナンプレのルールを満たす答えがただ一つに決まる問題を正当な問題と呼びます。
問題を自動生成するにあたりナンプレを解くプログラムは次の 2 種類必要です。

  • 人間が使うテクニックを使って問題を解くプログラム
  • 初期のヒントからナンプレのルールを満たす全ての答えを探索するプログラム

1 つ目のプログラムは自動生成した問題の難易度の判定に使用します。ただし、このプログラムは初期のヒントを満たす答えが複数個ある場合に、その一つしか見つけられない可能性があります。答えが複数個存在する問題は正当なナンプレの問題とみなされないので確実に判別して取り除く必要があります。また、上で述べたように、正当な問題であっても 0.5% の問題は解けません。正当な問題を解けない場合があると、初期のヒントとナンプレのルールを満たす答えがそもそも存在しないのか、単にこのプログラムで解けないだけなのか判別できません。よって、このプログラムだけで自動生成をすることはできません。

そこで 2 つ目のプログラムを用意します。このプログラムに必要な要件は次の 2 つです。

  • 正当な問題はすべて解くことができる
  • 初期のヒントとナンプレのルールを満たす答えを全て見つけることができる

puzzle.dev ではこれらの要件を満たすプログラムの実装に Sat Solver と呼ばれるソフトウェアを使用しています。

Sat Solver の使用場所

Sat Solver 自体について説明する前に Sat Solver の使用場所を下の図に従って説明します。

SatSolverの使用場所
SatSolverの使用場所
まず 1 のナンプレのルールを満たす数字の配置を探索する際に Sat Solver を使用しています。ちなみに、ナンプレのルールを満たす数字の配置は 6,670,903,752,021,072,936,960通りあるそうです(参考: ■数独の解は何通りか?: ガスコン研究所)。
次に、ヒントとなる数字を配置が点対称になるようにピックアップします。ヒントの配置が何かしらの対称性を持っているのはナンプレ業界の暗黙の了解でヒントの配置にこだわる人もいます。
最後に、もう一度 Sat Solver を使用してヒントとナンプレのルールを満たす全ての答えを探索します。図では赤い数字の位置が異なる 2 つの答えが見つかります。これは正当な問題ではないので、再度 2 のヒントのピックアップからやり直します。答えが 1 つしかない問題が見つかれば正当な問題として採用します。

Sat Solver とは

Sat Solver は充足可能性問題を高速に解くことに特化したプログラムです。
充足可能性問題とは、変数と、否定  \lnot、論理和  \lor、論理積  \land から構成される論理式を与えらえれた時に、論理式全体を True にするような変数の True もしくは False の割り当てが存在するかどうかを問う問題です。
私が使用した Sat Solver の実装のひとつ MiniSat は論理式を連言標準形で受け取ります。連言標準形は以下のように構成されます。

  • 変数  x,またはその否定  \lnot xリテラルと呼ぶ
  • リテラルを論理和  \lor で結合した論理式をと呼ぶ
  • 節を論理積  \land で結合した論理式を連言標準形と呼ぶ

例えば、以下の論理式は連言標準形の例です。
\begin{align*}
\lnot x_{0} \land (x_{1} \lor x_{2})
\end{align*}
この論理式に対しては
\begin{align*}
[ x_{0} \mapsto \rm{False},\, x_{1} \mapsto \rm{True},\, x_{2} \mapsto \rm{True}]
\end{align*}
などが論理式を充足する割り当てです。Sat Solver はこのような変数への割り当てを高速に求めます。
Sat Solver の実装について興味がある方は以下の書籍が参考になるでしょう。

ナンプレに限定すると、Sat Solver は上で説明した仮置きを高速に非常に効率よく実行していると考えられます。

ナンプレのルールを連言標準形で表現する

いくつかの用語を説明なしに使用するので用語の説明で確認してください。

ナンプレを Sat Solver で解くためにはナンプレのルールを連言標準形で表現する必要があります。ナンプレのルールを確認しておきます。

  1. 各セルには数字が 1 つ入ります。
  2. 各行には 1 から 9 の各数字が 1 度ずつ入ります。
  3. 各列には 1 から 9 の各数字が 1 度ずつ入ります。
  4. 太い線で囲まれた各 3x3 の枠内には 1 から 9 の各数字が 1 度ずつ入ります。
  5. 正解は1つだけです。

ルール 1 を連言標準形の形に変換します。
座標が (1, 1) のセルについて考えます。このセルには 1 から 9 の数字が 1 つ入ります。そこで、このセルの数字に対応する変数として 9 つの変数を用意します。
\begin{align*}
q_{1_{(1,1)}},\, q_{2_{(1,1)}},\, q_{3_{(1,1)}},\, q_{4_{(1,1)}},\, q_{5_{(1,1)}},\, q_{6_{(1,1)}},\, q_{7_{(1,1)}},\, q_{8_{(1,1)}},\, q_{9_{(1,1)}}
\end{align*}
この 9 つの変数の中で True が割り当てられた変数に対応する数字がこのセルに入ると解釈します。例えば、以下のような割り当てを Sat Solver がした場合は、数字の 3 がセルに入ると解釈します。
\begin{align*}
[ q_{1_{(1,1)}} \mapsto \rm{False},\, q_{2_{(1,1)}} \mapsto \rm{False},\, q_{3_{(1,1)}} \mapsto \rm{True},\, q_{4_{(1,1)}} \mapsto \rm{False},\, q_{5_{(1,1)}} \mapsto \rm{False},\\
q_{6_{(1,1)}} \mapsto \rm{False},\, q_{7_{(1,1)}} \mapsto \rm{False},\, q_{8_{(1,1)}} \mapsto \rm{False},\, q_{9_{(1,1)}} \mapsto \rm{False} ]
\end{align*}
変数の割り当ての中には、9 つの変数全てに False を割り当てたり複数個の変数に True を割り当てるものも存在するので、そのような割り当てを禁止する必要があります。
9 つの変数全てに False を割り当てる場合はこのセルに入る数字が 1 つもないのでルール 1 に反します。そこで、少なくとも 1 つの変数は True になるという論理式を Sat Solver に与える連言標準形に追加します。追加する論理式は以下の論理式です。
\begin{align*}
(q_{1_{(1,1)}} \lor q_{2_{(1,1)}} \lor q_{3_{(1,1)}} \lor q_{4_{(1,1)}} \lor q_{5_{(1,1)}} \lor q_{6_{(1,1)}} \lor q_{7_{(1,1)}} \lor q_{8_{(1,1)}} \lor q_{9_{(1,1)}})
\end{align*}
9 つの変数全てに False を割り当てるとこの論理式は False になります。すると Sat Solver は連言標準形で与えられた論理式を True にできないので、少なくとも 1 つの変数に True を割り当てます。
次に複数個の変数に True を割り当てることを禁止する論理式を追加します。
まず  q_{1_{(1,1)}} q_{2_{(1,1)}} で考えます。この 2 つの変数が同時に True になることを禁止するためには、2 つの変数に True が割り当てられた時にのみ False になる論理式を連言標準形に追加します。追加する論理式は以下の論理式です。
\begin{align*}
(\lnot q_{1_{(1,1)}} \lor \lnot q_{2_{(1,1)}})
\end{align*}
 q_{1_{(1,1)}} q_{2_{(1,1)}}が同時に True になることは禁止できたので、他の  {}_9 \mathrm{C} _2 - 1 = 35 通りの組み合わせについても論理式を追加します。
以上で、上の論理式と合わせて座標が (1, 1) のセルについてルール 1 の各セルには数字が 1 つ入るという条件を表現できました。
同様に残りの 80 個のセルについても変数と論理式を追加します。

次にルール 2 について考えます。
1 行目の数字の 1 に注目します。つまり、ルール 1 の場合と同様に 1 行目にあるセルの数字 1 に対応する 9 つの変数に注目します。
\begin{align*}
q_{1_{(1,1)}},\, q_{1_{(1,2)}},\, q_{1_{(1,3)}},\, q_{1_{(1,4)}},\, q_{1_{(1,5)}},\, q_{1_{(1,6)}},\, q_{1_{(1,7)}},\, q_{1_{(1,8)}},\, q_{1_{(1,9)}}
\end{align*}
1 行目に 数字の 1 は少なくとも 1 つ入ります。また複数回出てきてはいけません。この条件はルール 1 について考えた場合と同じです。
そこで以下の論理式を追加します。
\begin{align*}
(q_{1_{(1,1)}} \lor q_{1_{(1,2)}} \lor q_{1_{(1,3)}} \lor q_{1_{(1,4)}} \lor q_{1_{(1,5)}} \lor q_{1_{(1,6)}} \lor q_{1_{(1,7)}} \lor q_{1_{(1,8)}} \lor q_{1_{(1,9)}})
\end{align*}
また、 {}_9 \mathrm{C} _2 通りの組み合わせについて以下の論理式を追加します。
\begin{align*}
(\lnot q_{1_{(1,i)}} \lor \lnot q_{1_{(1,j)}})
\end{align*}
これで 1 行目の数字の 1 について、ちょうど 1 回入るという条件を表現できました。同様に、数字 2 から 9 についても追加します。同様に 2 行目から 9 行目についても条件を追加します。
以上でルール 2 を連言標準形に追加できました。

ルール 3 とルール 4 についてもルール 2 と同様に表現できます。
この状態で Sat Solver に可能な割り当てを求めさせると先に述べた 6,670,903,752,021,072,936,960 通りの配置のうちのどれかに対応する割り当てを返します。

ナンプレの問題を Sat Solver で解く

初期のヒントがすでに入っているナンプレの問題を Sat Solver で解くための手順を下の例を使って説明します。

Sat で解く問題例
Sat で解く問題例
問題例の座標が (1, 1) のセルを見ると数字の 6 が入っています。これは変数  q_{6_{(1,1)}} に True が割り当てられている状態だと考えます。
Sat Solver に対して  q_{6_{(1,1)}} に必ず True を割り当てるように強制するためにはナンプレのルールを表現する連言標準形に変数をそのまま追加します。
\begin{align*}
(\text{ナンプレのルールを表現する論理式}) \land q_{6_{(1,1)}}
\end{align*}
 q_{6_{(1,1)}} に False を割り当てると Sat Solver は連言標準形で与えられた論理式を True にできないので、必ず q_{6_{(1,1)}}に True を割り当てます。
同様に他のヒントについても対応する座標の対応する変数を連言標準形に追加していきます。
\begin{align*}
(\text{ナンプレのルールを表現する論理式}) \land q_{6_{(1,1)}} \land q_{5_{(1,2)}} \land q_{4_{(1,7)}} \land \dots \land q_{7_{(9,9)}}
\end{align*}
この論理式を True にする割り当てを Sat Solver が見つければ、それがこの問題の答えです。

答えが 1 つしかないことを Sat Solver で確認する

上の例題に対する論理式を True にする割り当てを探索すると下の答えが見つかります。

Sat で解く問題例の答え
Sat で解く問題例の答え
現状では、この数字の配置が初期のヒントと数独のルールを満たす答えの 1 つであるということしか確認できていません。これがただ 1 つの答えであることを確認する必要があります。そのために、問題を解いた時の論理式に見つけた答えに対応する割り当てを禁止する論理式を追加して再度 Sat Solver で問題を解きます。
追加する論理式は以下のようになります。
\begin{align*}
\lnot (q_{6_{(1, 1)}} \land q_{5_{(1,2)}} \land q_{9_{(1,3)}} \land \dots \land q_{3_{(9,8)}} \land q_{7_{(9,9)}})
\end{align*}
この論理式のままでは連言標準形の論理式に追加できないのでド・モルガンの法則を用いて以下のように変形します。
\begin{align*}
(\lnot q_{6_{(1, 1)}} \lor \lnot q_{5_{(1,2)}} \lor \lnot q_{9_{(1,3)}} \lor \dots \lor \lnot q_{3_{(9,8)}} \lor \lnot q_{7_{(9,9)}})
\end{align*}
この論理式は、見つけた答えに対応する割り当てと全く同じ割り当てをした場合にのみ False になります。Sat Solver に与える論理式は以下になります。
\begin{align*}
(\text{ナンプレのルールを表現する論理式}) \land (\text{ヒントに対応する論理式}) \land \\
(\lnot q_{6_{(1, 1)}} \lor \lnot q_{5_{(1,2)}} \lor \lnot q_{9_{(1,3)}} \lor \dots \lor \lnot q_{3_{(9,8)}} \lor \lnot q_{7_{(9,9)}})
\end{align*}
Sat Solver は論理式全体を True にするために先ほど見つけた割り当てとは違う割り当てを探索します。新たな割り当てが見つかれば答えが複数個存在することになるので、その問題は正当なナンプレの問題ではありません。新たな割り当てが見つからなければ正当な問題として採用します。

連言標準形への変換

Sat Solver は連言標準形の形の論理式しか受け付けてくれないので、解きたい問題を連言標準形の論理式に変換する必要があります。そこが難しいと感じた人も多いと思いますが、私はこの変換作業こそ面白いと感じます。ここでは変換の際に使えるテクニックを紹介します。
問題によっては、論理記号のならば  \Rightarrow を使って考えた方が考えやすい場合もあります。
\begin{align*}
X \Rightarrow Y
\end{align*}
は以下の論理式と同値なので変換は簡単にできます。
\begin{align*}
\lnot X \lor Y
\end{align*}
以下の論理式はどうでしょうか。
\begin{align*}
(X_{1} \wedge Y_{1})\vee (X_{2}\wedge Y_{2})\vee \dots \vee (X_{n}\wedge Y_{n})
\end{align*}
これを分配法則を用いて連言標準形の形に変換すると  2^{n} 個の節に変換されます。Sat Solver は非常に高速なのですが、節の数が多くなるとそれだけ計算に時間がかかるようになります。
実は、上の論理式を節の数が少ない論理的同値な論理式に変換する手法としてTseitin 変換という手法が知られています。
まずは、連言標準形の形にこだわらずに問題を論理式に変換した後でこれらの手法を用いて連言標準形に変換すると変換しやすくなります。

Sat Solver の応用例

ナンプレのルールは連言標準形に変換しやすい問題です。私はCalcBlocksを作成する際に以下のパズルも Sat Solver を用いて自動生成するプログラムを作成しています。
Sat Solver に習熟したい人はぜひこれらのパズルについても自動生成 + 答えの探索に挑戦してください。抽象的な問題を論理式に変換するとてもいい練習になります。

計算ブロック

  • 各行、各列には 1 から 4 の各数字が1度ずつ入ります。
  • 数字と演算子は各領域の和(+)、大きい数と小さい数の差(-)、積(×)、大きい数を小さい数で割った商(÷)、大きい数を小さい数で割った余り(%) を表しています。
  • 正解は 1 つだけです。

計算ブロック
計算ブロック

ビルディングパズル

  • 高さが 1 から 4 のビルを上から見ています。
  • 各行、各列にはビルの高さを表す 1 から 4 の各数字が1度ずつ入ります。
  • 枠の外の数字はその方向から見えるビルの数を表しています。
  • 正解は 1 つだけです。

ビルディングパズル
ビルディングパズル

ナンバーリンク

  • 同じ数字どうしを 1 本の線でつなぎます。
  • それぞれの線は枝分かれしたり、交わったりしてはいけません。
  • それぞれのマスを通過する線は 1 本だけです。また空白のマスはありません。
  • 正解は1つだけです。

ナンバーリンク
ナンバーリンク

スリザーリンク

  • 点と点を線でつなぎ、全体で 1 つの閉じた輪をつくります。
  • 4 つの点で作られた正方形の中にある数字は、その正方形の辺に引く線の数を表しています。数字のない正方形には何本の線を引くかわかりません。
  • 線を交差させたり、枝分かれさせたりしてはいけません。
  • 正解は 1 つだけです。

スリザーリンク
スリザーリンク

対称性を用いた問題の複製

ナンプレの問題を 1 つ見つけた後で Sat Solver のように計算のコストが高い処理をせずに別のナンプレの問題を作ることは可能でしょうか?
ヒントの数字を好き勝手移動すると正解のない問題や正解が複数ある問題になる可能性があります。するともう一度 Sat Solver で確認する必要があります。一方で次の例のように、ヒントの数字全体を同時に 90 度回転した問題は、正解も 90 度回転したものになるので正当なナンプレの問題になります。

ガンマ変換
問題の 90 度回転
90 度の回転のように特定の規則に従ってヒントの数字を移動してできた問題は、再度チェックしなくても新しい問題として使えそうです。ではこのような移動にはどのようなものがいくつあるでしょうか?

わかりやすくするために 4 つの角に数字を振った正方形を考えます。この 4 つの数字を何らかの対称性に従って移動する方法には以下の方法があります。

対称変換リスト
対称変換リスト
それぞれの対称性に従った移動を次のように名付けます。

  • 点対称による移動は  \delta 変換
  • 線対称による上下移動は  \alpha 変換
  • 線対称よる右上と左下の数字の移動を  \beta 変換
  • 回転対称にる 90 度の回転移動を  \gamma 変換

図では 1 度の移動しか行なっていませんが続けて複数回の移動をする場合も考えます。この時、初めの配置から複数回の変換を行うことでたどり着くことができる数字の配置をすべて求めます。これは数学的には以下のように表現されます。

 \alpha,\beta,\gamma,\delta 変換によって生成される群の位数を求めよ

それぞれの変換の間には以下の等式が成り立ちます。変換を全く行わない場合を恒等変換と呼び  \bf{Id} で表します。
\begin{align*}
\alpha^{2} &= \bf{Id} \\
\beta^{2} &= \bf{Id} \\
\gamma^{4} &= \bf{Id} \\
\delta^{2} &= \bf{Id} \\
\gamma^{2} &= \delta \\
\alpha \beta &= \gamma \\
\beta \alpha &= \gamma^{3} \\
\alpha \gamma &= \beta \\
\gamma \alpha &= \gamma^{2} \beta = \beta \gamma^{2} \\
\beta \gamma &= \alpha \gamma^{2} = \gamma^{2} \alpha \\
\gamma \beta &= \alpha
\end{align*}

この等式を用いて全ての変換を  \alpha 変換と  \beta 変換だけで表すと以下の 8 つになります。
 \{ \bf{Id}, \alpha, \beta, \alpha \beta, \beta \alpha, \alpha \beta \alpha, \beta \alpha \beta, \alpha \beta \alpha \beta \}
それそれの変換に対応する数字の位置は以下の通りです。

変換に対応する数字の配置
変換に対応する数字の配置
結論として、1 つナンプレの問題が見つかるとその問題から追加で 7 つの問題を変換のコストだけで作成できます。
ただし、元の問題が正当なナンプレの問題であるときに、 \alpha 変換等を適用した後の問題も正当なナンプレの問題になっていることを証明しないといけません。正当なナンプレの問題が満たすべき論理式を正確に定義した上で証明をしてみてください。

大学数学の個別指導を始めます

はじめに

圏論に最短で入門する - 俺の Colimit を越えてゆけ の中で以下のように書きました。

数学にもともと興味があって数学科に進学した学生でも、大学以降で学ぶ数学についていけなくて挫折してしまう人は多いようです。私の考えでは、

  • 大学受験までの計算主体の数学から、大学以降の証明主体の数学への移行を明確に意識させること
  • 移行のためのトレーニングを積ませること

を学生が認識できる形で教育機会として大学が提供できていないことが原因なのではないかと考えています。

このブログを初めて以来、何人かの学生の方から数学の学習について相談を受けています。彼らと話をしているとどうも証明主体の数学の勉強を進める上での基礎が十分ではないように感じます。結果、数学の勉強の進め方、勉強の仕方に問題を抱えているように感じました。

私も数学の勉強を始めた当初は同じ問題を抱えていました。当時私が感じていた問題は次ようのなものです。

  • 何度も教科書を読み返して内容を記憶しようとはするのだけど、単なる暗記になってしまっていて理解した気になれない
  • 証明を読んでもその証明が本当に正しいのか自分で検証することができない
  • 練習問題を自分で解くことができないので、ほとんどの練習問題は解かずに飛ばし読みしてしまう
  • 練習問題を解いてみても、解答がないあるいは解答が一語一句自分の証明と一致していないと自分の証明が合っているのかどうか確信がもてない

大学の証明主体の数学に触れて、私と同じような問題を感じている人は多いのではないでしょうか。大学院に進みたいと思っていても、このような状態だと院試に合格できるかどうかも不安ですよね。

私もしばらくはこのような問題を感じながら勉強を続けていたのですが、あるきっかけによってこの問題を解決し、その後圏論を理解できる程度にまで数学を独学することができるようになりました。Steve Awodey の Category Theory を読む - 俺の Colimit を越えてゆけ を見ていただければ、教科書やネットの他のサイトには載っていない詳細な証明がなされているのが確認できると思います。それらの証明は私が自分で考えて構成したものであり、その正しさについても 100% 確信して書いています。みなさんにも私と同程度の能力を身につけてもらいたいと思っています。

そこで、昔の私と同じ問題を抱えている人に私の経験を伝えるために数学の個別指導を始めようと思います。一人でも多くの数学徒が数学の学習に関しての不安を解消し、数学を楽しめるようになることの一助になれれば幸いです。個別指導を始めようと思った一番の理由は、いよいよ私の貯金残高がやばくなってきたからです

個別指導を受けた結果あなたが得られるもの

突然ですが問題です。

ここに白いボールだけが入った袋があります。この袋から任意に一つボールを取り出した時、そのボールが白いことを証明しなさい。

問題を読んで何をしたらいいのかわからなかった人、あるいは、わかった風を装おうとして「定義より明らかだろjk」と思った人は私の個別指導を受けると学ぶところがあると思います。

大学数学の教科書では、定義や定理は上の問題のように自然言語で記述されています。数学の学習を進める際には、自然言語で書かれた定義や定理を論理式として表現し、許された手順のみを用いて具体的に証明を構成する必要があります。上の問題を読んで何をすればいいのかわからなかった人、「定義より明らかだろ」で済まそうとした人は数学書を読んでいる時にも、この必要な手順をこなさずにあたかも小説を読むかのように数学書を読んでいる可能性があります。

私の個別指導では、自然言語で書かれた定義や定理を論理式として表現し、許された手順のみを用いて具体的に証明を構成する能力を身につけるための指導をします。能力が身につけば、上の問題も実際に証明することができるようになります。

内容

はじめに基礎的な講義を行います。その後に、松坂の集合・位相入門もしくは代数系入門を用いて、定義、定理の証明、練習問題などを一つずつ証明しながら読み進めます。
書籍を通読することが目的ではなく、読むことを通して上の能力を身につけることが目的です。週 1 回、2–3 時間の講義で 6 ヶ月程度講義を受けてもらえば、上の能力は身につくと思います。

集合・位相入門

集合・位相入門

代数系入門

代数系入門

受講するかどうか悩んでいる人へ

ここまで読んでみて受講してみたいなと思っていても、値段も決して安くないし、本当に自分が求めている内容を教えてもらえるのだろうか?

と考えられていると思います。そこで、はじめの 1 日 2 時間分を体験授業ということで無料で受講可能にします。体験授業を受けてみて、続けて見ようかなと思った場合のみ引き続き受講していただきます。やっぱりやめておこうと思えば、お代をいただくことはありません。

ぜひお気軽に体験授業を受けてみてください。

詳細

対象

大学数学を先取りしたい高校生・大学生・社会人

場所

基本は京都市内の図書館やカフェ、セミナールームの予定です。
もし関東方面の方の希望が多ければ、曜日を限定して東京に私が行きます。関東方面の方で希望の方は、希望だけでもお伝えいただけると嬉しいです。

時給

7500 円/h 1 回 2 時間以上
複数人同時受講の場合は割引します

期間

週 1 回の場合は 6 ヶ月
週 2 回の場合は 3 ヶ月
計 50 時間程度

人数

複数人(1–3 人)の同時受講も可

連絡先

メールアドレス: takuya.0101 at gmail.com

補足

私は数学の研究者や数学科卒ではありません。私の最終学歴は東京大学情報理工学系研究科創造情報学専攻修士で、コンピュータ系の人です。
コンピュータ科学の研究に必要性を感じて数学の勉強を 30 歳を超えてから開始し、大学数学の学習時間は 5000 時間程度だと思います。よって、数学の特定の分野に関する専門知識を要求されても困ります。あくまでも、初心者よりは少しだけ数学の素養があるおじさんだと考えてください。

Steve Awodey の Category Theory を読む : Chapter 10

Steve Awodey の Category Theory を読む シリーズトップ

10.2 Monads and adjoints

Example 10.5

Exercise 6 と同様の表記を採用すると、任意の  f \colon X \to Y と任意の  U \in \mathcal{P}(X) に対して  \mathcal{P}(f)(U) = \left\{ f(x) \in Y \,\middle|\, x \in U \right\} と表せる。また任意の  \alpha \in \mathcal{PP}(X) に対して  \bigcup(\alpha) = \left\{ x \in X \,\middle|\, \exists U \in \alpha,\, x \in U \right\} と表せることに注意して以下を証明する。

 Lemma
\begin{align*}
(\mathcal{P}, \{-\}, \bigcup) \text{ is a monad on } {\bf{Sets}}.
\end{align*}

 Proof.

  •  \eta \colon 1 \to \mathcal{P} が natural であること

任意の  f \colon X \to Y に対して以下の diagram を考える。
f:id:hitotakuchan:20161102131405p:plain

すると、任意の  x \in X に対して  \left( \mathcal{P}(f) \circ \eta_{X} \right)(x) = \left\{ f(x) \right\} = \left( \eta_{Y} \circ f \right)(x) が成り立つ。よって diagram は可換になる。

  •  \mu \colon \mathcal{PP} \to \mathcal{P} が natural であること

任意の  f \colon X \to Y に対して以下の diagram を考える。
f:id:hitotakuchan:20161102132128p:plain

任意の  \alpha \in \mathcal{PP}(X) に対して

\begin{align*}
\left( \mathcal{P}(f) \circ \mu_{X} \right)(\alpha) &= \mathcal{P}(f) \left( \left\{ x \in X \,\middle|\, \exists U \in \alpha,\, x \in U \right\} \right) \\
&= \left\{ f(x) \in Y \,\middle|\, \exists U \in \alpha,\, x \in U \right\}
\end{align*}

が成り立つ。一方、

\begin{align*}
\left( \mu_{Y} \circ \mathcal{PP}(f) \right)(\alpha) &= \mu_{Y} \left( \left\{ \mathcal{P}(f)(U) \,\middle|\, U \in \alpha \right\} \right) \\
&= \left\{ y \in Y \,\middle|\, \exists U' \in \left\{ \mathcal{P}(f)(U) \,\middle|\, U \in \alpha \right\},\, y \in U' \right\} \\
&= \left\{ y \in Y \,\middle|\, \exists U \in \alpha,\, y \in \mathcal{P}(f)(U) \right\} \\
&= \left\{ y \in Y \,\middle|\, \exists U \in \alpha,\, y \in \left\{ f(x) \in Y \,\middle|\, x \in U \right\} \right\} \\
&= \left\{ f(x) \in Y \,\middle|\, \exists U \in \alpha,\, x \in U \right\}
\end{align*}

が成り立つ。よって diagram は可換になる。

  • 結合則を満たすこと

任意の  X \in {\bf{Sets}} に対して以下の diagram が可換になることを示せばよい。
f:id:hitotakuchan:20161103072530p:plain

任意の  \beta \in \mathcal{PPP}(X) に対して

\begin{align*}
\left( \mu_{X} \circ \mathcal{P}\mu_{X} \right)(\beta) &= \mu_{X} \left( \left\{ \mu_{X}(\alpha) \,\middle|\, \alpha \in \beta \right\} \right) \\
&= \left\{ x \in X \,\middle|\, \exists U \in \left\{ \mu_{X}(\alpha) \,\middle|\, \alpha \in \beta \right\},\, x \in U \right\} \\
&= \left\{ x \in X \,\middle|\, \exists \alpha \in \beta,\, x \in \mu_{X}(\alpha) \right\} \\
&= \left\{ x \in X \,\middle|\, \exists \alpha \in \beta,\, U \in \alpha,\, x \in U \right\}
\end{align*}

が成り立つ。一方、

\begin{align*}
\left( \mu_{X} \circ \mu_{\mathcal{P}X} \right)(\beta) &= \mu_{X} \left( \left\{ U \in \mathcal{P}(X) \,\middle|\, \exists \alpha \in \beta,\, U \in \alpha \right\} \right) \\
&= \left\{ x \in X \,\middle|\, \exists U' \in \left\{ U \in \mathcal{P}(X) \,\middle|\, \exists \alpha \in \beta,\, U \in \alpha \right\},\, x \in U' \right\} \\
&= \left\{ x \in X \,\middle|\, \exists \alpha \in \beta,\, U \in \alpha,\, x \in U \right\}
\end{align*}

が成り立つので diagram は可換になる。

  • 単位則を満たすこと

任意の  X \in {\bf{Sets}} に対して以下の diagram が可換になることを示せばよい。
f:id:hitotakuchan:20161103074643p:plain

任意の  U \in \mathcal{P}(X) に対して左の triangle に関して

\begin{align*}
\left( \mu_{X} \circ \eta_{\mathcal{P}X} \right)(U) &= \mu_{X} \left( \left\{ U \right\} \right) \\
&= \left\{ x \in X \,\middle|\, \exists U' \in \left\{ U \right\},\, x \in U' \right\} \\
&= U
\end{align*}

が成り立つ。次に右の triangle に関して

\begin{align*}
\left( \mu_{X} \circ \mathcal{P}\mu_{X} \right)(U) &= \mu_{X} \left( \left\{ \left\{ x \right\} \,\middle|\, x \in U \right\} \right) \\
&= \left\{ x' \in X \,\middle|\, \exists U' \in \left\{ \left\{ x \right\} \,\middle|\, x \in U \right\},\, x' \in U' \right\} \\
&= \left\{ x \in X \,\middle|\, x \in U \right\} \\
&= U
\end{align*}

が成り立つので diagram は可換になる。

 \square

10.3 Algebras for a monad

Example 10.7

free monoid adjunction に対する monad を  (T, \eta, \mu) とすると、 {\bf{Mon}} \cong {\bf{Sets}}^{T} が成り立つことを示します。

 Lemma
 {\bf{Mon}} \cong {\bf{Sets}}^{T}

 Proof.
はじめに  \Phi \colon {\bf{Mon}} \to {\bf{Sets}}^{T} を定義する。
任意の monoid  (M, u_{M}, \cdot_{M}) に対して  \Phi\left( (M, u_{M}, \cdot_{M}) \right) = (M, \alpha) と定義する。ただし  \alpha \alpha( [ m_{1}, \dots , m_{n}] ) = m_1 \cdot_{M} \dots \cdot_{M} m_{n} を満たす関数とする。このとき書籍にあるように  (M, \alpha) T-algebra となる。
また任意の monoid homomorphism  h \colon (M, u_{M}, \cdot_{M}) \to (N, u_{N}, \cdot_{N}) に対して以下の diagram を考える。
f:id:hitotakuchan:20161106133829p:plain

任意の  [m_{1}, \dots, m_{n}] \in TM に対して  (\beta \circ Th)( [m_{1}, \dots, m_{n}] ) = h(m_{1}) \cdot_{N} \dots \cdot_{N} h(m_{n}) が成り立つ。一方、 (h \circ \alpha)([m_{1}, \dots, m_{n}]) = h(m_{1} \cdot_{M} \dots \cdot_{M} m_{n}) が成り立つが  h が monoid homomorphism であることから両者は等しい。
そこで  \Phi(h) = h \colon (M, \alpha) \to (N, \beta) で定義する。すると  \Phi が functor の条件を満たすことは明らかである。

次に  \Psi \colon {\bf{Sets}}^{T} \to {\bf{Mon}} を定義する。
任意の  (A, \alpha) に対して  u_{A} = \alpha([]) \cdot_{A} = \alpha([-,-]) とするとき、 \Psi\left( (A, \alpha) \right) = (A, u_{A}, \cdot_{A}) で定義する。このとき  (A, u_{A}, \cdot_{A}) が monoid となることを示す。
任意の  a,b,c \in A に対して
 \begin{align*}
a \cdot_{A} (b \cdot_{A} c) &= \alpha \left(  \left[ a, \alpha( [b, c] ) \right] \right) \\
&= \alpha \left( \left[ \alpha([a]), \alpha( [ b, c ] ) \right] \right) \\
&= ( \alpha \circ T\alpha) \left( \left[ [ a ], [b, c] \right] \right) \\
&= (\alpha \circ \mu) \left( \left[ [ a ], [b, c] \right] \right) \\
&= \alpha \left( [ a, b, c ] \right)
\end{align*}

一方、

 \begin{align*}
(a \cdot_{A} b) \cdot_{A} c &= \alpha \left( \left[ \alpha( [a, b]), c \right] \right) \\
&= \alpha \left( \left[ \alpha( [a, b]), \alpha([c]) \right] \right) \\
&= (\alpha \circ T\alpha) \left( \left[ [a, b], [c] \right] \right) \\
&= (\alpha \circ \mu) \left( \left[ [a, b], [c] \right] \right) \\
&= \alpha \left([a, b, c] \right)
\end{align*}

が成り立つので、 \cdot_{A} は結合則を満たす。また

 \begin{align*}
u_{A} \cdot_{A} a &= \alpha \left( \left[ \alpha([]), a \right] \right) \\
&= \alpha \left( \left[ \alpha([ ]), \alpha([a]) \right] \right) \\
&= (\alpha \circ T\alpha) \left( \left[ [ ], [a] \right] \right) \\
&= (\alpha \circ \mu) \left( \left[ [ ], [a] \right] \right) \\
&= \alpha ([a]) \\
&= a
\end{align*}

が成り立つ。同様に  a \cdot_{A} u_{A} = a が成り立つので  \cdot_{A} は 単位則を満たす。以上より  (A, u_{A}, \cdot_{A}) は monoid となる。
また任意の  h \colon (A, \alpha) \to (B, \beta) と任意の  a, b \in A に対して、

 \begin{align*}
h(a \cdot_{A} b) &= h \left( \alpha([ a,b]) \right) \\
&= (h \circ \alpha)([a, b]) \\
&= (\beta \circ Th)([a,b]) \\
&= h(a) \cdot_{B} h(b)
\end{align*}

が成り立ち、同様に  h(u_{A}) = u_{B} が成り立つので、 h は monoid homomorphism となる。そこで  \Psi(h) = h \colon (A, u_{A}, \cdot_{A}) \to (B, u_{B}, \cdot_{B}) とすれば  \Psi は明らかに functor の条件を満たす。

最後に、 \Psi \circ \Phi = 1_{\bf{Mon}} かつ  \Phi \circ \Psi = 1_{{\bf{Sets}}^{T}} が成り立つので  {\bf{Mon}} \cong {\bf{Sets}}^{T} が成り立つ。

 \square

10.4 Comonads and coalgebras

任意のadjoint pair  F \dashv U に対して unit を  \eta \colon 1_{\bf{C}} \to UF、counit を  \epsilon \colon FU \to 1_{\bf{D}} とするとき、 (G = FU, \epsilon, \delta = F\eta_{U}) が comonad となることを確認します。

 Lemma
 (G, \epsilon, \delta) \text{ is a comonad}.

 Proof.
10.2 節と同様に証明する。

  • coassociativity law が成り立つこと

任意の  f \colon X \to Y \in {\bf{C}} に対して  \eta が natural であることより、以下の diagram が可換になる。
f:id:hitotakuchan:20161107125109p:plain

 Y UFX f \eta_{X} で置き換えると、以下の diagram を得る。
f:id:hitotakuchan:20161107125424p:plain

 X UD として、全体に  F を適用すると以下の diagram を得る。
f:id:hitotakuchan:20161107125820p:plain

記号を置き換えると以下の diagram が可換となる。
f:id:hitotakuchan:20161107130311p:plain

  • counit law が成り立つこと

次の diagram が可換になることを示せばよいが、これは triangle identities より明らかである。
f:id:hitotakuchan:20161107131043p:plain

 \square

10.5 Algebras for endofunctors

Lemma 10.10

任意の endofunctor  P \colon \mathcal{S} \to \mathcal{S} に関して次の事柄が成り立つことを証明します。

 Lemma
 i \colon P(I) \to I \text{ is an initial } P\text{-algebra} \Rightarrow i \text{ is an isomorphism}.

 Proof.
 i が initial  P-algebra であることより、次の diagram が可換となるような  j \colon I \to P(I) がただ一つ存在する。
f:id:hitotakuchan:20161108142551p:plain

そこで以下の diagram を考える。
f:id:hitotakuchan:20161108142956p:plain

明らかに diagram は可換になるので、 i が initial であることより  i \circ j = 1_{I} が成り立つ。
そこでもう一度以下の diagram を考えると
f:id:hitotakuchan:20161108142551p:plain

 j \circ i = P(i) \circ P(j) = P(1_{I}) = 1_{P(I)} が成り立つ。よって  i は isomorphism である。

 \square

Corollary 10.13

任意の finite polynomial functor  P \colon {\bf{Sets}} \to {\bf{Sets}} \omega-colimit を保存することを証明します。

 Lemma
 P \text{ preserves } \omega \text{-colimits}.

 Proof.
index category  \omega に対しては
 \varinjlim_{n} \dashv \Delta_{n} \dashv \varprojlim_{n}

が成り立つこと、また、任意の集合  J に対しては

 \sum_{J} \dashv \Delta_{J} \dashv \prod_{J}

が成り立つことに注意する。
polynomial functor  P P(X) = \sum_{i \in I} C_{i} \times X^{B_{i}} で表すと、任意の  D \colon \omega \to \bf{Sets} に対して、証明するべきことは  P \left( \varinjlim_{n} D_{n} \right) = \sum_{I} C_{i} \times \left( \varinjlim_{n} D_{n} \right)^{B_{i}} \cong \varinjlim_{n} \left( \sum_{I} C_{i} \times D_{n}^{B_{i}} \right) = \varinjlim_{n} P(D_{n}) である。
任意の  X \in \bf{Sets} に対して
\begin{align*}
\text{Hom}\left( \sum_{I} C_{i} \times \left( \varinjlim_{n} D_{n} \right)^{B_{i}}, X \right) &\cong \text{Hom} \left( C_{i} \times \left(\varinjlim_{n} D_{n} \right)^{B_{i}}, \Delta_{I} X \right) \\
&\cong \text{Hom} \left( \left(\varinjlim_{n} D_{n} \right)^{B_{i}}, \Delta_{I} X^{C_{i}} \right) \\
&\cong \text{Hom} \left( \varinjlim_{n} D_{n}^{B_{i}}, \Delta_{I} X^{C_{i}} \right) \\
&\cong \varprojlim_{n} \text{Hom} \left( D_{n}^{B_{i}}, \Delta_{I} X^{C_{i}} \right) \\
&\cong \varprojlim_{n} \text{Hom} \left( C_{i} \times D_{n}^{B_{i}}, \Delta_{I} X \right) \\
&\cong \varprojlim_{n} \text{Hom} \left( \sum_{I} C_{i} \times D_{n}^{B_{i}}, X \right) \\
&\cong \text{Hom} \left( \varinjlim_{n} \left( \sum_{I} C_{i} \times D_{n}^{B_{i}} \right), X \right) \\
\end{align*}

が成り立つ。これらの同型射は adjoint pair の同型射であるから Chapter8 で証明した内容と合わせると  X に関して natural である。
よって米田の補題より  \sum_{I} C_{i} \times \left( \varinjlim_{n} D_{n} \right)^{B_{i}} \cong \varinjlim_{n} \left( \sum_{I} C_{i} \times D_{n}^{B_{i}} \right) が成り立つ。

 \square

参考書籍

Category Theory (Oxford Logic Guides)

Category Theory (Oxford Logic Guides)

  • 作者:Awodey, Steve
  • 発売日: 2008/01/10
  • メディア: ペーパーバック
圏論 原著第2版

圏論 原著第2版

Steve Awodey の Category Theory を読む : Chapter 9

Steve Awodey の Category Theory を読む シリーズトップ

9.1 Preliminary definition

Example 9.3

 F \colon {\bf{Pos}} \to \mathcal{C}{\bf{Pos}} F_{0}(P) = \left\{ U \subseteq P \ \middle| \ p' \leq p \in U \text{ implies } p' \in U \right\} で定義した時、 F が forgetful functor  U の left adjoint となることを証明します。はじめに  F_{0} の定義が well-defined であることを証明します。

 Lemma
 F_{0} \text{ is well-defined}.

 Proof.
任意の  P \in {\bf{Pos}} に対して  F_{0}(P) が cocomplete poset となることを示せばよい。 F_{0}(P) \subseteq を順序として入れると poset になることは明らかであるから、  F_{0}(P) が cocomplete になることを示す。
任意の index set  I に対して  \bigcup_{i \in I} U_{i} \in F_{0}(P) となることを示せばよい。任意の  a \in \bigcup_{i \in I} U_{i} と任意の  a' \leq a に対して  a \in \bigcup_{i \in I} U_{i} より  \exists i \in I,\ a \in U_{i} が成り立つ。 U_{i} \in F_{0}(P) であるから、 F_{0}(P) の定義より  a' \in U_{i} が成り立つ。よって  a' \in \bigcup_{i \in I} U_{i} が成り立つので  \bigcup_{i \in I} U_{i} \in F_{0}(P) が成り立つ。

 \square

次に、任意の  f \colon P \to Q \in {\bf{Pos}} に対して  F_{1}(f) を定義する必要があります。その前に、任意の  p \in P に対して  p\!\downarrow p\!\downarrow \,= \left\{ p' \in P \ \middle|\ p' \leq p \right\} と定義するとき、次のことが成り立つことを証明します。

 Lemma
 U \in F_{0}(P) \Rightarrow U = \bigcup_{p \in U} p\!\downarrow

 Proof.
任意の  a \in U に対して  a \in a\!\downarrow であるから  a \in \bigcup_{p \in U} p\!\downarrow が成り立つ。
逆に  a \in \bigcup_{p \in U} p\!\downarrow とすると  \exists p,\ a \in p\!\downarrow が成り立つので  a \leq p が成り立つ。すると  U \in F_{0}(P) であることから  a \in U が成り立つ。

 \square

上の事実をもとに、任意の  f \colon P \to Q \in {\bf{Pos}} と任意の  U \in F_{0}(P) に対して  F_{1}(f) F_{1}(f)(U) = F_{1}(f)\left( \bigcup_{p \in U} p\!\downarrow \right) = \bigcup_{p \in U} f(p)\!\downarrow で定義します。このとき  F_{1} が well-defined であることを証明します。

 Lemma
 F_{1} \text{ is well-defined}.

 Proof.
任意の  f \colon P \to Q と任意の  U \in F_{0}(P) に対して  F_{1}(f)(U) = \bigcup_{p \in U} f(p)\!\downarrow \in F_{0}(Q) となることを示せばよい。
任意の  q \in \bigcup_{p \in U} f(p)\!\downarrow と任意の  q' \leq q に対して、 \exists p \in U,\ q \in f(p)\!\downarrow が成り立つから、 q' \leq q なら  q' \in f(p)\!\downarrow となり  q' \in \bigcup_{p \in U} f(p)\!\downarrow が成り立つ。よって  \bigcup_{p \in U} f(p)\!\downarrow \in F_{0}(Q) である。

 \square

このとき、証明は省略しますが  F \colon {\bf{Pos}} \to \mathcal{C}{\bf{Pos}} は functor の条件 (a), (b), (c) を満たすので functor となります。

次に  F が forgetful functor  U の left adjoint となることを証明します。はじめに、任意の  f \colon P \to U(\mathcal{C}) に対して  \overline{f} \colon F(P) \to \mathcal{C} を任意の  U \in F(P) に対して  \overline{f}(U) = \bigvee_{p \in U} f(p) で定義します。このとき  \overline{f} が monotone かつ cocontinuous であることを証明します。

 Lemma
 \overline{f} \text{ is monotone and cocontinuous}.

 Proof.

  • monotone であること

任意の  U' \subseteq U に対して  \bigvee_{p' \in U'} f(p') \leq \bigvee_{p \in U} f(p) を示せばよい。任意の  p' \in U' に対して  p' \in U であるから、 f(p') \leq \bigvee_{p \in U} f(p) が成り立つので colimit の UMP より  \bigvee_{p' \in U'} f(p') \leq \bigvee_{p \in U} f(p) が成り立つ。

  • cocontinuous であること

任意の index set  I に対して  \overline{f}\left( \bigcup_{i \in I} U_{i} \right) = \bigvee_{i \in I} \overline{f}(U_{i}) が成り立つことを示せばよい。定義よりこれは  \bigvee_{a \in \bigcup_{i \in I} U_{i}} f(a) = \bigvee_{i \in I} \bigvee_{a \in U_{i}} f(a) と同値である。
任意の  a \in \bigcup_{i \in I} U_{i} に対して  f(a) \leq \bigvee_{i \in I} \bigvee_{a \in U_{i}} f(a) が成り立つので、colimit の UMP より  \bigvee_{a \in \bigcup_{i \in I} U_{i}} f(a) \leq \bigvee_{i \in I} \bigvee_{a \in U_{i}} f(a) が成り立つ。
一方、任意の  i \in I と任意の  a \in U_{i} に対して  f(a) \leq \bigvee_{a \in \bigcup_{i \in I} U_{i}} f(a) が成り立つので、colimit の UMP より  \bigvee_{i \in I} \bigvee_{a \in U_{i}} f(a) \leq \bigvee_{a \in \bigcup_{i \in I} U_{i}} f(a) が成り立つ。

 \square

次に  \eta \colon 1_{\bf{Pos}} \to U \circ F \eta_{P}(p) = p\!\downarrow で定義します。このとき  \eta が natural transformation になることを証明します。

 Lemma
 \eta \text{ is a natural transformation}.

 Proof.
任意の  f \colon P \to Q に対して以下の diagram が可換になることを示せばよい。
f:id:hitotakuchan:20160902093405p:plain
これは任意の  p \in P に対して  f(p)\!\downarrow\, = \bigcup_{p' \in p\downarrow} f(p')\!\downarrow が成り立つことと同値である。

  • only if case

 q \in f(p)\!\downarrow とすると、 q \leq f(p) が成り立つ。すると  p \in p\!\downarrow であるから  q \in \bigcup_{p' \in p\downarrow} f(p)\!\downarrow となる。

  • if case

 q \in \bigcup_{p \in p\downarrow} f(p)\!\downarrow とすると、ある  p' \in p\!\downarrow が存在して  q \in f(p')\!\downarrow が成り立つ。  f は monotone であるから  q \leq f(p') \leq f(p) が成り立つので、 q \in f(p)\!\downarrow が成り立つ。

 \square

 Lemma
 U(\overline{f}) \circ \eta_{P} = f

 Proof.
任意の  p \in P に対して  \bigvee_{p' \in p\downarrow} f(p') = f(p) となることを示せばよい。
 p \in p\!\downarrow より  f(p) \leq \bigvee_{p' \in p\downarrow} f(p') となることは明らかである。逆に、任意の  p' \in p\!\downarrow とすると  p' \leq p であり、 f が monotone であるから  f(p') \leq f(p) が成り立つ。よって colimit の UMP より  \bigvee_{p' \in p\!\downarrow} f(p') \leq f(p) が成り立つ。

 \square

最後に  \overline{f} の唯一性について証明する。

 Lemma
 \forall g \colon F(P) \to \mathcal{C},\ U(g) \circ \eta_{P} = f \Rightarrow g = \overline{f}

 Proof.
任意の  U \in F(P) に対して  U = \bigcup_{p \in U} p\!\downarrow が成り立つことと  g が cocontinuous であることに注意すると、
\begin{align*}
g(U) &= g\left( \bigcup_{p \in U} p\!\downarrow \right) \\
&= \bigvee_{p \in U} g(p\!\downarrow) \\
&= \bigvee_{p \in U} f(p) \\
&= \overline{f}(U)
\end{align*}
が成り立つ。

 \square

9.2 Hom-set definition

 \eta_{C} = \phi(1_{FC}) で定義された  \eta \colon 1_{\bf{C}} \to U \circ F が natural transformation であることを証明します。

 Lemma
 \eta \text{ is a natural transformation}.

 Proof.
任意の  h \colon C' \to C に対して以下の diagram が可換になることを示せばよい。
f:id:hitotakuchan:20160905110844p:plain
 \phi が natural であることから以下の diagram が可換になることに注意すると、
f:id:hitotakuchan:20160905112152p:plain
\begin{align*}
UF(h) \circ \eta_{C'} &= UF(h) \circ \phi_{C', FC'}(1_{FC'}) \\
&= \left( UF(h)_{\ast} \circ \phi_{C', FC'} \right)(1_{FC'}) \\
&= \left( \phi_{C', FC} \circ F(h)_{\ast} \right)(1_{FC'}) \\
&= \phi_{C', FC}\left( F(h) \right) \\
&= \phi_{C', FC} \left( 1_{FC} \circ F(h) \right) \\
&= \left( \phi_{C', FC} \circ F(h)^{\ast} \right)(1_{FC}) \\
&= \left( h^{\ast} \circ \phi_{C, FC} \right)(1_{FC}) \\
&= \phi_{C, FC}(1_{FC}) \circ h \\
&= \eta_{C} \circ h
\end{align*}
が成り立つ。

 \square

9.4 Order adjoints

この節で出てくる例は、adjoint functor の domain も codomain も Preorder set を圏と見なしたものなので、任意の対象間には高々一つの写像しか存在しません。
よって同型射が natural になることは自明に成り立つのでその証明は省略されています。

Example 9.12

こちらの記事でも言及したのですが、ここの記述は正確ではありません。ただし位相空間に詳しくない方は飛ばして構いません。

書籍にあるように dual image function を  f_{\ast}(U) = \left\{ b \in B \,\middle|\, f^{-1}(b) \subseteq U \right\} と定義した場合、 f_{\ast} \colon \mathcal{P}(A) \to \mathcal{P}(B) は確かに  f^{-1} の right adjoint になります。これは、 f^{-1}(V) \subseteq U \Rightarrow V \subseteq f_{\ast}(U) かつ  V \subseteq f_{\ast}(U) \Rightarrow f^{-1}(V) \subseteq U が成り立つことを確認すればいいです。

問題はその次で、 f^{-1} を開集合に制限して  f^{-1} \colon \mathcal{O}(B) \to \mathcal{O}(A) とした場合にも  f_{\ast} f^{-1} の right adjoint になるという記述です。というのも  U を任意の  A の開集合とした時に  f_{\ast}(U) は必ずしも  B の開集合とはならないからです。よって  f_{\ast} f^{-1} の right adjoint にはなり得ません。

そこで  {\it{Sheaves\ in\ Geometry\ and\ Logic}} という書籍を参照すると、そこでは dual image function を以下のように定義しています。
 f_{\ast}(U) = \bigcup \left\{ V \in \mathcal{O}(B) \,\middle|\, f^{-1}(V) \subseteq U \right\}
この定義を用いると、任意の  A の開集合  U に対して  f_{\ast}(U) B の開集合になり  f^{-1} の right adjoint になることが証明できます。一方で開集合に制限しない  f^{-1}
\colon \mathcal{P}(B) \to \mathcal{P}(A) に対しては right adjoint になりません。

以上の二つの定義とその結果が、ここの記述ではごちゃ混ぜになっています。上で述べたことを是非自分で確認してみてください。

9.5 Quantifiers as adjoints

Figure 9.1 の説明がわかりにくいかもしれないので補足しておきます。ちなみに Figure 9.1 にある  \phi \psi の誤りです。
Figure 9.1 の左下を原点として、水平方向を  x 軸、垂直方向を  y 軸とします。また  x 上の任意の領域  R に対して  \pi^{-1}(R) によって生成される長方形をそのまま  \pi^{-1}(R) と書くことにします。さらに斜線で塗られた領域を、領域  \psi と呼ぶことにします。

 \frac{\exists y. \psi(x,y) \dashv \phi(x)}{\psi(x,y) \dashv \phi(x)}

  • 上から下に読む場合

 \phi(x) を満たす  x 軸上の領域  R \exists y. \psi(x,y) を満たす  x 軸上の領域、つまり Figure 9.1 の  \exists \psi と書かれた領域を含むのであれば、 \pi^{-1}(R) は領域  \psi を含むと読みます。

  • 下から上に読む場合

 \psi(x) を満たす  x 軸上の領域  R に対して  \pi^{-1}(R) が領域  \psi を含むのであれば、 R \exists \psi を含むと読みます。

同様に
 \frac{\phi(x) \dashv \psi(x,y)}{\phi(x) \dashv \forall y. \psi(x,y)}

  • 上から下に読む場合

 \phi(x) を満たす  x 軸上の領域  R に対して  \pi^{-1}(R) が領域  \psi に含まれるならば、 R \forall \psi に含まれると読みます。

  • 下から上に読む場合

 \phi(x) を満たす  x 軸上の領域  R \forall \psi に含まれるのであれば、 \pi^{-1}(R) は領域  \psi に含まれると読みます。

9.6 RAPL

Proposition 9.16

ここでは  {F_{!}}_{1} の定義と  F_{!} が functor になることの証明、 {F^{\ast}}_{1} の定義と  F^{\ast} が functor になることの証明が省略されています。
さらに natural isomorphism であることを示すところで、isomorphism であることは示されていますが、natural であることの証明が省略されています。 E に関して natural になることは Chapter 8 で確認しましたが  P に関して natural になることは確認していないので、ここで確認しておきます。

 Lemma
 F_{!} \text{ is a functor}.

 Proof.

  •  {F_{!}}_{1} の定義

任意の natural transformation  \theta \colon P \to Q に対して次の diagram を考える。
f:id:hitotakuchan:20160915131833p:plain
ここで任意の  h \colon (x', C') \to (x, C) \in \int\!P に対して  \phi_{P} \circ i_{h} = i_{(x', C')} \psi_{P} \circ i_{h} = i_{(x, C)} \circ F(h) である。
 i_{\left( \theta_{C}(x), C \right)} F \circ \pi(x,C) \overset{1_{FC}}{\to} F \circ \pi \left( \theta_{C}(x), C \right) \overset{i_{\left( \theta_{C}(x), C \right)}}{\to} \coprod_{\int\!Q} F \circ \pi(z,C) の合成である。
また  \theta が natural であるから  \left( Q(h) \circ \theta_{C} \right)(x) = \left( \theta_{C'} \circ P(h) \right)(x) = \theta_{C'}(x') が成り立つことから  h h \colon \left( \theta_{C'}(x'), C' \right) \to \left( \theta_{C}(x), C \right) \in \int\!Q となることに注意する。すると
\begin{align*}
c_{Q} \circ \left[ i_{\left( \theta_{C}(x), C \right)} \right] \circ \phi_{P} \circ i_{h} &= c_{Q} \circ i_{\left( \theta_{C'}(x'), C' \right)} \\
&= c_{Q} \circ \phi_{Q} \circ i_{h} \\
&= c_{Q} \circ \psi_{Q} \circ i_{h} \\
&= c_{Q} \circ i_{\left( \theta_{C}(x), C \right)} \circ F(h) \\
&= c_{Q} \circ \left[ i_{\left( \theta_{C}(x), C \right)} \right] \circ \psi_{P} \circ i_{h}
\end{align*}
が成り立つ。よって coproduct の UMP と colimit の UMP より diagram を可換にする写像  {F_{!}}_{1}(\theta) \colon \varinjlim_{\int\!P} F \circ \pi(x,C) \to \varinjlim_{\int\!Q} F \circ \pi(z, C) がただ一つ存在する。これを  {F_{!}}_{1}(\theta) と定義する。

  •  F_{!} が functor であること

 {F_{!}}_{1}(\theta \colon P \to Q) \colon {F_{!}}_{0}(P) \to {F_{!}}_{0}(Q) となるから  F_{!} は functor の条件 (a) を満たす。
 {F_{!}}_{1}(1_{P}) は上の diagram の  \theta 1_{P} で置き換えると、colimit の UMP より  {F_{!}}_{1}(1_{P}) = 1_{{F_{!}}_{0}(P)} が成り立つことがわかる。よって  F_{!} は functor の条件 (b) を満たす。
 {F_{!}}_{1}(\theta' \circ \theta) \left[ i_{\left( \theta'_{C}(z), C \right)} \right] \circ \left[ i_{\left( \theta_{C}(x), C \right)} \right] = \left[ i_{\left( (\theta' \circ \theta)_{C}(x), C \right)} \right] が成り立つので colimit の UMP より  {F_{!}}_{1}(\theta' \circ \theta) = {F_{!}}_{1}(\theta') \circ {F_{!}}_{1}(\theta) が成り立つ。よって  F_{!} は functor の条件 (c) を満たす。

 \square

次に  F^{\ast} が functor であることを証明します。

 Lemma
 F^{\ast} \text{ is a functor}.

 Proof.

  • 任意の  E \in \mathcal{E} に対して  F^{\ast}(E) が functor であること

任意の  h \colon C' \to C に対して  {F^{\ast}(E)}_{1}(h) \colon \text{Hom}(FC, E) \to \text{Hom}(FC', E) {F^{\ast}(E)}_{1}(h) = F(h)^{\ast} で定義する。
 {F^{\ast}(E)}_{1}(h \colon C' \to C) \colon {F^{\ast}(E)}_{0}(C) \to {F^{\ast}(E)}_{0}(C') となるので  F^{\ast}(E) は functor の条件 (a) を満たす。
 {F^{\ast}(E)}_{1}(1_{C}) = F(1_{C})^{\ast} = 1_{F(C)}^{\ast} = 1_{\text{Hom}(FC, E)} = 1_{{F^{\ast}(E)}_{0}(C)} が成り立つので  F^{\ast}(E) は functor の条件 (b) を満たす。
 {F^{\ast}(E)}_{1}(h \circ h') = F(h \circ h')^{\ast} = F(h')^{\ast} \circ F(h)^{\ast} = {F^{\ast}(E)}_{1}(h') \circ {F^{\ast}(E)}_{1}(h) が成り立つ。よって  F^{\ast}(E) は functor の条件 (c) を満たす。

  •  F^{\ast} が functor であること

任意の  f \colon E \to E' に対して  {F^{\ast}}_{1}(f) を任意の  C \in {\bf{C}} に対して  {F^{\ast}}_{1}(f)_{C} = f_{\ast} で定義する。
f:id:hitotakuchan:20160916132529p:plain
任意の  h \colon C' \to C と任意の  g \colon FC \to E に対して  \left( F^{\ast}(E')(h) \circ f_{\ast} \right)(g) = f \circ g \circ F(h) = \left( f_{\ast} \circ F^{\ast}(E)(h) \right)(g) が成り立つので、上の diagram は可換になる。よって  {F^{\ast}}_{1}(f) は natural transformation である。
このとき  {F^{\ast}}_{1}(f \colon E \to E') \colon {F^{\ast}}_{0}(E) \to {F^{\ast}}_{0}(E') が成り立つので  F^{\ast} は functor の条件 (a) を満たす。
 {F^{\ast}}_{1}(1_{E}) = 1_{{F^{\ast}}_{0}(E)} は定義より明らか。よって  F^{\ast} は functor の条件 (b) を満たす。
 {F^{\ast}}_{1}(f' \circ f)_{C} = (f' \circ f)_{\ast} = f'_{\ast} \circ f_{\ast} = {F^{\ast}}_{1}(f')_{C} \circ {F^{\ast}}_{1}(f)_{C} = \left( {F^{\ast}}_{1}(f') \circ {F^{\ast}}_{1}(f) \right)_{C} が成り立つので、 F^{\ast} は functor の条件 (c) を満たす。

 \square

最後に  \text{Hom}(P, F^{\ast}(E)) \cong \text{Hom}(F_{!}(P), E) P に関して natural であることを証明します。
 \text{Hom}(\varinjlim_{j \in J} yC_{j}, F^{\ast}(E)) \cong \varprojlim_{j \in J} \text{Hom}(yC_{j}, F^{\ast}(E)) の場合は  \text{Hom}(\varinjlim_{j \in J} FC_{j}, E) \cong \varprojlim_{j \in J} \text{Hom}(FC_{j}, E) の場合と同様に示せるので、 \eta \colon \text{Hom}(\varinjlim_{j \in J} FC_{j}, E) \cong \varprojlim_{j \in J} \text{Hom}(FC_{j}, E) が natural であることの証明のみを示します。それ以外の箇所は Chapter 8 で示した証明と同様に証明できるので省略します。 \eta の定義は Chapter8 の 8.7 節の証明を参照してください。

 Lemma
 \eta \text{ is a natural transformation}.

 Proof.
任意の  \theta \colon Q \to P について考える。 \eta が natural であるためには以下の diagram が可換になることを示す必要がある。
f:id:hitotakuchan:20160916140213p:plain
しかし diagram の右の写像がどのような写像なのか明らかではない。そこで以下の diagram を考える。
f:id:hitotakuchan:20160916141840p:plain
ここで  \theta が natural であることから、任意の  h \colon (z', C') \to (z, C) in \int\!Q h \colon \left( \theta_{C'}(z'),C' \right) \to \left( \theta_{C}(z), C \right) となることに注意しておく。すると
\begin{align*}
\pi_{h} \circ \phi_{Q} \circ \left< \pi_{\left( \theta_{C}(z), C \right)}(-) \right>_{(z,C) \in \int\!Q} \circ e_{P} &= \pi_{(z',C')} \circ \left< \pi_{\left( \theta_{C}(z), C \right)}(-) \right>_{(z,C) \in \int\!Q} \circ e_{P} \\
&= \pi_{\left( \theta_{C'}(z'), C' \right)} \circ e_{P} \\
&= \pi_{h} \circ \phi_{P} \circ e_{P} \\
&= \pi_{h} \circ \psi_{P} \circ e_{P} \\
&= F(h)^{\ast} \circ \pi_{\left( \theta_{C}(z), C \right)} \circ e_{P} \\
&= F(h)^{\ast} \circ \pi_{(z,C)} \circ \left< \pi_{\left( \theta_{C}(z), C \right)}(-) \right>_{(z,C) \in \int\!Q} \circ e_{P} \\
&= \pi_{h} \circ \psi_{Q} \circ \left< \pi_{\left( \theta_{C}(z), C \right)}(-) \right>_{(z,C) \in \int\!Q} \circ e_{P}
\end{align*}
が成り立つので、product の UMP と limit の UMP より diagram を可換とする唯一つの  \overline{\theta} が存在する。

次に  \pi_{(z,C)} \circ e_{Q} \circ \overline{\theta} \circ \eta_{P} = \pi_{(z,C)} \circ e_{Q} \circ \eta_{Q} \circ F_{!}(\theta)^{\ast} を示す。すると product の UMP と  e_{Q} が monic であることから  \overline{\theta} \circ \eta_{P} = \eta_{Q} \circ F_{!}(\theta)^{\ast} が成り立つ。
任意の  f \colon \varinjlim_{(x,C)} F \circ \pi(x,C) \to E に対して
\begin{align*}
\left( \pi_{(z,C)} \circ e_{Q} \circ \overline{\theta} \circ \eta_{P} \right)(f) &= \left( \pi_{\left( \theta_{C}(z), C \right)} \circ e_{P} \circ \eta_{P} \right)(f) \\
&= \left( \pi_{\left( \theta_{C}(z), C \right)} \circ \left< - \circ i_{(x,C)} \right>_{(x,C) \in \int\!P} \circ c_{P}^{\ast} \right)(f) \\
&= f \circ c_{P} \circ i_{\left( \theta_{C}(z), C \right)} \\
&= f \circ c_{P} \circ \left[ i_{\left( \theta_{C}(z), C \right)} \right] \circ i_{(z,C)}
\end{align*}
が成り立つ。一方、
\begin{align*}
\left( \pi_{(z,C)} \circ e_{Q} \circ \eta_{Q} \circ F_{!}(\theta)^{\ast} \right)(f) &= \left( \pi_{(z,C)} \circ \left< - \circ i_{(z,C)} \right>_{(z,C) \in \int\!Q} \circ c_{Q}^{\ast} \circ F_{!}(\theta)^{\ast} \right)(f) \\
&= f \circ F_{!}(\theta) \circ c_{Q} \circ i_{(z,C)}
\end{align*}
が成り立つ。これは  F_{!}(\theta) の定義より等しい。よって  \eta は natural isomorphism である。

 \square

最後にこのように定義した  F_{!} に対して  F_{!}(yC) \cong FC が成り立つことを証明します。

 Lemma
 F_{!}(yC) \cong FC

 Proof.
 \int\!yC において  (1_{C},C) は terminal object になるので、任意の  (f, C') \in \int\!yC に対して  F(f) \colon F \circ \pi(f, C') \to F \circ \pi(1_{C},C) が存在する。このことに注意すると、任意の natural transformation  \phi \colon F \circ \pi \to \Delta E に対して次の左の diagram は可換となる。
f:id:hitotakuchan:20161005121121p:plain
また任意の  \psi \colon F \circ \pi(1_{C},C) \to E が存在して同様に diagram を可換にするとすると、上の右の diagram が可換になることより  \psi = \phi_{(1_{C}, C)} が成り立つ。
よって colimit の UMP より  F_{!}(yC) = \varinjlim_{(f,C) \in \int\!yC} F \circ \pi(f,C) \cong F \circ \pi(1_{C}, C) = FC が成り立つ。

 \square

9.7 Locally cartesian closed categories

Proposition 9.20

はじめに、任意の  f \colon A \to B に対して  \sum_{f} \dashv f^{\ast} \dashv \prod_{f} が成り立つとき、 \sum_{f} \circ\, f^{\ast} \dashv \prod_{f} \circ\, f^{\ast} が成り立つことを確認してください。
 \sum_{f} \dashv f^{\ast} \dashv \prod_{f} の二つの natural isomorphism を合成すればいいです。

次に  !_{A} \colon A \to \ast に対して  \sum_{!_{A}} \circ\, !_{A}^{\ast} A \times - となることは Proposition 5.14 で確認しました。すると  A \times - の right adjoint は  (-)^{A} に unique up to isomorphism で決まるので、 B^{A} = (\prod_{!_{A}} \circ\, !_{A}^{\ast})(B) で定義すればよいことがわかります。

次に証明なしに出てくる "a slice of a slice is a slice" の確認をしておきます。

 Lemma
 \text{a slice of a slice is a slice}.

 Proof.
f:id:hitotakuchan:20161021121200p:plain
任意の  X,Y \in \mathcal{E} と任意の  f \colon X \to Y について  \left( \mathcal{E} / Y \right) /\, f \cong \mathcal{E} / X となることを示す。
はじめに functor  \Phi \colon \left( \mathcal{E} / Y \right) /\, f \to \mathcal{E} / X を定義する。
任意の  a' \colon a \to f \in \left( \mathcal{E} / Y \right) /\, f に対して  \Phi_{0}(a') = a' と定義すると、 a' \colon A \to X であるから  a \in \mathcal{E} / X となる。
また任意の  h \colon a' \to b' \in \left( \mathcal{E} / Y \right) /\, f に対して  \Phi_{1}(h) = h と定義すると、 h b' \circ h = a' を満たすので  h \in \mathcal{E} / X となる。
このとき、 \Phi_{1} \left(h \colon (a' \colon a \to f) \to (b' \colon b \to f) \right) = h \colon (a' \colon A \to X) \to (b' \colon B \to X) = h \colon \Phi_{0}(a') \to \Phi_{0}(b') が成り立つので、 \Phi は functor の条件 (a) を満たす。
次に  \Phi_{1}(1_{a'}) = 1_{a'} = 1_{\Phi_{0}(a')} が成り立つので  \Phi は functor の条件 (b) を満たす。
最後に  \Phi_{1}(h' \circ h) = h' \circ h = \Phi_{1}(h') \circ \Phi_{1}(h) が成り立つので  \Phi は functor の条件 (c) を満たす。

次に functor  \Psi \colon \mathcal{E} / X \to \left( \mathcal{E} / Y \right) /\, f を定義する。
任意の  a' \colon A \to X \in \mathcal{E} / X に対して  \Psi_{0} \Psi_{0}(a') = a' \colon (f \circ a') \to f で定義する。明らかに  \Psi_{0}(a') \in \left( \mathcal{E} / Y \right) /\, f である。
また任意の  h \colon a' \to b' \in \mathcal{E} / X に対して  \Psi_{1}(h) = h と定義すると、 h f \circ b' \circ h = f \circ a' を満たすので、 \Psi_{1}(h) = h \colon \Psi_{0}(a') \to \Psi_{0}(b') となり functor の条件 (a) を満たす。
次に  \Psi_{1}(1_{a'}) = 1_{a'} = 1_{\Psi_{0}(a')} が成り立つので  \Psi は functor の条件 (b) を満たす。
最後に  \Psi_{1}(h' \circ h) = h' \circ h = \Psi_{1}(h') \circ \Psi_{1}(h) が成り立つので  \Psi は functor の条件 (c) を満たす。

以上のように定義した  \Phi \Psi に対して  \Psi \circ \Phi = 1 かつ  \Phi \circ \Psi = 1 が成り立つことは明らかであるから、 \left( \mathcal{E} / Y \right) /\, f \cong \mathcal{E} / X が成り立つ。

 \square

任意の  f \colon (a \colon A \to X) \to (b \colon B \to X) \in \mathcal{E}/X に対して composition functor  \sum_{f} \colon (\mathcal{E}/X)/\,a \to (\mathcal{E}/X)/\,b を考えます。
上の同型射を用いると  \sum_{f}' \colon \mathcal{E}/A \to \mathcal{E}/B が構成できます。 \mathcal{E} が locally cartesian category なら、 \sum_{f}' に対して right adjoint  {f^{\ast}}' \prod_{f}' が構成できます。よって再び同型射を用いることで  \sum_{f} に対して right adjoint を構成できるので  \mathcal{E}/X も locally cartesian category になります。

逆の  \text{2} \Rightarrow \text{1} の証明は exponential が突然出てきて難しいですね。 \mathcal{F} を使った置き換えがなぜ必要なのかもよくわかりません。また1対1に対応するとは書かれていますが、それが  Y p に対して natural であることの証明は省略されています。

 Lemma
 F^{\ast} \dashv \prod_{F}

 Proof.
f:id:hitotakuchan:20161021133911p:plain
任意の  F \colon A \to B の composition functor の right adjoint  F^{\ast} は pullback functor である。よって上の図のように任意の  Y \colon C \to B \in \mathcal{E}/B に対して  F^{\ast}(Y) = \pi_{2} \in \mathcal{E}/A となる。 Y F \mathcal{E} における射であるから  Y \times F \mathcal{E} の object のように記述するのはおかしいが、 \mathcal{E}/B においては  F \circ \pi_{2} = Y \circ \pi_{1} は確かに  Y \times F となるのでこのように記述している。このとき  \pi_{1} \pi_{2} は実際に  \mathcal{E}/B において projection function になっている。

以上の注意を元に、任意の  Y \colon C \to B p \colon X \to A に対して  \theta_{Y,p} \colon \text{Hom} \left( F^{\ast}(Y), p \right) \to \text{Hom}\left(Y, \prod_{F}(p) \right) を定義する。
任意の  l \colon F^{\ast}(Y) \to p に対して以下の diagram を考える。
f:id:hitotakuchan:20161021135558p:plain
 l l \colon F \circ \pi_{2} \to F \circ p \in \mathcal{E}/B と考えると  l \colon Y \times F \to F \circ p と見なせる。 \mathcal{E}/B は cartesian closed であるので exponential の UMP より  \exists !\, \widetilde{l} \colon Y \to {F \circ p}^{F} が存在する。 p p \colon F \circ p \to F \in \mathcal{E}/B と見なせることに注意して以下の pullback diagram in  \mathcal{E}/B を考える。
f:id:hitotakuchan:20161021141034p:plain
すると、 \epsilon \circ (p^{F} \times 1) \circ (\widetilde{l} \times 1) = p \circ \epsilon \circ (\widetilde{l} \times 1) = p \circ l = \pi_{2} が成り立つ。一方、
 \epsilon \circ ( \widetilde{\pi_{2}} \times 1) \circ (! \times 1) = \pi_{2} \circ (! \times 1) = \pi_{2} が成り立つので exponential の UMP より  p^{F} \circ \widetilde{l} = \widetilde{\pi_{2}} \circ ! が成り立つ。よって pullback の UMP より  \exists !\, m \colon Y \to \prod_{F}(p) が存在する。そこで  \theta_{Y,p}(l) = m で定義する。これは各 UMP により well-defined である。

次に  \theta^{-1}_{Y,p} \colon \text{Hom}\left(Y, \prod_{F}(p) \right) \to \text{Hom} \left( F^{\ast}(Y), p \right) を定義する。
任意の  m \colon Y \to \prod_{F}(p) \in \mathcal{E}/B に対して、上の diagram において  n \circ m を考える。すると exponential の UMP より  \exists !\, \overline{n \circ m} \colon Y \times F \to F \circ p が存在する。この  \overline{n \circ m} \overline{n \circ m} \colon \pi_{2} \to p \in \mathcal{E}/A とみなして、 \theta^{-1}_{Y,p}(m) = \overline{n \circ m} で定義する。
f:id:hitotakuchan:20161021143437p:plain

 \theta^{-1}_{Y,p} \theta_{Y,p} の逆射になるので、 \theta_{Y,p} は isomorphism である。次に natural であることを示す。

  •  \theta_{Y,p} Y に関して natural であること

任意の  h \colon Y' \to Y \in \mathcal{E}/B に対して Two-pullback Lemma より以下の diagram が可換になる。
f:id:hitotakuchan:20161024130748p:plain
すると  h' h' \in \mathcal{E}/A とみなすことができる。そこで次の左の diagram を考える。
f:id:hitotakuchan:20161024140733p:plain
任意の  l \colon F^{\ast}(Y) \to p に対して、 (h^{\ast} \circ \theta_{Y,p})(l) = \theta_{Y,p}(l) \circ h が成り立つ。一方、 (\theta_{Y',p} \circ h'^{\ast})(l) = \theta_{Y', p}(l \circ h') が成り立つ。
 \theta_{Y,p}(l) \circ h に対して  \theta の定義より、 \epsilon \circ \left( n \circ \theta_{Y,p}(l) \circ h \times 1 \right) = \epsilon \circ \left( n \circ \theta_{Y,p}(l) \times 1 \right) \circ ( h \times 1) = l \circ (h \times 1) が成り立つ。同様に \theta_{Y', p}(l \circ h') に対して  \epsilon \circ n \circ \theta_{Y', p}(l \circ h') = l \circ h' が成り立つ。
Two-pullback Lemma による diagram より上の右の diagram は可換になる。よって  h \times 1 = h' が成り立つので、exponential の UMP と pullback の UMP より  \theta_{Y,p}(l) \circ h = \theta_{Y', p}(l \circ h') が成り立つ。

  •  \theta_{Y,p} p に関して natural であること

任意の  h \colon (p \colon X \to A) \to (p' \colon X' \to A) \in \mathcal{E}/A に対して Two-pullback Lemma より以下の diagram が可換になる。
f:id:hitotakuchan:20161024140052p:plain
そこで次の diagram を考える。
f:id:hitotakuchan:20161024140723p:plain
任意の  l \colon F^{\ast}(Y) \to p に対して、 ( {h^{F}}'_{\ast} \circ \theta_{Y,p})(l) = {h^{F}}' \circ \theta_{Y,p}(l) が成り立つ。一方、 (\theta_{Y,p'} \circ h_{\ast})(l) = \theta_{Y,p'}(h \circ l) が成り立つ。
上の Two-pullback Lemma による diagram と  \theta の定義より
\begin{align*}
\epsilon \circ \left( n' \circ {h^{F}}' \circ \theta_{Y,p}(l) \times 1 \right) &= \epsilon \circ \left( h^{F} \circ n \circ \theta_{Y,p}(l) \times 1 \right) \\
&= h \circ \epsilon \circ \left( n \circ \theta_{Y,p}(l) \times 1 \right) \\
&= h \circ l
\end{align*}
が成り立つ。一方、 \epsilon \circ \left( n' \circ \theta_{Y, p'}(h \circ l) \times 1 \right) = h \circ l が成り立つ。よって exponential の UMP と pullback の UMP より  {h^{F}}' \circ \theta_{Y,p}(l) = \theta_{Y,p'}(h \circ l) が成り立つ。

以上より  \theta は natural isomorphism である。

 \square

Lemma 9.23

ここでは  \Psi \colon {\bf{Sets}}^{(y/P)^{\text{op}}} \to {\bf{Sets}}^{{\bf{C}}^{\text{op}}}/P を定義し、 1 \simeq \Psi \circ \Phi かつ  1 \simeq \Phi \circ \Psi を示す必要があります。
はじめに  \Psi を定義するために、任意の  G \in {\bf{Sets}}^{(y/P)^{\text{op}}} に対して functor  \coprod G \colon {\bf{C}}^{\text{op}} \to {\bf{Sets}} を定義します。

 Lemma
  \coprod G \text{ is a functor}.

 Proof.
任意の  C \in {\bf{C}} に対して1つ目の成分が  C であるような  \int_{\bf{C}} P の object の集合を  \mathcal{L}_{C} と表す。このとき  (\coprod G)(C) = \coprod_{(C,x) \in \mathcal{L}_{C}} G( (C,x)) で定義する。
次に任意の  f \colon C' \to C に対して、 yf \colon yC' \to yC は任意の  x \colon yC \to P に対して  yf \colon x \circ yf \to x \in \int_{\bf{C}} P となる。すると  G(yf) G(yf) \colon G( (C,x)) \to G( (C', x \circ yf)) となることに注意して、 (\coprod G)(f) = \left[ i \circ G(yf) \right]_{(C,x) \in \mathcal{L}_{C}} \colon \coprod_{(C,x) \in \mathcal{L}_{C}} G( (C,x)) \to \coprod_{(C',x') \in \mathcal{L}_{C'}} G( (C',x')) で定義する。
このとき  \coprod G が functor の条件をみたすことは coproduct の UMP により明らかである。

 \square

本当に  \coprod G が functor の条件を満たすか確認してください。
次にこの  \coprod G を用いて  \Psi(G) \Psi(G) \colon \coprod G \to P で定義する。このとき  \Psi が functor となることを示す。

 Lemma
  \Psi \text{ is a functor}.

 Proof.
任意の  (C,x) \in \int_{\bf{C}} P と任意の  l \in G( (C,x)) に対して  (\coprod G)(C) の要素を  ( (C,x), l) で表すとすると、 \Psi(G) (\Psi(G))_{C}( (C,x), l) = x_{C}(1_{C}) で定義する。このとき  \Psi(G) が natural transformation であることを示す。
f:id:hitotakuchan:20161027142513p:plain
任意の  f \colon C' \to C \in {\bf{C}} と任意の  ( (C,x), l) \in (\coprod G)(C) に対して  \left( P(f) \circ \Psi(G)_{C} \right)( (C,x), l) = P(f)(x_{C}(1_{C})) が成り立つ。一方米田の補題より
\begin{align*}
\left( \Psi(G)_{C'} \circ (\coprod G)(f) \right)( (C,x), l) &= \Psi(G)_{C'}\left( (C', x \circ yf), G(yf)(l) \right) \\
&= (x \circ yf)_{C}(1_{C}) \\
&= P(f)(x_{C}(1_{C}))
\end{align*}
が成り立つので、上の diagram は可換となり  \Psi(G) \in {\bf{Sets}}^{{\bf{C}}^{\text{op}}}/P となる。

次に、任意の  \theta \colon G \to G' に対して  {\Psi(\theta)}_{C} \colon (\coprod G)(C) \to (\coprod G')(C) {\Psi(\theta)}_{C} = \left[ i \circ \theta_{(C,x)} \right]_{(C,x) \in \mathcal{L}_{C}} で定義する。このとき  \Psi(\theta) が natural であることを示す。
f:id:hitotakuchan:20161028105839p:plain
任意の  f \colon C' \to C と任意の  ( (C,x), l) \in (\coprod G)(C) に対して
 \left( (\coprod G')(f) \circ \Psi(\theta)_{C} \right) \left( ( (C,x), l) \right) = (\coprod G')(f)\left( ( (C, x), \theta_{(C,x)}(l)) \right) = \left( (C', x \circ yf),  \left( G'(yf) \circ \theta_{(C,x)} \right)(l) \right)
一方
 \left( \Psi(\theta)_{C'} \circ (\coprod G)(f) \right)\left( ( (C,x), l) \right) = \Psi(\theta)_{C'} \left( ( (C', x \circ yf), G(yf)(l) ) \right) = \left( ( C', x \circ yf), \left( \theta_{(C',x \circ yf)} \circ G(yf) \right)(l) \right)
が成り立つ。これらは  \theta が natural であることより等しい。上の左の diagram は可換であるので  \Psi(\theta) は natural である。

また任意の  ( ( C,x), l) \in (\coprod G)(C) に対して
 \left( \Psi(G')_{C} \circ \Psi(\theta)_{C} \right)\left( ( (C,x), l) \right) = x_{C}(1_{C}) = \Psi(G)_{C} \left( ( (C,x), l) \right)
が成り立つので、 \Psi(\theta) \colon \Psi(G) \to \Psi(G') \in {\bf{Sets}}^{{\bf{C}}^{\text{op}}}/P となる。

 \Psi が functor の条件をみたすことは coproduct の UMP 等により明らかである。

 \square

 Lemma
 1 \simeq \Psi \circ \Phi

 Proof.
natural isomorphism  \phi \colon 1 \to \Psi \circ \Phi を構成すればよい。
任意の  q \colon Q \to P と任意の  C \in {\bf{C}} に対して  (\Psi \circ \Phi)(q)(C) \colon \coprod_{(C,x) \in \mathcal{L}_{C}} \text{Hom}(x,q) \to PC となることに注意して、 {\phi_{q}}_{C} \colon QC \to \coprod_{(C,x) \in \mathcal{L}_{C}} \text{Hom}(x,q) を任意の  l \in QC に対して  {\phi_{q}}_{C}(l) = ( ( C, q \circ \widetilde{l}), \widetilde{l}) で定義する。ただし  \widetilde{l} \colon yC \to Q は米田の補題により一意に定まる  \widetilde{l}_{C}(1_{C}) = l を満たす natural transformation とする。

任意の  ( (C, x), m) \in \coprod_{(C,x) \in \mathcal{L}_{C}} \text{Hom}(x,q) に対して  {\phi_{q}}_{C}^{-1}\left( ( (C,x), m) \right) = m_{C}(1_{C}) {\phi_{q}}_{C}^{-1} を定義すれば、明らかに  {\phi_{q}}_{C} は isomorphism となる。

 \phi_{q} C に関して natural であることを示す。
任意の  f \colon C' \to C に対して以下の diagram を考える。
f:id:hitotakuchan:20161028121845p:plain
任意の  l \in QC に対して
 \left( \left( \coprod \Phi(q) \right)(f) \circ {\phi_{q}}_{C} \right)(l) = ( (C', q \circ \widetilde{l} \circ yf), \widetilde{l} \circ yf)
が成り立つ。一方、 \left( {\phi_{q}}_{C'} \circ Q(f) \right)(l) = ( (C', q \circ \widetilde{Q(f)(l)}), \widetilde{Q(f)(l)}) が成り立つ。 (\widetilde{l} \circ yf)_{C}(1_{C}) = Q(f)(l) が成り立つので両者は等しい。よって diagram は可換となる。

この  \phi_{q} に対して以下の diagram が可換になることは明らかなので、
f:id:hitotakuchan:20161028123226p:plain
 \phi_{q} \colon q \to (\Psi \circ \Phi)(q) \in {\bf{Sets}}^{{\bf{C}}^{\text{op}}}/P となる。

最後に任意の  \theta \colon q \to q' に対して以下の diagram を考える。
f:id:hitotakuchan:20161028124537p:plain
任意の  l \in QC に対して
 \left( (\Psi \circ \Phi)(\theta)_{C} \circ {\phi_{q}}_{C} \right)(l) = ( \Psi \circ \Phi)(\theta)_{C}( ( (C, q \circ \widetilde{l}), \widetilde{l}) ) = ( ( C, q \circ \widetilde{l}), \theta \circ \widetilde{l})
が成り立つ。一方、 ( {\phi_{q'}}_{C} \circ \theta_{C})(l) = ( (C, q' \circ \widetilde{\theta_{C}(l)}), \widetilde{\theta_{C}(l)}) が成り立つ。
ところが  (\theta \circ \widetilde{l})_{C}(1_{C}) = \theta_{C}(l) が成り立つので、両者は等しい。よって上の diagram は可換となる。

以上より  \phi は natural isomorphism である。

 \square

 Lemma
 1 \simeq \Phi \circ \Psi

 Proof.
natural isomorphism  \psi \colon 1 \to \Phi \circ \Psi を構成すればよい。
任意の  G \in {\bf{Sets}}^{(y/P)^{\text{op}}} と任意の  (C,x) \in y/P に対して  {\psi_{G}}_{(C,x)} \colon G(C,x) \to \text{Hom}\left( x, \Psi(G) \right) を次のように定義する。
任意の  l \in G(C,x) に対して  ( (C,x), l) ( (C,x), l) \in \coprod_{(C,x) \in \mathcal{L}_{C}} G(C,x) つまり  ( (C,x), l) \in (\coprod G)(C) であるから米田の補題より一意に対応した  \widetilde{l} \colon yC \to \coprod G が得られる。

この  \widetilde{l} に対して以下の diagram を考える。
f:id:hitotakuchan:20161028144902p:plain
任意の  f \colon C' \to C に対して米田の補題と  \coprod G の定義より、
\begin{align*}
\left( \Psi(G)_{C'} \circ \widetilde{l}_{C'} \right)(f) &= \Psi(G)_{C'}( (C', x \circ yf), G(yf)(l)) \\
&= (x \circ yf)_{C'}(1_{C'}) \\
&= P(f) \left( x_{C'}(1_{C'}) \right) \\
&= x_{C'}(f)
\end{align*}
が成り立つので、上の diagram は可換になる。よって  \widetilde{l} \colon x \to \Psi(G) となるので  {\psi_{G}}_{(C,x)}(l) = \widetilde{l} と定義する。

次に  \psi_{G} が isomorphism であることを示す。
 {\psi_{G}}_{(C,x)}^{-1} \colon \text{Hom}\left( x, \Psi(G) \right) \to G(C,x) を次のように定義する。
任意の  m \colon x \to \Psi(G) に対して、 m m \colon yC \to \coprod G と見なせるので米田の補題より  ( (C, x'), \overline{m}) が一意に存在して  m_{C}(1_{C}) = ( ( C, x'), \overline{m}) を満たす。このとき  m x = \Psi(G) \circ m をみたすことから  x = x' が成り立つ。よって  \overline{m} \in G(C,x) である。
そこで  {\psi_{G}}_{(C,x)}^{-1}(m) = \overline{m} と定義すると、米田の補題より  {\psi_{G}}_{(C,x)} の逆射となり  {\psi_{G}}_{(C,x)} は isomorphism となる。

次に  \psi_{G} が natural であることを示す。
任意の  yf \colon (C',x') \to (C,x) に対して次の diagram を考える。
f:id:hitotakuchan:20161028195553p:plain
任意の  l \in G( (C,x)) に対して  (yf^{\ast} \circ {\psi_{G}}_{(C,x)})(l) = \widetilde{l} \circ yf が成り立つ。一方  \left( {\psi_{G}}_{(C',x')} \circ G(yf) \right)(l) = \widetilde{G(yf)(l)} が成り立つ。
今、 (\widetilde{l} \circ yf)_{C'}(1_{C'}) = \widetilde{l}(f) = ( ( C', x \circ yf), G(yf)(l)) \widetilde{G(yf)(l)}_{C'}(1_{C'}) = ( (C', x'), G(yf)(l)) が成り立ち両者は等しいので、米田の補題より diagram は可換となる。よって  \psi_{G} は natural である。

最後に  \psi が natural であることを示す。
任意の  \theta \colon G \to G' と任意の  (C,x) に対して次の diagram を考える。
f:id:hitotakuchan:20161028195604p:plain
任意の  l \in G( (C,x)) に対して  \left( (\Phi \circ \Psi)(\theta)_{(C,x)} \circ {\psi_{G}}_{(C,x)} \right)(l) = (\Phi \circ \Psi)(\theta)_{(C,x)}(\widetilde{l}) = \Psi(\theta) \circ \widetilde{l} が成り立つ。一方  \left( {\psi_{G'}}_{(C,x)} \circ \theta_{(C,x)} \right)(l) = \widetilde{\theta_{(C,x)}(l)} が成り立つ。
 \left( \Psi(\theta) \circ \widetilde{l} \right)_{C}(1_{C}) = \Psi(\theta)_{C}( ( (C,x), l)) = ( (C,x), \theta_{(C,x)}(l)) \widetilde{\theta_{(C,x)}(l)}_{C}(1_{C}) = ( (C,x), \theta_{(C,x)}(l)) が成り立つので、米田の補題より上の diagram は可換となる。

以上より  \psi は natural isomorphism である。

 \square

9.8 Adjoint functor theorem

Theorem 9.29

書籍にある Solution set condition が微妙に間違ってます。書籍にある通り論理式で表現すると
 \forall X \in {\bf{X}},\ \exists I,\ \exists (S_{i})_{i \in I},\ \forall C \in {\bf{C}},\ \forall f \colon X \to UC,\ \exists i \in I,\ \exists \phi \colon X \to US_{i},\ \exists \overline{f} \colon S_{i} \to C,\ f = U(\overline{f}) \circ \phi
となりますが、正しくは
 \forall X \in {\bf{X}},\ \exists I,\ \exists (S_{i})_{i \in I},\ \exists (\phi_{i} \colon X \to US_{i})_{i \in I},\ \forall C \in {\bf{C}},\ \forall f \colon X \to UC,\ \exists i \in I,\ \exists \overline{f} \colon S_{i} \to C,\ f = U(\overline{f}) \circ \phi_{i}
となります。

こちらの条件でないと、Theorem 9.29 の証明の中で Lemma 9.30 を使用することができません。

参考書籍

Category Theory (Oxford Logic Guides)

Category Theory (Oxford Logic Guides)

  • 作者:Awodey, Steve
  • 発売日: 2008/01/10
  • メディア: ペーパーバック
圏論 原著第2版

圏論 原著第2版

Steve Awodey の Category Theory を読む : Chapter 8

Steve Awodey の Category Theory を読む シリーズトップ

8.3 The Yoneda lemma

書籍の lemma 8.2 の証明は contravariant 版の米田の埋め込みに関する証明ですが、covariant 版の米田の埋め込みに対しても同様の lemma が成立します。
つまり  y \colon {\bf{C}}^{\text{op}} \to {\bf{Sets}}^{\bf{C}} を 任意の  C \in {\bf{C}} に対して  yC = \text{Hom}_{\bf{C}}(C, -) \colon {\bf{C}} \to {\bf{Sets}}、任意の  f \colon C \to D に対して  yf = \text{Hom}_{\bf{C}}(f, -) \colon \text{Hom}_{\bf{C}}(D, -) \to \text{Hom}_{\bf{C}}(C, -) で定義します。
このとき lemma 8.2 と同様に、任意の  C \in {\bf{C}} と任意の  F \in {\bf{Sets}}^{\bf{C}} に対して  \text{Hom}(yC, F) \cong FC が成立し、 y は埋め込みになります。
証明自体は書籍にある lemma 8.2 の証明とほとんど同じなので省略します。理解の確認のためにこちらの証明を書籍を見ながらやってみるといいと思います。

8.4 Applications of the Yoneda lemma

 y \left( (A^{B})^{C} \right) \cong y \left( A^{(B \times C)} \right)

 \text{Hom} \left( X, (A^{B})^{C} \right) \cong \text{Hom}(X \times C, A^{B}) \text{Hom}(X \times C, A^{B}) \cong \text{Hom} \left( (X \times C) \times B, A \right) \text{Hom} \left( X \times (B \times C), A \right) \cong \text{Hom} \left( X, A^{(B \times C)} \right) に関しては transpose を取る対応なので、exponential の UMP より同型となります。

 Lemma
  \text{Hom} \left( (X \times C) \times B, A \right) \cong \text{Hom} \left( X \times (B \times C), A \right)
 Proof.
同型射として  \left< \left<\pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right>^{\ast} \colon \text{Hom} \left( (X \times C) \times B, A \right) \to \text{Hom} \left( X \times (B \times C), A \right) \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right>^{\ast} \colon \text{Hom} \left( X \times (B \times C), A \right) \to \text{Hom} \left( (X \times C) \times B, A \right) を取る。
このとき、任意の  f \colon (X \times C) \times B \to A に対して  \left( \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right>^{\ast} \circ \left< \left<\pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right>^{\ast} \right)(f) = f を示せばよい。つまり   \left< \left<\pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right> = 1_{(X \times C) \times B} を示せばよい。

\begin{align*}
& \pi_{X} \circ \pi_{X \times C} \circ \left< \left<\pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right> \\
&= \pi_{X} \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right> \\
&= \pi_{X} \circ \pi_{X \times C}
\end{align*}

\begin{align*}
& \pi_{C} \circ \pi_{X \times C} \circ \left< \left<\pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right> \\
&= \pi_{C} \circ \pi_{B \times C} \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right> \\
&= \pi_{C} \circ \pi_{X \times C}
\end{align*}

\begin{align*}
& \pi_{B} \circ \left< \left<\pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right> \qquad \\
&= \pi_{B} \circ \pi_{B \times C} \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right> \\
&= \pi_{B}
\end{align*}

が成り立つので、product の UMP より   \left< \left<\pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right> = 1_{(X \times C) \times B} が成り立つ。
任意の  g \colon X \times (B \times C) \to A に対して  \left( \left< \left<\pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right>^{\ast} \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right>^{\ast} \right)(g) = g の証明も同様である。

 \square

次にそれぞれの同型射に関して、それが natural transformation であることを証明します。

 Lemma
 transpose \colon \text{Hom} \left( -, (A^{B})^{C} \right) \to \text{Hom}( - \times C, A^{B}) \text{ is a natural transformation}.
 Proof.
f:id:hitotakuchan:20160715153254p:plain
任意の  f \colon X' \to X g \colon X \to (A^{B})^{C} に対して

\begin{align*}
(f \times 1_{C})^{\ast}(\overline{g}) &= \overline{g} \circ (f \times 1_{C}) \\
&= \epsilon \circ (g \times 1_{C}) \circ (f \times 1_{C}) \\
&= \epsilon \circ \left( (g \circ f) \times 1_{C} \right) \\
&= \overline{g \circ f} \\
&= \overline{f^{\ast}(g)}
\end{align*}

 \square

 Lemma
 transpose \colon \text{Hom}( - \times C, A^{B}) \to \text{Hom} \left( (- \times C) \times B, A \right) \text{ is a natural transformation}.
 Proof.
f:id:hitotakuchan:20160715153305p:plain
任意の  f \colon X' \to X g \colon X \times C \to A^{B} に対して

\begin{align*}
\left( (f \times 1_{C}) \times 1_{B} \right)^{\ast}(\overline{g}) &= \overline{g} \circ \left( (f \times 1_{C}) \times 1_{B} \right) \\
&= \epsilon \circ (g \times 1_{B}) \circ \left( (f \times 1_{C}) \times 1_{B} \right) \\
&= \epsilon \circ \left( (g \circ (f \times 1_{C}) \times 1_{B} \right) \\
&= \overline{g \circ (f \times 1_{C})} \\
&= \overline{(f \times 1_{C})^{\ast}(g)}
\end{align*}

 \square

 Lemma
 \left< \left<\pi_{-}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right>^{\ast} \colon \text{Hom} \left( (- \times C) \times B, A \right) \to \text{Hom} \left( - \times (B \times C), A \right) \text{ is a natural transformation}.
 Proof.
f:id:hitotakuchan:20160715153316p:plain
任意の  f \colon X' \to X g \colon \left( (X \times C) \times B \right) \to A に対して

\begin{align*}
\left( (f \times 1_{B \times C})^{\ast} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right>^{\ast} \right)(g) &= g \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ (f \times 1_{B \times C}) \\
&= g \circ \left( (f \times 1_{C}) \times 1_{B} \right) \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \\
&= \left( \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right>^{\ast} \circ \left( (f \times 1_{C}) \times 1_{B} \right)^{\ast} \right)(g)
\end{align*}

が成り立つことを示せばよい。これはつまり
  \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ (f \times 1_{B \times C}) =  \left( (f \times 1_{C}) \times 1_{B} \right) \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right>
を示せばよい。

\begin{align*}
\pi_{X} \circ \pi_{X \times C} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ (f \times 1_{B \times C}) &= \pi_{X} \circ (f \times 1_{B \times C}) \\
&= f \circ \pi_{X}
\end{align*}

\begin{align*}
\pi_{X} \circ \pi_{X \times C} \circ \left( (f \times 1_{C}) \times 1_{B} \right) \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> &= \pi_{X} \circ (f \times 1_{C}) \circ \pi_{X \times C} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \\
&= f \circ \pi_{X} \circ \pi_{X \times C} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \\
&= f \circ \pi_{X}
\end{align*}

\begin{align*}
\pi_{C} \circ \pi_{X \times C} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ (f \times 1_{B \times C}) &= \pi_{C} \circ \pi_{B \times C} \circ (f \times 1_{B \times C}) \\
&= \pi_{C} \circ \pi_{B \times C}
\end{align*}

\begin{align*}
\pi_{C} \circ \pi_{X \times C} \circ \left( (f \times 1_{C}) \times 1_{B} \right) \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> &= \pi_{C} \circ (f \times 1_{C}) \circ \pi_{X \times C} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \\
&= \pi_{C} \circ \pi_{X \times C} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \\
&= \pi_{C} \circ \pi_{B \times C}
\end{align*}

\begin{align*}
\pi_{B} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ (f \times 1_{B \times C}) &= \pi_{B} \circ \pi_{B \times C} \circ (f \times 1_{B \times C}) \\
&= \pi_{B} \circ \pi_{B \times C}
\end{align*}

\begin{align*}
\pi_{B} \circ \left( (f \times 1_{C}) \times 1_{B} \right) \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> &= \pi_{B} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \\
&= \pi_{B} \circ \pi_{B \times C}
\end{align*}

以上が成り立つことと product の UMP より   \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ (f \times 1_{B \times C}) =  \left( (f \times 1_{C}) \times 1_{B} \right) \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> が成り立つ。

 \square

 Lemma
 transpose \colon \text{Hom} \left( - \times (B \times C), A \right) \to \text{Hom}( -, A^{B \times C}) \text{ is a natural transformation}.
 Proof.
f:id:hitotakuchan:20160715153323p:plain
任意の  f \colon X' \to X g \colon X \times (B \times C) \to A に対して

\begin{align*}
\overline{f^{\ast}(\widetilde{g})} &= \overline{\widetilde{g} \circ f} \\
&= \epsilon \circ ( \widetilde{g} \circ f \times 1_{B \times C}) \\
&= \epsilon \circ (\widetilde{g} \times 1_{B \times C}) \circ (f \times 1_{B \times C}) \\
&= g \circ (f \times 1_{B \times C}) \\
&= (f \times 1_{B \times C})^{\ast}(g)
\end{align*}

が成り立つので、exponential の UMP より  f^{\ast}(\widetilde{g}) = \widetilde{(f \times 1_{B \times C})^{\ast}(g)} が成り立つ。

 \square

Proposition 8.6

上の証明と同様に証明できるので省略しますが、ここでは covariant 版の米田の埋め込みが使われていることに注意してください。

8.5 Limits in categories of diagrams

Proposition 8.7

ここでは  \varprojlim_{i \in J}{F_{i}} \colon {\bf{C}}^{\text{op}} \to {\bf{Sets}} が functor であること。またそれが  {\bf{Sets}}^{{\bf{C}}^{\text{op}}} において limit となることの証明が省略されています。これらの事柄を確認しておきましょう。証明を考える前に Proposition 5.21 を復習して、任意の small category  J と任意の functor  F \colon J \to  {\bf{Sets}}^{{\bf{C}}^{\text{op}}} に関して  F の limit が具体的にどのように構成されるかを再度確認しておいてください。

 Lemma
  \left( \varprojlim_{i \in J} F_{i} \right) \text{ is a functor}.
 Proof.
任意の  C \in {\bf{C}} に対して  \left( \varprojlim_{i \in J}{F_{i}} \right)(C) = \varprojlim_{i \in J} (F_{i}C) で定義する。
次に任意の  f \colon C' \to C に対して次の diagram を考える。ただし  \phi,\psi などは Proposition 5.21 と同様に定義されているとする。
f:id:hitotakuchan:20160722162832p:plain
このとき任意の  \alpha \colon i \to j に対して  F(\alpha) が natural transformation であるから以下の diagram が可換となる。
f:id:hitotakuchan:20160722163817p:plain
このことに注意すると
\begin{align*}
\pi_{\alpha} \circ \psi \circ \left< F_{i}(f) \circ \pi_{i} \right>_{i \in J} \circ e_{C} &= F(\alpha)_{C'} \circ \pi_{i} \circ \left< F_{i}(f) \circ \pi_{i} \right>_{i \in J} \circ e_{C} \\
&= F(\alpha)_{C'} \circ F_{i}(f) \circ \pi_{i} \circ e_{C} \\
&= F_{j}(f) \circ F(\alpha)_{C} \circ \pi_{i} \circ e_{C} \\
&= F_{j}(f) \circ \pi_{\alpha} \circ \psi \circ e_{C} \\
&= F_{j}(f) \circ \pi_{\alpha} \circ \phi \circ e_{C} \\
&= F_{j}(f) \circ \pi_{j} \circ e_{C} \\
&= \pi_{\alpha} \circ \phi \circ \left< F_{i}(f) \circ \pi_{i} \right>_{i \in J} \circ e_{C}
\end{align*}
が成り立つので、product の UMP より  \psi \circ \left< F_{i}(f) \circ \pi_{i} \right>_{i \in J} \circ e_{C} = \phi \circ \left< F_{i}(f) \circ \pi_{i} \right>_{i \in J} \circ e_{C} が成り立つ。よって equalizer の UMP より diagram を可換とするような  f' \colon \varprojlim_{i \in J} F_{i}C \to \varprojlim_{i \in J} F_{i}C' がただ一つ存在する。
そこで   \left( \varprojlim_{i \in J} F_{i} \right)(f) = f' と定義する。


 \left( \varprojlim_{i \in J} F_{i} \right)(f) \colon \varprojlim_{i \in J} F_{i}C \to \varprojlim_{i \in J} F_{i}C' = \left( \varprojlim_{i \in J} F_{i} \right)(C) \to \left( \varprojlim_{i \in J} F_{i} \right)(C') より  \left( \varprojlim_{i \in J} F_{i} \right) は functor の条件 (a) を満たす。
次に equalizer の UMP より  \left( \varprojlim_{i \in J} F_{i} \right)(1_{C}) = 1_{\left( \varprojlim_{i \in J} F_{i} \right)(C)} が成り立つので、 \left( \varprojlim_{i \in J} F_{i} \right) は functor の条件 (b) を満たす。
最後に任意の  f \colon C' \to C g \colon C'' \to C' に対して、
\begin{align*}
\pi_{i} \circ e_{C''} \circ \left( \varprojlim_{i \in J} F_{i} \right)(f \circ g) &= \pi_{i} \circ \left< F(f \circ g) \circ \pi_{i} \right>_{i \in J} \circ e_{C} \\
&= F(g) \circ F(f) \circ \pi_{i} \circ e_{C} \\
&= \pi_{i} \circ \left< F(g) \circ \pi_{i} \right>_{i \in J} \circ \left< F(f) \circ \pi_{i} \right>_{i \in J} \circ e_{C} \\
&= \pi_{i} \circ e_{C''} \circ \left( \varprojlim_{i \in J} F_{i} \right)(g) \circ \left( \varprojlim_{i \in J} F_{i} \right)(f)
\end{align*}
が成り立つので、product の UMP と equalizer の UMP より  \left( \varprojlim_{i \in J} F_{i} \right)(f \circ g) = \left( \varprojlim_{i \in J} F_{i} \right)(g) \circ \left( \varprojlim_{i \in J} F_{i} \right)(f) が成り立つ。よって  \left( \varprojlim_{i \in J} F_{i} \right) は functor の条件 (c) を満たす。

 \square

次に  \theta_{i} \colon \left( \varprojlim_{i \in J} F_{i} \right) \to F_{i} を任意の  C \in {\bf{C}} に対して  {\theta_{i}}_{C} = \pi_{i} \circ e_{C} で定義します。ここで  e_{C} は上で  \left( \varprojlim_{i \in J} F_{i} \right) を定義する際に出てきたものとします。このとき  \left( \left( \varprojlim_{i \in J} F_{i} \right), (\theta_{i})_{i \in J} \right) F の limit となることを証明します。

 Lemma
 \left( \left( \varprojlim_{i \in J} F_{i} \right), (\theta_{i})_{i \in J} \right) \text{ is a cone of diagram } F.
 Proof.
はじめに  \theta_{i} が natural transformation となることを示す。
任意の  f \colon C' \to C に対して以下の diagram が可換になることを示せばよい。
f:id:hitotakuchan:20160722180440p:plain
\begin{align*}
{\theta_{i}}_{C'} \circ \left( \varprojlim_{i \in J} F_{i} \right)(f) &= \pi_{i} \circ e_{C'} \circ \left( \varprojlim_{i \in J} F_{i} \right)(f) \\
&= \pi_{i} \circ \left< F_{i}(f) \circ \pi_{i} \right>_{i \in J} \circ e_{C} \\
&= F_{i}(f) \circ \pi_{i} \circ e_{C} \\
&= F_{i}(f) \circ {\theta_{i}}_{C}
\end{align*}
よって  \theta_{i} は natural transformation である。

次に任意の  \alpha \colon i \to j に対して
\begin{align*}
F(\alpha)(C) \circ {\theta_{i}}_{C} &= F(\alpha)(C) \circ \pi_{i} \circ e_{C} \\
&= \pi_{\alpha} \circ \psi \circ e_{C} \\
&= \pi_{\alpha} \circ \phi \circ e_{C} \\
&= \pi_{j} \circ e_{C} \\
&= {\theta_{j}}_{C}
\end{align*}
が成り立つので  \left( \left( \varprojlim_{i \in J} F_{i} \right), (\theta_{i})_{i \in J} \right) は diagram  F の cone である。

 \square

最後に  \left( \varprojlim_{i \in J} F_{i} \right) が limit であることを証明する。

 Lemma
 \left( \varprojlim_{i \in J} F_{i} \right) \text{ is a limit of diagram } F.
 Proof.
f:id:hitotakuchan:20160723133652p:plain
 \left( G, (\eta_{i})_{i \in J} \right) を diagram  F の任意の cone とする。このとき Proposition 5.21 の議論にあるように、任意の  C \in {\bf{C}} に対して  \phi \circ \left< {\eta_{i}}_{C} \right>_{i \in J} = \psi \circ \left< {\eta_{i}}_{C} \right>_{i \in J} が成り立つので、 e_{C} \circ \mu_{C} = \left< {\eta_{i}}_{C} \right>_{i \in J} を満たす  \mu_{C} \colon G(C) \to \left( \varprojlim_{i \in J} F_{i} \right)(C) がただ一つ存在する。このとき  \mu \colon G \to \left( \varprojlim_{i \in J} F_{i} \right) が natural transformation となることを示す。
f:id:hitotakuchan:20160723133707p:plain
任意の  f \colon C' \to C と任意の  i \in J に対して
\begin{align*}
\pi_{i} \circ e_{C'} \circ \mu_{C'} \circ G(f) &= \pi_{i} \circ \left< {\eta_{i}}_{C'} \right>_{i \in J} \circ G(f) \\
&= {\eta_{i}}_{C'} \circ G(f) \\
&\underset{\eta_{i} \text{ is natural}}{=} F_{i}(f) \circ {\eta_{i}}_{C} \\
&= \pi_{i} \circ \left< F_{i}(f) \circ \pi_{i} \right>_{i \in J} \circ e_{C} \circ \mu_{C} \\
&= \pi_{i} \circ e_{C'} \circ \left( \varprojlim_{i \in J} F_{i} \right)(f) \circ \mu_{C}
\end{align*}
が成り立つので、product の UMP と equalizer の UMP より  \mu_{C'} \circ G(f) = \left( \varprojlim_{i \in J} F_{i} \right)(f) \circ \mu_{C} が成り立つ。

次に任意の  \nu \colon G \to \left( \varprojlim_{i \in J} F_{i} \right) が cone  \left( G, (\eta_{i})_{i \in J} \right) から cone  \left( \left( \varprojlim_{i \in J} F_{i} \right), (\theta)_{i \in J} \right) への写像とすると任意の  C \in {\bf{C}} と任意の  i \in J に対して  \pi_{i} \circ e_{C} \circ \mu_{C} = {\theta_{i}}_{C} \circ \mu_{C} = {\eta_{i}}_{C} が成り立つので、product の UMP と equalizer の UMP より  \nu_{C} = \mu_{C} が成り立つ。よって  \left( \varprojlim_{i \in J} F_{i} \right) は diagram  F の limit である。

 \square

8.6 Colimits in categories of diagrams

Proposition 8.10

証明が省略されている箇所がいくつかあるので補っておきます。
任意の  x \in P(C) に対して米田の補題によって対応する natural transformation をここでは  \theta_{x} と書くことにします。米田の補題の証明を見返して  \theta_{x} の定義を再確認してください。
はじめに任意の  h \colon (x', C') \to (x, C) に対して  \theta_{x} \circ yh = \theta_{x'} が成り立つことを証明します。

 Lemma
 \theta_{x} \circ yh = \theta_{x'}
 Proof.
f:id:hitotakuchan:20160728135800p:plain
任意の  C'' \in {\bf{C}} と任意の  f \colon C'' \to C' に対して
\begin{align*}
\left( (\theta_{x})_{C''} \circ yh \right)(f) &= P(h \circ f)(x) \\
&= \left( P(f) \circ P(h) \right)(x) \\
&= P(f)(x') \\
&= (\theta_{x'})_{C''}(f)
\end{align*}

 \square

次に  \theta \colon P \to Q \theta_{C}(x) = (\theta_{(x,C)})_{C}(1_{C}) で定義するとき、 \theta \circ \theta_{x} = \theta_{(x,C)} が成り立つことを証明します。

 Lemma
 \theta \circ \theta_{x} = \theta_{(x,C)}
 Proof.
f:id:hitotakuchan:20160729171552p:plain
任意の  g \colon C'' \to C に対して、 Q が cocone であることより上の右の diagram が可換になることに注意すると
\begin{align*}
\left( \theta_{C''} \circ (\theta_{x})_{C''} \right)(g) &= \theta_{C''} \left( P(g)(x) \right) \\
&= \left( \theta_{\left( P(g)(x), C'' \right)} \right)_{C''}(1_{C''}) \\
&= \left( (\theta_{(x, C)})_{C''} \circ \text{Hom}(-, g) \right)(1_{C''}) \\
&= (\theta_{(x, C)})_{C''}(g)
\end{align*}
が成り立つ。

 \square

次に  \theta が natural transformation であることを証明します。

 Lemma
 \theta \text{ is a natural transformation}.
 Proof.
f:id:hitotakuchan:20160909101920p:plain
任意の  f \colon C' \to C と任意の  x \in PC に対して、 \theta_{(x, C)} が natural transformation であるから上の右の diagram が可換になることに注意すると
\begin{align*}
\left( Q(f) \circ \theta_{C} \right)(x) &= \left( Q(f) \circ ( \theta_{(x, C)})_{C} \right)(1_{C}) \\
&= \left( (\theta_{(x,C)})_{C'} \circ \text{Hom}(f, -) \right)(1_{C}) \\
&= (\theta_{(x,C)})_{C'}(f)
\end{align*}
が成り立つ。一方先程の証明と同様に  \theta_{\left( P(f)(x), C' \right)} = \theta_{(x, C)} \circ yf が成り立つことに注意すると
\begin{align*}
\left( \theta_{C'} \circ P(f) \right)(x) &= (\theta_{\left( P(f)(x), C' \right)})_{C'}(1_{C'}) \\
&= \left( (\theta_{(x, C)})_{C'} \circ \text{Hom}(-, f) \right)(1_{C'}) \\
&= (\theta_{(x, C)})_{C'}(f)
\end{align*}
が成り立つ。

 \square

最後に  \theta が unique に決まることを証明します。

 Lemma
 \forall \varphi \colon P \to Q,\ \forall C,\ \forall x \in PC,\ \varphi \circ \theta_{x} = \theta_{(x, C)} \Rightarrow \varphi = \theta
 Proof.
任意の  x \in PC に対して
\begin{align*}
\varphi_{C}(x) &= \left( \varphi_{C} \circ (\theta_{x})_{C} \right)(1_{C}) \\
&= (\varphi \circ \theta_{x})_{C}(1_{C}) \\
&= (\theta_{(x,C)})_{C}(1_{C}) \\
&= \theta_{C}(x)
\end{align*}
が成り立つので  \varphi = \theta である。

 \square

8.7 Exponentials in categories of diagrams

ここでは  \theta_{j} \times B が cocone となることの証明が省略されていますが、これは簡単なので確認しておいてください。
次の  \theta_{C} が isomorphism であることを証明する箇所で  A_{j},B が集合であるとみなしてよいという点がわかりにくいかもしれません。
Propostiion 8.7 や 8.8 の議論から functor category においては limit や colimit は pointwise に定義されるのでした。そこで  \theta_{C} \colon \left( \varinjlim_{j}(A_{j} \times B) \right) (C) \to \left( (\varinjlim_{j} A_{j}) \times B \right)(C) の domain と codomain を展開すると  \theta_{C} \colon \varinjlim_{j} \left( A_{j}(C) \times B(C) \right) \to \left( \varinjlim_{j} A_{j}(C) \right) \times B(C) となります。 A_{j}(C) B(C) は集合です。そこで、 (C) の部分を書くのを省略して(記号を乱用して)  A_{j}, B を初めから集合とみなして考えましょうということです。

書籍では covariant 版の米田の補題を用いて  \varinjlim_{j}(A_{j} \times B) \cong (\varinjlim_{j} A_{j}) \times B を証明するという方針がとられています。証明では同型射であることは示されていますが、 X に関して natural であることの証明が省略されているので、これを補っておきます。

 \text{Hom} \left( \varinjlim_{j}(A_{j} \times B), X \right) \cong \varprojlim_{j} \text{Hom} (A_{j} \times B, X)

まず、任意の  X に対して  \text{Hom} \left( \varinjlim_{j}(A_{j} \times B), X \right) \cong \varprojlim_{j} \text{Hom} (A_{j} \times B, X) を証明します。

 Lemma
 \text{Hom} \left( \varinjlim_{j}(A_{j} \times B), X \right) \cong \varprojlim_{j} \text{Hom} (A_{j} \times B, X)
 Proof.
Proposition 5.21 の議論から colimit は以下の diagram によって具体的に構成される。
f:id:hitotakuchan:20160804114324p:plain
Corollary 5.27 より contravariant representable functor によって全ての colimit は limit に移されることに注意して以下の diagram を考える。
f:id:hitotakuchan:20160804121117p:plain
ここで  (- \times B) \circ A A \times B と表すとすると、 \phi',\ \psi' はそれぞれ  \pi_{\alpha} \circ \phi' = \pi_{i},\ \pi_{\alpha} \circ \psi' = (A \times B)(\alpha)^{\ast} \circ \pi_{j} を満たす。

  •  \theta_{X} の定義

任意の  f \colon \varinjlim_{i} (A_{i} \times B) \to X に対して、 (\phi^{\ast} \circ e^{\ast})(f) = f \circ e \circ \phi = f \circ e \circ \psi = (\psi^{\ast} \circ e^{\ast})(f) が成り立つ。よって  f \circ e \circ i_{i} = f \circ e \circ \phi \circ i_{\alpha} = f \circ e \circ \psi \circ i_{\alpha} = f \circ e \circ i_{j} \circ (A \times B)(\alpha) が成り立つことに注意すると、
\begin{align*}
(\pi_{\alpha} \circ \phi' \circ \left< - \circ i_{i} \right>_{i \in J} \circ e^{\ast})(f) &= \pi_{i} \circ \left< f \circ e \circ i_{i} \right>_{i \in J} \\
&= f \circ e \circ i_{i} \\
&= f \circ e \circ i_{j} \circ (A \times B)(\alpha) \\
&= (A \times B)(\alpha)^{\ast} \circ \pi_{j} \circ \left< f \circ e \circ i_{i} \right>_{i \in J} \\
&= (\pi_{\alpha} \circ \psi' \circ \left< - \circ i_{i} \right>_{i \in J} \circ e^{\ast})(f)
\end{align*}
が成り立つ。よって product の UMP と equalizer の UMP より  e' \circ \theta_{X} = \left< - \circ i_{i} \right>_{i \in J} \circ e^{\ast} を満たすただ一つの  \theta_{X} が存在する。

  •  \theta_{X}^{-1} の定義

任意の  g \in \varprojlim_{i} \text{Hom} \left( (A_{i} \times B), X \right) に対して、 \left( \phi^{\ast} \circ \left[ \pi_{i}(-) \right]_{i \in J} \circ e' \right)(g) = \left[ \pi_{i} \left( e'(g) \right) \right]_{i \in J} \circ \phi であることに注意すると、
\begin{align*}
\left[ \pi_{i} \left( e'(g) \right) \right]_{i \in J} \circ \phi \circ i_{\alpha} &= \left[ \pi_{i} \left( e'(g) \right) \right]_{i \in J} \circ i_{i} \\
&= \pi_{i} \left( e' (g) \right) \\
&= (\pi_{\alpha} \circ \phi' \circ e')(g)
\end{align*}
同様に、
\begin{align*}
\left[ \pi_{i} \left( e'(g) \right) \right]_{i \in J} \circ \psi \circ i_{\alpha} &= \left[ \pi_{i} \left( e'(g) \right) \right]_{i \in J} \circ i_{j} \circ (A \times B)(\alpha) \\
&= \pi_{j} \left( e'(g) \right) \circ (A \times B)(\alpha) \\
&= (\pi_{\alpha} \circ \psi' \circ e')(g)
\end{align*}
が成り立つ。よって  \phi' \circ e' = \psi' \circ e' であるから、coproduct の UMP と equalizer の UMP より  e^{\ast} \circ \theta_{X}^{-1} = [ \pi_{i}(-) ]_{i \in J} \circ e' を満たすただ一つの  \theta_{X}^{-1} が存在する。

  •  \theta_{X} が isomorphism であること

 \left< - \circ i_{i} \right>_{i \in J} \circ \left[ \pi_{i}(-) \right]_{i \in J} = 1_{\prod_{i} \text{Hom} \left( (A_{i} \times B), X \right)} \left[ \pi_{i}(-) \right]_{i \in J} \circ \left< - \circ i_{i} \right>_{i \in J} = 1_{\text{Hom} \left( \coprod_{i}(A_{i} \times B), X \right)} が成り立つことは product の UMP、coproduct の UMP より容易に証明できる。
よって equalizer の UMP より  \theta_{X}^{-1} \circ \theta_{X} = 1_{\text{Hom} \left( \varinjlim_{i} (A_{i} \times B), X \right)} かつ  \theta_{X} \circ \theta_{X}^{-1} = 1_{\varprojlim_{i} \text{Hom} \left( (A_{i} \times B), X \right)} が成り立つので、 \theta_{X} は isomorphism である。

 \square

次に  \theta_{X} \colon \text{Hom} \left( \varinjlim_{j}(A_{j} \times B), X \right) \to \varprojlim_{j} \text{Hom} \left( (A_{j} \times B), X \right) が natural in X であることを証明します。任意の  h \colon X \to Y に対して  \varprojlim_{i} \text{Hom}\left( (A_{i} \times B), h \right) がどのように定義されるかは Proposition 8.7 の証明を参照してください。

 Lemma
 \theta \text{ is a natural transformation}.
 Proof.
f:id:hitotakuchan:20160804141626p:plain
任意の  h \colon X \to Y と任意の  f \colon \varinjlim_{i} (A_{i} \times B) \to X に対して、
\begin{align*}
\left( \pi_{i} \circ e'_{Y} \circ \varprojlim_{i} \text{Hom} \left((A_{i} \times B), h \right) \circ \theta_{X} \right)(f) &= \left( \pi_{i} \circ \left< \text{Hom}\left( (A_{i} \times B), h \right) \circ \pi_{i} \right>_{i \in J} \circ e'_{X} \circ \theta_{X} \right)(f) \\
&= \left( \text{Hom} \left( (A_{i} \times B), h \right) \circ \pi_{i} \circ \left< - \circ i_{i} \right>_{i \in J} \circ e^{\ast} \right)(f) \\
&= h \circ f \circ e \circ i_{i}
\end{align*}
一方で
\begin{align*}
(\pi_{i} \circ e'_{Y} \circ \theta_{Y} \circ h_{\ast})(f) &= \left( \pi_{i} \circ \left< - \circ i_{i} \right>_{i \in J} \circ e^{\ast} \circ h_{\ast} \right) (f) \\
&= h \circ f \circ e \circ i_{i}
\end{align*}
が成り立つ。よって product の UMP と  e'_{Y} が monic であることより  \theta は natural transformation となる。

 \square

 \varprojlim_{j} \text{Hom} \left( (A_{i} \times B), X \right) \cong \varprojlim_{j} \text{Hom} (A_{i}, X^{B})

任意の  i \in J に対して  \text{Hom} \left( (A_{i} \times B), X \right) \cong \text{Hom}(A_{i}, X^{B}) は exponential の UMP より成り立ちます。このとき、 \varprojlim_{j} \text{Hom} \left( (A_{i} \times B), X \right) \cong \varprojlim_{j} \text{Hom} (A_{i}, X^{B}) が成り立つことは自明でしょうか?
証明は上の証明とほとんど同じなので概略だけ示しておきます。

 Lemma
 \varprojlim_{j} \text{Hom} \left( (A_{i} \times B), X \right) \cong \varprojlim_{j} \text{Hom} (A_{i}, X^{B})
 Proof.
f:id:hitotakuchan:20160805111721p:plain
上の証明と同様に diagram を可換とするような  \theta_{X} \theta_{X}^{-1} が equalizer の UMP よりただ一つ存在する。
 \left< \widetilde{\pi_{i}(-)} \right>_{i \in J} \left< \overline{\pi_{i}(-)} \right>_{i \in J} は明らかに逆射となるので equalizer の UMP により  \theta_{X} は isomorphism である。

 \square

次に  \theta が natural transformation となることを証明します。任意の  h \colon X \to Y に対して  h^{B} \colon X^{B} \to Y^{B} がどのように定義されるのか Proposition 6.7 の証明をみて再確認してください。

 Lemma
 \theta \text{ is a natural transformation}.
 Proof.
f:id:hitotakuchan:20160805114221p:plain
任意の  f \in \varprojlim_{i} \text{Hom} \left( (A_{i} \times B), X \right) に対して、
\begin{align*}
\left( \pi_{i} \circ e'_{Y} \circ \varprojlim_{i} \text{Hom} (A_{i}, h^{B}) \circ \theta_{X} \right)(f) &= \left( \pi_{i} \circ \left< \text{Hom}(A_{i}, h^{B}) \circ \pi_{i}(-) \right>_{i \in J} \circ e'_{X} \circ \theta_{X} \right)(f) \\
&= \left( \text{Hom}(A_{i}, h^{B}) \circ \pi_{i} \circ \left< \widetilde{\pi_{i}(-)} \right>_{i \in J} \circ e_{X} \right)(f) \\
&= h^{B} \circ \widetilde{\pi_{i} \left( e_{X}(f) \right)}
\end{align*}
が成り立つ。また、
\begin{align*}
\left( \pi_{i} \circ e'_{Y} \circ \theta_{Y} \circ \varprojlim_{i} \text{Hom} \left( (A_{i} \times B), h \right) \right)(f) &= \left( \pi_{i} \circ \left< \widetilde{ \pi_{i}(-) } \right>_{i \in J} \circ e_{Y} \circ \varprojlim_{i} \text{Hom} \left( (A_{i} \times B), h \right) \right)(f) \\
&= \left( \widetilde{ \pi_{i}(-) } \circ \left< \text{Hom} \left( (A_{i} \times B), h \right) \circ \pi_{i}(-) \right>_{i \in J} \circ e_{X} \right)(f) \\
&= \widetilde{h \circ \pi_{i} \left( e_{X}(f) \right)}
\end{align*}
が成り立つ。一方
\begin{align*}
eval_{Y} \circ \left( h^{B} \circ \widetilde{\pi_{i} \left( e_{X}(f) \right)} \times 1_{B} \right) &= eval_{Y} \circ ( h^{B} \times 1_{B}) \circ \left( \widetilde{ \pi_{i} \left( e_{X}(f) \right)} \times 1_{B} \right) \\
&= h \circ eval_{X} \circ \left( \widetilde{ \pi_{i} \left( e_{X}(f) \right)} \times 1_{B} \right) \\
&= h \circ \pi_{i} \left( e_{X}(f) \right)
\end{align*}
が成り立つので、exponential の UMP と product の UMP より  \varprojlim_{i} \text{Hom} (A_{i}, h^{B}) \circ \theta_{X} = \theta_{Y} \circ \varprojlim_{i} \text{Hom} \left( (A_{i} \times B), h \right) が成り立つ。

 \square


上の証明でわかるように natural transformation になることの証明が非常に面倒です。より簡単な証明はないのでしょうか?
今考えている圏が  {\bf{Sets}} であることを利用すると、もっと直接的に  \varinjlim_{j}(A_{j} \times B) \cong (\varinjlim_{j} A_{j}) \times B を示すことができます。

 Lemma
 \varinjlim_{j}(A_{j} \times B) \cong (\varinjlim_{j} A_{j}) \times B
 Proof.
ここでは  \coprod_{i} (A_{i} \times B) の要素を  \left( i, (a_{i}, b) \right) と表します。 u \colon \coprod_{i} (A_{i} \times B) \to \left( \coprod_{i} A_{i} \right) \times B u\left( \left( i, (a_{i}, b) \right) \right) = \left( (i, a_{i}), b \right) で定義する。すると  u が isomorphism となることは明らかである。このとき以下の diagram を考える。
f:id:hitotakuchan:20160808100525p:plain
任意の  \left( \alpha, (a_{i}, b) \right) \in \coprod_{\alpha \colon i \to j} (A_{i} \times B) に対して  (e' \circ u \circ \phi) \left( \alpha, (a_{i}, b) \right) = (e' \circ \phi') \left( (\alpha, a_{i}), b \right) = (e' \circ \psi') \left( (\alpha, a_{i}), b \right) = (e' \circ u \circ \psi) \left( \alpha, (a_{i}, b) \right) が成り立つので coequalizer の UMP より diagram を可換とする  \theta がただ一つ存在する。同様に  \theta^{-1} がただ一つ存在して、 u が isomorphism であるから coequalizer の UMP より  \theta は isomorphism となる。

 \square

Theorem 8.14

証明するべきことは  y(A \times B) \cong yA \times yB y(A^{B}) \cong yA^{yB} です。

 Lemma
 y(A \times B) \cong yA \times yB
 Proof.
natural isomorphism  \theta \colon y(A \times B) \to yA \times yB を構成すればよい。任意の  C \in {\bf{C}} に対して  \theta_{C} \colon \text{Hom}(C, A \times B) \to \text{Hom}(C,A) \times \text{Hom}(C, B) を任意の  h \colon C \to A \times B に対して  \theta_{C}(h) = (\pi_{A} \circ h, \pi_{B} \circ h) で定義する。すると product の UMP より  \theta_{C} は isomorphism となる。
次にこの  \theta C に関して natural であることを示す。
f:id:hitotakuchan:20160809104348p:plain
任意の  f \colon C' \to C と任意の  h \colon C \to A \times B に対して、 \left( (f^{\ast} \times f^{\ast}) \circ \theta_{C} \right)(h) = (\pi_{A} \circ h \circ f, \pi_{B} \circ h \circ f) = (\theta_{C'} \circ f^{\ast})(h) が成り立つ。

 \square

 Lemma
 y(A^{B}) \cong yA^{yB}
 Proof.
任意の  C \in {\bf{C}} に対して
\begin{align*}
y(A^{B})(C) = \text{Hom}(C, A^{B}) &\cong \text{Hom}(C \times B, A) \\
&= yA(C \times B) \\
&\cong \text{Hom} \left( y(C \times B), yA \right) \\
&\cong \text{Hom} ( yC \times yB, yA ) = yA^{yB}(C)
\end{align*}
が成り立つので、この isomorphism を  \theta_{C} とする。このとき  \theta C に関して natural であることを示せばよい。
その証明は今までの証明と同様なので省略する。

 \square

Theorem 8.14 は contravariant 版の米田の埋め込みに対しての定理ですが、covariant 版の米田の埋め込みに関してはどのようなことが成り立つでしょうか?考えて、証明してみてください。

8.8 Topoi

Proposition 8.18

書籍で  u_{C} の定義が与えられていますが、この表記はわかりにくいです。より正確には、 \theta \colon U \rightarrowtail E とすると任意の  e \in E(C) に対して  u_{C}(e) = \left\{ f \colon D \to C \ \middle|\ \exists y \in U(D),\ E(f)(e) = \theta_{D}(y) \right\} と定義されます。
このとき、 u_{C}(e) が sieve となること、つまり precomposition に対して閉じていることを確認する必要があります。さらに pullback condition に関しても証明する必要があります。

 Lemma
 u_{C}(e) \text{ is a sieve}.
 Proof.
任意の  g \colon F \to D と任意の  f \in u_{C}(e) に対して、 \exists y' \in U(F) が存在して  E(f \circ g)(e) = \theta_{F}(y') となることを示せばよい。
 f \in u_{C}(e) より、 \exists y \in U(D) が存在して  E(f)(e) = \theta_{D}(y) が成り立つ。 一方で  \theta が natural transformation であることより  E(g) \circ \theta_{D} = \theta_{F} \circ U(g) が成り立つことに注意すると、 E(f \circ g)(e) = \left( E(g) \circ E(f) \right)(e) = \left( E(g) \circ \theta_{D} \right)(y) = \left( \theta_{F} \circ U(g) \right)(y) = \theta_{F} \left( U(g)(y) \right) が成り立つ。
よって  y' = U(g)(y) とすれば、 f \circ g \in u_{C}(e) となるので  u_{C}(e) は sieve である。

 \square

 Lemma
 t \colon 1 \to \Omega \text{ is a subobject classifier}.
 Proof.
任意の  (X, \phi, \psi) u \circ \phi = t \circ \psi を満たすとする。このとき natural transformation  \exists \alpha \colon X \to U がただ一つ存在して  \phi = \theta \circ \alpha を満たすことを示せばよい。
任意の  C \in {\bf{C}} と任意の  x \in X(C) に対して  t_{C} が total sieve であることより、 1_{C} \colon C \to C \in u_{C} \left( \phi(x) \right) が成り立つ。言い換えると  \exists y \in U(C) が存在して  E(1_{C}) \left( \phi(x) \right) = \phi(x) = \theta_{C}(y) が成り立つ。そこで  \alpha_{C}(x) = y と定義する。このとき  \phi_{C}(x) = (\theta_{C} \circ \alpha_{C})(x) が成り立つ。

次に、任意の  f \colon C' \to C に対して
\begin{align*}
\theta_{C'} \circ U(f) \circ \alpha_{C} &= E(f) \circ \theta_{C} \circ \alpha_{C} \\
&= E(f) \circ \phi_{C} \\
&= \phi_{C'} \circ X(f) \\
&= \theta_{C'} \circ \alpha_{C'} \circ X(f)
\end{align*}
が成り立つ。 \theta_{C'} は monic であるから、 U(f) \circ \alpha_{C} = \alpha_{C'} \circ X(f) が成り立つ。よって  \alpha は natural transformation である。

最後に  \beta \colon X \to U を diagram を可換とするような natural transformation であるとする。
すると任意の  x \in X(C) に対して  \theta_{C} \left( \beta_{C}(x) \right) = \phi_{C}(x) = \theta_{C} \left( \alpha_{C}(x) \right) が成り立つが、 \theta_{C} は monic であるから、 \beta_{C}(x) = \alpha_{C}(x) となる。よって  \beta = \alpha となる。

 \square

参考書籍

Category Theory (Oxford Logic Guides)

Category Theory (Oxford Logic Guides)

  • 作者:Awodey, Steve
  • 発売日: 2008/01/10
  • メディア: ペーパーバック
圏論 原著第2版

圏論 原著第2版