Github repository: furea2/NGB The NBG Set Theory Axiom of Extensionality Axiom of Universe Axiom of Difference Axiom of Pair Axiom of Product Axiom of Inversion Axiom of Domain Axiom of Membership Axiom of Cycleimport Axiom of Replacement Axiom of Union Axiom of PowerSet Axiom of Infinity Axiom of Foundation Axiom of GlobalChoice 0. Prerequires The…
Author: furea2
Lean4で圏論
Lean4で圏を定義しました。（圏、関手の定義のみ） 圏 関手 ※参考：mathlib
∞-圏
この記事では、過去のNOTICE OF AMSに掲載されたLurieの記事を解説しています。LurieはJoyalの推し進めたquasi圏を圏論の正統な一般化として採用して [katex]\infty[/katex]-圏という名前でさらに理論を展開させました。Lurieはその記事の中で、quasi圏が圏論の正統な一般化であるといういくつかの根拠を述べています。今回はそれを見ていきたいと思います。 Lurieの主張は、 [katex]\infty[/katex]-圏とは圏論と古典ホモトピー論の一般化であるということです。 話の構成は、まず位相空間から誘導される基本亜群の例を見ます。この（圏である）基本亜群は高次のホモトピー群を反映しないので空間から構成される圏で高次のホモトピー群の情報まで持っている圏の一般化として適当なものは何であるかの話をします。次に空間から誘導される単体集合の性質をみて、それがもとの空間の情報と本質的に変わらないことをみます。一方で、圏はある種の単体集合と対応していることを述べて、空間由来の単体集合と圏由来の単体集合の２つの性質の比較を行います。そして、 [katex]\infty[/katex]-圏がそれら２つの一般化になっていることを確認します。最後に、位相空間から誘導される [katex]\infty[/katex]-圏がホモトピー不変であることから、古典ホモトピー論の一般化としての位置づけであることを主張して記事を終えています。 What is an ∞-Category? 基本亜群 代数トポロジーにおいて最も重要な不変量のひとつに基本群があります。基本群 [katex]\pi_1(X,x)[/katex] とは与えられた空間 [katex]X[/katex] と基点 [katex]x\in X[/katex] に対し、 [katex]X[/katex] 上の [katex]x[/katex] から [katex]x[/katex] への道の集合（をホモトピーで割ったもの）で定義されます。 [katex]\pi_1(X,x) = \text{Map}_X(x,x)/(homotopy).[/katex] もし、特別な基点 [katex]x\in X[/katex] をとりたくない場合、基本群の代わりに基本亜群 [katex]\pi_{\leq 1}X[/katex] を考えることが出来ます。この場合の基本亜群 [katex]\pi_{\leq 1}X[/katex] は対象が [katex]X[/katex] の各点 [katex]x[/katex] であって、2点の間の射はその間の道の集合 [katex]\text{Map}(x,y)[/katex] をホモトピーで割ったものです。Xの基本亜群はその基本群よりも少し多く情報を持っています。Xの基本亜群は道の連結成分の集合 [katex]\pi_0X[/katex] と、各連結成分の基本群を決めます。この場合の連結成分は [katex]\pi_{\leq 1}X[/katex] の対象で、基本群 [katex]\pi_1(X,x)[/katex] は圏 [katex]\pi_{\leq…
Eilenberg-MacLane Object
Connection 定義（T.6.5.1.10） Let [katex]f : X → Y[/katex] を [katex]\infty[/katex]-トポス [katex]\mathcal{X}[/katex] の射とし [katex]0 \leq n \leq \infty[/katex] とする。[katex]f[/katex] が [katex]n[/katex]-連結であるとは、それがeffective epimorphismかつ [katex]0 \leq n \leq n[/katex] に対して [katex]\pi_k(f) = \ast[/katex] であると定義する。対象 [katex]\mathcal{X}[/katex] が [katex]n[/katex]-連結であるとは [katex]f : X → 1_\mathcal{X}[/katex] が [katex]n[/katex]-連結であると定義する。ここで [katex]1_\mathcal{X}[/katex] は [katex]\mathcal{X}[/katex] の終対象とする。簡便のため、[katex]\mathcal{X}[/katex] の任意の射 [katex]f[/katex] は [katex](-1)[/katex]-連結であるとする。 連結ならばホモトピー同値であるというWhiteheadの定理の類似を述べるためにはまた別の概念を要するので、それはまた別の機会に述べることにします。 Eilenberg-MacLane Object 定義（T.7.2.2.1） [katex]\mathcal{X}[/katex] を…
Homotopy Group
古典ホモトピー論において、（基点付き）空間 [katex]X[/katex] の最も重要な不変量はそのホモトピー群 [katex]\pi_i(X,x)[/katex] です。 ここでは任意の [katex]\infty[/katex]-トポス [katex]\mathcal{X}[/katex] の対象 [katex]X[/katex] に対し、類似の不変量を定義したいと思います。[katex]\infty[/katex]-トポスについてはまた詳しく述べたいと思いますのでここでは、ある条件を満たす特別な [katex]\infty[/katex]-圏と思ってください。 [katex]\infty[/katex]-トポスにおけるホモトピー群の定義は通常の群でなく、代わりに底トポスを [katex]\text{Disc}(\mathcal{X})[/katex] とする、群を値に持つ層で定義されます。 ここで定義したホモトピーの性質についてはまた別の機会に述べたいと思います。 Truncation 定義（T.2.3.4.15） Let [katex]k \leq -1[/katex] を整数とする。Kan複体 [katex]X[/katex] が [katex]k[/katex]-truncated であるとは、任意の [katex]i > k[/katex] と任意の点 [katex]x \in X[/katex] に対し、 [katex]\pi_i(X, x) \simeq \ast.[/katex] となることと定義する。簡便のため、[katex]X[/katex] が [katex](-2)[/katex]-truncated であるとは、[katex]X[/katex] が可縮のときとする。 定義（T.5.5.6.1） [katex]\mathcal{C}[/katex] を [katex]\infty[/katex]-圏とし [katex]k \leq -1[/katex] を整数とする。 [katex]\mathcal{C}[/katex] の対象 [katex]C[/katex]…
The ∞-Category of Spectra
The ∞-Category of pointed spaces 定義（T.1.2.16.1） 基点付き単体圏 [katex]\mathcal{K}\text{an}_\ast[/katex] を [katex](\mathcal{S}\text{et}_\Delta)_\ast[/katex] の基点付きKan複体からなる充満部分圏とする。このとき、[katex]\mathcal{S}_\ast = \text{N}(\mathcal{K}\text{an}_\ast)[/katex] を基点付き空間の[katex]\infty[/katex]-圏と定義する。 [katex]\mathcal{K}\text{an}_\ast[/katex] の任意の対象の対 [katex]X, Y[/katex] に対し、基点付き単体集合 [katex]\text{Map}_{\mathcal{K}\text{an}_\ast}(X, Y) = Y^X[/katex] はKan複体なので、[katex]\mathcal{S}_\ast[/katex] は [katex]\infty[/katex]-圏になります。 Spectrum object ここでは極限と余極限を持つ任意の [katex]\infty[/katex]-圏に対し、[katex]\mathcal{C}[/katex] のスペクトラム対象から成る安定 [katex]\infty[/katex]-圏 [katex]\text{Sp}(\mathcal{C})[/katex] が構成します。 特に、[katex]\mathcal{C}[/katex] を空間の [katex]\infty[/katex]-圏とした場合は、古典安定ホモトピー論になります。 定義（S.8.1） Let [katex]\mathcal{C}[/katex] be an [katex]\infty[/katex]-圏とする。A prespectrum object of [katex]\mathcal{C}[/katex] のprespectrum対象とは以下の条件を満たす関手 [katex]X : \text{N}(\mathbb{Z}\times\mathbb{Z}) \to\mathcal{C}[/katex] のこと: 任意の整数対 [katex]i…
安定∞圏上の Suspension functor
Cokernel 命題（S.2.6） [katex]\mathcal{C}[/katex]を基点付き[katex]\infty[/katex]-圏とし、[katex]g:X\to Y[/katex]を[katex]\mathcal{C}[/katex]の射とする。[katex]g[/katex]の余核とは、以下の余完全三角（＝pushout square）をいう; [katex display=true]\begin{CD} @. X @>g>> Y \\ @. @VVV \ulcorner @VVV \\ @. 0 @>>> Z. \end{CD}[/katex] このとき、[katex]W[/katex]を[katex]g[/katex]の余核と呼び、[katex]\text{coker}(g)[/katex]と書く。 [katex]\mathcal{C}[/katex]を基点付き[katex]\infty[/katex]-圏とし、[katex]g:X\to Y[/katex]を[katex]\mathcal{C}[/katex]の射とします。 もし余核は存在すれば、ホモトピー同型を除いて一意となることを示します。 [katex]\mathcal{E}\subseteq\text{Fun}(\Delta^1\times\Delta^1,\mathcal{C})[/katex]を余完全三角からなる充満部分圏とします。 [katex]\theta:\mathcal{E}\to\text{Fun}(\Delta^1,\mathcal{C})[/katex]を忘却関手とし、[katex]g[/katex]に対応する図式を [katex display=true]\begin{CD}@. X @>g>> Y \\@. @VVV \ulcorner @VVV \\@. 0 @>>> Z.\end{CD}[/katex] とします。 T.4.3.2.15を適用することで [katex]\theta[/katex] がKan fibrationであり、そのfibersは空集合または可縮のいずれかです。 [katex]\begin{array}{ccccc}\mathcal{E} & \xrightarrow{\theta} & \text{Fun}(\Delta^1,\mathcal{C}) \\ \\^\exists \bigcirc &…
Hopf Algebroid
球面の安定ホモトピー群を計算するためのAdams-Novikovスペクトル系列のE2項は [katex]E_2^{\ast,\ast} = \text{Ext}_{BP_\ast BP}^{\ast,\ast}(BP_\ast,BP_\ast)[/katex] になります。 今回、というか今シリーズはこの右辺を計算するためのcobar complexの定義をしたいと思います。 流れとしては、 [katex]\text{Hom}_{BP_\ast BP}^{\ast,\ast}(BP_\ast, – )[/katex] の右導来関手による複体を計算しやすいある加群に置き換えること、そして [katex]BP_\ast[/katex] 余加群の標準的な射影分解（projective resolution）を見つけることが大きな目標になります。 [katex]K[/katex]を可換環とします。 [katex]K[/katex]上のHopf亜代数（Hopf algebroid）とは可換[katex]K[/katex]代数の圏の、亜群対象のことを言います。が、この定義はピンと来ないので代わりの具体的な定義を述べます。 [katex]K[/katex]上のHopf亜代数の定義は以下のとおりです。 命題（HTT 4.3.2.15） [katex]K[/katex]を可換環とする。[katex]K[/katex]上Hopf亜代数とは、以下の構造射を持つ可換[katex]K[/katex]代数の対[katex](A, \Gamma)[/katex]のこと。 [katex] \begin{array}{ll} \eta_L:A\to\Gamma & left\ unit, \\ \eta_R:A\to\Gamma & right\ unit, \\ \Delta:A\to\Gamma\otimes_A\Gamma & coproduct, \\ \varepsilon:\Gamma\to A & counit, \\ c:\Gamma\to\Gamma & conjugation. \end{array} [/katex] ここで [katex]\Gamma[/katex] は [katex]C[/katex]に関し左[katex]A[/katex]-加群であり[katex]C[/katex]に関して右[katex]A[/katex]-加群。[katex]C[/katex]は通常のテンソル積。[katex]C[/katex]と[katex]C[/katex]は[katex]A[/katex]加群の射。更にこれらの構造射は以下の条件を満たすものとする。…
Hello React Native!
仕事ではReactで開発を行っていますが、React Nativeを使った開発をしたことがなかったので調べてみました。 expo-cliをインストール。 Expo CLIでReact Nativeプロジェクトを作成します。 プロジェクトの作成が終わったらディレクトリに入って開発サーバーを起動してみます。 ここで起動されるサーバーは、プロジェクトの管理サーバーのようです。 サイドバーのRun in web browserを押してローカルで起動させてみます。 ブラウザが開いて下のフレーズが画面に出てくればうまくいっています。 Open up App.tsx to start working on your app! サーバーがうまく立ち上がっていることを確認出来たら、いつものフレーズを追加します。 ファイルを保存すると画面に表示されているテキストが変わっているはずです。 Open up App.tsx to start working on your app!Hello React Native! スマホアプリの開発が思ったより簡単に始められることがわかったので、テンションあがりますね！ 参考： ゼロから始める React Native + Expo 入門
Cantorの対角線論法
今回はLean4でCantorの定理（と同等の定理）を証明します。 Cantorの定理 集合Aに対し、集合Aからその冪集合への全射写像 [katex]f : A \to 2^A[/katex] は存在しない。 ※厳密なCantorの定理はCardinalを定義する必要がありますので、その話はまた別の機会に行いたいと思います。 Lean4でCantorの定理は以下でかけます。 これをLean4で解いてみます。 Cantorの定理を証明する場合、αのある部分集合を使って証明する手法がよく採用されます。 Cantorの補題 Aを集合Aとし、fを集合Aからその冪集合への写像 [katex]f : A \to 2^A[/katex] とする。このとき、Bを [katex]\{ a \in A | a \notin f(a) \}[/katex] とすると、 [katex]f(a)=B[/katex] なる [katex]a \in A[/katex] は存在しない。 この補題を絡めて、証明を途中まで埋めます。 Cantorの補題の証明は [katex]a \in A[/katex] と、[katex]a \notin A[/katex] についてどちらも矛盾となることで示します。 Lean4の証明でもその方針で証明してみます。Lean4で排中律を使いたい場合は by_cases を使います。 sorryの部分を埋めます。 D ∈ f D の場合…