241→《理论计算机科学电子札记》44卷第1期（2001）网址：http://www.elsevier.nl/locate/entcs/volume44.html13页模态规则是共蕴涵亚历山大·库尔茨CWI，P.O.Box 94079，NL-1090 GB Amsterdam，The Netherlands摘要在[13]中，证明了余代数的模态逻辑是代数的关于可本文建立了，类似地，模态规则对偶蕴涵：它表明，一类余代数是可定义的模态规则i它是封闭的H（图像）和i（不相交的联盟）。作为一个推论，无限模态逻辑的规则在Kripke框架上的表达能力的特点。1介绍余代数是变迁系统的一种推广，这一点推动了模态逻辑与余代数关系的研究。第一个主要成就是莫斯 从那时起，模态逻辑作为余代数的一种特殊语言已经在许多论文中进行了研究，例如[17，18，12，10，9，5，16]。另一方面，它也是有趣的应用cet-gorical和（共）代数工具，以获得新的见解模态逻辑。例如，在[13]中表明，可以通过对偶化Birkho多样性定理的证明来证明无穷模态逻辑在Kripke框架上的表达能力（这反过来又表征了表达能力）。代数上的等式逻辑在这里，我们继续这条研究路线我们从蕴涵i∈Iti=tJi→s=SJ，I是集合或类，还有代数。 关于隐含定义的经典结果-能够类是由于Banaschewski和Herrlich [3]（也见Wechler [20]）：一类代数是隐式可定义的，如果它在子代数和积（和同构）下是闭的。类似于[13]，我们的目的是利用代数和coal-代数的对偶性来证明这个定理在余代数上的对偶。事实证明，与蕴涵对偶的概念是模态规则。定理4.1建立了一类余代数是规则可定义的，如果它在态射和不交并的象下是闭的。定理5.2将这个结果应用于克里普克框架：一类克里普克框架可由无穷模态逻辑的规则定义，如果它在p-态射和不交并的图像下是封闭的。2000年1月，出版社dbyElsevierScienceB。 V.操作访问和C CB Y-NC-ND许可证。库尔茨242→→Gumm [8]采用了一种代数上相似但逻辑上不同的方法。在那里，也结果等式和蕴涵可定义的代数类是对偶的。但是用于余代数的逻辑是不同的：公式f是余自由余代数TC的载体的元素，并且f在余代数Mi f中对所有赋值α：UM成立C.公式α #不在诱导态射α#：M TC的象中.如果我们考虑Gumm意义下的模态规则或上蕴涵的语义是由相应的核投射态射给出的（参见[14]中定理4.1或第2章的证明），那么这两种方法是等价的。自1999年2月以来，该草案的前一个版本已经以电子方式提供。1999年在克拉科夫举行的第11届国际逻辑、方法论和科学哲学大会上提出。本文的主要改进是定理4.1不再依赖于集合X中余自由余代数的存在性。因此，定理5.2中对Kripke框架的应用不需要框架分支度的界 这一结果相当令人惊讶，不可转移在[13]中的covariance定理的情况下是显而易见2余代数我们介绍符号和简要回顾余代数作为模态逻辑的模型关于余代数的经典论文是Rut- ten [19]。给出了余代数w.r.t.一个范畴C和一个闭函子C → C。一个M-余代数M=（UM，fM）则由一个对象UM∈ C和一个箭头fM：UM→UM（UM）在C中给出. n-余代数形成范畴Cn，其中余代数态射α：（UM，fM）→（UN，fN）是C中的箭头α：UM→UN使得nα<$fM=fN<$α。作为一个例子，考虑函子：Set→Set由X =PX给出，其中P表示幂集。1.则n-余代数是Kripke框架：给定余代数M和世界x∈UM，fM（x）是x的后继集。集合P中的余代数态射是泛函互模拟，即p-态射关于集合X中epis和monos的注记：由于态射α：（UM，fM）→（UN，fN）也是一个函数α：UM→UN，如果α是Set中的epi（mono），则α也是Set中的epi（mono）。反之对于epis也是如此（参见Rutten[19]，4.7），也就是说，在SetEisisepi i Eisit中的态射是满射。关于单射，它成立：α∈Setismono inSeti it is strong mono inSet（见附录），即Set中的态射是强单射i it是单射。[1]这只定义了一个子集合。在函数上，λ A以标准的方式定义，P是协变幂集函子：给定f：X→Y，λf=λA∈PX。{f（a）：a∈A}.库尔茨243α→→→∈→PP→◦×→→×→∈→∈2.1余代数我们首先给出余自由余代数的定义，然后展示如何在模态逻辑的背景下解释它们。为了定义上自由余代数的概念，考虑下面的图表：UTC“你#C❄❅C语言α设f是一个函子。一个余代数TC（和一个映射TC：UTC C）称为C i上的余自由的，对所有的余代数M和所有的映射α：UM C，存在唯一的态射α#：M TC使得图交换.[2]与泛代数相比，颜色集合C对应于变量集合，颜色α对应于变量赋值。与P =P的情形一样，余自由余代数可能不存在于集合P中。这个问题可以通过将函子扩展为函子来避免在SET3上，定义K={ XX：XX XK，Xa set}对于类K。然后它由Aczel和Mendler [2]的一个定理得出：对任意函子集和任意C集，上自由余代数TC存在于SET集上.因此，在下文中，我们将允许，而无需进一步提及，余自由余代数存在于集合n中而不是集合n中。作为一个例子，考虑P =和C=P，其中P是一组命题变量。设M是一个余代数，即.克里普克框架函数α：UM C是赋值：M中的每个世界x被赋予在x中保持的比例变量集，即（M，α）是Kripke模型。(Note证明了一个C-余代数M加上一个赋值α：UMC是一个C-余代数;以及C与UMC之间的态射n-余代数f：（M，α）（N，β）是n-态射f：M N使得β f= α，见[13]。上图表明，任何Kripke模型（M，α）在模型（TC，αC）中都有唯一的p态像。我们可以把（TC，CXC）看作是所有基于双标架的模型的不相交的并集，其附加特征是任何两个双相似世界都是可识别的。2.2余代数的强单核对偶类强单核映射的概念是余自由度概念的推广，强mono在这里出现是因为它们是描述子余代数的范畴方式（见附录）。 使用核心概念类2 注意，每个态射α#：M TCSet是通过定义Set也是一个映射α#：UMUTCSet。3SET是类和类映射的范畴，如Aczel [1]，第7章，以及Aczel和Mendler [2]。库尔茨244MϵMMMM∈MM✻❅因为，一方面，它们正是那些在算子H（在余代数态射的像下的闭包）和H（在余代数的不交并（余积，和）下的闭包）下封闭的类，另一方面，因为设：Set→Set是一个函子。一类强单上反射余代数RK M和强单态射给出了余代数的KK：RK M→M，对所有M∈SetK，使得对所有N∈K，每个态射α：N→M因子，唯一通过K：KMMRK M阿哈那α❅NRK M称为M与RK的核连接M.的核截射态射命题2.1（强单余反射的存在性）设K是集合上的函子，K是一类K余代数。则对于所有M ∈ Set，是RK M∈Set，且强monoK：RK M→M∈Set，使得对于在集合n中，所有N∈K和所有α：N→M，存在唯一的α：N→RK M，设置，使得Kα= α。 此外，R K M∈ H <$H K.证据设M∈Set.设A={α：N→M|N∈K}是所有余代数态射N→M的集合，其中N∈K。 现在，所有α∈A的像的并集定义了M的一个子余代数RK M，其中包含RK。显然，对于每个N∈K，上述因式分解性质成立。此外，并是不相交并的商的事实表明RK M∈H <$HK。✷定义2.2（Strong-mono-co-reflective-classes，smc）设k是集合上的一个函数，K是一类k-余代数. K称为强单核映射，简称smc，它在同构下是闭的，包含所有核映射R K M。 5强满射代数类的特征在于恰好是那些在子代数和积下闭的代数类。通常，余代数的smc-类的特征在于同态像下的闭包（用H表示）和不交并下的闭包，即余积（用H表示）。命题2.3设K是集合上的函子，K是一个余代数类.K是smc i，它在H和H下闭合。4每一个余代数态射α集都通过它的象Imα分解，见Rutten [19]，定理7.1;余代数态射的象的并总是存在，见[19]，定理6.4。5范畴地：K是smc i，它在同构和包含函子下是封闭K→集合K有一个右伴随R K，它有一个计数（即， （1）强有力的单声道。ϵ库尔茨245M∈∈MM×P证据“only if”：H下的闭包是[4]的（对偶），I.3.6.4。对于小M i K下的闭合（对于所有iI）和M是所有M i的和。 注意，RK Mi同构于Mi。我们必须证明R，K， M，同构于M。K作为一个强大的单声道，它表面上表明，是集合中的epi（因此epi在设置为 0）。这是从观察到每个x∈UM都在 i 中包含的图像中得出的：Mi→M，并且每个包含因子都通过K。“if”：从R K M ∈ H <$H K导出。✷在H和H ∞下的闭包等价于在算子H ∞下的闭包。 这与以下事实是对偶的：在泛代数中，SP是子代数和乘积算子下的闭包（关于余代数上的闭包算子的详细信息，请参见Gumm和S cr？der[6]）。因此，我们可以将上面的命题表述为Ksmc i <$K= H <$（K）。2.3例为了说明上述概念及其与模态逻辑的联系，我们给出一个例子。设B=B，其中B是布尔集。 也就是说，每个状态都被分配（b，Y），其中b是布尔值，Y是集合。我们将b解释为一个固定命题的真值，Y解释为后继命题的集合。这个函子的模态语言是由通常的连接词、模态算子和集合P中的命题变量，加上一个由start表示的命题常数构建的。一个集合M-余代数M=（UM，f）是一个Kripke框架，一个谓词解释的开始。更精确地说，令α：UM→ PP，x∈UM，p∈P.然后（布尔情况和往常一样，π1，π2表示从乘积B×P到其分量的投影）：M，α，x |=开始优惠π1 f（x）= trueM，α，x|= p惠p∈ α（x）M，α，x |f（x）：M，α，y |=满足第一个子句的状态x称为以start标记的状态。接下来，我们想用模态规则公理化这些Kripke框架的一个子类模态规则/（其中，是模态公式）通过以下方式解释：M| =/α：UM → P P：M，α =100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000=||模态公理是具有真前提的规则。 现在，考虑以下规则：（re）p→p（transs）p→p（start）start→p/p前两个是著名的公理，定义了Kripk e框架上的自反性和传递性。 第三个是Kro？ger[11]提出的起始规则。在库尔茨246MMϵMMML（M，α）（M，α）自反性和传递性的存在，它表示每个状态都必须从一个以start为标记的状态可达。称Φ为上述三个规则的集合，令K为Φ定义的Kripke框架类。我们证明K是smc。定义RK M为满足Φ的M的最大子余代数（即，为了找到RK M，取M的最大子余代数，该子余代数是自反的和传递的，然后切割所有状态，不能由开始标记的状态到达）。K：RK M→M是正则的嵌入，它是一个强单声道，因为它是内射的。 回想一下核心对偶子范畴的定义，我们还需要证明，对于所有满足Φ的N∈ Set，对所有f：N→M，存在唯一的g：N→R K M，使得f=<$K <$g：KMMRK M. ✻”“是的。- 是的f.N考虑f的因子分解N→eImf→mM。因为规则是不可改变的，拍摄图像（见命题3.5），可以得出Im f| = Φ。而且m：Imf→M是M的一个子余代数，由于RK M是最大的子余代数对于满足Φ的M，m通过<$K因子化为m =<$K<$gJ，对于某些gJ。现在我想，g=gje是所需的态射，g是唯一确定的，因为K是内射的最后，让我们注意到K在像和不交并（余积）下是闭的，但在子余代数下不是。因此K是一个不属于余簇的余拟簇的例子.3余代数的模态逻辑模态逻辑有许多不同的类型，但它们中的大多数都具有以下特征，这些特征对于余代数逻辑是必不可少的：公式在点（世界，状态）中求值，并且它们在互模拟下是不变的。与关于余变种的论文[13]相比，下面的定义略有变化：由于我们不要求函子有界，逻辑必须有任意大的颜色集合的公式定义3.1设f是一个函子。余代数的模态逻辑由以下给出：• 集合类Col（Col中的集合称为L的色集合），其中Col对每个基数κ包含一个基数 ≥κ的集合，对每个C ∈Col包含一类公式 LC，• 对所有的C∈Col，对所有的M ∈Setα，对所有的赋值α：UM →C a关系|= CUM × LC. （记为M、α、x |= for（x，）∈ |= C .）• 对所有C∈Col，M，N ∈SetC，α：UM →C，β：UN →C，C ∈ LC，G库尔茨247||∈L→⊂ ⇒⊂x∈UM，且所有C×n-态射6f：（M，α）→（N，β），它必须保持M，α，x |= N，β，f（x）|= 0。最后一个条件是，公式在互模拟下必须是不变的，这不仅与余代数的结构有关，而且与给定的值有关。像往常一样，M，x=x，（M=x）通过量化M的所有估值（和所有元素）来定义。公式C定义了余自由余代数（TC，C）的子集。是有用的是引入以下符号：[[]] TC，C={x∈UTC：TC，C，x|{\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}.根据互模拟下公式的不变性，它遵循允许减少有效性w.r.t.的基本属性在任何模型中对cofree模型有效性的估值M，α |= Im α#[[]] TC，C.接下来，我们表明，对偶的概念，代数中的蕴涵，我们得到的概念，一个模态规则。读者可能想回忆一下泛代数中蕴涵的语义。前两个基本事实：设X是一组变量，TX是变量X上的代数项。则每个赋值α：X→A都有唯一的提升到代数态射αb：TX→A。每个代数态射αb：TX→A确定TX上的一个同余关系，记为kerαb. 接下来，考虑一个蕴涵i∈Iti=tJi→s=sJ. 它确定了两个同余关系P，Q在TX的载体上，P代表由i∈Iti=tJi和Q为s=SJ诱导的关系。不难看出，蕴涵在代数Ai <$PkerαbQkerαb中成立，α：XA。下面的模态规则的定义使蕴涵的这种特征二重化。定义3.2（规则）给定两个公式<$，<$∈ LC ，我们称表达式<$/<$a规则。 由L C中的公式建立的所有规则的类表示为 关于Ru C德费恩|=M| = /i α：UM→C：Im α#[[]] TC，C Imα#定义3.3（规则可定义）设L：Set→Set是一个函子，L是一个模逻辑。如果存在类Φ C <$Ru C，C ∈ Col，使得M ∈ K惠C ∈ Col：M |= Φ C。到目前为止，我们只要求模态逻辑的公式在点上求值，并且在互模拟下不变我们还需要一6回想一下f：（M，α）→（N，β）是一个C×N-态射i <$f是一个N-态射，使得βf = α。库尔茨248LL→LMMMMMMMM保证足够表达能力的属性。定义3.4余代数L的模态逻辑称为表达的，如果对所有C∈Col和（TC，<$C）的每个C× <$-子余代数S，存在公式<$US使得US={x∈TC：TC，<$C，x| {\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}.余代数模态逻辑定义的一个重要结果规则是在图像和不相交的联合下保存命题3.5设是一个关于余代数的模态逻辑，设K是一个可规则定义的余代数类。 则K在算子H下是闭的，- 是的证据 设C∈Col，且λ，λ∈LC.“H”: Suppose 我们必须展示M|=/=N|=/。 F或一个conn悖论假设N|=//，即存在β：UN→C和y∈UNs. t。 N，β，y|=N，β，y|=/. 德费恩α：UM→C，通过α=βf，即f是（M，α）和（N，β）之间的C×π-互模拟。现在，由于集合中的f epi蕴涵集合中的f epi，并且由于|=与C × M-互模拟相容，存在x ∈ UM使得M，α，x |=M，α，x|=/h，其中h是期望的contradiction。“”：与上面的类似。 设（Mi）i∈I是K中的一类模型，M=i∈IMi. 辅助位置M|=//。也就是说，存在α：UM→C，x∈UMsuch，M，α，x|=和M，α，x|=/. 因为集合中的和是构造为集合7中的和，存在j∈I使得x∈Mj。现在，使用M j到M中的包含是互模拟，表明M j，i j，x| =和Mj，ij， x|=/.✷4余代数的规则可定义类我们已经看到，规则可定义类在H和H下是封闭的。为了证明相反的情况，我们使用了每个闭于H和H的类K都是强单核投射（smc），然后证明了K是定理4.1（规则可定义类的特征）设SetSet是余代数的函子和表达模态逻辑. 那么类K可以由以下规则定义：i K在H下关闭 和。证据“只有当”是命题3.5。对于现在，定义规则由核心定义决定phisms：RK M→M。 对于C∈Col，定义ΦC如下。 对于M∈Set，| ≤ |C|，选择一个内射映射i：UM → C。|, choose an injective mapping i :UM → C.通过表达-存在公式<$C，<$C∈ LC，使得[<$C]] TC，<$C = 我#和[[C]] TC，C =Im（i#K）. 设Φ C={φ C/φ C：M∈Setφ，|嗯|≤ |C|}。7 分类：U：Set→Set创建所有的上极限，参见[19]，定理4.5。库尔茨249MMMMN∈∈→PP公司简介|=MMMMMMMMNNNNNN我们必须证明N∈K惠函C∈Col：N| = Φ C。““：设C /C ∈ Φ C，并假设N，β| = C，即Im β#[[C]] TC，C。通过定义UMC，有i：UM → C，其中[UMC]] TC，UMC = Im i#。因此，β#通过i#的因子为β#=i#<$f对于某些f：N→M。由于N∈K且K是smc，f通过k的因子分解为f = k Kk g，对于某些g：N → R K M。它遵循Imβ#= Im（i#K g）Im（i#K）=[[C]] TC，C，即N，β |= 100℃。“选择C∈Col，|C| ≥ |联合国|i：UN→ C使得Imi# =[[kC]]TC，kC。 我们证明Im i#= Im（i#K）（这意味着，由于i#和n ∈K是单射，N RK N，因此N∈K）。“ ”是明显的，并且Im i#[[C ]] T C，C = Im（i #K）由于N，i而成立|= 100C/100C。✷注4.2在设T = T的情况下，余自由余代数TC不存在于集合T中，而存在于集合T中。 这对证明没有影响，因为对所有的α#：MTC、M设，也称Imα# 准备好。注意，这个推理不能转移到[13]中的余变定理的证明中，因为需要考虑余自由余代数的核心子集R K TC（在[13]中称为F K C），如果TC ∈ Set <$，则这些余代数通常只在Set<$i中（对于<$i = P和C/={}，情况并非如此）。5规则可定义的Kripke框架类定理4.1的一般性允许许多应用。例如，有可能给出这个定理的一个版本，用于余代数逻辑（Moss [15]）。对于余变种而不是smc类，这已经在[13]中进行了余代数逻辑的优点是它给出了所有函子的余代数的模态逻辑的定义但这里我们只想给出一个（具体的）模态逻辑的例子。我们选择α =，并证明我们的定理成为关于规则可定义的Kripke框架类的陈述我们用ML表示无穷模态逻辑，它是由一个适当的命题变量类Prop、常数φ、算子φ、φ和conjunc构成的。在任何一组公式上。和" 当PProp和P是我们写的一个集合（P），用于只从P中取变量的公式类。为了应用定理4.1，我们需要以下引理：引理5.1所有ML（P）的集合，其中P在Prop的子集上的范围是余代数w.r.t.的表达模态逻辑。函子P.因此，类Ru PP（见定义3.2）是ML（P）的规则类。证据通过{PP：PProp，Pa set}实例化定义3.1的Col，以及C（M，α）根据模态逻辑的通常的满足关系，满足定义3.1的条件 表现力可以表示为在[13]中。其次，设M是一个Kripke框架.然后，根据模态逻辑中规则的定义，M=/iα：UM→PP：M，α=100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 = 0，符合定义3.2。|||✷库尔茨250M定理5.2设K是一类Kripke框架。则K是规则可定义的，如果K在p-态像和不交并下是闭的证据回想一下Col={PP：PProp，Pa set}。“if”: Bylemma 5.1 and theorem“only if”：K是规则可定义的，也就是说，存在类Φ {M/M：M，M ∈ ML}使得K = { M ∈ Set M：M| = Φ}。 设KPP={M∈Set<$：M| = Φ Ru PP}。 我们可以写K={KPP：PP∈Col}，命题3.5，K={ H <$KPP：PP∈Col}.这是一位将军关于闭包算子K<$H <${KPP：PP∈Col}，因此，KH K。✷有些读者可能会觉得通过余代数的“迂回”是不必要的，从第一原理证明定理可以更短。因此，让我们强调，我们的证明实际上是简单而简短的：一旦我们建立了一个在p-态像和不相交并下封闭的类K，由核反射态射确定（见第2.3条），仅为了检查核心部分射态射（或更一般地，生成的子帧，即，强单）确实可以用规则来定义（见引理5.1和定理4.1的证明）。6结论本文证明了代数中的子代数与余代数中的子coal-gebra之间的对偶性不仅允许Birkho簇定理的对偶，而且允许刻画隐式可定义代数类的此外，还证明了对应于一个蕴涵的模态概念不是一个公式→的模态概念，而是一个规则/的模态概念。研究包含模态规则和适当的演绎演算的余代数的有限规范语言是留给未来研究的。让我们提到代数和余代数的对偶性在这里被用作一种推理。定理4.1的证明不是代数的相应证明的形式（范畴）对偶，因为它依赖于集合的范畴（并且集合上的余代数与集合上的代数是对偶的）。所示[14] 可以对模态逻辑和等式逻辑的对偶性作出说明，这使得对偶性在范畴意义上是精确的确认我要感谢亚历山大·纳普对前一稿的评论。图表是用保罗·泰勒的宏包制作的库尔茨251引用[1] 彼得·阿采尔。非良基集。斯坦福大学语言与信息研究中心，1988年。[2] Peter Aczel和Nax Mendler一个最终余代数定理In D. H. Pitt等人，编辑，Category Theory and Computer Science，LNCS第389卷，第357-365页。Springer，1989年。[3] B. Banaschewski 和 H. 赫里奇子类别 已定义 通过 影响Houston Journal of Mathematics，2（2）：149[4] 弗朗西斯·博索分类代数手册。剑桥大学出版社，1994年。[5] 罗伯特·戈德布拉特什么是Birkho簇定理的余代数类似物？理论计算机科学出现。[6] H. P. Gumm和T. 请点菜。Covarietiesanddcompletecovarieties.在B.雅各布斯湖Moss，H. Reichel和J. Rutten，编辑，Coalgebraic Methods计算机科学（CMCS'98），1998年理论计算机科学电子笔记第11卷。[7] H. P. Gumm和T. 请点菜。 弱极限保持函子的余代数结构。芽孢杆菌中雅各布斯湖Moss，H. Reichel和J.Rutten，编辑，计算机科学中的共代数方法（CMCS'00），理论计算机科学电子注释第33卷，第113-134页，2000年。[8] H.彼得·古姆余代数的方程类和蕴涵类。抽象延伸RelMiCS '4.第四届逻辑、代数和计算机科学中的关系方法国际研讨会，华沙，1998年。[9] 巴特·雅各布斯。余代数经由伽罗瓦代数的时态逻辑。技术报告CSI-R9906，奈梅亨计算科学研究所，1999年。[10] 巴特·雅各布斯。 走向二元结果 在 共代数 模态 逻辑 在Horst Reichel，编辑，Coalgebraic Methods in Computer Science（CMCS[11] FredKr？ger.P rg ram s的技术原理。Springer，1987年。[12] 亚历山大·库尔兹用模态逻辑证明余代数。理论计算机科学，260（1-2）。出现。[13] 亚历山大·库尔兹模态逻辑的余簇定理。模态逻辑进展论文集2，乌普萨拉，1998年。斯坦福大学语言与信息研究中心，2000年。[14] 亚历山大·库尔兹余代数逻辑及其在计算机科学中的应用。博士论文，路德维 希 - 马 克 西 米 利 安 大 学 ， 2000 年 。http： //www.informatik.uni-muenchen.de/~kurz。库尔茨252✠[15] 劳伦斯·莫斯。共代数逻辑Annals of Pure and Applied Logic，96：277[16] 德克·帕丁森。余代数模态逻辑中的语义原则。第18届计算机科学理论方面国际研讨会论文集（STACS 2001），计算机科学讲义，柏林，2001年。斯普林格。出现。[17] 马丁·罗西格。从模逻辑到终结余代数。《计算机科学》，260（1-2）。出现。[18] 马丁·罗西格。余代数与模态逻辑。在HorstReichel，编辑，CoalgebraicMethods in Computer Science（CMCS[19] J.J.M. M.拉顿泛余代数：系统理论。理论计算机科学，249：3[20] 沃尔夫冈·韦克勒计算机科学家通用代数，第25卷EATCS理论计算机科学专著。 Springer，1992年。一 强单态射我们证明了余代数集合集合中的强mono恰是内射态射，即。子余代数首先，请记住强单声道的定义（参见例如。Borceux [4]，I.4.3）。定义A.1（强单声道）单声道f：M→N称为强i，对于所有epis g：X→Y和所 有 u： X→M， v： Y→N ， 使 得 f<$u=v<$g存 在 （ 必 然 唯 一 ） w：Y→M，使得 w<$g=u和 f<$w=v：XgYw. . . .你好。. .vMNf从技术的角度来看，这种因式分解性质对本文的结果至关重要一个直接的结果是以下有用的命题。命题A.2（极值monos）一个强monom是极值的，即，如果m因子为m =f∈ e，e epi，则e是iso。在集合monos范畴中，极值monos和强monos都是单内射映射。在余代数范畴中，monos不一定是内射的（参见Gumm和S chr？oder[7]）。下面的命题表明，强monos正是集合n中的内射态射。提案A.3(i) 如果f∈Set_n作为一个映射在Set_n中是mono的，则f在Set_n中是强mono的。❄库尔茨253∈∈◦◦M/◦→◦(ii) 每一个态射f都是一个epi后跟一个强mono的唯一因子。此外，这种因式分解是作为集合中f的epi/mono因式分解而获得的。(iii) Set中的强单声道是Set中的单声道。证据(i) 设f，g，u，v为上图中的集合，fmono为集合，g epi为集合。由于集合中的gepi（Rutten [19]，4.7），所需的w作为集合中的映射存在。还需要证明w是集合X中的态射，即X wfY= fMw，其中fY，fM分别是余代数Y，M的结构映射。画一个适当的图，这可以从Set中的g，u态射，Set中的gepi和Set中的wg=u得出。(ii) 设h：X→Y∈SetX，UX→eImh→UY是h在通过它的形象IMH设置。 我们必须证明Imh可以装备在一种具有余代数结构的唯一方法，使得e，m成为集合n中的态射。这是从“对角线填充”得出的用户体验俄罗斯联邦fImh/联系我们fYm❄Ω Imh联系我们布勒姆中的对角线填充存在，因为Imh/ ={}和Immono8和eepi或Imh={}，空映射使图可交换。从（1）可以得出m在集合n中是强的中因子分解的唯一性集合A可以在[4]，I.4.4.5中找到(iii) 通过（2），在集合X中的强单声道h：XY因子为epi/强单声道h=em。因为h也是极值，e是epi，所以它遵循eiso。m是强的，h也是。✷8Imhi ={}，并且mmono意味着m个分裂的mono，因此m个mono。
