“匕首紧闭范畴图形语言与CPM构造在量子计算中的应用”

理论计算机科学电子笔记170（2007）139-163www.elsevier.com/locate/entcsDagger紧闭范畴与完全正映射（延伸摘要）彼得·塞林格1加拿大新斯科舍省哈利法克斯达尔豪西大学摘要匕首紧闭范畴最近由Abramsky和Coecke引入，名为我们提出了一种匕首紧闭范畴的图形语言，并给出了它在方程推理中的完备性证明。我们给出了一个一般的建设，CPM建设，其中关联到每个匕首紧凑封闭范畴的我们将这些思想应用于Abramky和Coecke的in t er p r e t io n o f u a n t u m p r o t o c ol，以及D ' H o n t和D P a n a n ga de n的谓词Transformer语义。保留字：范畴模型，量子计算，匕首范畴，CPM构造。1引言在过去的几年里，已经有几个关于量子编程语言和/或协议的公理语义的提议在[9]中，我提出了“基本量子流图范畴”的概念在这样一个范畴中，我们可以对具有经典控制和有限经典和量子数据类型的一阶量子编程语言进行1电子邮件：selinger@mathstat.dal.ca。由NSERC支持的研究。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.12.018140P. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139大约在同一时间，Abramsky和Coecke引入了他们的“强紧闭范畴”的概念（本文将这个公理化框架捕捉到了有限维希尔伯特空间范畴的足够多的性质，从而能够表达基本的量子力学概念，如酉映射、标量、投影、内积等。[9]和[1]各自的公理在一开始就非常不同：前者试图用混合态、密度矩阵和完全正映射来捕捉冯·诺依曼的量子力学公式，而后者则以纯态、幺正映射和投影仪为中心来形式化希尔伯特空间的本文的目的是证明，尽管有这些明显的区别，这两种方法实际上有很多共同之处。本文证明了文[9]中所考虑的完全正映射范畴实际上是一个双积匕首紧闭范畴。我们进一步引入了一个一般的构造，称为CPM构造，它将任何匕首紧闭范畴C与其通过这种方式，我们获得了从“希尔伯特式”到“冯诺依曼式”设置的规范和非常一般的方式作为这些思想的应用，我们讨论了Abramsky和Coecke对量子协议的解释.Abramsky和Coecke认为，双积可以用来模拟经典的信息流在他们的神经网络设置。我们表明，适当的地方，这样的解释是不是希尔伯特空间的范畴，但它的派生类别的完全正映射。作为匕首结构在完全正映射范畴上的另一个应用，我们还简要地讨论了在对monoidal范畴的许多变体进行推理时，一个重要的工具是使用图形语言[5]。在这里，我们描述了一个图形语言匕首紧凑封闭范畴。在阿布拉姆斯基和科克的论文中，类似的语言已经以一种更非正式的方式我们进入一些关于这种语言的细节，并勾勒出它的完整性证明匕首紧闭范畴中的方程推理。2Dagger紧闭范畴Dagger紧闭范畴是由Abramsky和Coecke在[ 1 ]中以“强紧闭范畴”的名义引入的他们扩展了紧闭范畴[6]，引入了态射的伴随概念（这里是P. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139141一词匕首紧闭范畴公理化了有限维希尔伯特空间范畴的许多结构性质，因此它们似乎形成了公理化量子力学的合适框架。2.1紧闭范畴回想一下，对称么半群范畴是一个范畴C加上一个双函子，一个区别对象I，以及自然同构αA，B，C：（A<$B）<$C→A<$（B<$C），λA：A→I<$A，和σA，B：A<$B→B<$A，服从标准凝聚条件[7]。通常我们也记为ρA= σI，A<$λA：A→A<$I。紧闭范畴是一个对称幺半群范畴，其中每个对象A都被赋予一个对偶对象A，以及一个单位映射ηA：I→AA和一个可数映射→I，使得λ−1◦ （A）−1∗A A∗ηA）（AA）<$αA<$，A，A<$$>（ηA<$A）<$λA=idA<$.注2.1在任何紧闭范畴中，运算（-）通过映射f：A→B到f：B→A而扩展到逆变函子，定义为−1∗ ∗ ∗ ∗ρA<$$>（A<$$>B）<$（A<$f <$B）<$（ηA<$B）<$λB <$。这一功能的出现，对称的非对称的结构，并且假设一个非对称的结构是对称的，即A的对称性= A。2.2匕首分类定义2.2（Dagger范畴）Dagger范畴是一个范畴C，它与一个对合的、关于对象的恒等式、逆变函子<$：C→C结合在一起。具体地说，这意味着对于每个态射f：A→B，我们关联一个态射f<$：B→A，称为f的伴随，使得对于所有f：A→B和g：B→C：id† = idA：A→A，（gf）<$=f<$g<$：C→A，f<$<$=f：A→B，（一）定义2.3（酉映射，自伴映射）在匕首范畴中，态射f：A→B称为酉的，如果它是同构且f−1=f<$。一个态射f：A→A称为自伴的或厄米特的，如果f=f†。142P. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139=一一ID2.3Dagger对称幺半群范畴定义2.4（匕首对称monoidal范畴）匕首对称monoidal范畴是具有匕首结构的对称monoidal范畴C，使得逆变函子<$：C→C相干地保持对称monoidal结构。具体地说，对于所有f：A → B和g：C → D，“相干地保持对称幺半群结构”的要求意味着以下内容（fg）<$=f<$g<$：BD→AC，†A、B、C−1A、B、C：A<$（B<$C）→（A<$B）<$C，（二）† =λ−1σ†=σ−1：IA→A，：BA→A B。A，B A，B注2.5等价地，“相干地”保持对称幺半群结构另一个来自于一个事实，那就是，对象函子：A<$B<$IDAB（AB）†由于垂直态射和水平态射实际上是恒等式，在这种情况下，相干性等于要求保持对称幺半群结构2.4Dagger紧闭范畴定 义 2.6 （ Dagger 紧 闭 范 畴 [1] ） Dagger 紧 闭 范 畴 是 一 个 Dagger 对 称monoidal范畴，它也是紧闭的，并且使得下图对所有A交换：є †IAAAηAσA，AAA（三）注2.7Abramsky和Coecke为匕首紧闭范畴创造了术语然而，一个匕首结构α=αλP. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139143一一可以添加到几乎任何类型的类别中，因此具有可以扩展到这些情况的术语学是有用的。因为它听起来很傻，例如，说一个注2.8在任何匕首紧闭范畴中，我们有f<$<$t=f<$t。这是等式（3）的结果。反之则不然，即，一个紧闭匕首范畴，其中f=f不一定是匕首紧闭的。为了构造一个反例，取一个匕首紧闭范畴C，其中有一个可逆的但不是酉的标量φ：I→I（例如，有限维希尔伯特空间范畴，φ（x）= 2x）。定义C上一个新的紧闭结构，令ηJ=ηA<$φ，J=φ−1A。在修改的紧致闭结构中，f的定义是不变，因此f<$<$t=f<$t仍然成立。然而，等式（3）不再是满意了。定义2.9（低星运算）给定f：A→B在一个匕首 组合中，我们定义f：A→Byf=f=f。 这个赋值定义了一个协变函子。2.5双产品回想一下零对象和双积的定义。一个对象被称为零对象，如果它是初始的和终结的。如果0是一个零对象，那么在任何两个对象之间存在一个可区分的映射A→0→B，记为0A ， B。如果 A1和 A2是对象，则它们的双积是对象A1<$A2，加上态射qi：Ai→A1<$A2和pi：A1<$A2→Ai，其中i= 1， 2，使得对p1，p2形成乘积锥，对q1，q2形成余积锥，并且pi<$qj=δij。 他eδii=idAi和δij=0Aj，Ai，其中n ii=j。我们说C有有限个双积，如果它有一个零对象0对象回想一下，如果每个hom-set都配备有一个与单元0结合的交换加法运算，使得复合是线性的：（f+g）h=fh+gh，则说C范畴富含交换幺半群，h（f+g）=hf+hg，0h = 0，h0= 0。如果范畴C有有限个双积，则它带有一个这样的正则扩充：给定f，g：A→B，我们可以定义f + g：A→B为f + g = [id B，id B] id A，id A。这个加法的单位是0 A，B，注2.10我们有q1<$p1+q2<$p2= idA<$B。引理2.11设C，D是具有有限双积的范畴，设F：C→D是一个仿函数。 如果F有左或右伴随（特别是，如果F是一个ϵ144P. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139[p<$，p<$]1 2我我等价范畴），则F保持双积直到同构。实际上，在这种情况下，[F（q1），F（q2）]：F（A）<$F（B）→F（A<$B）F（p1），F（p2）F（A）→F（A）<$F（B）是相互对立的。Q这个引理的两种特殊情况特别有趣：在具有双积的紧闭范畴中，张量关于bipro管道，即，则存在一个可按m（A<$B）<$C<$=ACC。此外，如果C是一个具有双积的匕首范畴，则函子自同构地保持双积。然而，一般来说，保持下面的引理给出了实现这一点的四个等价条件引理2.12设C是具有双积的dagger范畴。 则以下条件是等价的。这里Δ = Δ id，id Δ：A→AΔA，并且Δ = [id，id]：AΔA→ A。（a）pt=qi，其中i= 1， 2，（b）（fg）<$=f<$g<$且Δ <$=，（c）f，g=[f<$，g<$]，(d)下图为通勤。A<$B<$IDAB（AB）†id为Q注2.13引理2.12（d）中的图可以看作是一个相干图，类似于注2.5中的图。定义2.14（双积dagger紧闭范畴）一个双积dagger紧闭范畴是一个dagger紧闭范畴，双积，使得p=qi：Ai→A1<$A2，对于所有对象A1，A2和i= 1， 2.P. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139145A、B、C一2.6示例例2.15有限维复向量空间和线性映射的范畴Vect是一个具有双积的紧闭范畴，但它不是dagger紧闭范畴。例2.16有限维希尔伯特空间的范畴FdHilbert是双积匕首紧闭的。f：A→B的伴随是用内积定义的;也就是说，它是唯一的映射f<$：B→A，满足B.F.V.|w=v|f<$w<$，对所有v∈A，w∈ B。例2.17集合和关系的范畴Rel是双积匕首紧闭的。在这一范畴中，A<$B=A×B是集合的卡累利阿积，A<$B=A+B是不交并，A<$=A。对于一个关系R：A → B，我们有R= R<$={（y，x）|（x，y）∈ R}，R∈ R= R.3图形语言对称monoidal范畴和紧闭范畴的图形语言是众所周知的[5，6]。我们简要回顾了这些语言，然后将它们推广到匕首对称monoidal范畴和匕首紧闭范畴。3.1对称monoidal范畴：术语语言在描述对称monoidal范畴的图形语言之前，对它们的术语语言作一个简要的概括是有益的。我们假设给定一个可数的对象变量集，记为α，β，γ等。对象项集是通过二元运算由对象变量和单位对象项I自由构建的。 宾语项的例子有α、I<$α、（α<$β）<$γ等等。 我们用字母A、B、C表示宾语.进一步，我们假设给定一个可数的态射变量集，记为f，g，h等。我们假设每个态射变量都被赋予了A→B形式的固定类型，有时我们写fA→B来显式地指示类型。我们假设有可数多个态射变量，每一种类型。 我们进一步给出态射常数idA，αA，B，C，α−1，λA，λ−1，σA，B，以及它们的通常类型，由对象项A，B，C参数化。类型化态射项的集合是递归定义的：态射变量和态射常数是态射项，如果t：A→B、s：B→C和r：C→D是态射项，那么s<$t：A→C和t<$s：A<$C→B<$D也是态射项。146P. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139不我们还考虑了匹配类型的态射项s，t：A→B之间的方程s = t。 对称么半群范畴的方程理论是由对称么半群范畴的公理生成的方程组。注3.1正如形式语言中通常的那样，我们区分变量的概念（如α或f）和项的概念（如A或t）。当然，符号我们将在下面描述的图形语言中进行类似的区分。3.2对称monoidal范畴：图形语言对称monoidal范畴的图形语言首先由Joyal和Street [5]以数学上严格的方式定义在此之前，它被物理学家非正式地使用了很多年，可以追溯到彭罗斯[8]。在我们将要使用的公式中，对象变量α由标记线α，（4）一个态射变量f：α1<$α2<$... <$αn→ β1<$β2<$. β m由带标签的框表示αn...α2α1βm...β2β1（五）图形语言将对称么半群范畴语言中的每个对象项A与特定的连线相关联，并将每个态射项t与特定的图相关联，该图由连线（4）和盒子（5）组成我们示意性地写A类（6）对于对象项A的表示，以及阿乙（7）对于态射项t的表示：A→B。定义3.2布线（6）是由表1（a）中的对象项A上的递归定义的注意，对象I由零线表示，即，空的线路图（7）是由表1（b）中的态射项t上的递归定义的除了表1所示的情况外，映射αA、B、C、λA及其逆映射也以相同的方式表示。FP. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139147不ts什特(a)对象(b) 态射I：=（空）AB：= B一一个C ：=AC AA：=ACDCA B：=D B一BAB AB：=A B表1对称monoidal范畴注3.3注意，严格地说，图形语言只使用符号（4）和（5），其中α和f是变量。更一般的符号（6）和（7）属于元语言。因此，当我们谈到图的属性（如同构）和图上的操作（如组合）时，我们总是指底层的图语言，而不是元语言。约定3.4当方便使用文本标记时，我们也分别为与对象项A和态射项t：A→B相关联的图写[[A]]和[[t]换句话说，我们写[[A]]：=A[[t]]：=AB备注3.5我们已经用从左到右的方向标记了每根电线，并在每个盒子的左上角标记了一个正方形现在，这些标记是无用的;当我们在下面的紧闭范畴和匕首对称monoidal范畴的图形语言中引入额外的标记时，它们的意义将变得显而易见例3.6方程σAJ，BJ<$（f<$g）=（g<$f）<$σA，B对称的monoidal范畴可以被翻译成一个图解等式，S不σA，BIDA一不 B S148P. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139GFBJ一个一个JBJ通过分别翻译左手边和右手边B B AA=A B这个方程在图形语言中显然是关于图同构在此上下文中的技术上严格的形式化，请参见[5]。事实上，由于Joyal和Street [5]，人们有以下定理定理3.7（对称Monoidal范畴的图形语言）对称Monoidal范畴语言中的态射之间的良型方程由对称Monoidal范畴的公理导出当且仅当它在图形语言中直到图同构都成立。 Q3.3紧闭范畴紧闭范畴的图形语言推广了对称monoidal范畴的现在，可以从右到左或从左到右定向各个导线 A的解释是通过转动接线获得的接线[A]颠倒自下而上的电线顺序。我们把[A]写成[ A]A.. 更正式地说，我们在Meta中定义了以下符号，语言：A：= 一A：= 一I：=（空）AB：=AB注意，从右到左方向的张量积中的线的顺序是从上到下，而不是从下到上。”于是，他又“转”了一圈。结构图ηA：I→A<$A和ηA：A<$A<$→I表示如下：[[ηA]] =A AA[[A]]=一注意，如果t：A→B，则态射t：B→A，它被定义为FG一个JBJP. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139149不不FF一A）α在备注2.1中，给出如下：B[[t]]=A B一这与“倒t图”在逻辑上是相同的[[t]]=B A因为我们已经标记了代表t的盒子的一个角，所以当这样一个盒子被倒置时，我们就有可能知道。当然，这种符号属于元语言。在commpactclosedcategories语言中的方程，如λ−1<$（ηA<$），−1A，A，A◦ （A<$ηA）<$ρA= idA转化为图形方程，例如一A=A一利用图同构的适当概念，可以得到下面的定理，该定理由Kelly和Laplaza [6]隐式证明定理3.8（紧闭范畴的图形语言）紧闭范畴语言中的态射之间的良型方程由紧闭范畴的公理导出当且仅当它在图形语言中直到图同构都成立。Q3.4Dagger对称幺半群范畴dagger对称monoidal范畴的图形语言推广了对称monoidal闭范畴的图形语言。对对象没有附加如果f：A→B是态射变量A B，则f：B→A由如下的新类型的盒表示：[[f†]]：=BA150P. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139FGF我们把它看作是，关于y轴的函数。请注意，对象A和B已交换，但导线的方向保持不变（在本例中为从左到右）。 更一般地说，如果t：A → B是一项，则[t<$]]通过绕y轴反射整个图[t]来获得。公司现采用国际符号：[[t<$]]=B一、我们跳过“反射”的正式递归定义，并给出一个例子：例3.9（图的重绘）假设f：A→ B、C和g：E→C→D，令t=（id B<$g<$）<$αB，C，D<$（f <$id D）.那么t和tt的相应图形表示为：DEt=A CBEt†=BDCA匕首对称么半群范畴的图形语言满足通常的相干定理：定理3.10（dagger对称monoidal范畴的图形语言）dagger对称monoidal范畴语言中的态射之间的一个良型方程由dagger对称monoidal范畴的公理导出当且仅当它在图形语言中直到图同构都成立。证据合理性是通过归纳得出的。为了完备性，假设s，t：A→B的图是同构的。利用等式（1）和（2），我们可以发现项sJ，tJ使得s = sJ和t = tJ在匕首范畴的方程理论中成立，并且使得在sJ，tJ中的唯一应用是态射variable es。 我们不将变量αt视为一个自由变量αt。 Since [[sJ]]和[[tJ]是同构的，sJ= tJ在所有对称么半群范畴中由定理3.7成立。因此，在匕首对称幺半群范畴的语言中，s = SJ= TJ= t。Q不GP. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139151FFFF一一3.5Dagger紧闭范畴将紧闭范畴的图形语言与dagger对称monoidal范畴的图形语言相结合，得到dagger紧闭范畴的图形语言。我们还介绍了符号η†以及：[[]]=A[[η<$]]= 一AAAA†在此基础上，提出了一种新的无功补偿补偿器的定义公式，即ηA=σA，A=σ A，然后显然满足了图形语言中的图形同构A A A†[[ηA]]=A=AA=[[σA，AA]]。定理3.11（Dagger紧闭范畴的图形语言）Dagger紧闭范畴语言中的态射之间的良型方程由Dagger紧闭范畴的公理导出当且仅当它在图形语言中直到图同构都成立。证据该证明与定理3.10相同，只是使用了附加方程（3）并相对于定理3.8工作。QRemark3.12Iff：A→B，thenf，ft：B→A，ft：At→Bt，anddf：B→A的图形表示如下：f=A B f†=B Af=ABf=BA因此，f可以用图形表示为“从x -a x i s中提取“。3.6双积匕首紧闭范畴上述图形语言的方法不容易推广到双积的存在。这是由于对象上存在两个二进制操作（AB和AB）。由于不能通过并置对象来表示这两种操作，因此需要一种更结构化的语法来表示对象术语。最近，Abramsky和Duncan提出了一种基于Girard证明网的这种语言的图形表示方法我们不会在本文中进一步讨论这个问题。152P. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139GG4积极性与CPM构建匕首紧闭范畴是由阿布拉姆斯基和科克引入的，作为量子力学的公理基础，提供了希尔伯特空间中通常公理化的替代（和推广）酉映射、投影、甚至测量和玻恩定则等概念都可以在这个框架中形成[1]。另一方面，本文作者认为，量子编程语言语义的合适框架不是希尔伯特空间和线性映射的范畴，而是完全正算子的范畴CPM[9，10]。使用完全正映射的优点是量子特征（如幺正演化）和经典概率特征（如测量的不同分支）都可以在内部建模为同一范畴内的态射。这一节的目的是证明：（1）从FdHilb构造CPM推广到任何dagger紧闭范畴C以代替FdHilb，以及（2）由此得到的完全正映射范畴也是dagger紧闭的。我们称这种构造为CPM构造。4.1正映射定义4.1（正映射）匕首范畴中的态射f：A→A称为正的，如果存在一个对象B和一个态射g：A→B使得f=g<$g。注4.2如果f：A→A是正的，则一般存在许多形式为f=g<$g的不同分解。我们只对这种分解的存在感兴趣，而不是对特定的分解感兴趣。例4.3在有限维希尔伯特空间的匕首范畴FdHilbert中，正态射正是正算子，即，那些满足条件的|对于所有v，v = 0。例4.4在集合和关系范畴Rel中，正态射恰好是对称且满足xRy<$xRx的关系R：A→A。约定4.5在图形语言中，正映射是映射f：A→A，其形式为A B AP. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139153FA A FI−→AA−→AA−→I.一些B和G。 通过视觉抽象，我们使用符号A A来表示一般的正映射。定义4.6（迹）给定紧致闭范畴中的态射f：A→A，其迹trf：I→I定义为trf=σηAf∗єA利用图形语言，f的迹定义如下：一trf=引理4.7（正映射的性质）下列性质在任何双积匕首紧闭范畴中成立：(a) 如果f是正的，则对任何h，h<$$>f<$h都是正的。(b) 恒等态射idA是正的。另外，如果f：A→A和g：B→B为正，则f g：AB → AB和f g：AB → AB也为正。(c) 零态射0A，A：A→A是正的。此外，如果f，g：A→A为正，则f+g也为正。(d) 如果f是正的，则f=f。(e) 如果f：A → A为正，则f：A→ A和tr f：I → I也为正。(f) 如果f，g：A→A是正的，那么tr（f<$g）：I→ I也是正的。证据（a）-（e）从定义和（-）†所保留的结构来看是直截了当的。对于（f），设g=h<$<$h。则tr（fg）= tr（hfh<$），它对于（a）和（e）是正的。Q注4.8引理4.7（d）的逆命题不成立：例如，对称映射σA，A：A <$A→A<$A满足σ† =σ，但在Rel或FdHilb中不是正的。4.2正矩阵定义4.9（名称，正矩阵）在紧闭范畴中，154P. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139一FFGGKK一G一个态射f：A→B的名字是f'：I → A →BA B[[f态射的名称有时也称为它的矩阵，与向量空间类似一个正矩阵是一个态射f注4.10在图形语言中，正矩阵是以下形式A A=A B A=B AA AB A对于某些B和k=g。 因此，我们使用特殊符号一一一般的正矩阵。4.3全正映射定义4.11（完全正映射）设A，B是dag-ger紧闭范畴中的对象。我们说一个态射f：AA→BB是完全正的，如果对所有对象C和所有正矩阵g：I→CAC，态射C（CfC）g=ABfBC是一个正矩阵。引理4.12设f：A<$A → B<$B。 则f是完全正的，如果且HP. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139155一一BG一BBF仅当一χf：=AB一 fB一是一个正矩阵。证据通过选择C = A和g =（ηA）ηA，从左到右的蕴涵是平凡的。 对于右左蕴涵，设χf是一个正态矩阵. 则（C<$$>f<$C）<$g等于下面的矩阵，它被图形语言看作是正的：（CfC）g=.Q引理4.12是线性代数中Choi定理[ 3 ]的范畴化版本我们也称矩阵χf为f的特征矩阵（cf.[9，Sec.6.7]）。推论4.13使用引理4.12和图形语言，可以直接得出以下等价：(a) f：AA→BB是完全正的，(b) 地图一ABA BB是积极的。(c) 存在正映射g：B<$A <$→B<$A <$，使得f=GC一一B×fB一一C156P. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139FKKHH(d) 存在一个对象C和一个态射h：A→C<$B，使得ABCf=CAB(e) 存在一个对象C和一个态射k：C<$A→B，使得ABCf=CABQ约定4.14根据推论4.13（c）ABAB表示一般的完全正映射f：A<$A→B<$B。注4.15如果f：A→B→B是完全成立的，则f=f → B. 相反的情况一般不成立，参见。备注4.8.注4.16正矩阵g：I→AA与完全正映射f：II→AA（模同构II=I）是一回事。引理4.17（a）恒等映射id：AA→AA是完全正的。(b) 如果f：AA→BB和g：BB→CC是完全正的，那么gA→CC也是完全正的。(c) 如果f：AA→BB和g：CC→DD是完全正的，则∗ ∗∼=∗ ∗C<$A<$A <$C−→A<$A <$C<$CF-1−−→BBD−→DB你好(d) 如果f：A→B是任意的同态，则f∈f：A∈A→B∈B是完全正的.证据 立即，使用图形语言。Q∗P. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139157GFFG4.4CPM建设定义4.18（CPM构造）给定一个匕首紧闭范畴C，我们定义一个新范畴CPM（C），其对象与C的对象相同。CPM（C）中的态射f：A→B是C中的完全正映射f：AA→BB。态射的合成和C中一样。注4.19通过引理4.17（a）和（b），CPM（C）确实是一个范畴。此外，引理4.17（d）得到一个函子F：C→CPM（C），定义为F（A）=A和F（f）=ff。定理4.20 CPM（C）又是匕首紧闭的。对象上的张量积是从C继承的;态射上的张量积由引理4.17（c）给出。结构图αA，B，C，λA，σA，B，ηA和σA都是由C在F下的相应映射的图像给出的。如果f：AA→BB，则CPM（C）中的f f由ff f：BB→AA在C中给出。函子F：C→CPM（C）保持了Dagger紧闭结构。证据所需的方程很容易验证。为了帮助完成这项任务，表2给出了CPM（C）图形语言到C语言的翻译。我们证明一个方程作为一个例子：证明C D B C A BA B D =A C D在CPM（C）中成立，我们必须在C中证明：D D B CD B D A=B B D AB D B CB BB DD DD B这显然是正确的图同构。其他方程的证明也是类似的。Q例4.21范畴CPM（FdHilbert）以有限维希尔伯特空间作为其对象，以完全正映射作为其态射f：AA→BB。它与[9]的范畴W的简单对象的全子范畴相同。 参见下面的示例5.4。 我们注意到正则函子F：FdHilb→CPM（FdHilb）是C一CCG一C一C一AFC一一 F一CGC158P. Selinger/Electronic Notes in Theoretical Computer Science 170（2007）139BGFCCCFGFFFF在的图形语言CPM（ C）：在C语言中：Bf：ABBf†：BABBf：BAB BB Bf：A BA一IDA：Ag/f：AAAA B C一个Cf/g：CDABσA，B：B AABBAABABBA对于所有常数c∈ {id，α，α−1−1，η ，G}：A A，B，CA，B，C，λA，λA，σA，BA Ac：XYXYXY表2图形语言中的CPM构造且仅当存在单位标量φ使得f=φg。换句话说，函子F标识那些只通过相位的全局变化而不同的态射。一一FF一一F一一一一一一FBBBBFBGCC一一CCCAAGFDDBBDBBD