用户: Ice1000/综合代数几何

无疑是本次旅行最大的惊喜.

1动机

使用类型论的方法研究代数几何, 代替 Zariski 意象. Kevin Buzzard 说同伦类型论对于现在的数学没用, 这个工作是对他的反击.

想要的效果应该是类似同伦类型论中类型解释为$\infty$-群胚的那种感觉, 只不过换成是类型解释为概形. 这通过在同伦类型论中新增公理来实现对于概形的描述.

注 1.1. 此时同伦类型论是我们形式化时使用的理论基础. 这个理论本身不是同伦类型论.

整个构造有两个参数: 局部交换环 $R$ 和有限可表 (finitely presented) $R$-代数 $A$. 通过引入一个公理 (SQC) 来对概形的理论建模, 最后的效果是拟紧拟分离概形.

首先定义谱 $\mathrm{Spec}(A):={\mathrm{Hom}}_{R\text{-Alg}}(A,R)$ 为从 $R$-代数 $A$ 出发到 $R$ 自己的环同态.

这有一些基本的结论:

•	$\mathrm{Spec}(R[x])=R$.
•	$\mathrm{Spec}(A)=\varnothing ⟹A$ 是单位类型.
•	$\mathrm{Spec}(R/(r))$ 对应命题 $r=0$.
•	$\mathrm{Spec}(R/(r^{-1}))$ 对应命题 “$r$ 可逆”.

我们现在想要一个全忠实的函子 $A\mapsto \mathrm{Spec}(A)$, 在经典代数几何和综合代数几何中分别采用不同的方案:

经典	综合
加一些结构, 比如 Zariski 拓扑, ${\mathcal{O}}_{\mathrm{Spec}(A)}$	直接加综合拟融贯公理 (SQC, synthetic quasi coherence)

命题 1.2 (综合拟融贯公理). $$\begin{array}{rl}A& \to R^{\mathrm{Spec}(A)}\\ a& \mapsto (\phi \mapsto \phi (a))\end{array}$$是一个等价 (类型论). 这似乎还是某对伴随函子的单位.

2具体定义

定义 2.1. 综合代数几何是满足如下三公理的类型论.

•	$R$ 为局部交换环.
•	综合拟融贯公理 1.2.
•	谱上的选择公理, 即对于任何类型族 $P:\mathrm{Spec}(A)\to \mathcal{U}$, 都有$$\prod _{x:\mathrm{Spec}(A)}|P(x)|\to \left|\prod _{x:\mathrm{Spec}(A)}P(x)\right|$$

可以看出, 在这个模型的定义里就首先需要能描述逻辑截断类型等概念, 所以首先需要一个性质良好的相等类型. 此时, 我们可以将这个模型中的类型类比为某种版本的概形, 或者干脆认为满足这些公理的类型为概形, 并且有 $\mathrm{Sch}\hookrightarrow \mathcal{U}$ 的包含关系.

进一步定义命题的开闭:

定义 2.2. 首先给出辅助定义$$\begin{array}{rl}V(\overline{r})& ::=\forall r,r=0\\ D(\overline{r})& ::=\forall r,r可逆\end{array}$$于是有 (此处命题是指类型论意义上的命题 (类型论)):

•	开命题宇宙:$$\sum _{p:\mathrm{Prop}}\exists \overline{r}.p=D(\overline{r})$$
•	闭命题宇宙:$$\sum _{p:\mathrm{Prop}}\exists \overline{r}.p=V(\overline{r})$$

进一步得到开子概形和闭子概形, 思路类似命题宇宙作为语境范畴的子对象分类子时, 换成开/闭的命题宇宙后, 用特征映射定义子对象即可.

定理 2.3 (依值和下闭合). 若 $X:\mathrm{Sch}$, $Y:X\to \mathrm{Sch}$, 那么 ${\sum }_{x:X}Y(x):\mathrm{Sch}$.

事实上, 概形宇宙不仅在依值和下闭合, 在有限极限下都是闭合的.

推论 2.4. 概形之间映射的纤维也是概形.

注意讨论纤维需要先定义相等类型. 这样可以得到性质良好的 “子概形分类子” 的概念, 不用再讨论开闭.

3正在进行的工作

•	定义 Čech 上同调. 这个讲座我基本听不懂, 太难了
•	真概形 (proper scheme)
•	$A^1$ 同伦论
•	综合微分几何 (即用户:Ice1000/光滑无穷小分析那一套)
•	可计算模型, 或许需要先选定一个合适的 $R,A$. Thierry 推荐了 $R=\mathbb{Z},A=$ 某个像区间类型的东西.