Research on homotopy type theory using simplicial methods

点击翻译按钮获取中文摘要

本年度は，本研究において設定された第一の大目的を達成した．最も主要な成果は，前年度までに定義した単体的集合の幾何的実現の性質をしらべて，これがホモトピー群を保存することを証明したことである．このために，新たな構成として，単体的集合の幾何的実現を拡張する新たな構成を導入した．単体的集合はホモトピー論的な空間の組合せ論的表現であるが，ある空間の各点に対して連続的に空間が対応する族を，単体的集合におけるホモトピー論ではファイブレーションと呼ばれる種類の写像で表現する．単体的集合からホモトピー型理論的空間(これを型という)を作る操作を単体的集合から位相空間を作る操作の名から幾何的実現と呼んでいるが，単体的集合のファイブレーションをホモトピー型理論における型上の型の族に翻訳するという，幾何的実現の拡張を定義した．これにより，型上の型の族として自然に定義されるホモトピー型理論における道空間と，単体的集合のファイブレーションの幾何的実現を比較することができ，単に定義を行っただけの昨年の段階に比べ様々な性質の調査を行えるようになった．ホモトピー論的空間の不変量の中で最も重要なものの一つであるホモトピー群が，幾何的実現によって保存されることは，この直接の系である．ホモトピー論的空間の性質は，集合論におけるホモトピー論で証明可能であっても，ホモとピー論的操作しか許さないホモトピー型理論において証明可能であるかは直ちに明らかではない．一方で，集合を離散空間とみなすことで集合論のホモトピー型理論への埋込みが可能であるため，単体的集合に対する事実は同様に証明可能である．本年度の結果により，集合論で証明可能な幾何的実現のホモトピー群の計算結果が，ホモトピー型理論においても証明可能であることが示される．この成果のために，海外での研究集会で収集した情報を，本年度購入したタブレット端末に収集して用いた．