没有合适的资源?快使用搜索试试~ 我知道了~
128《理论计算机科学电子札记》44卷第1期(2001)网址:http://www.elsevier.nl/locate/entcs/volume44.html18页代数、余代数、单子和余单子NeilGhania,1ChristophLu?thb,2FedericodeMarchia,3,5John Powerc,4一 莱斯特大学数学与计算机科学系bFB3-MathematikundInformatik,UniversitaütBremenc爱丁堡大学计算机科学基础实验室摘要虽然初始代数和单子之间的关系已经很好理解,但最终余代数和余单子之间的关系还没有很好地探索。本文表明,这个问题是更微妙的,最终余代数可以很容易地形成单子作为comonads和对偶,初始代数形成单子和comonads。在发展这些理论的过程中,我们努力为它们提供一个相关的句法概念在初始代数和单子的情况下,这对应于由签名和方程组成的代数理论的标准概念:这样的代数理论的模型正是表示单子的代数。我们试图通过定义一个概念cosignature和coequation来模拟这个结果,然后证明这个语法的模型正是表示comonad的coalgebra。1介绍虽然闭函子的余代数理论已经很成熟,但对余代数的研究却很少。我们觉得这是一个遗憾,因为集合上单子的对应理论解释了泛代数的关键概念,如签名,变量,项,替换,方程等。此外,在许多情况下,对集合以外的基范畴的应用已被证明是富有成效的例如研究多排序代数理论作为单子集A,顺序排序理论作为单子集Pos,研究范畴与结构1电子邮件地址:ng13@mcs.le.ac.uk2电邮地址: cxl@informatik.uni-bremen.de3 电子邮件地址:fdm2@mcs.le.ac.uk4电子邮件地址:ajp@dcs.ed.ac.uk5由EPSRC资助的研究GRM 96230/01:分类重写:Monads和模块化2000年1月,出版社dbyElsevierScienceB。 V.操作访问和C CB Y-NC-ND许可证。GHANI,LÜTH,DEMARCHI,POWER129××A → A使用图或猫上的monads[8],使用Pre或Cat上的monads重写的研究 [16,17]以及使用F[9][我们的目标是一个类似的框架,基于comonads的理论,解释- ing上述概念的coalgebraic之间的关系,并奠定了基础的应用程序中的类别除了集。本文是朝着这个方向迈出的第一步。传统上,人们从一个签名T开始,然后为每个变量集合X,定义术语代数T(X)。下一个定义替换,并显示这与作为左和右单位的变量相关联最后,给定方程E,我们还定义了商代数T∈E(X)。将泛代数的这种处理推广到不仅包括具有额外结构的集合,而且还包括其他数学对象的代数结构,可以使用这些思想的范畴重新表述来在这个范畴框架[14]中,人们从签名f中构造了一个内函子Ff(可以认为它将变量的对象X发送到深度为1的项,其中变量来自X)。术语代数T可以被描述为F上的自由单子。作为一个单子给了T一个很好的替换概念,而自由则抓住了代数这个术语的归纳性质通过将代数理论的方程解释为两个自由单子之间的单子态射对,由方程诱导的商代数被建模为它们的余均衡器。重要的是,代数理论的模型同构于代表代数理论的单子的代数的Eilenberg-Moore范畴我们的目的是二元化这种范畴治疗的普遍代数,特别是得出coalgebraic的上述关键概念。因此,我们首先需要对偶化一个签名上的内函子的构造事实证明,存在不止一种可能的二元论,这就是本文的主题 例如,给定一个有限内函子F:,可以考虑将对象X发送到初始X +F-代数的底层对象的映射,将X发送到最终X+F-余代数的底层对象的映射,将X发送到初始XF-代数的底层对象的映射,以及将X发送到最终XF-余代数的底层对象的映射。这四个映射中的每一个都形成一个单子或一个共单子,如表1所示因此,也许不是一个二元论在起作用,而是两个可能的、正交的二元论,给出了四个值得我们注意的概念。我们并不认为本文对上述问题提供了完整的答案然而,我们确实认为,我们解决的问题将是根本的重要性,以CMCS的观众,我们的方法是新颖的,比大多数更抽象。特别是,我们希望我们的概念的共同签名,coequations和分类表示这种语法通过comonads将普遍感兴趣,并刺激进一步的研究。GHANI,LÜTH,DEMARCHI,POWER130AADD◦B C → A CA → BCN → A A → AAMonads科莫纳德初始代数µY。X + FYµY。公司简介最终余代数是的。X +FY是的。公司简介表1构成单子和余单子的代数和余代数本文件其余部分的结构如下:Sect.2、初步定义。节中3,我们简要回顾了我们在本文其余部分(表1左上角的条目)中寻求二元化的fifentarymonads的表示第4节和第5节探讨了对偶化的不同可能性,第4节探讨了表1的左下角,第5节包含了我们提出的共代数语法以及相关的表示和正确性结果(表1的右侧2初步定义和符号我们假设读者熟悉标准范畴理论,可以在[18]中找到。为了从集合范畴中抽象出来,我们不得不使用某些结构,有些读者可能并不完全熟悉这些结构。我们在这里给出一个简短的定义;更多的细节可以在[18,3]中找到。局部可表示范畴和局部可表示范畴:设κ是正则基数。一个图是κ-过滤的,如果每一个具有小于κ个对象和态射的子范畴在中有一个相容的余锥。一个范畴的对象X称为κ-可表示的,如果hom-functor(X,)保持κ-过滤余极限。一个范畴是局部κ-可表示的(简写为lκ p),如果它是余完备的,并且直到同构,有一个κ-可表示对象的集合Nκ,使得每个对象都是来自Nκ的对象的κ-滤余极限。一个范畴是κ-可达的,只要它是lκ p,除了它只有κ-过滤的上极限而不是所有的上极限。一个函子是κ-可达的,如果它保持κ-过滤的余极限;我们也说它有秩κ。Nκ上的离散范畴记为Nκ。充分κ-可表示对象的子范畴记为Aκ。包含函子记为Jκ:κκ和Iκ:κ.当=集合,集合N<$0可以被认为是我们表示为N的自然数。Kan扩张:给定一个函子I和一个范畴,用F定义一个函子 我:[ 、 ][ 、 ]. 左和右Kan扩张的问题是寻找左和右伴随的问题,◦ I. 更具体地,给定函子F:A → C,左和右KanGHANI,LÜTH,DEMARCHI,POWER131def→∈联系我们→T扩张满足自然同构[B,C](LanIF,H)=[A,C](F,H<$I)[B,C](H,Ra nIF)=[A,C](HnI,F)。Kan扩张可以使用上极限和极限来逐点给出,或者更优雅地使用端点和余端点(详见[18,第X章])。3初始代数与单子我们首先回顾一下集合范畴上的(无穷)单子与泛代数之间的著名等价性,以及这种等价性对局部可表示范畴的推广[14,21]。我们用一个特定的例子来说明这些想法,使用Set作为基本范畴-其他基本范畴的例子可以在[21,8]中找到。签名声明了从中构造项的操作通常,签名是作为一组操作和一个函数给每个操作分配一个arity,但我们可以等价地认为它是一个函数n:NSet,为每个arity分配该arity的操作集。为了从集合范畴中抽象出来,我们需要一个适合于不同范畴的arity概念。关键的观察是,Set中的通常的arity,即自然数N,表示Set中的有限可表示对象。因此,lκ p-范畴中的零的自然概念是集合Nκ。因此,签名是一个函数:Nκ→|一|,它等价于一个函子:Nκ→A:定义3.1(签名)设A是lκp范畴。一个签名是一个函数<$:Nκ→ A,并且<$的e元运算的对象是<$e=<$(e)。我们现在提出两个这样的签名的例子,我们稍后将增加适当的方程。例3.2(幺半群)幺半群理论的签名<$M:N→集合定义为<$M(0)= e,<$M(2)= m,m(n)= 对于所有其他的N。因此,BRM声明了一个arity为0的操作e(一个常数)和一个二元操作m。例3.3(有T的范畴)有终结对象的范畴可以看作是Cat上的代数范畴。 签名RINT必须声明终端对象,并且对于每个对象X,声明唯一的映射!X:X。 因为终端对象不依赖于任何数据,所以它的arity是空类别0。 从地图开始!X依赖于一个对象,它的元数是一个对象范畴1。因此,T(0)= 1,T(1)=(→)(即, 具有两个对象和一个箭头的类别),而对于所有其他可表示的类别c,则T(c)= 0。现在我们转向构造一个在签名上的内函子GHANI,LÜTH,DEMARCHI,POWER132E N A → AA不一在Set上工作,例如见[23],一个定义函子F(X)=Xnf∈N(n)其计算深度1的项,其变量来自集合X。例如,给定例3.2的签名,关联的内函子是FM(X)= 1+X2。这样的多项式内函子(即,由乘积和余积构建的)已知保持所有κ-过滤余限-这是一个重要的性质,稍后将确保可以容易地计算自由单子不幸的是,目前还不清楚如何将其推广到集合以外的类别,因此我们采取了另一种方法。回想一下,通过定义,左Kan扩张左伴随于限制LanJκJκ:[κ,] [κ,],因此我们定义F(X)=(LanJκ)X(1)左Kan扩张的标准公式表明,在A=Set的情况下,F的两个定义都一致,如例3.2所示:(LanJ<$0<$M)X=n∈N集合n 0(n,X)×nM(n)=Set(0,X)×1+Set(2,X)×1=1 +X2注意F的定义域是Aκ而不是A,因此F不是闭函子。然而,一个内函子F:A → A是κ-可达的,如果它是(同构于)它对Aκ的限制的左Kan扩张;因此,在κ-可达的内函子和函子Aκ→ A之间存在一个等价关系(2),我们可以把Fκ看作一个κ-可达的内函子。◦ 我的天[A,A]κπ兰岛[Aκ,A](2)概括一下,我们已经给出了lκ p-范畴上签名的抽象定义和签名上相关的内函子F的构造。在集合的情况下,这些定义和构造与通常的定义一致于是,相关项代数T:A → A是闭函子F上的自由单子,有多种构造方式:引理3.4设F是lκp-范畴上的κ-可达内函子。 则F上的自由单子T满足(i) 对于A中的每个X,TX是初始X + F-代数的载体。(ii) 从F-代数范畴到A的遗忘函子U:F−Alg→ AA有一个左伴随L,且T=ULGHANI,LÜTH,DEMARCHI,POWER133⬦fI⊥κ→(iii) T是<序列 Si的上极限colim i κ Si,其中S0=JSn+1=J+F SnSλ=colimSi(3)i λF,E:A→A的组成为F∈E=def(LanF. E)的情况。证据大部分的证据都是标准的,可以在[14,12]中找到。然而,请注意,在最后一个主张中,为了计算自由单子,我们开始形成内函子序列Si,并且我们不需要比κ-过滤的colimi κSi更进一步,因为F是κ-过滤的。因此T是κ-可达的,因此与F具有相同的秩。✷当我们在第5节中谈到这个构造的对偶时,像上面这样的构造将是不可能的,因为人们会对上链的极限感兴趣,并且没有理由让一个可达的内函子保持这样的极限。结果表明,可达内函子上的余自由余子的秩可以增加.这种等级的变化是技术上的困难,这将出现在第。五、我们得到了(4)中的两个推论,它们构成了一个附加项,F−−|签名和单子之间的U。[N,A]LanJ⊥◦ Jκ[Aκ,A]H(4)温度范围V引理3.4中(3)中的序列Si称为自由代数序列[12]并且可以看作是初始X+F代数的一致计算。作为这种构造的一个例子,考虑签名CARM。正如我们已经看到的,Lan JM(X)= 1 + X2。然后,自由代数序列专门化为S0X=X,Sn+1(X)=X+e∈NA(e,Sn(X))×M(e)=X+1 +Sn(X)由此我们可以看出,Sn定义的深度项最多为n,例如:S0(X)包含变量X,S1(X)包含变量X,1的标准元素代表幺半群的单位,S0(X)的一对元素可以被认为是这些元素的乘积在这个框架内,给出方程就是给出另一个签名E和两个自然变换σ,τ:EUFB。人们应该把E看作是给出方程的形式,而σJ和τJ则是实际的方程。例3.5给出幺半群的例子,我们想要断言三个等式:左单位、右单位(都是一元)和结合性(三元)。 因此,对于所有其他n,我们设置E(3)={a},E(1)={l,r}和E(n)={l,r}。2GHANI,LÜTH,DEMARCHI,POWER134→一N → A一⇒A→→ ∈ AAσ和 τ分别定义方程的左侧和右侧σ(l)=m(e,x)σ(r)=m(x,e)σ(a)=m(x,m(y,z))τ(l)=xτ(r)=xτ(a)=m(m(x,y),z)例如3.3,需要一个方程来强制唯一性!× ×:X→T,即!Y. f=!X对于所有f:X→Y(详见[8])。这种方程定义的优点是它允许一个代数理论的表示单子的优雅推导:给定这样一个理论σ,τ:E UFB,在附加式(4)下,我们有两个单子态射σJ,τJ,它们的余均衡器是表示单子T。这种构造是有意义的,因为代数理论的模型范畴同构于表示单子的Eilenberg-Moore范畴。在(4)中,两个代数都是一元的,它们的合成是下降型的,这意味着数εB:FUB的每个分量都是一个余均衡器。这意味着每个κ-可达单子T=(T,η,μ)在是两个签名B,E上的两个自由单子的余均衡器:在上的κ-可达单子范畴中,或者每个单子都由这个一般意义上的方程表示4末余代数与单子给定一个签名f,我们构造了一个关联的内函子Ff,它可以被认为是计算深度为1的闭项。通过在复合下封闭F,或者更正式地通过考虑F上的自由单子,我们得到术语代数T。具体地,T<$X是初始X+F<$的载体-代数在这一节中,我们研究了映射T∞将对象X发送到最后的X+F余代数的载体,并应用我们的结果简化最近的一些发展是函数式编程语言中的惰性数据库的语义。引理4.2的一个更一般的版本出现在[1]中,并隐含在[20]中。在比较μY.X+FY和νY.X+FY时,第一个观察结果[5]是,集合闭函子的最终余代数可以被视为初始代数的柯西完备化。因此,如果F由一个签名产生,因此μY.X+FY是通常的项代数,那么νY.X+FY是有限项和无限深项的集合。文[2]将这一结果推广到了lfp范畴本节的目的是确定将X发送到最终X+F余代数的载体的映射所具有的结构我们的答案是,这个映射也形成了一个单子。为了证明这个结果,我们使用下面的结果[2]:引理4.1假设是lfp,即唯一映射! :01是强单态映射,F保持monos和ωop-链,且存在映射p:1F 0.则对于每个对象X,(X,μF)和(X,νF)是度量空间,后者是前者的柯西完备化。GHANI,LÜTH,DEMARCHI,POWER135一一不/我们用这个结果来证明我们的主要引理:引理4.2设F是多项式内函子,且满足引理4.1的前提。 则将对象X赋给最终X+ F-余代数的载体的映射T ∞具有单子的结构。证据我们实际上证明了case = Set的引理,因为一般情况下涉及到稍微笨拙的hom-sets推理,但完全类似。本文通过构造T∞的Kleisli结构证明了T∞是单子,即通过定义下列运算:i)对于每个对象X,一个函数ηX∞:X→T∞X; ii)对于每对对象X,Y,一个函数sX,Y:A(X,T∞Y)→ A(T∞X,T∞Y),使得sX,X(ηX∞)=1T∞X sX,Z(sY,Zg<$f)=sY,Zg<$sX,Yf sX,Y(f)<$ηX∞=f首先定义ηX∞=<$X<$ηX,其中η是F上自由单子的单位,<$X是初始X+F-代数与最终X+F-余代数之间的唯一比较6接下来定义sX,Y(f)如下XηXTXX∞Xf![f,h]❄T∞Ys(f)=![f,h]其中h:FT∞Y→T∞Y是由T∞Y的结构映射导出的明显映射。 则[f,h]:X+FT∞Y→T∞Y赋予T∞Y一个X+F-代数结构,从而导出一个唯一映射![f,h]:TX→T∞Y.图追逐显示![f,h]关于相关度量是一致连续的,因此根据引理4.1,存在一个扩展!X[f,h]可以称为X ,Y(f). 第一个方程是唯一的![ηX∞,h]=<$X,<$X的扩张是恒等式.方程sX,Z(sY,Zg<$f)=sY,Zg<$sX,Yf成立,如果它们的限制条件为X是相同的,这反过来又成立,如果它们产生于T∞Z上的相同代数结构。这是因为这两个代数结构都是从映射sY,Z(g)<$f:X→T∞Z继承的。最后一个方程如下,因为sX,Y(f)<$ηX∞=sX,Y(f)<$ηX<$ηX=![f,h]ηX=fη与单子T不同,单子T∞的秩比F大:引理4.3设F是集合上的多项式闭函子。然后单子T∞的秩为1。证据 引理可以直接使用极限和过滤余极限之间的交换律来证明。✷6实际上应用引理4.1要求X+F 0非空,这是当X = 0时的情况。因此,必须分别建立映射η0∞和s0,Y及其性质,但这一切都是从0的初始性出发的GHANI,LÜTH,DEMARCHI,POWER136⊥∀∀← ← ←···⊥注意引理4.2表明没有必要为单子T∞建立一个新的syntax,因为规范syntax应该是相关单子T∞的有限和无限深度项。最后,我们将这个结果应用于函数式编程中的推理。4.1通用近似引理通用近似引理[10]是一个在惰性函数式编程语言(如Haskell)中推理函数近似引理本身适用于给定函数的列表和状态近似值(n+1)[]=[]近似(n+1)(x:xs)= x:(近似n xs)两个列表xs和ys是相等的。大约nxs =大约nys。注意缺少基本情况:大约0 x是(即,unfined的表示),但由于不严格,定义了约nx(n>0)。这一原则也适用于其他数据库,如树:数据树a =叶子a|节点树一棵树近似(n+1)(叶子x)=叶子x近似(n+1)(节点l x r)=节点(近似n l)x(近似n r)两棵树t1和t2是相等的。 约n t1 =约n t2。[10]使用函数式编程语言的标准指称语义证明了通用近似引理,其中类型被解释为CPO也就是说,证明原则的正确性取决于所选择的语义范畴;我们已经看到了在定义上,近似。我们提出了一种替代方案,我们相信,更自然的推导的近似引理是独立的特定的指称模型选择。多态数据类型的定义通常被解释为在其签名上的自由单子T。然而,这并没有捕捉到懒惰,因为T只由有限的术语组成。相反,我们对这样一个数据t由单子T_∞表示。由于T_∞(X)是最终的X+ω-余代数,并且F_∞是一个多项式内函子,所以T_∞(X)可以被计算为下列ωop-链1的极限(X+F)1(X+F)21.极限的普适性质表明,这个极限的两个元素x和y将是对于每个n,πn(x)=πn(y),其中πn是第n个投影。但这些投影恰恰是数据类型的近似函数请注意,分类参数如何使用以1开头的共链来替换对的语义依赖 这建立了独立于任何特定指称模型的通用近似引理的正确性。更一般地说,像Haskell这样的懒惰函数式语言将各个方面适当地由monad建模(被有限地生成),而其他方面则更适当地由最终语义(懒惰和非终止)捕获。GHANI,LÜTH,DEMARCHI,POWER137×一A → AA A →AA → A5最终余代数与余子群现在我们转向第3节的另一种可能的对偶,它基于这样的思想:对于某个κ-可达函子F,将对象X映射到最终X的F-余代数的载体上。优雅的一元方法代数理论表明,我们可以应用这些技术的发展coalgebraic语法的二元化他们appropriately。5.1余签名及其余代数回想一下,泛代数的范畴方法的核心是ad- junction(4)。本节中概述的对偶可以总结为用右伴随替换U的左伴随,并用共单子替换单子。因此,共同签名的定义在形式上与签名的定义相同定义5.1(余签名)设A是一个lκ p-范畴,其基数为Nκ。一κ-cosignature是函子B:Nκ→ A。回想一下,在第3节中,我们首先通过左Kan扩张,然后使用等价性,从签名构造了一个κ-可达内函子(2)得到一个κ-可达的内函子因此,在这一节中,我们取一个余签名B的右Kan扩张来得到一个函子RanJκB:κ,然后用同样的等价来得到一个上的κ-可达内函子。右Kan扩张的标准公式给出了(RanJκB)(X)=c∈NκA(X,c)MBc其中,UMB是B的U重积,或者更正式地说,是函子[U,(,B)]的表示对象:Set。当=Set时,则该操作只是取幂,即UMB= [U,B]。因此,虽然签名和共同签名在形式上是相同的,但它们生成的内函子是非常不同的。例如,请注意,虽然签名的默认值为0,但如果存在单个元数c使得B(c)= 0,则(RanJκB)(X)= 0。实际上,由于UM1 = 1,所以联合签名的默认值是1,因此如果c是一个元数,使得B(c)= 1,那么这个元数对右Kan扩展没有任何贡献。下面是两个示例共同签名,我们将在下面进一步探讨:例5.2定义连署式Bp,对于所有其他的情况,定义为Bp(2)= 2和Bp(c)=1。 则Ran JκBp(X)=[Set(X,2),2]=[[X,2],2]。对于所有其他的点,定义余签名Bpω(2)= ω和Bpω(c)= 1。则(Ran JκBpω)(X)=[Set(X,2),ω]=[[X,2],ω]。回想一下,为了把函子κ变成κ-可达的尾函子,需要取它的左Kan扩张。给定一个余签名B,我们可以考虑闭函子LanIκ RanJκB的余代数。以下是GHANI,LÜTH,DEMARCHI,POWER138−−→→→一个重要的结果[11]:引理5.3设F:A → A是局部可表示范畴上的可达内函子.则F−coalg是局部可表示的,并且F − coalg的κ-可表示对象仅仅是那些其底层对象在A中是κ-可表示的余代数。证据证明使用的事实是,所有(小)可达范畴的范畴具有所有加权极限[19,定理5.1.6]。 那么范畴F可以构造为这样的极限,即插入器[13]:1C CF引理的第二部分是从F中的余极限这一事实引出的。是逐点形成的。✷这个结果允许我们考虑κ-可表示的LanIκ RanJκB-余代数:引理5.4设B是κ-余签名。一个κ-可表示的Lan IκRan JκB-coal-gebra由一个κ-可表示的对象X和一个函数hc组成,对于每个元c,hc:A(X,c)→ A(X,Bc)。证据给定任意κ-可达内函子F和κ-可表示对象X,LanIκF(X)=F(X)。因此,上述形式的余代数是A(X,(RanJκB)(X))<$=A(X, c∈NκA(X,c)MBc)n=c∈NκA(X,A(X,c)MBc)n=c∈Nκ[A(X,c),A(X,Bc)]在单子理论中,一个重要的结果是代数表示的模型同构于表示单子的理论的代数范畴。为了模拟这个结果,我们需要一个κ-余签名B的模型(或者如果你喜欢的话,也可以是余模型)的概念,引理5.4表明这是LanIκ RanJκB-余代数。例5.5联合签名Bp的模型由有限集合X和函数Set(X,2)Set(X,2)给出。如果我们把一个映射f:X 2看作X的一个子集,或者看作X上的一个谓词,那么这样一个模型就可以看作是谓词之间的映射。类似地,联合签名Bpω的模型由有限集合X和函数Set(X,2)Set(X,ω)组成。如果我们把它看作是把X的二进制划分映射到ω-ary划分,那么这显然与前面的例子有关。5.2一个联合签名回想一下,在代数的情况下,我们从一个签名开始,构造一个内函子,然后考虑内函子上的自由单子。对偶的第二部分是考虑在一个函子上的余自由余元.[11]中的以下两个结果提供了以下框架:GHANI,LÜTH,DEMARCHI,POWER139→A×一A−-A−A →A- → −⇒A a a AA → AA →A这次讨论:引理5.6函子F:A → A上的下列条件是等价的:(i) 在F上有一个cofree comonad。(ii) 遗忘函子F − coalg → A是余单进的。(iii) 健忘函子F−coalg → A有一个右伴随(iv) (如果有积)对于每个对象X,函子XF有一个最终余代数。类似于一元的情况,只有可达的内函子有一个上自由的comonad。例如,幂集函子P:Seet设余代数是同构X∈PX. 的[19,11]的重要结果如下:引理5.7如果是局部可表示的,且F是可达的,则F是局部可表示的,且F上存在余自由余子。证据回想引理5.3,Fcoalg是可达的。Fcoalg的余完备性是因为健忘函子创建了余极限并且是余完备的. 由于遗忘函子是局部可表示范畴之间的保余限函子,因此从特殊伴随函子定理[18,定理V.8.1]可以得出,遗忘函子有右伴随。根据引理5.6,F上存在一个余自由余单子。✷设Comκ(A)是A上的κ-可达余单子范畴,而ACom(A)是A上的可达余单子范畴.对于每个κ,Comκ()是ACom()的一个全子范畴。类似地,设[,]κ是秩为κ的内函子的范畴,AEnd()是可达内函子的范畴将上述结果拼凑在一起,我们有以下结果:引理5.8健忘函子V:ACom()AEnd()有一个右伴随R。证据 给定一个可达的内函子F,令遗忘函子UF:F−coalg→ A的右伴随为KF。然后选择R(F)为UFKF,我们可以推导出R(F)是可达的,因为UF是可达的(作为左伴随,它保持所有的余极限),并且KF是可达的[3,命题1.66在p。52]。右伴随对可及闭函子的作用已经给出。 给定一个自然变换α:F1F2,这诱导出一个函子α:F1coalgF2coalg,与相应的遗忘函子可交换。利用[6]的对偶,定理3在p.[128]和commonadicity的这些范畴的余代数,这反过来又导致一个自然变换R(α):R(F1)R(F2). 10.函数R:AEnd()ACom(). 它是V的右伴随的事实很容易证明。✷与一元情况相反,秩为λ的内函子M:上的余自由余元RM不需要秩为λ;作为一个简单的反例,def考虑内函子M:Set→Set定义为MX=A×X,对于aGHANI,LÜTH,DEMARCHI,POWER140×⊆ℵ◦× ××ℵ一不defN →κJκA是一个固定的集合,它显然是无限的(秩为0)。 我们知道RM对于集合X的值由RM(X)= νY给出。X我 = νY。X一 Y是X的所有无限元素流的集合A. 现在考虑 一个可数无限集合Y,则RM(Y)包含一个序列,其中有无穷多个与Y不同的元素。这个序列不能从任何有限子集Y0Y中给出,这表明RM的秩大于0。正如我们在Sect中看到的那样4,一般来说,计算可及内函子的余代数似乎总是增加它们的秩-参见[24]对这一现象的研究使用[Aκ,A]和[A,A]κ之间的等价性,我们现在有以下函子,其中Jκ是与Jκ的预复合,V是秩为κ的comonads的遗忘U:兰乔[Nκ,A]不◦ Jκ[Aκ,A]=[A,A]κ∩❄A结束(A)Comκ()V(五)RACom(A)V我们进一步定义了复合函子Vκ:Comκ(A)→[Nκ,A]Vκ=(N Jκ)。VR:[N,A]→ACo m(A)R=defR. 跑正如我们已经看到的,RκB的秩可能大于B的秩,因此Rκ的上域不是Vκ的域,而是ACom(A)。因此,尽管Rκ和Vκ不能是伴随的,但存在以下同构:引理5.9对于任意κ-可达余子G和κ-余签名B:κA存在同构[Nκ,A](VκG,B)=ACom(A)(G,RκB)(6)这在G和B中是正常的。证据 同构由(5)中的两个分解提供的下列自然同构链以及[A,A] κ到AEnd(A)中的完全和忠实嵌入表示:[Nκ,A](VκG,B)=[Nκ,A](JκVG,B)n=[Aκ,A](VG,RanJκB)=AEnd(A)(VG,RanJκB)n=ACom(A)(G,RRanJκB)=ACom(A)(G,RκB)✷GHANI,LÜTH,DEMARCHI,POWER141−→ ∈ NAAA → A→∈ A因此,给定一个κ-余签名B,我们构造了它的表示余名RκB。注意,根据引理5.6,余代数范畴RκB−Coalg同构于范畴LanIκ RanJκBcoalg。将我们自己限制在κ-可表示余代数,我们得到表示余子RκB的κ-可表示余代数同构于前面定义的余签名B的κ-可表示模型这是我们的部分二元论的结果,说明模型的签名是同构的Eilenberg-Moore范畴的代表单子。5.3余等式表示及其表示余项在本节中,我们通过定义余方程表示、推导这种余方程表示的表示余子以及将表示余子的余代数与表示的模型相正如我们在上面看到的,方程被解释为自由单子之间的一对单子态射;方程表示的表示单子被定义为这些单子态射的余均衡器对偶这需要一个coequational表示,以形成一对cofree comonad之间的comonad态射,并采取coequational表示的表示comonad是这些comonad态射的均衡器。定义5.10(余方程表示)余方程表示由两个余签名B:Nκ→ A和E:Nλ→ A(其中RκB是λ-可达的)和两个余单态射σ,τ:RκB→ RλE给出。在(6)中,映射σ,τ:RκB→RλE由映射σJ,τJ:VλRκB→E给出,而映射σj,τj:V λ R κ B→E又是族σCJ,τCJ:RκBcc的地图的Ecλ。因此, 与一元情况相反,方程由一对项给出,余方程由余项的两个划分组成;例如,如果E(n)=2,σ和τ将RκB(n)划分为两个子集.如上所述,给定一个余等式表示,我们的意图是定义它的表示余单态射为余单态射的均衡器σGκBτλ英(7)通过我们的抽象范畴设置,可以更容易地证明这些均衡器的存在,这为我们提供了一个余代数的另一种定义。回想一下,这样的余代数是由一个对象x和一个映射α:xGx给出的,该映射与G的单位和计数可交换。首先,观察一个物体x,由映射X:1给出(其中1是单对象类别)。此外,函子范畴[1,]同构于,我们有A(x,Gx)<$=[1,A](X,G<$X)<$=[A,A](LanXX,G),(8)GHANI,LÜTH,DEMARCHI,POWER142∼⇒◦⇒◦一---A−−=所以给出一个映射x→Gx等价于给出Lan XX<$G的一个自然变换。事实上。LanXX is a comonad:引理5.11 Lan XX是一个comonad。如果X是κ-可表示的,则LanXX是κ-可访问。证据使用左Kan扩张的标准公式,LanXX(a)=A(X,a)<$X(其中<$X是张量;例如在Set中,它由通常的乘积给出)。如果X是κ-可表示的,则A(X,−)保持所有κ-过滤的余极限,就像− <$X一样;因此LanXX是κ-可达的。为了有一个comonad结构,我们需要自然变换Lan XX 1和Lan XX兰XXLanXX满足共形律。 其中第一个由X上的恒等变换的图像给出在同构[1,A](X,X)下,n=[A,A](LanXX,1A). 二是由变 换的同 构 [1,A](X,LanXX<$LanX < $X)= [A,A](LanXX,LanXX<$ LanXX)X=0LANXXLanX LanX兰XX其中,X是正则变换X兰XXX. 那个委员会而余乘服从余乘定律是很容易验证的。✷LanXX是一个comonad的事实允许我们加强方程(8)以获得comonad的余代数的所承诺的特征命题5.12一个余单子G的余代数由一个对象X给出,A和一个地图兰X XG在ACom(A)。证据 我们已经看到,余代数的结构映射恰是两个函子之间的自然变换。然后,它是例行的,以验证的性质的结构映射的一个余代数对应的法律的一个余单态射。✷通过命题5.12,我们可以证明均衡器的存在引理5.13可达共名范畴ACom()有所有的equals-er。证据 考虑两个共单态射M是的。 我们定义美食,τ由余代数α:Lan X X给出的gory(M,E)余代数M/M这样的这个σ。α= τ。α。回想一下引理5.4的证明,我们是如何将余代数的范畴构造为加权极限的;使用一个类似的图,称为等价器,我们也可以构造(M,E)Coalg作为加权极限,使其可访问。当(M,E)Coalg,M和E可达时,从(M,E)Coalg到的遗忘函子有一个右伴随;这个右伴随与遗忘函子的后合成给出了M和E的均衡器。✷XXXGHANI,LÜTH,DEMARCHI,POWER143→我们通过将coequational表示的模型与其表示comonad的coalgebras相关联来完成。 若G是余方程表示σ,τ:RκB→RλE的表示余子,则G-余代数是一个映射α:Lan XX→G,根据均衡器的泛性质,它是一个映射αJ:Lan XX→ RκB, 使得σ. α= τ。α,或者换句话说,B的余代数它等于σ和τ。在这种情况下,我们说余代数LanXX→RκB满足余方程表示σ,τ:RκB→RλE。根据上面的计算,如果X是κ-可表示的,则映射α:Lan XX→RκB给出了两个RλE-余代数,根据引理5.4,这两个RλE -余代数是对所有c∈ Nλ的映射族σJJ:A(X,c)→A(X,Ec)和τJJ:A(X,c)→A(X,Ec),如果α:Lan XX→RκB满足表示σ,τ:RκB→RλE,则它们必须相等。6结论、相关工作和进一步工作本文从可达单子理论出发,分析了单代数范畴化方法的实质,并导出了它们的虽然仍然只是工作进展中,我们觉得我们已经做出了明确的贡献,这将是一般的余代数社区的兴趣。特别是,对应于最终X+F-余代数集合的无穷单子的推导似乎在懒惰函数式编程中有此外,推导出的cofree comonad表 示 一 个 cosignature 和 解 释 的 co-equational 表 示 作 为一 个 equaliser 的cofree comonad的标准理论中的相应结果的对偶。我们还涉及到的代表comonad的coalgebras的coequational介绍的模型主要的技术挑战是由从共同签名传递到其代表共同签名时的等级增加引起的。例如,这意味着余代数的刻画只适用于达到一定秩的余代数此外,这种秩的增加使得每个可访问的comonad不太可能作为coequational表示(即作为cofree comonad的均衡器)给出,而对于fennitarymonad来说是可能的。当然,仍有许多工作要做。我们的方法非常抽象,也许最重要的下一步是明确我们的方法与社区中其他方法之间例如,Cirstea [7]定义了一个抽象的共同签名为函子F:C → C,其中C具有所有有限极限和ωop-链的极限,F保持回调和这样的极限。然后,观察者由函子K:C → C和自然变换c:U→K给出。U,以及由两个观测者(K,l)和(K,r)得到的一个协方程。因此,观察者是所有F-余代数α:X→FX的映射族β:C→KC。这个概念大致对应于一个共单态射RκB<$RλE,因为我们总是有上自由余代数RκBX RκBRκBX。然而,差异是更强的假设 抽象共同签名F保持ωop的极限,这允许GHANI,LÜTH,DEMARCHI,POWER144结构的final余代数,并推理它;在我们更抽象的设置,我们所有的是存在的权利伴随和相应的较弱的性质。我们还没有发展出作为共单元语义学的范畴结构基础的逻辑演算似乎这种潜在的逻辑将有一个模态的解释,因此在这一领域的研究,例如。”[15]这是一个很好的例子。最后,在最近的工作中使用的co-Birkho定理[4,22]余方程应该与我们的余方程。引用[1] P. Aczel,J.Adamek和J.维勒比尔迭代单子。在us蒙塔纳里,编辑,Proceedings CMCS[2] J. Adamek关于连续函子的最终余代数出现。[3] J. Adamek和J. 罗茜。本地可靠和可接受的类别。第189章伦敦数学会讲座笔记系列剑桥大学出版社,1994年。[4] S. Awodey和J.休斯。birkho簇定理的余代数对偶。http://www.contrib.andrew.cmu.edu/user/jesse/papers/CoBirkhoff.ps.gz,2000年。[5] M. Barr.良基集合论中的终端代数。理论计算机科学,114:299[6] M. 巴尔 和C.井托波斯, 三个和理论数学科学基础278号。Springer Verl
下载后可阅读完整内容,剩余1页未读,立即下载
![.pdf](https://img-home.csdnimg.cn/images/20210720083646.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)