205⟨⟩⟨⟩⟨⟩《理论计算机科学电子札记》44卷第1期（2001）网址：http://www.elsevier.nl/locate/entcs/volume44.html22页余方程的模态算子Jesse Hughes部卡内基梅隆大学匹兹堡，宾夕法尼亚州15213jesse@cmu.edu摘要我们提出了对偶Birkho的簇定理的谓词在一个cofreed余代数的载体。然后，我们讨论的对偶Birkho的完备性定理，显示如何关闭演绎规则下二元化产生两个模态算子作用于coequations。我们讨论了这些运营商的性质，并表明他们交换，我们证明了不变性定理，这是形式的对偶的完整性定理。1介绍扬Rutten此外，他证明了对偶Birkho余变定理指出，一个余代数类V在epis的（正则）子余代数、余积和余域下是闭的，只要V是余方程和余方程满足的概念是作为代数范畴中方程集和方程满足的形式对偶而产生的PeterGumm和TobiasSchrder在[GS 98]中对集合上余代数的Birkho定理的推广进行了研究，并对演绎完备性定理进行了也就是说，他们证明了，给定一个正则内射余代数A，α，由A，α上的条件余方程定义的拟余簇的偏序同构于A，α的不变子余代数。在这里，不变性的概念作为方程组在项替换变量下的闭包的对偶而出现。在同上，我们还发现了第一次讨论“完全”或“行为”共变。这些余变种可以用一种“颜色”上的余方程来定义*这项研究是卡内基梅隆大学Dana Scott指导下的类型逻辑和计算项目的一部分。2000年1月，出版社dbyElsevierScienceB。 V.操作访问和C CB Y-NC-ND许可证。休斯206∧ →或者，等价地，在全互模拟下上簇是闭的。例如，[RJT 01]中关于共代数规范的工作涉及到在面向对象语言中为类给出模型，作为适当类别的共代数中的行为共变种。因此，我们可以用单一颜色上的余方程来这些余方程是一类泛代数的无变量方程的对偶，因此人们有这样的想法，即在余方程理论中有更多的表达能力可以利用我们在这里提供了一些余方程的例子，这些例子说明了当人们从行为余变种转移到一般余变种时可用的一些另见[Ros00]讨论了被称为“汇”的病毒变异，[AH00]或[Hug01]综合了[GS 98]和[R o s00]的工作本文从逻辑的观点发展了余方程理论.色集C上的余方程是UHC的正则子对象，是C上的余自由余代数的载体。因此，我们可以将UHC视为UHC的谓词。特别地，我们可以通过逻辑连接词等从旧的余方程中构造新的余方程。此外，我们还可以利用一个模态算子将余方程取为最大子余代数的（载体）。余方程中包含的变量这个模态运算符与取集合是对偶的因此，它与Birkho方程逻辑的前四个推理规则下的E的闭包是对偶的。 所以我们看到，E在演绎推理下的闭包与在Sub（UHC）中添加相关的模态运算符。我们引入了一个模态算子，它在Birkho算子下是闭包的对偶推理的有限规则，用项代替变量。我们证实了，是一个S4算子，并表明，在某些条件下，与交换。然后，我们证明了不变性定理的条件下，和。通过这种方式，我们通过用两个模态算子和扩充UHC上的谓词来发展余方程作为谓词的观点，并证明C上的余方程可定义的余变种的偏序同构于UHC上的谓词的偏序，使得=。第二节总结了Birkho簇定理的对偶在第三节中，我们推广了余簇定理，使其适用于拟余簇和条件余方程。第四节是Birkho的演绎完备性定理及其对偶--不变性定理的一个范畴化表述。我们在第5节中讨论了著名的最大子余代数算子，并证明了它是一个S4模态算子，沿着同态与拉回交换。在第6节中，我们引入了第二个S4算子，S_n，将一个余方程带到它的最大不变子余方程。这使得在第7节中用算子λ和λ来证明不变性定理变得容易这项工作的一部分，作者斯科特和史蒂夫·阿沃迪教授休斯207E斯科特建议研究的双重Birkho我也从与JirıAdamek的谈话中受益，他把我们带到了Banaschewski和Herrlich的文章中，Peter Gumm和Bart Jacobs。2Birkho簇定理的对偶我们首先简要地总结了Birkho簇定理的对偶。本节总结了[AH00]中的工作，可以将其视为[Rut 96]和[GS 98]的概括。在[Kur00]中可以找到一个类似的关于余簇定理的说明，在[BH 76]中可以找到一个类似的关于代数范畴的簇定理的范畴方法我们从一些术语开始。回想一下，一个态射是一个正则单声道，只是在它是某对映射的均衡器的情况下，而一个子对象是正则的，如果它的包含是一个正则单声道。在下文中，我们称一个对象C为正则内射，如果它对正则子对象是内射的;也就是说，如果只要B是A的正则子对象，则每个f：B C可以扩展为（不一定是唯一的）映射g：A C使得下面的图1是上下班的。AgC，，_，fB我们说一个范畴E有足够的正则内射，如果对每个对象，A∈ E，存在正则内射C，使得A是C的正则子对象.定义2.1我们说一个范畴是拟余Birkho范畴，如果它是正则良幂的，余完备的，并且有上正则单因子分解。此外，如果E有足够的规则内射词，则E是co-Birkho-n。拟余Birkho范畴的一个满子范畴是一个拟余簇，它在epis的余积和余域下是闭的。一个co-Birkho范畴的拟余簇是一个余簇，它在正则子范畴下也是闭的事实上，我们可以在下面的内容中用强monos替换常规monos，这里显示的结果仍然适用。这需要削弱某些假设（例如，E只需要具有epi-strong单因子化），同时加强其他假设（例如，E需要足够强1Weu se.zto表示正则单声道。休斯208CEEEE⟨⟩注射剂）。我们倾向于用正则单声道来呈现这些材料，因为在代数环境中，正则epi和方程组之间存在着自然的关系例2.2余代数的范畴EG，其中余代数G=G，ε，δ，形成函子G的余代数范畴EG中的余簇。给定一个映射f：AB在一个具有epi正则单因子分解的范畴中，我们用Im（f）（读作我们用Sub（A）表示A的正则子代数的偏序。地图f：AB诱导一个函子f：Sub（B）Sub（A），通过沿着f拉回B的正则子对象。这个函子有左伴随，Sub（A）Sub（B），其中涉及常规子对象i：P。zAtoIm（fi）.回想一下，对象A与箭头f正交：BC（写作A<$f）如果对每个g：AC，存在唯一映射h：AB使得g=f<$h（参见[Bor 94，Volume 2]）。给定E的箭头的集合2S<$E1，类S<$E0是所有A的集合，使得对所有f∈S，A<$f。下面的定理可以在[AH00]或[Hug01]中找到定理2.3如果 是co-Birkho范畴，则V是余簇i <$V= S<$对于具有正则内射余域的正则mono的集合S。可以证明，如果G= G，ε，δ∈是拟余Birkho范畴上的余单元，且G保持正则单元，则EG继承E的上正则单元分解.我们用这个事实来证明以下几点。定理2.4设G= G，ε，δ是（拟）余Birkho代数上的余单元，且G保持正则单元。则G是（拟）co-Birkho。事实上，定理2.4的应用比所述的更普遍。若是拟余Birkho范畴，且Γ是任何保持正则单的内函子，则内函子Γ的余代数范畴Γ是拟余Birkho范畴.对于这个结果，我们不需要余自由的Γ-余代数在下文中，我们用余代数的形式来陈述我们的定理，尽管我们经常指出定理何时也适用于闭函子的余代数。使用余代数的优点是，EG中的余变种本身是E上的余单进，因此这里的结果可以并且，任何余代数范畴EΓ，2.当我们使用集合这个词时，我们允许它是一个适当的类。我们经常滥用集合表示法，并在下面的类中采用它休斯209E_，，|⟨⟩∈⟨⟩⟨⟩∧→一个内函子，如果存在余自由余代数，等价于一个余代数范畴 G（见[Tur96]）。由于我们在下面的内容中经常我们让U：EGE（或U：EIE，分别）表示余代数遗忘函子，H：EEG（H：EEΓ，如果存在的话） 是U的右伴随。我们在方便的时候省略U，把U写成A，α写成A，把UP写成p。定理2.4保证了余代数的范畴是（拟）余Birkho范畴，假设基范畴是且G保持正则monos。因此，抽象的co-Birkho定理适用。为了在余代数范畴中理解定理2.3，我们引入了余方程的概念。定义2.5设C∈ E是正则内射。C上的余方程是正则子对象<$C ≤GC（=UHC）。 我们说，一个余代数<$A，α<$满足<$A（记作<$A，α<$|=）以防万一，对于每个同态p：α-H2O，α-H2OC（等价地，每个p：A使得下面的图表可以上下班。一个p GC，，z轴如果V是一类余代数，我们记V=α，仅当每个A，αV满意度换句话说，αA，αB|如果，对于每个同态p：α-H2OA，α- H2OC，我们有Im（p）≤n，或者等价地，T ≤p≤n。我们以同样的方式定义，p：α-H2OA，α-H2OC，αα|=（p）i Im（p）≤。同样，在[AN82]（也见于[AR94]）介绍后，我们可以说，一个余代数A，α满足C上的一个余方程λ，仅仅是在A，α是关于包含λ的射影的情况下。zUHC. 在这些定理2.3说，对于某个集合S，任何余簇都是S-Proj具有正则内射余域的正则monos。C上的一个余方程可以看作是GC上的一个谓词。因此，如果Sub（GC）是一个Heyting代数，我们可以构造余方程，等等，所以我们看到C上的余方程有一个自然的结构。p休斯210继续这种解释，如果，∈Sub（GC），我们通常写表示≤。很容易看出，如果α和α，|=，则A，α| = 0。如果我们把C上的余方程看作是GC类型变量x的谓词，那么我们可以沿着同态p：α-A，α- G-C作为p（y）（其中y是类型A的变量）对x的替换，即，p =[p（y）/x]。因此，αA，αB|对于每个同态p，我们有T [p（y）/x]。注2.6在方程的情况下，人们可以很容易地区分单个方程和方程组。Gumm在[Gum01]中对单余方程和余方程集进行了类似的区分，将余方程满足解释为排除条件。我们倾向于保留上述满意度的定义，这与我们将余方程视为谓词的观点一致。因此，我们不区分单一的余方程和余方程集这个概念的coequation允许一个更熟悉的陈述的对偶Birkho定理2.7设E是co-Birkho半群，G保持正则单调和。 则E G的一个全子范畴V是一个余簇i，存在一个余方程集合S，使得对于所有的i，A，α，<$A，α<$∈ Vi <$<$A，α<$|= 0。此外，如果G由C有界，则对于每个余簇V，存在C上的余方程，使得A，α<$∈Vi| = 0。有界函子的定义可以在[Rut 96]或[GS 98]中找到，例如，其中定理2.7是针对集合上的余代数证明的。这个定理在更一般的情况下的证明可以在[Hug01]或[Kur00]中找到下面的推论是[Jac95]中定理12的推广，其中作者对Set上的一类受限制的余方程，即那些作为与函子G有关的一对项的均衡器出现的余方程证明了它。推论2.8设E是co-Birkho幺半群，G保持正则幺半群，设V是E G的余变种。 那么健忘的函子VE是共同的。此外，相关联的余单子保持正则单子，因此V再次是co-Birkho。休斯211EE证据健忘函子VE是复合材料VUVEGUE。为了证明这个复合是共单子的，它表面上表明（通过[Bor94，第2卷，定理4.4.4]的对偶）以下成立：(i) U UV有一个右伴随;(ii) U<$ UV反映同构;(iii) U UV创建对的均衡器F·g ·使得U∈UVf、U∈UVg在E中具有分裂均衡器。条件（i）由下面的定理3.4得出条件（ii）很容易验证，（iii）由U的相同条件和UV创建均衡器的事实得出。✷注2.9在下面的例子中，我们倾向于把coalge- bras描述为一个闭函子的余代数，而不是一个comonad的余代数因为这些例子涉及范畴EΓ，其中遗忘函子有一个rightadjoint，有一个共形Gsuch，使得Γr=G[Tur96]，因此前面的结果适用。例2.10固定一组“输入”I，设Γ：设t定义为Γ S =（PfinS）I，其中Pfin是协变有限幂集函子。 一个Γ-余代数εS，σε canbe被视为一个非确定性自动机上的一个，其中的结构映射给出了过渡函数。解释地，对于每个状态s∈S和每个输入i∈I，我们写为sisJ仅当SJ∈σ（s）（i）时。确定性自动机是这样的自动机：S，σ，使得对于每个s∈S和eac hi∈I，最多有一个sJsuc h使得sisJ。LetDet表示确定性自动机类，因此Det∈SetΓ。那么很容易看出Det是集合Γ中的余簇。事实上，我们可以证明，在2种颜色上存在一个余方程，Det. 也就是说，通过以下方式定义UH2：n={x ∈ UH 2 |<$i ∈ I <$y，z ∈ δ（x）（i）. ε2（y）= ε2（z）}，其中δ：UH2= ΓUH2是H2的结构图. 那么，很容易证明，αα |= i A，α∈ Det.休斯212C∈⟨⟩ℵ中文（ 简体） |}⟨⟩⟨⟩|例2.11固定一个集合Z，令Γ：Set设t是函子Γ X = Z× X。任何一个Γ-余代数A，α都可以看作是Z上的流的集合，那么，其中同一个流可以乘地表示为A的元素。余自由余代数HN是最终的N×Z×−余代数-即， HN=（N×Z）ω。给定一个元素σ∈HN，我们可以定义Col（σ）={π1<$σ（i）|i< ω}（等价地，ol（σ）=εNti（σ）i ω，其中t是尾部析构函数）。 换句话说，ol（σ）是流σ中出现的所有颜色的集合。定义N上的一个余方程，={σ|卡（Col（σ）<）0}，（其中card（X）是X的基数），所以σ只是在σ中只出现有限多个颜色的情况下。我们可以证明，对于任意的Γ-余代数<$A，α <$A，α <$A，α <$B，|对于所有的a ∈ A，存在n ≥ 0，m> 0，使得tn（a）=tn+m（a），（其中α=h，t）。换句话说，A，α=iA中的每个流只有有限个注2.12如果人们对状态的相等性不感兴趣，而对流的可解行为感兴趣，那么人们可能要求，对每个a∈A，存在n≥0，m>0，使得对所有i≥0，htn+i（a）=htn+m+i（a）。这个条件可以通过一个颜色上的余方程来指定注2.13使用例2.11可以很容易地生成其他有趣的余方程。首先，很第二，我们可以要求每个状态在析构函数的n个应用中开始重复，方法是在函数的定义中将0替换为n。3条件余方程在定义2.5中，我们将C上的余方程定义为正则子对象- 是的zUHC休斯213E≤⟨⟩⟨⟩ |⟨⟩|⟨⟩∧⟨⟩ |⟨⟩ |⇒⟨ ⟩−⟨⟩ |→⟨⟩ |⇒→→in. 在本节中，我们将余方程的概念推广到包括正则子方程- 是的zA，α其中，αA，αB是任意余代数。定义3.1环A，α上的条件余方程是任意正则子对象A = U A，α。 我们说B、β =α（或仅 B、β =）当且仅当，对于每个同态Im（p）≤m。p：β-B，β- D-A，α-D-A，我们有时会放弃“条件”这个词方程在λ A，αλ上。我们采用条件余方程这个名称，是因为在定义3.1中引入的语义给定C上的两个余方程，β和β，我们说，|为了以防万一p：β-H2OB，β- H2OC，若B，β=π（p），则B，β=π（p）. [99]现在，对于C上的任何一对余方程，都有一个余代数和一个条件余方程，使得对于所有的，α-β-D-β-D-β-D-β-D-|= iB，β| = απ。也就是说，我们可以取A，α= []HC（[ ]的定义见第5节），并且=A。 另一方面，给定一个条件余方程， A，α，我们可以把α和A看作是A上的余方程，也就是说，作为UHA的子对象.很容易检查，α-β-D-β-D-β-D-β-D-|= αiB，β| = A。注3.2给定C上的余方程和，可以考虑C上的余方程，其中是Sub（UHC）中的指数。 我们可以证明，如果A，α=，则A，α=，但反之亦然。一般不持有例3.3设Γ− =−× −，A={a，b}。让εA，l，r A×UHA×UHA是HA的结构图。 定义A上的余方程：σ ={σ∈UHA|σ = l（σ）}，σ ={σ∈UHA|σ =r（σ）}。休斯214CE设α（a）= b，b，α（b）=b，a. 然后是αA，αβ |=，但A，α/|=→条件余方程提供了一种解释余拟簇定理的方法。和前面一样，我们首先陈述拟簇定理的一个抽象形式，然后在类范畴中解释该定理定理3.4及其推论的证明可以在[AH00]中找到。这个定理也被Alexander Kurz在[Kur00]中独立证明定理3.4设C是拟余Birkho范畴，V是C的满子范畴。以下是等价的。(i) V是一个拟余簇。(ii) 包含UV：VC有一个右伴随HV，使得εV：1CU VHV的每个分量都是正则单声道.(iii) V= S对于某些正则单声道的集合S。推论3.5设C是拟余Birkho范畴，V是C的拟余簇。然后(i) 包含UV：V C有一个右伴随HV。(ii) 单位ηV：idVH V U V是一个同构。(iii) 对于每个C∈ C，C∈Vi <$C <$εV，其中εV是附加词UVE HV.(iv) 相应的余项G V=<$U VHV，ε，U Vη HV <$，是幂等的。(v) 共调GV保持了常规的单调。下面的推论重申了定理3.4中关于余代数范畴的结果。推论3.6设E是拟余Birkho算子，且设Γ：EE是保持正则monos的函子。如果存在条件余方程的集合S使得B，β|= 0。如果我们用一个余单子G代替闭函子Γ，同样的主张也成立。4演绎完备性与不变性我们现在集中在Birkho而多样性定理给出了代数类的封闭条件与方程可定义性之间的等价性，完备性定理则陈述了演绎封闭方程集与代数类的方程理论之间的等价性我们首先回顾一下经典环境中的完备性定理设f是签名，r是相关的多项式函子（因此，休斯215×⟨⟩Alg（n）=Setr），令F：SetSetSet是遗忘函子U的左伴随：好吧我们说，一组方程E除以X（即，UFX UFX的子集），如果满足以下条件，如下：(i) 对每个x∈X，x=x∈E;(ii) 对每个t1=t2∈E，t2=t1∈E;(iii) 若t1=t2∈E且t2=t3∈E，则t1=t3∈E;(iv) 对于每个函数符号f（n）∈f（n），以及每个n元组的方程，s1= t1，.，sn= tn，在E中，方程f（n）（s1，...，sn）=f（n）（t1，.，tn）∈ E.(v) E在用项代替变量时是封闭的。 也就是说，对于每个t1=t2∈E，t∈UFX，x∈X，t1[t/x]=t2[t/x]∈E.定理4.1（Birkho是在E是闭的情况下，一类V-代数的方程理论。我们说UFX上的（二元）关系E对每个同态都f：FX FX，E在f下的像包含在E中，即，如果E≤E，用范畴术语来说，则X上的方程组E仅在（iJ）E是同余的情况下是闭的;(iiE是稳定的。在 代 数 环 境 中 的 稳 定 方 程 组 的 概 念 对 偶 的 概 念 ， 自 同 态 不 变 的coequations 这个定义首先在[GS98]中找到。这里定义的术语自同态不变不应与不变谓词的定义混淆，不变谓词是允许结构映射的谓词（即，是一个子余代数的载体），如[Jac99，M aB01，PZ01]和其他地方所用。尽管如此，在下文中，我们使用定义4.2设A，α是G-余代数. A的正则子对象A是自同态不变的（以下简称为不变的），对每个同态p：αA，αB αA，αB α，休斯216||►⟨⟩E∈ EE⟨⟩p下的p的图像包含在p中，即，p注4.3若αA，αB是最终余代数的子余代数，则αA，αB上的任何余方程αB是自同态不变的.给定一个共等式簇V ={λB，β λ}| α-β-D-β-D-β-D-β-D-|=}，我们感兴趣的是最小余方程，使得V=。这样的最小余方程可以被看作是生成V满足的余方程的集合，在这个意义上，对于任何余方程，如果V=π，则π。 在 在这个意义上，最小余方程代表了V- 它代表了V所包含的平等承诺。这种直觉激发了下面的定义。定义4.4设A是A上的（条件）余方程，α和V是余代数的集合。为了以防万一，我们说V是V的生成（条件）余方程。(i) V|= 0;(ii) 对于C上的任何条件余方程，如果V|那就来吧。定理4.5（不变性定理）C上的余方程是余代数的某个集合V的生成余方程，只要余代数是HC的不变子余代数。我们推迟证明，直到我们定义了模态运算符和。不变性定理首先出现在[GS98]中，在那里它被证明为集合上的余代数。该定理在他们的工作中以不同的术语陈述，因为它不是由我们在这里采取的coequation-as-predicate观点所激发的。5子余代数算子在剩下的部分中，我们构造了用于不变性定理证明的模态算子，并证明了关于这些算子的一些基本结果在下文中，我们假设是co-Birkho，并且有回调，G保持正则monos和正则monos的回调，因此G是co-Birkho，U创建正则monos的回调（特别是有限交集）。我们进一步假设，对于每个A，Sub（A）是一个Heyting代数。在本节中，我们将介绍模态运算符。给定一个子对象A=U A， α的最大子余代数.这种结构是众所周知的，尽管认为“”是一个模态算子的观点可能不太熟悉。在[Jac99]中讨论了该算子，其中它扮演一个休斯217≤EE−- ◦中心角色。正是从这一工作中，我们认为，作为一个“从今以后”的由于余代数遗忘函子U：G 保持正则monos，有一个诱导的遗忘函子，Uα：Sub（αA，αB）Sub（A），从A的正则子代数的偏序到A的正则子代数的偏序.众所周知，Uα有一个右伴随，我们记为[]α（方便时去掉下标右伴随将子对象BA映射到包含在B中的最大子余代数。更准确地说，[B]={C，γ≤A，α|C≤ B}。在这里，我们使用Uα创建连接的事实或者，可以将[B]定义为如下所示的回调。[B].. zHB_r_zJ._rzJα α zHA这个伴随对产生一个模态算子α：Sub（A）Sub（A），通常，取复合函数α=[]αUα。同样，我们在方便的时候去掉定理5.1 π是一个S4必要算子，即，满足以下要求：(i) 如果你不愿意，那你就不愿意(ii) ✷ϕ►ϕ(iii) ✷ϕ► ✷✷ϕ(iv) （证据 条件（i）是函子性，条件（ii）和（iii）是余单子的可数和余乘。最后一项是由Uα保持满足的事实得出的，因此也保持满足。从这里得出的（iv）的论证是标准的，但我们在这里也包括它（一）我们有因此，（（（故（→）→。✷休斯218⟨⟩定理5.2在沿着同态的拉回下是稳定的。也就是说，对于任何我们有f：αA，α BB，βC，<$α<$f<$= f <$$><$β。证据图1中的底面是对易的，因为f是同态。前面和后面是通过定义的回调，右边的面是回调，因为G通过假设沿着正则monos保持回调。因此，左边的脸是一个回调。✷好吧zGfP_r，z，、、，，vz_r，z，、、，，vz好吧zGP_rz_rzJ.JA，z、、、、，vJzGA，，、、、、、vJzB. zGBFig. 1. 沿着同态，pullback与pullback交换。定理5.2可以被理解为一个关于用项代替变量的陈述也就是说，我们把A，α上的条件余方程看作是A型单变量x的预测。然后，定理5.2说，对于任何同态，f：αB，βBA，αB，和任何类型B的变量y，我们有（x）[f（y）/x]=x（x[f（y）/x]）。因此，在变量的同态项的替换下，ε是稳定的（然而，在用任意项代替变量的情况下，它是不稳定的6不变性算子我们将与第5节相同的方法应用于不变余方程。也就是说，我们首先定义一个伴随对（伽罗瓦对应）之间的余方程在αA，αB和不变的余方程。然后，我们使用这个对来定义一个关于余方程的模态算子，α ∈A，α∈ C。、休斯219⟨ ⟩ ⟨ ⟩∃ ∃≤∃ ≤ ∃∈E≤相应地，设Inv（α）表示Sub（A）的全子范畴，该全子范畴由αA，αB上的不变余方程组成，并且设Iα：Inv（α）Sub（A）是包含函子。定理6.1 Iα有一个右伴随。证据设A ≤ A，定义P={≤A|p：我们定义了一个函子Jα：Sub（A）Sub（A）byJα（λ）=你好，∈P方便时省略下标我们首先证明J是不变的。让r：α αA，αβA，αβ B被给予。为了证明rJ J，表面上可以证明rJP，即，对每个同态p：A，αA，α，我们有p（rJ <$）<$。 快速计算显示p∈P=∈Pp接下来，我们展示了J。 设λ是不变的。如果是，则对于每个自同态p，p所以，因此。另一方面，如果n≤J，则≤ J✷设α=IαJα。我们证明了它是一个S4算子。再一次，它表面上表明，保留符合。定理6.2 π是一个S4必要算子。证据同样，由于“”是一个comonad，它表面上表明，“”保留满足，或者，更具体地说，☒ϕ ∧ ☒ψ ► ☒(ϕ ∧ ψ).休斯220ωD设p：αA，αA，αB是给定的（其中α A和α B是α A，α B上的条件余方程）. 然后p（同样地，p（）≤。因此，p（）≤。由于p是一个任意同态，所以（）。✷注6.3与π不同，算子π不与沿同态的回调交换。设Γ：Set Set t为恒等函子。我们将考虑一个2色上的余方程，即UH2 = 2ω的子集，即2上的流的集合。具体而言，让={0，1}，其中0和1是恒定流。请注意，是不变的。设p：H3H2是由着色p：32、在哪里p（0）= 0，p（1）= 0，p（2）= 1（即，p=H（p））。 那么p是集合{σ∈3| <$nσ（n）<2}<${2}。很容易检查，p就置换而言，并不是对每一个同态f：αB，βBA，αB，（x）[f（y）/x]=x（x[f（y）/x]）。我们回到第2节中的例子，来给大家一些关于网络是如何工作的概念在这些例子中，C上的余方程用染色εC来描述。通常情况下，如这些例子所示，Escherichia将一个用着色定义的协方程转化为一个用状态相等定义的类似协方程例6.4如例2.10所示，设ΓS=（PfinS）I。回想一下，确定性自动机et的类形成集合Γ的余种，其中定义2上的余方程由下式给出：n={x ∈ UH 2 |<$i ∈ I <$y，z ∈ σ（x）（i）. ε2（y）= ε2（z）}。很容易证明，UH ={x ∈ UH 2 |<$i ∈ I <$y，z ∈ σ（x）（i）.y = z}，或者更简单地说，UH ={x ∈ UH 2 |i∈ I. 卡（σ（x）（i））<2}。休斯221×n⟨⟩►⟨⟩|例6.5回想一下函子ΓX =ZX和N上的余方程定义为={σ|卡（Col（σ）<）0}，例2.11。 对于每个σ∈UHN，令St（σ）={t（σ）|n∈ ω}，式中，N，h，t= N×Z×UHN是HN的结构图。然后☒ϕ ={σ|卡（St（σ））<<$0}。7生成余方程我们回到不变性定理。首先，我们证明，对于A上的任何α，α和α具有与α定义相同的拟余簇。定理7.1设λA，αλ已知。 对任意的ε∈Sub（A），εB，βε ∈ EG，α-β-D-β-D-β-D-β-D-|= iB，β| = 0。证据 自2002年以来，但是，一个方向是微不足道的。 假设，然后， B，β=- 是的让p：β-B、β-D-A、α-D-A被给予。 为了证明Im（p）≤ Im（p），我们将证明，对于每个r：α αA，αβA，αβ，Im（p）≤Im（p） 但是，由于β ∈ B，β ∈ C，则β∈Im（p）= Im（r∈p）≤β|= 0。✷定理7.2设λA，αλ是已知的。 对任意的ε∈Sub（A），εB，βε ∈ EG，α-β-D-β-D-β-D-β-D-|= iB，β| = 0。证据 同样，一个方向是微不足道的。 令βB，ββ| =，让p：β-B、β-D-A、α-D-A被给予。 然后UαIm（p）=Im（Up）≤，因此，通过附加项UαE[−]α，Im（p）≤[π]α。因此，在本发明中，Im（Up）= UαIm（p）≤ Uα [] α= α。✷引理7.3设λ是C上的余方程。然后，余代数[zh]满足余方程[zh]。休斯222. .你|||►ECP⟨⟩⟨ ⟩ ⟨ ⟩ ⟨⟩证据令p：[1]HC给出。因为HC是正则内射，所以p扩张为同态HCHC，如下图所示。因此，因为✷☒ϕ☒ϕ如果是不变的，则存在唯一的映射使正方形和下面的三角形可以交换，如所期望的。UH，C，UHC.，，。. p.，，___ ._✷☒ϕ☒ϕ✷定理7.4（不变性定理）C上的余方程是余代数的某个集合V的生成余方程，仅当余代数是HC的不变子余代数时，即，=证据设=，并定义V ={λB，β λ}| α-β-D-β-D-β-D-β-D-|{\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}.那么，很明显，V=。我们将证明，如果V =，则。但是，从引理7.3，我们知道[] =[]在V中。因此，[]=，因此=✷注7.5对于A，α上的条件余方程也有同样的要求和证明，其中A，α是正则内射或A，α是HA的不变子余代数。也就是说，在这样的A，α上的条件余方程是某个类V的生成余方程，仅在条件余方程=的情况下。注7.6设λ是环上的余方程，V是它所定义的余簇。LetU：V ”（《易经》卷五：“。拉里3.5）。那么我们可以证明，UUHHC =。例7.7再次考虑函子Γ：Set Se t，其中ΓS =（finS）I和由下式定义的余方程：n={x ∈ UH 2 |<$i ∈ I <$y，z ∈ σ（x）（i）. ε2（y）= ε2（z）}。我们在例6.4中声称，UH ={x ∈ UH 2 |<$i ∈ I <$y，z ∈ σ（x）（i）.y = z}.休斯223D⟨ ⟩≤我们写s 如果存在i使得s isJ，我们把的传递闭包写成。可以进一步表明，✷ ☒ϕ={x∈UH2|好吧 x<$w→ <$i∈ I卡（σ（w）（i））<2}.根据定理7.4，Et是确定性自动机类et的生成余方程定理7.8对任意余代数<$A，α<$，✷☒ ≤☒✷.证据 通过定义同态，它表明，对于每个同态，p：αA，αBA，αC，αp≤αC。我们知道，对于每一个p，p 因此，由于Uα与αp交换，Uαp[]α=pUα[]α≤，故α=α，α = α，α=α。因此，在本发明中，p✷在进一步的假设下，我们可以证明也就是说，如果模态算子有一个左伴随D，则=。这样一个伴随的存在性是自然产生的，只要余单子G保持非空交集.在这种情况下，子余代数遗忘函子Uα有一个左伴随，Fα：Sub（A）Sub（αA，αB），取一个子对象β到最小子余代数B，β，使得β B。闭包算子Dα是复合算子UαFα。见[Gum 98 b]的讨论函子保留非空的inter-section和一个例子的函子没有这个属性。另见[Jac99]关于闭包算子Dα的讨论，其中记为α(and记为α）。⇐⇒定理7.9若α有一个左伴随Dα，则α= α。证据 为了证明≤，（通过附加词DE）证明D≤ 就 足 够 了 。设A ≤A = U<$A，α<$. 我们将证明，对于每个同态p：αA，αA，αB，αpD αA≤α，并（通过α的定义）得出D αA≤α。再一次，通过这些解释，它表明，☒✷ϕ≤✷p∗ϕ=p∗✷ϕ,或者，等价地，p≤。这一点直接来自于对“无”的定义。✷休斯224E×∧∧ ¬ ∃人们怀疑定理7.9并不依赖于闭包算子D的存在--也就是说，应该有一个证明，即不需要模态算子D的伴随。目前，我们还不知道这样的证据。我们也没有在某个G中对适当的G有一个余方程使得余方程>余方程的例子。在任何情况下，人们发现，对于许多感兴趣的函子（多项式，有限幂集等），运算符D确实具有伴随D，因此上述假设并不像人们可能怀疑的那样具有限制性。例7.10设ΓX =ZX，再次考虑余方程N来自实施例2.11，其中={σ|卡（Col（σ）<）0}。很容易检验出=，因此=（在例6.5中定义）是N上的最小余方程，使得A，α|以防万一αα |=。8未来研究我们在这里试图发展“作为谓词的对等式”的思想。这种方法自然地给出了一种通过使用标准逻辑运算符、、等来从旧余方程构造新余方程的方法以及模态运算符和。我们已经证明，对于任何余方程，余簇的余簇定义与余簇和余簇定义的余簇相同同样明显的是，余变种的定义是由和定义的余变种的交集。人们希望研究其他逻辑算子（尤其是量化算子）与上变的偏序之间的关系人们还想研究一下，好吧定理7.9表明，对于任何保持交的函子G但这个假设是否真的有必要还为此，考虑双重情况是有益的。人们假设，在同余条件下闭合一组方程，然后稳定，总是产生与在稳定条件下闭合相同的集合，但也许需要一个技术细节来证明这一点（甚至可能是一个对集合上的所有代数类别都成立的假设）。引用[AGM 92] S.作者：Abramsky，Dov M. Gabbay和T. S. E Maibaum编辑计算机科学中的逻辑手册，第1卷。牛津科学出版社，1992年。[AH00] Steve Awodey和Jesse Hughes。Birkho簇定理的余代数对偶。技术报告CMU-PHIL-109，卡内基梅隆大学，宾夕法尼亚州匹兹堡，15213，2000年11月
我的内容管理
展开
