Category: 未分類

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…

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…