Graphical calculi and proof assistants in monoidal n-categories and their application to topological quantum field theory.

幺半群 n 范畴中的图解演算和证明助手及其在拓扑量子场论中的应用。

• 批准号: 2431707
• 金额: --
• 依托单位: University of Birmingham
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2020
• 资助国家: 英国
• 起止时间: 2020 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2431707
• 关键词: Graphical; calculi; proof; assistants; monoidal

Category theory is the study of mathematical structure - a category C consists of a class of objects Obj(C) and, for every two objects A;B 2 Obj(C), a set HomC(A;B) of morphisms such that morphisms can be composed, composition is associative, and every object has an identity morphism to itself. Despite this rather abstract denition, one deals with categories regularly even without realising so - for example, Set has sets as objects and functions between sets as morphisms, while Vectk has vector spaces over a field k as objects and k-linear maps as morphisms. Category theory has a wide range of applications across computer science, physics and maths, including in functional programming, quantum computing and algebraic topology. I would like to apply tools from category theory to these areas during my research. Writing my master's project on category theory and homological algebra has led me to develop a strong interest in both areas, and especially with the interconnections between the two. After reading Algebra: Chapter 0 by Alu[1] and An introduction to homological algebra by Weibel [6] I would like to learn more about derived categories and their applications as they are of obvious importance in homological algebra and there is much current research on derived categories. I am also interested in Homological mirror symmetry as well as other (co)homology theories such as K-theory and how they may be used to solve physical problems.I recently attended the Sixth Symposium on Compositional Structures (SYCO6) where I was introduced to many applications of category theory and graphical calculi which I had not seen before - Vincent Wang's talk on \Graphical Grammar and Graphical Completion of Monoidal Categories" stood out to me as category theory seems natural to use in the study of grammatical structures, yet I had not previously heard of it being used here. Since the talk I have found Bob Coecke's papers on category theory in linguistics very interesting and would like to look further into this during my research. As well as this, Quanlong Wang's talk on \An algebraic axiomatisation of ZX-calculus" was very interesting to me and helped to show me how rigorous the use of diagramatic reasoning can be.Another area I would like to do research in is higher category theory. There are many recent applications of higher category theory in homotopy theory as well as theoretical physics which I have found very interesting and would like to look into, however higher categories are often hard to conceptualise. Proof assistants can be very powerful tools for visualising specific types of n-categories, allowing us to study n-categories without having to check that everything obeys the correct axioms (of which there are many for higher categories) as this is handled by the proof assistant. I aim to work with proof assistants such as homotopy.io to develop higher category theory and to study its applications intopological quantum field theory, specially in dimensions 3 + 1 and higher as these are less well understood.As well as applications of higher categories, I would also like to research different models of higher categories. In an n-category, there are not only sets of morphisms between each pair of objects, but also sets of k-morphisms between each pair of k1 morphisms for all k = 2; 3; :::; n; there are many different ways the composition of higher morphisms may be defined, making general higher categories hard to deal with. I plan to learn more about higher categories and to study which models of higher categories are the most powerful for physical applications. I have been fascinated with topology and I have tried to read as much as I can on it; especially since discovering category theory and seeing how important has been for recent developments in algebraic topology. I would like to be able to learn more about application of higher categories to homotopy theory and to do my own research into it in the future.

范畴论是数学结构的研究-范畴C由一个对象类Obj（C）和，对于每两个对象A;B 2 Obj（C），一个态射集合HomC（A;B）组成，使得态射可以组合，组合是结合的，每个对象都有一个自己的单位态射。尽管有这种相当抽象的定义，但人们经常处理范畴，甚至没有意识到这一点-例如，Set将集合作为对象，将集合之间的函数作为态射，而Vectk将域k上的向量空间作为对象，将k-线性映射作为态射。范畴论在计算机科学、物理学和数学中有着广泛的应用，包括函数编程、量子计算和代数拓扑。我想在我的研究中将范畴理论的工具应用到这些领域。写我的硕士项目的范畴论和同调代数使我在这两个领域发展了浓厚的兴趣，特别是与两者之间的相互联系。阅读代数之后：第0章由Alu[1]和介绍同调代数由Weibel [6]我想了解更多关于导出范畴及其应用，因为它们在同调代数中具有明显的重要性，并且目前有很多关于导出范畴的研究。我也对同调镜像对称和其他（上）同调理论如K-理论以及它们如何被用来解决物理问题感兴趣。我最近参加了第六届组合结构研讨会（SYCO 6），在那里我被介绍到范畴论和图演算的许多应用，这是我以前没有见过的-- Vincent Wang的演讲\Graphical Grammar and Graphical Completion of Monoidal Categories”对我来说，范畴理论似乎很自然地被用在语法结构的研究中，但我以前从未听说过它被用在这里。自从那次演讲以来，我发现Bob Coecke关于语言学范畴理论的论文非常有趣，并希望在我的研究中进一步研究这一点。除此之外，王泉龙的关于“ZX演算的代数公理化”的演讲对我来说非常有趣，并帮助我展示了数学推理的使用是多么严格。另一个我想研究的领域是更高的范畴理论。最近有许多应用程序的高类别理论同伦理论以及理论物理，我发现非常有趣，并希望研究，但更高的类别往往很难概念化。证明助手可以是非常强大的工具，用于可视化特定类型的n-范畴，使我们能够研究n-范畴，而不必检查所有东西都遵守正确的公理（其中有许多是更高的范畴），因为这是由证明助手处理的。我的目标是与证明助手，如homotopy.io合作，发展更高的范畴理论，并研究其在拓扑量子场论中的应用，特别是在3 + 1维和更高的维度，因为这些还不太清楚。在n-范畴中，不仅每对对象之间存在态射集，而且对于所有k = 2; 3;：; n，每对k1态射之间也存在k-态射集;有许多不同的方法可以定义高级态射的合成，使得一般的高级范畴很难处理。我计划学习更多关于更高类别的知识，并研究哪些更高类别的模型对于物理应用来说是最强大的。我一直着迷于拓扑结构，我试图阅读尽可能多的，我可以对它，特别是因为发现范畴理论，并看到如何重要的是最近的事态发展，代数拓扑。我希望能够学习更多关于应用更高的类别同伦理论，并做我自己的研究，它在未来。