Category: Mathematics

定義 三角圏 [katex]C[/katex] の 局所部分圏とは以下を満たす充満部分圏 [katex]D[/katex] を指す。 任意の cofiber列 [katex]X\to Y\to Z \to \Sigma X[/katex] に対し、[katex]X, Y, Z[/katex] の2つが [katex]D[/katex] の対象なら残りも [katex]D[/katex] 対象。 [katex]D[/katex] の任意の余積もまた [katex]D[/katex] の対象。 [katex]Y \in D[/katex] かつ写像 [katex]X \xrightarrow{i} Y \xrightarrow{p} X[/katex] が [katex]p\circ i = 1[/katex] なら [katex]X \in D[/katex]。 定義 [katex]C[/katex] を閉対象モノイダル加法圏とし、それぞれ、モノイダル積 [katex]X\land Y[/katex] 、単位 [katex]S[/katex] 、内部射の対象 [katex]F(X, Y)[/katex]…

命題（HTT 4.3.2.15） 与えられた [katex]\infty[/katex]-圏の図式 [katex]C \to D’ \xleftarrow{p} D[/katex] ただし [katex]p[/katex] は categorical fibration とする。 [katex]C^0[/katex] を [katex]C[/katex] の充満部分圏とする。[katex]K \subset \text{Map}_{D’}(C, D)[/katex] を [katex]F|C^0[/katex] の [katex]p[/katex]-左Kan拡張となる関手 [katex]F : C \to D[/katex] で満たされる充満部分圏とする。[katex]K’ \subset \text{Map}_{D’}(C^0, D)[/katex] を、任意の対象 [katex]c \in C[/katex] 関して誘導された図式 [katex]C^0_{/c} \to D[/katex] が [katex]p[/katex]-余極限を持つようなもので満たされる充満部分圏とする。この時、制限関手 [katex]p[/katex] は単体集合の自明 fibration となる。 例 命題の主張を少し簡単にして、[katex]D’ = \Delta^0[/katex] としてみる。 命題（HTT…

古典的Kan拡張 [katex]C[/katex] と [katex]J[/katex] を通常の圏として、[katex]\delta : C \to C^J[/katex] を自明な対角関手とします。この時もし [katex]C[/katex] が任意の小さな余極限を持つならば、[katex]\delta[/katex] は左随伴 [katex]\underrightarrow{\text{lim}} : C^J \to C[/katex] を持ちます。従って、余極限の理論は対角関手の左随伴の研究と考えることが出来ます。 より一般に、関手 [katex]i : J \to J'[/katex]が与えられた時、[katex]i[/katex] の合成により関手 [katex]J[/katex] を誘導します。この時 [katex]C[/katex] が十分な余極限を持てば、[katex]i[/katex] に関する左随伴が構成可能です。この時、この左随伴を、[katex]i[/katex] に関する左Kan拡張と呼びます。 余極限対 定義（HTT 4.3.1.1） [katex]f : C \to D[/katex] を inner fibration、[katex]\overline{p} : K^\triangleright \to C[/katex] を図式、[katex]p = \overline{p}|K[/katex] とする。この時、[katex]\overline{p}[/katex] が [katex]p[/katex] の [katex]f[/katex]-余極限であるとは、写像…

[katex]\infty[/katex]-圏の圏を考えるとき、ordinary圏の中で理論を展開するのはナンセンスです。ordonary圏の一般化として様々なものがありますが、やはりここは [katex]\infty[/katex]-圏、即ち、[katex]\infty[/katex]-圏の [katex]\infty[/katex]-圏を考えたいですよね。 Infinity Category of Infinity Category 定義（HTT 3.0.0.1） 単体圏 [katex]Cat^\Delta_\infty[/katex] を以下で定義する。 [katex]Cat^\Delta_\infty[/katex] の対象は（小さな） [katex]\infty[/katex]-圏。 [katex]\infty[/katex]-圏 [katex]C[/katex]、[katex]D[/katex] に対し、射の対象（＝単体集合）[katex]\text{Map}_{Cat^\Delta_\infty}(C, D)[/katex] を [katex]\infty[/katex]-圏 [katex]Fun(C, D)[/katex] に含まれる最大のKan複体で定義する。 さらに、[katex]Cat_\infty[/katex] で [katex]\text{N}(Cat^\Delta_\infty)[/katex] を表すとし、[katex]Cat_\infty[/katex] を（小さな）[katex]\infty[/katex]-圏 の [katex]\infty[/katex]-圏 とみなすことにする。 [katex]Cat_\infty[/katex] の射対象はKan複体なので、それ自体ちゃんと [katex]\infty[/katex]-圏となっています。 上の定義は、小さな [katex]\infty[/katex]-圏のみを対象としています。小さいと限らない [katex]\infty[/katex]-圏については [katex]\widehat{Cat}_\infty[/katex] で表すことにします。 Limits and Colimits 圏の構成問題でやはり気になるのは極限です。HTTでは極限・余極限を直接定義している他、[katex]Cat_\infty[/katex] をある simplicial model category [katex]\mathbf{A}[/katex] に付随する圏として実現し、[katex]Cat_\infty[/katex] の極限・余極限の存在性を [katex]\mathbf{A}[/katex] のhomotopy極限・homotopy余極限の存在に帰着させる方法が紹介されています。その鍵となるのは以下の定理です。 系（HTT 4.2.4.8） [katex]\mathbf{A}[/katex] を combinatorial simplicial model category とする。このとき、…

