良定义 coalgebra 与 König 引理

König 引理是关于具有无数应用的数学和计算机科学中的树的基本结果。以逆否形式表述，它指出：如果树是有限分支且良定义的（即没有无限路径），则其为有限。我们提出了 König 引理的 coalgebra 版本，包含两个维度的泛化：从有限分支树扩展到针对 finitary 内函子 H 的 coalgebra，以及从集合基底范畴扩展到局部有限可呈现范畴 C（如偏序集、名义集合或凸集范異）。我们的 coalgebra 版 König 引理指出：在 C 和 H 上的轻度假设下，每一个针对 H 的良定义 coalgebra 都是其具有有限生成状态空间的良定义子 coalgebra 的唯一向导和。特别是，良定义 coalgebra 的范畴是局部可呈现的。作为应用，我们推导出关于 topos 中图形的 König 引理版本，以及关于名义和凸转换系统的版本。此外，我们表明，关键构造 underpinning 证明的关键构造也产生两种简单的初始代数（等同于最终递归 coalgebra）的构造：初始代数既是所有良定义的且所有递归 coalgebra 具有有限可呈现状态空间的极限。惊人的是，这一结果即使在良定义 coalgebra 是递归 coalgebra 的 proper 子类的情况下也成立。第一种初始代数构造是全新的，而第二种方法则提供了简洁透明的新正确性证明。