König's lemma is a fundamental result about trees with countless applications in mathematics and computer science. In contrapositive form, it states that if a tree is finitely branching and well-founded (i.e. has no infinite paths), then it is finite. We present a coalgebraic version of König's lemma featuring two dimensions of generalization: from finitely branching trees to coalgebras for a finitary endofunctor H, and from the base category of sets to a locally finitely presentable category C, such as the category of posets, nominal sets, or convex sets. Our coalgebraic König's lemma states that, under mild assumptions on C and H, every well-founded coalgebra for H is the directed join of its well-founded subcoalgebras with finitely generated state space -- in particular, the category of well-founded coalgebras is locally presentable. As applications, we derive versions of König's lemma for graphs in a topos as well as for nominal and convex transition systems. Additionally, we show that the key construction underlying the proof gives rise to two simple constructions of the initial algebra (equivalently, the final recursive coalgebra) for the functor H: The initial algebra is both the colimit of all well-founded and of all recursive coalgebras with finitely presentable state space. Remarkably, this result holds even in settings where well-founded coalgebras form a proper subclass of recursive ones. The first construction of the initial algebra is entirely new, while for the second one our approach yields a short and transparent new correctness proof.

翻译：柯尼希引理是关于树的一个基本结果，在数学和计算机科学中有着无数应用。其逆否命题形式表明：若一棵树是有限分支且良基的（即不存在无穷路径），则该树是有限的。我们提出了柯尼希引理的余代数版本，其包含两个维度的推广：从有限分支树推广至有限自函子 H 的余代数，以及从集合的基范畴推广至局部有限可表现范畴 C，例如偏序集范畴、名义集范畴或凸集范畴。我们的余代数柯尼希引理表明：在 C 和 H 的温和假设下，每个 H 的良基余代数都是其具有有限生成状态空间的良基子余代数的有向并——特别地，良基余代数的范畴是局部可表现的。作为应用，我们推导出了拓扑斯中图的柯尼希引理版本，以及名义和凸转移系统的相应版本。此外，我们证明了证明所依赖的关键构造产生了函子 H 的初始代数（等价地，最终递归余代数）的两种简单构造：初始代数既是所有具有有限可表现状态空间的良基余代数的余极限，也是所有具有有限可表现状态空间的递归余代数的余极限。值得注意的是，即使在良基余代数构成递归余代数真子类的情形下，该结果依然成立。初始代数的第一种构造是完全新颖的，而对于第二种构造，我们的方法提供了一个简短且透明的新正确性证明。