accessible category（以後、到達可能圏と呼ぶ）とは、極限についてsmallの条件を課したものである。通常、大きな圏を扱うことが多い。ところが、粗い言い方をしてよければ、極限の議論をする上では大きな集合についての極限を数学的対象として扱うことは少ない。極限の議論をすることは最初から小さな極限に限って良いことになる。この仮定を数学的に定式化したものが到達可能圏である。 定義（Accessible Category） 局所小な圏 [katex]C[/katex] がある正則基数 [katex]\kappa[/katex] に対し、 [katex]\kappa[/katex] – accessible （ [katex]\kappa[/katex] – 到達可能）であるとは、 [katex]C[/katex] が accessible （到達可能）であるとは、ある [katex]\kappa[/katex] が存在してそれが [katex]\kappa[/katex] – accessible であることを言う。 無限圏のバージョン定義は以下となる。 定義（Accessible  [katex]\infty[/katex] – Category） 局所小な圏 [katex]C[/katex] がある正則基数 [katex]\kappa[/katex] に対し、 [katex]\kappa[/katex]-accessible （ [katex]\kappa[/katex] -到達可能）であるとは、ある小さな [katex]\infty[/katex] – 圏 [katex]C^0[/katex] と以下の同型が存在することを言う。 [katex]C[/katex] が accessible （到達可能）であるとは、ある [katex]\kappa[/katex] が存在してそれが [katex]\kappa[/katex] – accessible であることを言う。 上の定義がaccessibleである理由。 命題（HTT 5.4.2.2.） [katex]\infty[/katex] – 圏 [katex]C[/katex] と正則基数 [katex]\kappa[/katex] に対し、TFAE。 ※TFAE: The followigs are equivalent 参考文献：Michael Makkai, Robert Paré, Accessible categories: The…

数学の基本的な対象と言えば集合ですが、集合と集合の間の関係は等号や包含関係などの同じレベルの関係から、含意、べき集合などの集合と異なるレベルとしての関係等様々です。 もしこれらを集合の枠組みで二項関係を定義しようと思うと、集合の型に統一してから定義する必要があります。 また、通常の集合論的な集合では、集合の名前は全く重要ではなくその集合の要素だけが集合自体を特徴づけますが、型理論的な集合を定義しようとすると、集合の要素の型の情報が、集合の型として残っています。 これは型理論的に集合の型を定義しようとするときには余計な情報ですので、集合の方を区別しない定義を行う必要があります。 実際、LEANライブラリの集合ではまず、型と要素の型を集合への変換する関数の２組から成る前集合の型を定義し、集合の型は前集合の型から型の情報を取り除いた（即ち、型が違っても前集合として同じなら同じ集合とみなす）ものとして定義されます。 以下が前集合の定義です： 前集合は上から降りてくる形で帰納的に定義されます。つまり、例えばαが前集合であった場合、αの型を持つ要素も前集合であることを保証します。 これにより、前集合の枠組みで命題の証明や定義を行う場合は、外側の前集合で命題が成り立つことを仮定して、その要素について命題が成り立つを証明する流れになります。 例えば、集合が等しいことの定義はLEANでは以下のようにして行われます： pSet.recはpSetをinductiveとして定義した場合に一緒に定義されるもので、命題を、型を構成する要素の命題に置き換えます。 従って、実際に前集合のequivについて言及するときは、equivはmに置き換えて証明したりすることになります。

