一句话:用函子点方法为交换环上的预层(含 scheme)构造预层模范畴,并证明其构成直觉主义线性逻辑模型。
本文探讨代数几何与线性逻辑之间的深层联系。代数几何中,scheme 既有几何面,也配备拟凝聚模的对称幺半范畴。作者采用 Grothendieck 的函子点观点,把交换环范畴上的协变预层 X 视为广义空间,并在其“上方”构造预层模范畴 PshMod_X。该范畴是对称幺半闭的,因而给出直觉主义线性逻辑的一个模型;其指数模态通过以适当方式粘合环代数上的 Sweedler 对偶构造得到。这一结果将 scheme 等几何对象统一纳入线性逻辑的范畴语义框架,表明几何空间上的模范畴可系统地为线性逻辑提供模型。
The language of Algebraic Geometry combines two complementary and dependent levels of discourse: on the geometric side, schemes define spaces of the same cohesive nature as manifolds ; on the vectorial side, every scheme X comes equipped with a symmetric monoidal category of quasicoherent modules, which may be seen as generalised vector bundles on the scheme X. In this paper, we use the functor of points approach to Algebraic Geometry developed by Grothendieck in the 1970s to establish that every covariant presheaf X on the category of commutative rings — and in particular every scheme X — comes equipped “above it” with a symmetric monoidal closed category PshModX of presheaves of modules. This category PshModX defines moreover a model of intuitionistic linear logic, whose exponential modality is obtained by glueing together in an appropriate way the Sweedler dual construction on ring algebras.