闭范畴及其内部函数空间：Eilenberg-Kelly定理的分析与例证

⊗ ×→× → − E−可在www.sciencedirect.com在线获取理论计算机科学电子笔记352（2020）233-256www.elsevier.com/locate/entcs艾伦伯格-凯利Tarmo Uustalu1冰岛首都雷克雅未克理工大学爱沙尼亚首都塔林Niccolo`Veltri2爱沙尼亚塔林理工大学Noam Zeilberger3E'colePolyte chnique，Palaiseau，France摘要Eilenberg-Kelly定理指出，具有对象I和两个函子的范畴C：CCC和：CopCC与B有关联BB中的自然数是么半群，且它是闭的而且附加在内部也成立。我们仔细分析了这个定理的证明，并观察到关于闭性的一个边条件的必要性，因为闭范畴的标准定义在结合性方面是左偏的。 我们分析了Street关于左斜幺半群等价的观察左偏闭性，并建立么半群等价于闭性无条件下的调整定义的封闭性，需要正常的结合性。我们还定义了右斜闭性等价于右斜幺半群。我们给出了每种类型的结构的例子，特别是，我们看了左偏闭范畴上的左强单子的Kleisli范畴和左偏闭范畴上的Kleisli范畴。右斜闭范畴上的松弛闭单子的Kleisli范畴。我们还认为，斜和正常monoidal和封闭范畴的特殊情况下，斜和正常promonoidal范畴，并采取一个简短的看看左斜prounital-closed范畴。关键词：斜和正规么半群，闭，么半群闭和双闭范畴，Eilenberg-Kelly定理，promonoidal范畴，Kleisli构造1引言Eilenberg和Kelly[13]的闭范畴是具有单位对象I和对象A与B之间的内部函数空间AB的范畴。例子包括各种类型的结构化集合，如正规带和偏序集，其中AB1电子邮件：tarmo@ru.is2电子邮件：niccolo@cs.ioc.ee3电子邮件：noam. polytechnique.eduhttps://doi.org/10.1016/j.entcs.2020.09.0121571-0661/© 2020作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。234T. Uustalu等人/理论计算机科学电子笔记352（2020）233是正规带态射的集合（分别为单调函数）之间的A和B和它的正常带（分别。偏序集）结构。 在这种情况下，具有平凡结构的单例集扮演着单位I的角色。作为各种演绎系统基础的范畴，例如简单类型的λ演算，形成了另一类例子。 内部函数空间AB是介于A和B之间的函数类型，而外部函数空间由具有一个自由变量的良好类型项x：At：B组成在这种情况下，对象I是单位类型。在大量的例子中，闭结构（I，）来自于与monoidal范畴（C，I，C）中张量积的ad- junction[2，23]，但是Eilenberg和Kelly对闭范畴的最初定义并不要求范畴中存在monoidal结构。然而，如果范畴C配备了一个单位I和两个函子：C× C→ C和：Cop× C→ C由B中的一个附加函数− <$BEB− natural关联，则（C，I，<$）是么半群的当且仅当（C，I，）是闭的并且附加函数内部成立。这表明C的闭性由于某种原因比么半群弱。仔细观察，内部附加要求是结合子α成为同构的必要条件，正如在幺半群范畴的定义中所要求的那样，这是一个在闭范畴的定义中没有任何东西匹配的条件为了正确理解monoidal和closed结构之间联系的不平衡背后的原因，开始考虑monoidal和closed范畴的弱变体是有帮助的：Szlachanyi[30]的左斜monoidal范畴和Street [29]的左斜closed范畴。左斜么半群范畴是么半群范畴的一种弱化，其中单位子和结合子不需要是同构，而仅仅是在特定方向上的变换。斜幺半群范畴在许多情况下自然出现，例如在相对单子[1]和量子范畴[17]的研究中，并且已经被Street，Lack及其同事[18，7，4，5]彻底研究过。在以前的工作中，我们对左斜monoidal范畴的相干性的研究做出了贡献，首先采取重写方法[31]，后来使用证明理论技术[35，32]。左斜闭范畴是闭范畴的类似弱变体。Street[29]证明了Eilenberg-Kelly定理的一个变体，指出，给定一个附加项--EB−natural inB，（C，I，n）是左斜幺半群当且仅当如果（C，I，）是左斜闭的。 至关重要的是，原始的Eilenberg-Kelly结果不再存在。在本文中，我们继续由街发起的工作路线左斜么半群范畴不同于正规么半群范畴，因为它的两个单位子和结合子都不可逆。当一个或多个结构律是可逆的时，所得到的范畴是“更正常的”，在这个意义上，它的monoidal结构不那么偏斜，它看起来更像一个通常的monoidal范畴。类似的正态度也存在于左偏闭范畴和适当闭范畴之间。我们证明了Street的左斜变体的一个改进版本T. Uustalu等人/理论计算机科学电子笔记352（2020）233235Eilenberg-Kelly定理：C上的左斜monoidal（I，n）和左斜闭（I，n）结构在有一个附加函数− <$BEB−的情况下不仅存在同构，而且（I，n）上的每个正规性条件都对应在（I，）上的正规性条件。这使我们能够外推一个对应于结合子α可逆性的闭结构要求，它等价于内部附加的存在，但它完全可以用闭结构来表示，并且当范畴C缺乏幺半群结构时也可以公式化左斜闭范畴的这种关联正态性条件首先由Day和Laplaza发现[10，12]，但在后来的文献中没有被注意到。左斜闭范畴的正规性对应于其结构律的可逆性 通过丢弃这些定律而保留它们的逆定律（因此新的定律与原来的定律指向相反的方向），我们得到了右斜闭范畴的新概念。我们证明了一个右斜变形的街定理连接伴随右斜monoidal和右斜闭结构的范畴，和他们的正规性条件之间的类似关系。更有趣的是，我们观察到当C具有同构σA，B，C：C（A，BRC）→ C（B，ALC）自然于A，B时，范畴C上的左斜闭（I，L）和右斜闭（I，R）结构是双射对应的和C.我们称后一个要求为（外部）Lambek条件，因为它类似于Lambek语法演算的特征在整个文件中，我们讨论了大量的例子，特别是 为激发不同的正规性条件和右斜闭范畴的新概念。我们证明了左斜闭范畴上的左强单子的Kleisli范畴继承了左斜闭结构。我们还看到了范畴C上的右斜闭结构如何提升到C上的松弛闭单子的Kleisli范畴。我们讨论了进一步倾斜倾斜闭结构的可能方法：使用lax闭comonad，我们可以将左闭结构进一步向左倾斜（Street [29]也讨论了一个例子），而使用oplax闭monad，我们可以将右闭结构进一步向右倾斜。左斜闭范畴的另一个例子，实际上是一个生成元集合上的自由左斜闭范畴的表示，由单位类型的非交换线性类型λ-演算给出基于Day [10]的一个旧观察，Street注意到左斜monoidal和左斜闭范畴都是作为一般范畴的特殊实例出现的。左斜promonoidal范畴的概念[29]，其中单位I和函子分别用函子J：C→Set和分配器P：Cop× Cop×C→Set代替. 通过选择P（A，B; C）= C（A，BC.降低代表性条件，得到左斜闭范畴的另一个自然变体，Shulman的原单位闭范畴的左斜版本49]。这类范畴的一个典型例子来自于没有单位类型的非交换线性类型λ236T. Uustalu等人/理论计算机科学电子笔记352（2020）233、、⊗⊗（A）一（C）2左斜Monoidal范畴与闭范畴Szlach′anyi定义2.1左斜monoidal范畴是一个范畴C加上一个区别对象I，一个函子 C×C→ C和三个自然变换λ，ρ，αλA：I<$A→AρA：A→A<$IαA，B，C：（A<$B）<$C→A<$（B<$C）满足方程（m1）I（m2）（A<$I）<$BαA，I，B<$A<$（I<$B）（m3）（I）BαI，A，B中文（简体）ρIλIρABAλBt\cλA<$B z，sλA<$BI IIAA组B组A组B组（m4）（A<$B）IαA，B，I A、、、ρABAρBA组B组（m5）（A<$（B <$C））<$DαA，B<$C，D<$A<$（（B<$C）<$D）αA、B、C和D（（AB）C）αA<$B，C，D<$<$B）<$（C<$AαB，C，DαA，B，C D（B cD））注意，（m1）后来，Kelly[15]观察到当α，ρ和λ是自然同构时，定律（m1），（m3）和（m4）可以从（m2）和（m5）导出，但对于左斜monoidal范畴，情况并非如此在这里，我们提出了左斜monoidal范畴的一系列例子，它们在各种不同的背景下自然出现[30，17，7，31]。例2.2点集和点保持函数的范畴Ptd具有以下左斜monoidal结构。取I=（1，n）和（X，p）n（Y，q）=（X+Y，inlp）（注意选择点时的我们定义λX：（1，n）<$（X，p）=（1+X，inl <$）→（X，p）通过λX（inl <$）=p，λX（inrx）=x（这不是单射的）。 令ρX：（X，p）→（X+ 1，inlp）=（X，p）<$（1，<$），通过ρXx =inlx（这不是满射）。最后，设αX，Y，Z：（（X，p）<$（Y，q））<$（Z，r）=（（X+Y）+Z，inl（inlp））→（X+（Y+Z），inlp）=（X，p）<$（（Y，q）<$（Z，r））为显同构.例2.3给定一个左斜monoidal范畴（C，I，C）和一个余单子D，C.假设D是lax monoidal，即，有一个映射e：I→DI和一个自然变换m：DA<$DB→D（A<$B），它与λ，ρ，α，ε，δ相一致。 则范畴C也有一个左斜幺半群结构（I，D），其中DD）、T. Uustalu等人/理论计算机科学电子笔记352（2020）233237DAIAAρA一A、B、C甲乙丙TRmstTAB⊗一⊗一T（A）一ADB=AD B 单位和联合单位如下：D=I<$I <$εA <$λA<$ D=AρAAIAeADIDA，B，C=（A<$DB）<$D C（A<$DB）<$δC<$（A<$DB）<$D（DC）αA，DB，D（DC）<$A<$（D B<$D（DC））AmB，DCAD（BDC）通过取AT<$B=T A<$B，从C上的oplax monoidal monad（T，e，m）得到一个类似的左斜monoidal范畴.（稍后，在例4.10中，我们将取A<$TB = A<$T B，在给定的右斜幺半群范畴（C，I，）上产生一个新的右斜幺半群结构。）例2.4给定一个左斜monoidal范畴（C，I，n）和C上的一个monadT。假设T是laxmonoidal，即，带 有一个映射 e：I→TI和一个自 然变换mA ， B： T A<$T B→T（A<$B），它与λ，ρ，α，η，μ相一致（事实上，与η一致使得e是多余的，因为它迫使e=ηI）。则Kleisli范畴Kl（T）有一个左斜monoidal结构（I，<$T）其中A<$TB=A<$B，（f：A→TAJ）<$T（g：B→TBJ）=A<$Bf<$g<$TAJ<$TBJmA′，B′<$T（AJ<$BJ）单位元和结合元是纯的，直接取自基本范畴：不 =J λA，ρT=J ρA，αT=J αA，B，C其中J：C→Kl（T）为左伴随在Kleisli附连中，JA=A，J（f：A→B）=ηB<$f.代替松弛么半群，可以要求T是左强和右强的，即，自然变换mstA，B：A<$TB→T（A<$B）mstR：T A<$B→T（A<$B）分别与λ和λ相一致ρ和α、η、μ。这些自然变换还必须通过α（双强度方程）和通过μ（交换性方程）：mstA，BCmstRB，C（A）B）CαA，T B，CT（AT（（ATαA、B、CcmstcA（TBC）B，CT（BC）A，BC（BMSTT B T（TAB）A，BmstA，TB CTmstT T（A B）μμA/BT（A<$TB）A，B<$T T（A<$B）ABT（AcB）以这种方式彼此一致的T的左强度和右强度对（mst，mstR）与松弛幺半群见证人m处于双射对应。在没有交换性的情况下，（Kl（T），I，Kl（T））不是左斜么半群，实际上，Kl（T）甚至不是双函子;我们只是通过扩展Power和Robinson的术语得到了一个可以称为左斜预么半群的结构[26]。λαλ一238T. Uustalu等人/理论计算机科学电子笔记352（2020）233JAB4CCI（A）C）、我D）、（二）B）、例2.5考虑具有函子J：J → C的两个范畴J和C，并假设左Kan扩张Lan JF：C →C对每个F：J → C都存在。则函子范畴[J，C]有一个斜幺半群结构由I = J，FG=F·JG=LanJF·G给出.单位子和平衡子是正则自然变换λF：Lan JJ·F→F，ρF：F→ Lan JF·J，αF，G，H：Lan J（Lan JF·G）·H→Lan JF·Lan JG·H。这个例子来自Altenkirch et al.[1]的相对单子工作。J上的相对单子是左斜幺半群范畴[J， C]中的幺半群。左斜闭范畴是由斯特里特[29]引入的，作为艾伦伯格和凯利[13]闭范畴的一个变体。Zeilberger考虑了左斜闭范畴的一个posetal变体，他称之为imploids[34]。定义2.6左斜闭范畴是一个范畴C加上一个区别对象I，一个函子：Cop×C→C，以及三个自然变换j，i和L类型jA：I→A一i 答：我A→ALA ， B ， C：BC→（AB）、（阿、中）满足法律（c1）IjIi i I（c2）ACLA，A，C（AA）（阿、中）jA（AC）IzA、i、A、C 、c(c3)BLA，B，B（AB）（AB）（c4）BCLI，B，C 中文（简体）B）、（一C）iBCzt，（IB）iCI（IB）、C（c5）CDLA，C，D（AC）（AD）LA细介绍C、ADLB、C、D（（AB）、（A）（C））（（AB）、（A）（D））LA，B，C（（AB）、（A和D））（二）C）、（BC）LA，B，DC）（（Ac（A）（D））给定一个具有I的范畴C，自然变换j和L可以与自然变换^A，B ：C（A，B）→C（I，A）B）、L^A，B，C，D：<$XC（A，XD）×C（B，CX）→C（A，B（CD））[4]实际上，j和L是[29]第29话我们省略“额外的”形容词，把这些简单地得双曲余切值.JBC（二）T. Uustalu等人/理论计算机科学电子笔记352（2020）233239、、^ ^您的位置：AAA、B、C其中整数符号表示余尾。这是因为以下双射序列：5C（A，B）j^A→，B C（I，AB）IjBEC（A，ED）×C（B，CE）L^A，B→，C，DC（A，B（CD））C（A，E）D）× C（B，CE）→C（A，B）（C和D））C（A，E）D）→B C（B，CE）CQC（A，B）（C和D））C（A，E）D）→ C（A，（CE）的（C和D））LC，E，D→BBED→（CE）的（C）D）、解释性，jA，Bf = Af∈jA和LA，B，C，D（E，f，g）=g（CD）C，E，D.左斜闭范畴的例子在文献中并不常见左斜幺半群范畴然而，它们也很自然地出现，如下面的例子所示。第一个例子是来自Street [29，命题3]。例2.7给定一个左斜闭范畴（C，I，）和它上面的一个comonadD。假设D是lax闭的，即，带有映射e：I→DI和自然变换cB，C：D（BC）→DBDC相干（如适用），j、i、L、ε、δ。则范畴C也有一个左斜闭结构（I，D），其中BDC=DBC。左斜闭范畴的定律定义如下：Dj=IJAAAεA AIAA.A.DL=D BCLDA，DB，C（D ADB）（D C）（δADB）（D AC）、D（DA）DB）D ACc（DAC）D（DA B）（DA C）例2.8给定一个左斜闭范畴（C，I，）和其上的单子T。假设T是左强的（或内部函子的），即，具有自然的转换cstA，B：BC→T BT C与j、L、η适当地一致，μ。单子T是内部函子的和它是内部Kleisli的是一样的，即，配备了一个自然变换iextB，C：BT C→T BT C，满足Kleisli扩张系统a`laManes[25]（a.k.a. 无迭代形式的单子）：T的左强度cst和内部Kleisli扩张iext是双射对应的。则Kl（T）有左斜闭结构（I，T），其中BTC=BT C[5]在本文其余部分中，双射序列中的所有线代表在所有自由对象变量中自然的映射族。240T. Uustalu等人/理论计算机科学电子笔记352（2020）233T C T BT CBTT CBTC）T C T BLA，TB，TC一和（g：BJ→T B）T（h：C→T CJ）=J（BiextB，CgT hjJB′μC′jJ它的结构规律由以下定义：jT=J（IjA AAAηAATA）iT=ITAiT ATA一T A，B，C =J（BiextB，CiextB）一TC（A）T B）（A）T C）（AT B）ηATC<$（ATB）T（ATC） ）值得注意的是，所有gT h，jT，LT是纯映射（其中映射gTh是A A，B，C纯的，即使G和H不是），即，在左伴随J：C→Kl（T）的像中，克莱斯利的附加条款 只有地图iT是不纯的。例2.9用单位型非交换线性型λ-演算给出左斜闭范畴的另一个例子。类型由文法A，B：：= X生成|我|AB，其中X是原子类型。上下文是类型的列表。格式良好的术语构造如下：x：Ax：A：I我：Δu：AΓ， Δ让 =tinu：Ar，x：A，t：BΓ λx. t：AB联系我们BΔu：AΓ，Δtu：B项的定义相等由βη-相等给出（Hyland和de Paiva [14]的项相等的非交换变体）。自然变换j、i和L可导出如下：x：Ix：Iy：Ay：Ax：I，y：A小程序<$i=xiny：Ax：I= λy。设x=xiny：A一徐：我阿扎克斯：我一我：徐：我AiA=x：Ay：AB组：A组Bz：Az：Ax：BCx：BCy：AB，z：Ayz：Bx：BC，y：AB，z：Ax（y z）：Cx：BCLA，B，C= λy.λz。x（y z）：（AB）（AC）原子类型集At上的单位型非交换线性λ-演算是由At生成的自由左斜闭范畴的具体表示。下面的定理来自Street[29]（模关于内部右转置的观察，这不是显式的）。定理2.10设C是具有对象I和函子<$的范畴：C×C → C和：C op× C → C，在B中加上一个附加词−BEB−natural。则（C，I，n）是左斜么半群当且仅当（C，I，n）是左斜闭的。 更精确地说，（λ，ρ，α）左斜幺半群与（j，i，L）左斜闭结构之间分别存在一个双射.（C，I，）。LT. Uustalu等人/理论计算机科学电子笔记352（2020）233241^^一此外，α和L也可以用自然变换来定义。pA，B，C：（AB）C→A（BC）（右转置πA，B，C的内部版本：C（A<$B，C）→ C（A，BC））。结构的双射实际上更精细。首先，λ和j数据、ρ和i数据以及α和L数据（以及p）之间存在三个独立的双射。第二，方程（m1-m5）和（c1-c5）也彼此成对地蕴含。所以整体的双射是存在的，甚至在部分结构之间。证据上述数据对之间的必要双射由下面的双射序列得出。这些对于仅向前方向上的自然变换（与此相关）、对于两个方向上的自然变换，特别是自然同构（与下面的定理3.8、4.11相关）以及仅向后方向上的自然变换（与定理4.8相关）都成立。ρAλA«AIIA«AC（A，B）<

下载后可阅读完整内容，剩余1页未读，立即下载