Homotopy-rs项目教程：使用交互式证明工具验证范畴等价提升为伴随等价

前言

在范畴论中，等价关系与伴随关系是两个核心概念。本教程将指导您使用homotopy-rs项目中的交互式证明工具，通过可视化的方式证明一个重要定理：任何1-范畴的等价关系都可以提升为伴随等价关系。我们将从零开始构建证明所需的范畴结构，并逐步完成整个证明过程。

基础概念准备

在开始之前，我们需要理解几个关键概念：

1. 0-细胞：代表范畴中的对象
2. 1-细胞：代表范畴间的函子
3. 2-细胞：代表自然变换
4. 伴随等价：指存在两个自然变换满足特定的"蛇形方程"

环境配置

初始签名设置

首先我们需要构建证明所需的签名结构：

1. 创建两个0-细胞C和D，代表要证明等价的两个范畴
2. 创建两个1-细胞：
   • F: C → D
   • G: D → C
3. 创建两个可逆的2-细胞：
   • α: 1_C → G∘F
   • β: F∘G → 1_D

详细构建步骤

0-细胞创建

1. 使用添加功能创建两个0-细胞
2. 将它们分别命名为C和D（支持LaTeX语法）

1-细胞创建

1. 选择C作为源，D作为目标，创建函子F
2. 选择D作为源，C作为目标，创建函子G

2-细胞创建

创建自然变换α的步骤：

1. 选择C并创建其恒等变换作为源
2. 构造复合G∘F作为目标
3. 创建2-细胞α（呈现为"杯"形状）

创建自然变换β的步骤：

1. 选择D的恒等变换作为目标
2. 构造复合F∘G作为源
3. 创建2-细胞β（呈现为"帽"形状）

最后，将α和β标记为可逆变换。

定理证明

构造新的余单位

我们需要构造一个新的自然变换β'，使得α和β'满足伴随关系的蛇形方程。我们选择β' = β ∘ α⁻¹ ∘ β⁻¹。

构造步骤：

1. 选择β作为当前工作区图
2. 在底部插入α⁻¹
3. 再插入β⁻¹完成构造
4. 将结果保存为定理，命名为β'

证明第一个蛇形方程

我们需要证明在F上的蛇形方程成立：

1. 构造蛇形图：
   • 从α开始
   • 右侧插入F的恒等变换
   • 顶部插入β'完成构造
2. 提升维度开始证明：
   • 展开β'的定义
   • 通过四次交换移动α
   • 使用SHIFT键合并α和α⁻¹
   • 同样方式合并β和β⁻¹
3. 简化证明图以获得更清晰的证明结构
4. 将结果保存为"Snake 1"定理

证明第二个蛇形方程

在G上的证明略有不同：

1. 构造蛇形图：
   • 从α开始
   • 左侧插入G的恒等变换
   • 顶部插入β'完成构造
2. 提升维度开始证明：
   • 展开β'的定义
   • 插入α和α⁻¹气泡
   • 移动并合并变换
   • 最终消除所有气泡
3. 简化证明图
4. 将结果保存为"Snake 2"定理

结果导出与保存

完成证明后，我们可以：

1. 设置项目信息（标题、作者等）
2. 导出整个工作区
3. 导出特定维度的图表为多种格式（如TikZ、SVG等）

可视化技巧

1. 使用视图控制查看不同维度的证明结构
2. 通过拖拽操作简化证明图
3. 注意保持证明图的可读性，避免过度简化

总结

通过本教程，我们完成了从范畴等价到伴随等价的提升证明。homotopy-rs项目的交互式证明工具让我们能够：

• 直观地构建范畴结构
• 可视化地完成复杂证明
• 随时调整和优化证明过程

这种基于几何直觉的证明方法为范畴论研究提供了全新的视角和工具。