（再掲）La Mort de Socrate ソクラテスは人間である 人間はすべからく死ぬ ソクラテスは死ぬ 証明を言葉にして説明するのは簡単です。 死ぬ存在を示すには、 “Human_is_Mortal” により人間の存在を示せば十分です。一方で、人間の存在は “Socrates_is_Human” とソクラテスの存在から得ることが出来ます。従って死ぬ存在が示され、命題の証明が完了します。 また、演繹的な説明ももちろん可能です。ただし、この場合の証明は少し複雑なtacticsを用いることになるので今回は上の流れで記述を行います。 ソクラテスの存在が仮定されているので、 “Socrates_is_Human” により人間が結論付けられます。次に、 “Human_is_Mortal” により、人間から死ぬ存在であることを結論づけることが出来ます。 前者の論理説明をGlaceonを使って証明してみましょう。 Glaceonではルールとして “begin” ～ “end” の間の範囲のみ記述が許されていました。 “PならばQ” の形の主張ではまず P を仮定に持ち上げます。 主張の前条件を仮定に持ち上げるためのコマンドは “assume” です。下の証明エリアでは先にコマンドを配置してあります。 “assume Socrates,” の前後の行にカーソルを合わせて、証明の右エリアで途中の証明状況を確認してみてください。 “assume Socrates,” の次の行にカーソルをあわせると、証明途中は以下のような表示になっていると思います： ゴールとなる目標は “is_mortal” を証明することです。 上の状況を言葉で書き直すと以下のようになります： この状況から証明の続きを書いていきましょう。 “Human_is_Mortal” により人間の存在を示せば十分 これはtactic “apply” を用いて、”apply Human_is_Mortal” を使います。 人間の存在は “Socrates_is_Human” とソクラテスの存在から得られる この場合もtactic “apply”…

定理証明言語『LEAN』 以前の記事で述べたプラトンの三段論法を改めて記します。 ソクラテスは人間である 人間はすべからく死ぬ ソクラテスは死ぬ 今回はこれをプログラムによって証明したいと思います。 証明器『Glaceon』の説明 まずは下記の証明エリアをご覧ください。 ※実際の証明はこの記事の次の項目で行います！ 下の証明器はGlaceonと読んでいて、ふれぁがLEANを使って作ったものです。 それぞれのエリアはそれぞれ下記の役割を持っています。 証明器の左エリア　　：　実際に証明を書く場所 証明器の右エリア　　：　現在の証明状況を表示 証明器の右エリア下部：　問題の証明完了表示 証明器右下は “Solved!” か “not solved yet…” のいづれかになっていれば、解けたかどうかの判定がLEANによって行われた状態です。もしどちらでもなく、 “checking…” の表示となっていれば現在判定中であることを知らせます。その場合はしばらくお待ち下さい。 証明を行う際は右エリアを見ながら左エリアの中で証明を書いていくことなります。 証明記述エリア 左エリアの中を少し説明しましょう。 左エリアの中は点線で上部と下部に分かれていて、このうち上部は使用できる命題などの世界を管理しているので、特に絶対に触らないでください。 ※webの技術力がなくて物理的に書き換えない出来ないように出来ませんでした。。 “theorem” のワード以降が命題（または定理、補題）の主張となります。 そして “begin” と “end” で囲まれた部分が、実際に証明を記述する部分となります。この範囲より外を書き換えるのはルール違反です。 基本的に “begin” と “end” で囲まれた範囲は、デフォルトでsorryが最初から書かれています。 これは、証明が完了していない状況でエラーを一時的に回避するための特殊コマンドです。エラーは証明の完了・未完了とは別であって、エラーはいかなるときでも必ず回避しなければなりません。エラー状態では必ず証明未完了の判定となります。 今後、”sorry” コマンドは証明の記述中に最もお世話になると思います。 適当な意味のない文字を証明記述エリアに書き込んでみてください。Glaceonが証明を理解出来ずにエラーが出てしまう場合は証明記述エリアでエラーが発生している箇所が示されるはずです。 ※証明に用いるためのコマンド（=tacticsと呼ばれる）はたくさん存在します。今後、この豊富なtacticsを用いて様々な数学の定理を証明していくことになるでしょう。 最後に現在の証明状況表示エリアの表示確認を行ってみましょう。 証明記述内の “– この中に証明を書いてください” にテキストカーソルを合わせてみてください。カーソルを合わせると右の表示エリアに以下のような表示がされるはずです。 詳細は後ほど述べますが、記号 “⊢” の段が証明すべき主張で、それより上の段に書かれているものが、現在手元に存在している仮定になります。 この場合、証明状況は以下のように還元されます： […