论文标题
镜头下
Coequalisers under the Lens
论文作者
论文摘要
镜头编码用于同步系统的协议。我们继续由Chollet等人开始的工作。在2020年应用类别理论的伴随学校，以研究小型类别和不对称三角洲镜头类别的特性。众所周知，从镜头类别到函数类别的健忘函子已经反映了monos和epen和piseserve epip。我们证明它可以保留Monos，并提供了更简单的证据，证明它保留了EPIS。从其GET函子的基本特性角度来看，这共同对Monic和Epic镜头进行了完整的表征。 接下来，我们启动对镜片的固定器的研究。我们观察到，并非所有平行的镜头对都有固定器，并且从镜头类别到函子类别的健忘函子既没有保留也不反映所有的同性恋者。但是，一些固定式的反映；我们研究了何时发生，然后使用我们学到的东西表明每个史诗般的镜头都是规律的，并且离散的操作纤维构造沿Monic镜头沿着下降。推论包括每个一元镜头都是有效的，每个一元史诗般的镜头都是同构的，所有史诗般的镜头的类别和所有一元镜头的类别都是正交分解系统。
Lenses encode protocols for synchronising systems. We continue the work begun by Chollet et al. at the Applied Category Theory Adjoint School in 2020 to study the properties of the category of small categories and asymmetric delta lenses. The forgetful functor from the category of lenses to the category of functors is already known to reflect monos and epis and preserve epis; we show that it preserves monos, and give a simpler proof that it preserves epis. Together this gives a complete characterisation of the monic and epic lenses in terms of elementary properties of their get functors. Next, we initiate the study of coequalisers of lenses. We observe that not all parallel pairs of lenses have coequalisers, and that the forgetful functor from the category of lenses to the category of functors neither preserves nor reflects all coequalisers. However, some coequalisers are reflected; we study when this occurs, and then use what we learned to show that every epic lens is regular, and that discrete opfibrations have pushouts along monic lenses. Corollaries include that every monic lens is effective, every monic epic lens is an isomorphism, and the class of all epic lenses and the class of all monic lenses form an orthogonal factorisation system.
