文件名称：topos:精益拓扑理论
文件大小：349KB
文件格式：ZIP
更新时间：2024-06-18 19:00:49
topos-theory leanprover Lean
精益拓扑理论 该存储库包含拓扑理论中结果的形式验证，来自“几何和逻辑中的绳子”和“大象的草图”。 这里有什么？ 笛卡尔封闭范畴 筛子和格洛腾迪克拓扑，包括开集拓扑 (Trunc) 从二元积和终端构造有限积 局部笛卡尔封闭范畴和表观单因式分解 许多关于回调的引理（例如粘贴引理） 类别的骨架（假设选择） 子对象类别 子对象分类器和电源对象 自反一元定理 （内部）Beck-Chevalley 和 Pare 定理 拓扑的定义 每个拓扑都是有限共完备的 拓扑的局部笛卡尔闭合和拓扑理论的基本定理 Lawvere-Tierney 拓扑和滑轮 LT 拓扑的分层 证明 Lawvere-Tierney 拓扑可以概括 Grothendieck 拓扑 什么即将到来？ 证明 comonad 的那类余代数形成拓扑 逻辑函子 拓扑内部的逻辑 自然数对象 可能会发生什么？ 几何形态 拓扑上的过滤器/商构造 ET
【文件预览】：
topos-master
----.gitignore(31B)
----src()
--------equalizers.lean(3KB)
--------opens.lean(4KB)
--------cartesian_closed.lean(8KB)
--------sub.lean(31KB)
--------grothendieck.lean(9KB)
--------finite_products.lean(8KB)
--------equiv.lean(15KB)
--------construction.lean(13KB)
--------subobject_classifier.lean(5KB)
--------locally_cartesian_closed.lean(19KB)
--------sheaf.lean(48KB)
--------applications()
--------internal_category.lean(19KB)
--------sieve.lean(9KB)
--------power.lean(56KB)
--------pullback_colimit.lean(2KB)
--------topos.lean(19KB)
--------category()
--------over.lean(9KB)
----import-graph.png(279KB)
----.devcontainer()
--------Dockerfile(386B)
--------devcontainer.json(166B)
----.github()
--------workflows()
----README.md(2KB)
----leanpkg.toml(238B)