广延范畴中列表对象自函子 L 的多项式表示：通用有限基数 π2E 的可指数化

《Mathematical Structures in Computer Science》：The list object endofunctor is polynomial

　　

本文研究具有有限极限和参数化列表对象（parametrized list objects）的一般范畴 ?? 上的列表对象函子（list object functor） L : ?? → ??。研究人员证明，如果 ?? 是广延的（extensive），则通用有限基数（generic finite cardinal） π₂^E 是可指数化的（exponentiable），且 L 是其对应的多项式函子（polynomial functor）。特别地，研究人员在不假设 ?? 为局部笛卡尔闭（locally cartesian closed, LCCC）的情况下证明这一点。

研究背景：在集合范畴中，对象 X 上的有限列表集合 L(X) 可写成余积 ?_n∈? Xⁿ，故 L 是多项式函子。将“X 上的列表”推广到一般范畴需要列表对象（list object）概念，Cockett 提出的参数化列表对象使研究人员可在具有有限乘积的范畴中构造函子 L。已有关于 L 为多项式的结果通常假设环境范畴为局部笛卡尔闭（locally cartesian closed, LCCC），例如在集合、具有自然数对象（natural numbers object, NNO）的拓扑斯、自由幺半群构造、参数化初始代数等语境中，多项式函子 Σ_n∈N Xⁿ 的存在性先被假定。问题是：能否在不假设 LCCC 的情况下，直接证明 L 是多项式函子，并证明通用有限基数 π₂^E 可指数化。研究人员的结论是，在具有有限极限和参数化列表对象的广延范畴中这一目标可以实现，且该结果意味着 L 是多项式单子（polynomial monad）的一部分。

关键技术方法（不超过250字）：研究人员在具有有限乘积、参数化 NNO 和参数化列表对象的范畴中工作；建立内部语言（internal language）进行变量等式推理；利用列表对象的归纳泛性质定义长度 len、连接 ++、截断 tr、尾 tail、zerothDef、nthDef 等箭头；使用拉回（pullback）、余积（coproduct）稳定性、切片范畴（slice category）、伴随函子（adjoint functor）与普遍态射（universal morphism）构造证明；无样本队列来源，不涉及试剂、培养或质粒构建。

研究结果：5. Proof Setup and Outline：研究人员证明命题 5.1，将主定理化归为证明 L_N 是 Σ_E°Δ_π2^E 的右伴随；并引入弱于广延性的假设 (H1) 与 (H2)，证明广延性可推出二者。定理 5.3 断言在有限极限、参数化列表对象及 (H1)、(H2) 下，L_N 确为该右伴随，证明分三步：构造 nth、构造 h、证明唯一性。

6. Technical Calculations：该节用内部语言重述 (H1) 与 (H2)。命题 6.1 说明正长度列表可分解为 x :: ?′；命题 6.2 与推论 6.3 说明在 (H2) 下可按条件分裂余积；命题 6.4 给出 E×_NA ? {m:N,a:A | m < l_A(a)}；推论 6.7 构造 g′，将有限序列扩展为无限序列，同时保持所需计算性质。

7. Extracting Elements from Lists：研究人员在 (H1) 下构造默认元素 def_X，进而定义 nth_X:E×_NL(X)→X，即取出列表第 m 个元素。命题 7.2 证明这一族箭头给出自然变换 Σ_E°Δ_π2^E°L_N ? Id_??。

8. Constructing Lists and Computing Their Elements：该节引入 Seq[f] 与 List[f,p] 构造，用归纳法从映射 f:N×A→X 和长度 p:A→N 构造列表。命题 8.1 证明 len°List[f,p]=p；定理 8.5 证明当 m < p(a) 时 nth(m,List[f,p](a))=f(m,a)。定理 8.6 在 (H1)、(H2) 下证明存在性：给定 l_A:A→N 与 g:E×_NA→X，存在 h:A→L(X) 使得 l_A=len_X°h 且 g=nth_X°(Id_E×_Nh)。

9. Equality of Lists：该节处理唯一性。定理 9.4 在不假设 (H1)、(H2) 时证明，若 len(h₁(a))=len(h₂(a)) 且 nthDef 对二者一致，则 h₁(a)=_x,ah₂(a)。引理 9.5 在 (H1)、(H2) 下去除额外变量 x，得到 h₁=h₂；引理 9.6 将 nthDef 条件替换为 nth 条件；推论 9.7 证明若 len_X°h₁=len_X°h₂ 且 nth_X°(Id_E×_Nh₁)=nth_X°(Id_E×_Nh₂)，则 h₁=h₂。结合第 8 节存在性，得到定理 5.3，进而得到定理 1.1。

附录 A. Inequality for natural numbers objects：研究人员发展 NNO 上不等式关系的事实，包括 ≤ 与 < 的等化子刻画、≤ 为偏序、算术运算保持不等式、a < b 当且仅当 b?a > 0，以及相关余积与拉回图。

讨论部分与结论翻译：讨论主要体现在 1.3 Comparison to existing results。已有结果在集合范畴、局部笛卡尔闭正相干范畴、具有 NNO 的拓扑斯、自由幺半群构造、参数化初始代数等路径中都假定环境范畴至少为 LCCC。本文的关键区别是只假设列表对象存在，直接证明 π₂^E 可指数化，并证明所得多项式函子同构于 L。由于 L 已知是笛卡尔单子的一部分，定理 1.1 意味着 L 是多项式单子的一部分。假设还可弱化为 (H1) 与 (H2)；广延性推出它们。研究人员指出，为便于叙述未进一步弱化有限极限假设。研究结论翻译为：令 ?? 为具有有限极限和参数化列表对象的广延范畴。则通用有限基数 π₂^E 可指数化，且列表对象函子 L:??→?? 由多项式 ?? ← E —π₂^E→ N → ?? 表示。