著者
久我 健一 萩原 学 山本 光晴
出版者
千葉大学
雑誌
挑戦的萌芽研究
巻号頁・発行日
2015-04-01

我々は幾何的トポロジーにおいて位相同型写像を作る基本的な手法を提供するビング収縮定理を証明支援系Coq/SSReflectを用いて形式化した。この定理は直感的には異なるように見える空間の間に位相同型写像を与える時に用いられる。この定理の重要な応用例の一つはフリードマンによる4次元ポアンカレ予想の解決であり、そこでは、キャッソンハンドルと標準的ハンドルの間の位相同型写像が構成される。我々は、この定理を形式化するために、まだ多くの形式化を必要とするが、本質的な困難は形式化に必要な膨大な時間だけであると考えている。我々は形式化の負担軽減の目的で、Coqへの簡単なpythonインターフェースも作った。
著者
渚 勝 伊藤 隆 小高 一則 松井 宏樹 杉山 健一 吉田 英信 久我 健一 石村 隆一 宮本 育子
出版者
千葉大学
雑誌
基盤研究(C)
巻号頁・発行日
2000

多様体の非可換化として作用素環論の研究をすすめるという目標で、(1)無理数回転環をモデルとする帰納極限の環の構造解析、(2)幾何学的データとしてKー理論、次元の果たす役割、(3)より非可換な対象として作用素空間の構造を調べる、という3つの視点からのアプローチを試みた。まだまだ多くの問題を抱え、今後の研究課題として残ることは多いが、それぞれの視点から一応の成果を得ることができた。帰納極限の環の構造解析として、松井によるカントール集合上の力学系からできる環の解析が進展し、既にK-理論を用いて力学系の状態を把握する結果が得られていたが、その結果の不備と、更なるK-群の情報が必要であることなど緻密な関係がわかってきている。直接的に帰納極限の環ではないが、それに関連して核型でない環の中でも対象を絞ることによりK-群が環の同型を与えるクラスを方波見ー渚によって構成ができた。次元については、渚ー大坂ーPhillipsによって一応の結果を得ているが、K-群、次元の期待した直接的な成果は今後になる。より非可換な量子化としてハーゲラップテンソル積、環の自由積への実現などの作用素空間の話題がある。この方面は最近、成書の発行が多く、形が出来上がりつつ理論に見えるが、伊藤ー渚の研究によるハーゲラップテンソル積の拡張、シュアー写像との関連によって新しい視点が与えられたと自負している。今後の展開として自由群環のノルムの話題もこれに関係してくるが、これらの計算(自由確率論を用いる)の中で可逆元での近似が大きな意味を持つ事実があり、安定次元1などの次元概念との関係が見える。