观念
层语义 (sheaf semantics) 可用于解释层意象的内语言.
在概形上的层语义中, 结构层不过是内语言中的一个局部环, 向量丛不过是一个自由模. 层语义可以给出代数几何中一些基本概念更简单的定义, 以及一些基本命题更精炼的证明.
定义
Kripke–Joyal 语义
对语句 $\varphi$, 我们基于对 $\varphi$ 结构的归纳来定义 $U\models\varphi$ 的语义, 其直观是说 $\varphi$ 在 $U$ 上处处成立.
$$
\begin{array}
{l|l}
\text{内蕴} & \text{外蕴} \\
\hline
U\models\top & U=U\text{ (恒真)}\\
U\models\bot & U=\varnothing \\
U\models s=t:\mathcal F & s|_U = t|_U\in\Gamma(U,F);\\
U\models \bigwedge_{j\in J}\varphi_j &
\forall j,\,U\models\varphi_j;\\
U\models \bigvee_{j\in J}\varphi_j & \text{存在开覆盖 }U=\bigcup_i U_i,\\&\quad
\text{对任意 } i\text{ 存在 } j, U_i\models\varphi_j;\\
U\models \varphi\Rightarrow \psi & \text{对任意开集 }V\subset U,
V\models\varphi \text{ 推出 } V\models\psi;\\
U\models\forall s:\mathcal F,\varphi(s) & \text{对任意开集 }V\text{ 与 }s\in\Gamma(V,\mathcal F), V\models\varphi(s);\\
U\models\exists s:\mathcal F,\varphi(s) & \text{存在开覆盖 }U=\bigcup_i U_i,\\ &\quad\text{对任意 }i\text{ 存在 }s_i\in\Gamma(U_i,\mathcal F), U_i\models\varphi(s).
\end{array}
$$
为了突出所考虑的子意象, 我们也将 $U\models \varphi$ 记作 $\operatorname{Sh}(U)\models \varphi$.
简化
有的语句如果完全按照上面的定义展开会过于复杂. 如下的语句可以简化.
$U\models\forall s:\mathcal F. \forall t:\mathcal G. \varphi(s,t)$ 等价于对任意开集 $V\subset U$, 任意截面 $s\in\Gamma(V,\mathcal F), t\in\Gamma(V,\mathcal G)$, 都有 $V\models \varphi(s,t)$.
$U\models\forall s:\mathcal F. \forall t:\mathcal G. \varphi(s)\Rightarrow \psi(s)$ 等价于对任意开集 $V\subset U$, 任意截面 $s\in\Gamma(V,\mathcal F)$, 都有 $V\models\varphi(s)$ 推出 $V\models \psi(s)$.
$U\models\exists ! s:\mathcal F. \varphi(s)$ 等价于对任意开集 $V\subset U$, 存在唯一的截面 $s\in\Gamma(V,\mathcal F)$, $V\models \varphi(s)$.
性质
局部性
层语义是局部的, 即若 $X=\bigcup_i U_i$ 为覆盖, 一条内蕴语句在每个 $\operatorname{Sh}(U_i)$ 的内蕴语言中都成立, 那么它在 $\operatorname{Sh}(X)$ 中也成立. 这有时是优点, 但也带来了一些局限, 我们无法讨论 “一个层由全局截面生成”, “层上同调消失” 等整体的结论.
可靠性
内语言的可靠性 (soundness) 是指, 假若在直觉主义逻辑中一个公式 $\varphi$ 能推出 $\psi$, 那么 $U\models\varphi$ 就能推出 $U\models\psi$. 这个结论的证明也是基于对命题结构的归纳.
内蕴构造
使用内蕴语言可给出积, 余积, 幂集, 子集的构造, 使得这些构造在内蕴语言下满足直观的性质.
例如, 若 $\mathcal F$ 为层, $\varphi(s)$ 为一个变量 $s:\mathcal F$ 的公式, 定义
$$
\left[\left[\left\{s:\mathcal F \mid \varphi(s)\right\}\right]\right]
$$
是由 $U\mapsto \{s\in\Gamma(U,\mathcal F)\mid U \models \varphi(s)\}$ 给出的子层. 例如, 公式 $\varphi$ 的子对象分类子是
$$
\{x:1 \mid \varphi\} = (U\mapsto \{x\in\Gamma(U,1)\mid U\models \varphi\}),
$$
其中 $x$ 是不含于 $\varphi$ 的自由变量.
相关概念
叠语义