Graphical Symplectic Algebra

1,2]Robert I. Booth
3]Titouan Carette
4,5]Cole Comfort
[1]
University of Edinburgh, United Kingdom

[2]
University of Bristol, United Kingdom

[3]
LIX, CNRS, École polytechnique, Institut Polytechnique de Paris, 91120 Palaiseau, France

[4]
Department of Computer Science, University of Oxford, United Kingdom

[5]
Université de Lorraine, CNRS, Inria, LORIA, F 54000 Nancy, France

We give complete presentations for the †-compact props of affine Lagrangian and coisotropic relations over an arbitrary field. This provides a unified family of graphical languages for both affinely constrained classical mechanical systems, as well as odd-prime-dimensional stabiliser quantum circuits. To this end, we present affine Lagrangian relations by a particular class of undirected coloured graphs. In order to reason about composite systems, we introduce a powerful scalable notation where the vertices of these graphs are themselves coloured by graphs. In the setting of stabiliser quantum mechanics, this scalable notation gives an extremely concise description of graph states, which can be composed via “phased spider fusion.”  Likewise, in the classical mechanical setting of electrical circuits, we show that impedance matrices for reciprocal networks are presented in essentially the same way.

Graphical algebra, symplectic geometry, string diagrams, category theory, categorical quantum mechanics, quantum information, quantum computing, classical mechanics, quantum mechanics, quantum optics, stabiliser quantum mechanics, stabilizer codes, physics, graph theory

§ INTRODUCTION

Symmetric monoidal categories formalize  process theories with well-behaved notions of sequential and parallel composition. Just as groups can often be presented in terms of generators and equations, so can symmetric monoidal categories. However, in the symmetric monoidal setting, the generators are interpreted as boxes with wires dangling out of them, and the equations are instead between string diagrams which are built by wiring these boxes together.  Therefore,  unlike for a group, a presentation for a symmetric monoidal category allows one to reason about the underlying process theory using only diagrammatic rewrite rules: appealing to human beings' innate topological intuitions.

Graphical algebra   The research programme broadly construed as “graphical algebra” has produced presentations for categories of relations equipped with algebraic structure, where the monoidal product is given by the disjoint union/direct sum.  For example, the symmetric monoidal  categories of linear relations <cit.>, affine relations <cit.>, piecewise linear relations <cit.>, and polyhedral relations <cit.> have all been given presentations. These aforementioned presentations have notably been used as a syntax for signal flow diagrams in control theory <cit.>, systems with bounded resources <cit.>, and electrical circuits <cit.>.

Categorical quantum mechanics   On the other hand, consider  the process theory of quantum circuits.
Formally, quantum circuits are string diagrams in the symmetric monoidal category of Hilbert spaces with the bilinear tensor as the monoidal product.
The research programme of “categorical quantum mechanics” has produced numerous presentations for fragments of quantum circuits. Examples of which include the ZX-calculus <cit.>, ZW-calculus <cit.>, ZH-calculus <cit.>, ZX&-calculus <cit.> and their various incarnations.   Such presentations have been used for for the design of new quantum circuit optimization techniques <cit.> as well as quantum circuit verification <cit.>.  There are many more applications, which are oulined in the review article of van de Wetering <cit.>.

Graphical algebra meets categorical quantum mechanics   Structural similarities between the research programmes of graphical algebra and categorical quantum mechanics have been noticed for quite some time. Specifically, the symmetric monoidal category of linear relations over \(\mathbb{F}_2\) was observed by many people to be isomorphic to the phase-free fragment of the qubit ZX-calculus modulo scalars. This is written down explicitly in the PhD thesis of  [page 64]ih as well as in the work of [page 12]control. This connection has been exploited to reason about \(\mathbb{F}_2\)-linear subspaces in the qubit ZX-calculus, for example in the work of carette_szx-calculus_2019.  A deeper connection between both research programmes was conjectured in the PhD thesis of [page 146]ih. However, some structures of the ZX-calculus, such as the Hadamard gate/Fourier transform and phases were believed by some to be too inherently quantum to be captured in this way.

Zanasi's conjecture was later shown to be true by comfort_graphical_2021 who proved that the symmetric monoidal category of affine Lagrangian relations over \(\Zp\) is isomorphic to the odd-prime-dimensional qudit stabiliser ZX-calculus, modulo scalars. Affine Lagrangian relations can be seen to generalize linear relations, and it can accommodate for more notions in quantum circuits such as the Fourier transform and Clifford phases.   Later Comfort showed that one can take this correspondence even further by extending the relational semantics to affine coisotropic relations: in the quantum semantics, this corresponds to adding quantum discarding <cit.>. However, neither paper provides presentations for these symmetric monoidal categories.

Quantum mechanics meets classical mechanics   Before these developments of Comfort et al. in the relational semantics of quantum circuits, Baez et al., had already interpreted electrical circuits are in the symmetric monoidal category of affine/linear Lagrangian relations over the fields of real and real rational functions <cit.>.  This is also discussed in the PhD thesis of coya who was also a coauthor in <cit.>. In this research programme they refer to this interpretation as a “black-box” which determines the behaviour of the  electrical circuit, but which one can not look inside of: imparting an air of mystery on the compositional structure of affine Lagrangian relations.

In fact, categories of Lagrangian relations have a rich history in the context of the geometric quantisation of classical mechanics
So in retrospect, this connection between quantum and classical mechanics should have not been surprising. However, the rich research programme of geometric quantisation is generally not concerned with string diagrams, therefore, they also do not provide graphical presentations for these symmetric monoidal categories.

Our contribution   In this article  we give presentations for the symmetric monoidal categories of linear Lagrangian relations, affine Lagrangian relations, linear coisotropic relations and affine coisotropic relations over arbitrary fields: the prop of affine coisotropic relations being the most general one. These are symmetric monoidal subcategories of linear and affine relations; however they are quite special. They can be constructed by first doubling the dimension of the objects in linear and affine relations and then adding  “shearing operations” in both dimensions. As mentioned earlier, these symplectic categories of relations give semantics for the phase-space picture of both quantum and classical mechanics. Therefore, the presentations we give here yield a unifying treatment for classical mechanical circuits as well as a fragment of quantum circuits.

Therefore, from a conceptual point of view, in this paper we “open up the black box” of Baez et al. which was hitherto closed.  By giving presentations for these symplectic categories of relations, we reveal their underlying compositional structure: exposing some deep  connections between quantum and classical mechanical circuits. Moreover, by exploring the structure of the strictification of these categories, we obtain powerful scalable notation for composite systems. This allows us to give elegant and concise descriptions of the normal forms for stabiliser circuits, as well succinct descriptions of notions like graph states and impedance matrices for reciprocal networks.

Structure of paper   In section <ref> we review of string diagrams for symmetric monoidal categories and their close relatives.

In section <ref> we give a presentation for the symmetric monoidal category of affine relations over an arbitrary field.  The presentation which we gives differs slightly from that of gaa.  This is because we use a different set of generators inspired by the ZX-calculus which allows us to represent circuits in terms of undirected coloured graphs.  Using this presentation, we review how some basic notions in linear and affine algebra can be stated graphically.

In section <ref> we prove the core result of the paper: providing a presentation for the symmetric monoidal category of affine Lagrangian relations over an arbitrary field.  We begin this journey in subsection <ref> by defining the category of Lagrangian relations and giving a brief review of linear/affine symplectic geometry. Following this, in subsection <ref>, we give generators and equations for Lagrangian relations, without yet proving that this gives a complete presentation.  In subsection <ref>, we introduce scalable notation for affine Lagrangian relations where our generators are generalized to composite systems so that the graphs themselves become coloured by graphs.  In subsection <ref> we use this scalable notation to establish a normal form for affine Lagrangian relations, from which it follows that the generators and equations form a complete presentation.

In section <ref> we extend the results of section <ref> to the more general setting of affine coisotropic relations. Semantically, this is given by adding the relation which discards the plane; syntactically, this is given by adding a generator which discards isometries.  This connects coisotropic reduction in symplectic geometry to the essential uniqueness of purification in quantum mechanics.

In section <ref> we conclude the paper by giving  various applications of our calculus to concrete physical systems, both in the classical and quantum realm.

In appendix <ref>, we give axiom tables summarizing all of the presentations which we develop in this paper.

We put the gory technical details of the proofs, as well as technical lemmas in appendix <ref>.

§ GRAPHICAL LANGUAGES

As mentioned in the previous section, symmetric monoidal categories give mathematical semantics for processes with a certain notion of sequential and parallel composition.  A reference for symmetric monoidal categories can be found in Mac Lane   <cit.>.
Throughout this section, let \((\mathsf{C},\otimes,I)\) denote a symmetric monoidal category with tensor product $(-)\otimes(=):\mathsf{C}\times\mathsf{C}\to\mathsf{C}$ and tensor unit $I \in \operatorname{Ob}(\mathsf{C})$.  Denote the structure maps of the symmetric monoidal category  as follows:

* associators: \(\alpha_{X,Y,Z} : X \otimes (Y \otimes Z) \cong (X \otimes Y) \otimes Z\)

* unitors: \(\lambda_X : I \otimes X \cong X\)     and     \(\rho_X: X \otimes I \cong X\)

* symmetries: \(\sigma_{X,Y} : X \otimes Y \cong Y \otimes X\)

§.§ String diagrams

A symmetric monoidal category is strict when the unitors and associators are identities.  Strict symmetric monoidal categories are very convenient to work with because they enjoy a graphical calculus in terms of string

An arrow \(f : X_1 \otimes \cdots \otimes X_m \to Y_1 \otimes
\dots \otimes Y_n\) is drawn as a box with \(m\) input wires on the left,
and \(n\) output wires on the right, where each wire is labeled by the corresponding object:

\begin{equation}
\tikzfig{figures/strings/morphism}
\end{equation}

We will often drop the
labels on wires when the objects can be inferred from context. The identity on the monoidal
unit is drawn as an empty diagram, the identity on all other objects as a plain wire, and the components of the symmetry are drawn as wires crossing:

\begin{equation}
\tikzfig{figures/strings/monoidal_unit}
\quad\quad\quad
\tikzfig{figures/strings/identity}
\quad\quad\quad
\tikzfig{figures/strings/symmetry}
\end{equation}

The composition of  arrows is drawn by “plugging wires” and the monoidal product of
arrows as “vertical juxtaposition”:

\begin{equation}
\tikzfig{figures/strings/composition}
\quad\quad\quad
\tikzfig{figures/strings/monoidal_product}
\end{equation}

String diagrams for symmetric monoidal categories can be manipulated as one might expect:

\begin{equation}
\tikzfig{figures/strings/symmetry_equations}
\end{equation}

Arrows of type \(I\to X\) are called states, arrows of type \(X\to I\) are called effects, and endomorphisms \(I\to I\) are called scalars.

A prop is a strict symmetric monoidal category which is generated by a single object under the tensor product.
In other words, the monoid of objects under the tensor product is isomorphic the the natural numbers \(\N\).
Exploiting this isomorphism, we can always drop the wire labels because the types of arrows are uniquely identified by the number of input and output wires. For example,
an arrow \(f : 3 \to 2\) in a prop is represented as:

\begin{equation}
\tikzfig{figures/strings/prop_morphism}
\end{equation}

§.§ Strictification and scalable notation

Without loss of generality, using the following well-known result, it is always possible to use string diagrams to
reason about (not necessarily strict) symmetric monoidal categories:

Every symmetric monoidal category is symmetric monoidally equivalent to a strict symmetric monoidal category.

This process is called strictification. There is an explicit strictification
procedure for monoidal categories described by wilson presented in terms of generators and relations.
Similar results exist in the context of multiplicative linear logic: for example by robin. Although the
specific symmetric monoidal strictification procedure we use here has not explicitly appeared in the literature,
it follows straightforwardly from the aforementioned results:

Given a symmetric monoidal category \((\mathsf{C},\otimes,I)\), its strictification \(([\mathsf{C}],+,[])\)  has:

* Objects:  in \(\operatorname{List}(\mathrm{Ob}(\mathsf{C}))\).

* Arrows: For every arrow \(f:X\to Y\) in \(\mathsf{C}\) there is an induced arrow \([f]:[X]\to[Y]\) in \([\mathsf{C}]\).  Moreover, for all objects \( X,Y\) in \(\mathsf C\) we have the following arrows in  \([\mathsf{C}]\):

Dividers:       figures/strings/tensor_dividers
Gatherers:      figures/strings/tensor_gatherers

We impose the following equations between arrows:

\begin{equation}
\label{eq:functor}
[f]\circ [g] = [f\circ g], \ \ [1_X]=1_{[X]}
\end{equation}

\begin{equation}
\label{eq:strings_tensor_equations}
\tikzfig{figures/strings/tensor_equations}
\end{equation}

* Strict monoidal structure: The tensor unit is the empty list \([\ ]\).  The tensor product \(+\) is list concatenation.

* Symmetries: given by permutations of list elements.

The strictification functor  \([-] : (\mathsf{C},\otimes,I) \simeq ([\mathsf{C}],+,[\ ])\) takes arrows \(f:X\to Y\) to \([f]:[X]\to [Y]\).  For this reason we overload notation and take \([f]=f\). Equations (<ref>) witness the functoriality and  equations  (<ref>) witness the preservation of the symmetric monoidal structure. The dividers and gatherers are the components of the monoidal laxators for the strictification functor.

The components of the associator, unitors and symmetry in \(\mathsf{C}\) are in are internalized to the following string diagrams in \([\mathsf{C}]\):

\begin{equation}
\tikzfig{figures/strings/tensor_structure_maps}
\end{equation}

where their inverses are given by flipping the string diagrams around horizontally.

Scalable notation   In this paper, we only work with props.  Even though props are already strict, it will still be useful to work with their strictifications.
This allows for inductive arguments to be made using only string diagrams.  To this end, first remark that in the strictification of a strict symmetric monoidal category, the laxators and oplaxators obey the following equations:

\begin{equation}
\label{eq:scalablemonoid}
\tikzfig{figures/strings/monoid}
\quad
\tikzfig{figures/strings/comonoid}
\end{equation}

In order to make inductive arguments for props using only pictures, following Carette et al. <cit.>, as a matter of convention denote the object \([1]\) by a thin wire, and the objects \([n]\) for \(n \in \N\) by thick wires (often labelled by their type \(n\)).
For example, we use this notation to describe block matrices string digrammatically in subsection <ref>.

Call this collection of graphical notation scalable notation.

§.§ Duality and flexsymmetry

In this subsection, we extend symmetric monoidal categories with a notion of feedback:

A symmetric monoidal category is compact-closed when  for every object \(X\), there exists an object \(X^*\) together with a map \(\eta_X : I \to X \otimes X^*\) called the cup and a map  \(\epsilon_X : X^* \otimes X \to I\) called the cap, drawn as follows:

\begin{equation}
\tikzfig{figures/strings/cup}
\quad\qand\quad
\tikzfig{figures/strings/cap}
\end{equation}

We require that \((X\otimes Y)^*=X^*\otimes Y^*\) and \(I^*=I\).  We also require the cups and caps to satisfy the following equations:

\begin{equation}
\tikzfig{figures/strings/string_pulling}
\end{equation}

A compact prop is a compact-closed prop for which \(1^*=1\) and where cup and cap are symmetric, meaning that they satisfy $\epsilon_1 \circ \sigma_{1,1} = \epsilon_1 $ and $\sigma_{1,1} \circ \eta_1  = \eta_1 $.

Given a compact prop \((\mathsf{C},+ ,0)\), an arrow \(f : m \to n\) is flexsymmetric if for any permutation \(\varsigma\) of \(m+n\) wires:

\begin{equation}
\tikzfig{figures/strings/flexsymmetry}
\end{equation}

Notice that the cup and the cap are flexsymmetric. In some cases, compact props admit flexsymmetric presentations, that is, a presentation where all generators are flexsymmetric. In other words, the string diagrams can be treated as labeled graphs, and we no longer need to worry about the orientation of edges and arrows: only the connectivity of the diagram matters! This is very desirable from a computer science perspective, because it greatly simplifies the combinatorics of representing string diagrams with a data structure. More details on flexsymmetric presentations can be found in the PhD thesis of Carette <cit.>.

Dagger structure   In many settings, a process \(X\to Y\) is canonically associated to a process of the “reversed type” \(Y\to X \).  However, this map need not be the inverse.  This idea can be captured as follows:

A †-compact prop is a compact prop \((\mathsf{C}, \otimes, I)\) equipped with a functor of props \( (-)^\dag : \mathsf{C}^\mathsf{op}\to  \mathsf{C} \) such that:

* For all objects \( X \) in \(\mathsf{C}\), \(X^\dag = X\).

* For all maps \(f:X\to Y\) in \(\mathsf{C}\),  \( (f^\dag)^\dag=f  \).

* \(\sigma_{1,1}^\dag= \sigma_{1,1}^{-1}\) and \(\eta_1^\dag=\epsilon_1\).

In such a setting, an arrow \(f:X\to Y\) is an:

* isometry when \(f^\dag  f = 1_X\).

* coisometry when \(f f^\dag = 1_Y\).

* unitary when it is both an isometry and coisometry (so that \(f^\dag = f^{-1}\)).

§ GRAPHICAL LINEAR AND AFFINE ALGEBRA

In this section we review string diagrammatic presentations of the props of affine and linear subspacesby Bonchi et al. <cit.>, which we will respectively refer to as Graphical Linear Algebra (GLA)  and Graphical Affine Algebra (GAA). GAA can be seen as a strict extension of GLA, thus we will first give its presentation and then restrict it to GLA. Note that the presentations which we give follow directly but differ slightly from those contained in the work of Bonchi et al. <cit.>.

§.§ Props of linear and affine relations

Given some fixed set \(X\), an \(X\)-relation \(R:n\to m\) is a subset of the product \(R\subseteq X^n \times X^m\).  These form a compact prop:

Given a set \(X\), the compact prop of \(X\)-relations, \(\RX\), has:

* Arrows are relations between \(X^n\) and \(X^m\).

* Composition of relations \(R:n\to m\) and \(S:m\to k\) is defined as:

\[ S\circ R \coloneqq  \{ (x,z) \in X^{n}\times X^k \ | \ \exists y \in X^m: (x,y) \in R \wedge (y,z) \in S  \}:n\to k \]

* Identity on \(n\) is given by the diagonal relation \(\{(x,x) \in  X^n\times X^n \}:n\to n \)

* Monoidal structure is given by the object \(0\) and the Cartesian product:

\[ S\times T \coloneqq \left\{\left(\begin{bmatrix}x\\y \end{bmatrix},\begin{bmatrix}z\\w\end{bmatrix}\right)  \,\middle|\,   (x,z) \in S\wedge  (y,w)\in T \right\} \]

* Symmetric structure is generated by the relation:

\[\sigma_{1,1}\coloneqq \left\{\left(\begin{bmatrix}x\\y \end{bmatrix},\begin{bmatrix}y\\x\end{bmatrix}\right)  \,\middle|\,  x,y\in X\right\}:2\to 2 \]

* Compact structure is generated by the relations:
\[\eta_1\coloneqq \left\{\left(\bullet,\begin{bmatrix}x\\x\end{bmatrix}\right)  \,\middle|\,  x\in X\right\}:0\to 2\quad\text{and}\quad\epsilon_1\coloneqq \left\{\left(\begin{bmatrix}x\\x\end{bmatrix}, \bullet\right)  \,\middle|\,  x\in X\right\}:2\to 0\]

Given a function \(f:X^n\to X^m\) then its graph is a relation \(\Gamma_f\coloneqq \{(x,f(x))\ |\ x\in X \}:n\to m\). This assignment is functorial, so that the composition of functions corresponds to the relational composition of their graphs.

We restrict this prop to the linear and affine settings. To this end, first recall some basic linear and affine algebra:

Given a field \(\K\) and some \(n\in\N\), a \(\K\)-affine combination of vectors \(\vec v, \vec w \in \K^m\) is a vector \(a \cdot \vec v + (1-a)\cdot \vec w \) for some \(a\in\K\). More generally, \(\K\)-linear combination of vectors \(\vec v, \vec w \in \K^m\) is a vector \(a \cdot \vec v + b\cdot \vec w \) for some \(a,b\in\K\).

A \(\K\)-affine subspace of \(\K^n\) is subset \(V\subseteq \K^n\) which is closed under affine combinations. Similarly, a \(\K\)-linear subspace of \(\K^n\) is nonempty subset \(V\subseteq \K^n\) which is closed under linear combinations.

Given any nonempty affine subspace \(V\subseteq \K^n\), there exists a  vector \(\vec a\in\K^n\)  such that the coset \( V+ \vec a \coloneqq \{\vec v+\vec a \ | \ \forall \vec v \in V \}\subseteq \K^n \) is a linear subspace.  Call this vector, the affine shift associated to \(V+\vec a\).
Conversely, every linear subspace is an affine subspace, as affine combinations are particular linear combinations.  Conceptually, affine subspaces are linear subspaces without a fixed origin. This justifies why we don't require affine subspaces to be inhabited: since there is no fixed origin, it need not contain the zero vector.

Both of these notions of subspaces induce a compact prop:

Given a field \(\K\), the category, \(\AR\) (resp. \(\lR\)), of \(\K\)-affine (resp. linear) relations is the sub-prop of  \(\RK\) whose arrows \(n\to m\) are \(\K\)-affine (resp. linear) subspaces of the vector space \(\K^n\times\K^m \cong \K^{n}\oplus \K^m\).

This is a category because affine (resp. linear) subspaces are closed under relational composition, and that the diagonal subset is a linear subspace. This is a compact prop because the cup, the cap and symmetry are also linear subspaces.

By construction we have \(\lR \hookrightarrow \AR \hookrightarrow \RK\). In \(\lR\) and \(\AR\), the arrows \(0 \to n\) are exactly linear and affine subspaces of \(\K^n\).  In \(\lR\) there is a unique scalar \(1_0:0\to 0\), corresponding to the linear subspace \(\K^0 \subset \K^0\). But in \(\AR\) we have two scalars, the identity and the empty affine subspace \(\emptyset\subset \K^1\).

§.§ Graphical affine algebra and its interpretation

In this subsection, we review the graphical presentations for the props of affine and linear relations of Bonchi et al <cit.>.

Let \(\K\) be an arbitrary field, and  \(\K^*\) is the group of invertible elements of \(\K\) under multiplication.

We start with affine relations, and then restrict  to linear relations:

Let \(\GAA\) be the compact prop where the arrows are generated by  grey and white spiders, as well as scalar multiplication for every \(a \in \K\):

\[
\tikzfig{figures/AffRel/b-spider}\quad
\tikzfig{figures/AffRel/w-spider}\quad
\tikzfig{figures/AffRel/scalar}\quad
\]

Modulo the equations making the grey and white spiders flexsymmetric as well as the equations, for all \(a,b\in \K\) and \(c \in \K^*\):

\[\tikzfig{figures/AffRel/axioms}\]

With the derived generators, for all \(a\in\K\):

\[
\tikzfig{figures/AffRel/scalar-daggered}
\coloneqq
\tikzfig{figures/AffRel/scalar-twisted}
\]

There is an isomorphism of compact props  \(\interp{-}_{\gaa}^{\abbrar}:\GAA \cong \AR\)  defined on generators, for all \(n,m\in\N\) and \(a\in \K\):

\begin{align*}
\interp{\tikzfig{figures/AffRel/b-spider}}_{\gaa}^{\abbrar}
\left\{
\left(
\begingroup
\renewcommand*{\arraystretch}{.7}
\begin{bmatrix}
a\vspace*{-.2cm}\\ \vdots \\ a
\end{bmatrix}
\begin{bmatrix}
a\vspace*{-.2cm}\\ \vdots \\ a
\end{bmatrix}
\endgroup
\right) \in \K^{n}\oplus \K^m
\ \middle|\
a \in \K
\right\} \\
\interp{ \tikzfig{figures/AffRel/w-spider}}_{\gaa}^{\abbrar}
\left\{
(\vec b, \vec c)
\in \K^n \oplus \K^m
\ \middle|\
\sum_{j=0}^{n-1} b_j + \sum_{k=0}^{m-1} c_k  = a
\right\} \\
\interp{ \tikzfig{figures/AffRel/mult}}_{\gaa}^{\abbrar}
&\coloneqq \left\{ \left(b,ab \right) \ \middle|\ b \in \K \right\}
\end{align*}

The notions of white and grey spiders labelled by a phase-group will occur throughout the rest of this paper in different incarnations:

Given a group \(\mathcal{G}=(G,+,0)\), the compact prop of \(\mathcal{G}\)-labelled white spiders is generated by, for each \(a \in G\) and \(n,m \in \N \):

\[\tikzfig{figures/AffRel/labelled-w-spider}\]

modulo flexsymmetry (see definition <ref>) and the following equations for all \(a,b\in G \):

\[\tikzfig{figures/AffRel/labelled-w-spider-axioms}\]

Similarly, the compact prop of \(\mathcal{G}\)-labelled grey spiders is generated by, for each \(a \in G\):

\[\tikzfig{figures/AffRel/labelled-b-spider}\]

modulo flexsymmetry and the following equations for all \(a,b\in G \) and \(n,m \in \N \):

\[\tikzfig{figures/AffRel/labelled-b-spider-axioms}\]

In both cases, say that \(\mathcal{G}\) is the phase group of the white and grey spiders.

Therefore, we see that the white phase group of \(\GAA\) is the additive group of \(\K\); whereas the grey phase group is the trivial group.  As opposed to \(\AR\), we find that \(\lR\) has a more symmetric presentation:

By restricting the phase group of the  grey spider in \(\GAA\) to be the trivial group, and removing the rules involving non-zero phases, we obtain a presentation \(\GLA\) for \(\lR\).

Note that our presentations  \(\GAA\) of \(\AR\) and \(\GLA\) of \(\lR\) differ from their original presentations by Bonchi et al. <cit.>. The original presentation of affine relations is recovered from ours via the translation:

\[ \tikzfig{figures/AffRel/traduction} \]

Where the original presentation of  \(\lR\) can be recoverd by restricting \(a=0\).

In our presentations \(\GAA\) and \(\GLA\) both grey and white spiders are flexsymmetric generators. In particular, this means that affine relations over \(\Q\) and \(\Zp\) for prime \(p\) admit flexsymmetric presentations because all scalars are generated by the scalars \(1\) and \(0\) under addition, multiplication and division.

This flexsymmetric presentation makes typesetting diagrams much easier, as one doesn't have to worry about the direction which wires are connected to generators; however, it will be useful to keep both presentations in mind, as the original non-flexsymmetric presentations are more natural from an algebraic perspective. For example, the concrete semantics of the constructions in the following subsection are more easily interpreted in the non-flexsymmetric presentation.

§.§ Scalable notation for graphical linear and affine algebra

In this subsection we give notations for the strictification of \(\GAA\). This allows for many concepts
in linear and affine algebra to be expressed concisely using pictures.

Scalable spiders are defined by induction on the colour of wire \(k\in\N\).
The base case is given by the identity on the tensor unit:

\begin{equation}
\tikzfig{figures/AffRel/scaledspidef_basecase}
\end{equation}

The inductive step is given by:

\begin{equation}
\label{eq:GAAthickspiders}
\tikzfig{figures/AffRel/scaledspidef}
\end{equation}

These scalable spiders satisfy analagous axioms as before, except now the white \([k]\)-coloured spiders are indexed by the additive group of \(\K^k\).

As a matter of notation, for any \(n,m\in\N\) take \(\Matrices\) to be the set of \(m \times n\) matrices over \(\K\).

Block matrices are defined by induction on the domain and codomain.
The base cases are given by the unique matrices \(0_{0,0}\in \Matrices[0][0]\), \(0_{0,1}:\in \Matrices[0][1]\) and \(0_{1,0}\in \Matrices[1][0]\):

\begin{equation}
\tikzfig{figures/AffRel/matrixarrow_basecase}
\end{equation}

For the first inductive step given a vector \(\vec v \in \K^m\), and an element \(a\in\K\) we can build the matrix arrow  for \( [a  \ {\vec v}^\trans]^\trans \in \K^{m+1}\):

\begin{equation}
\label{eq:blockmatrixinductivestep0}
\tikzfig{figures/AffRel/matarrowdef}
\end{equation}

For the second inductive step, given a matrix \(A\in \Matrices[m][n]\) and a vector  \(\vec v\in \K^m \), we can build the matrix arrow for  \([\vec v \ A ] \in \Matrices[m][n+1]\):

\begin{equation}
\label{eq:blockmatrixinductivestep1}
\tikzfig{figures/AffRel/matarrowdef1}
\end{equation}

Unrolling this inductive definition, a block matrix divided once both horizontally and vertically is represented by:

\begin{equation}
\label{eq:arrow_decomposition}
\tikzfig{figures/AffRel/blockmatex}
\end{equation}

So that any affine transformation \((A,\vec v);\ x\mapsto Ax + \vec v \) is represented by the following diagram:

\begin{equation}
\label{eq:affinematrix}
\tikzfig{figures/AffRel/affinematex}
\end{equation}

Note that the extra white nodes on the right hand sides of equations (<ref>), (<ref>) and (<ref>) are artifacts of our flexsymmetric presentation. From this representation the following rules directly follow:

\begin{equation}
\label{matrules}\tikzfig{figures/AffRel/matrules}
\end{equation}

As a matter of notation, just like the converse of scalar multiplication, the converse of a matrix \(A\) is given by:

\begin{equation}
\tikzfig{figures/AffRel/matrix-daggered}
\coloneqq
\tikzfig{figures/AffRel/matrix-twisted}
\end{equation}

Using this notation, we can depict the image and the kernel of a matrix \(A\) using pictures:

\begin{equation}
\interp{\tikzfig{figures/AffRel/matarrowspace1}}_{\gaa}^{\abbrar}=\ker(A)\quad\interp{\tikzfig{figures/AffRel/matarrowspace2}}_{\gaa}^{\abbrar}=\im(A)
\end{equation}

And more generally the affine subspace of solutions for \(\vec v\) in the  equation \(A\vec v=\vec w\):

\begin{equation}
\interp{\tikzfig{figures/AffRel/matarrowspace3}}_{\gaa}^{\abbrar}=\left\{\vec w \,\middle|\,  A \vec w=\vec v\right\}
\end{equation}

Note that in this relational setting, it is perfectly fine to ask for the the image or kernel of an affine relation by replacing the matrix arrows with arbitrary maps.

We end this section by recalling diagrammatic reformulation of injectivity and surjectivity:

For any matrix $A$ we have the following two separate columns of equivalent propositions:

\((1)\)     \(A\) is injective               \((1)\)     \(A\) is surjective

\((2)\)     figures/AffRel/inj3         \((2)\)     figures/AffRel/surj3

\((3)\)     figures/AffRel/inj2         \((3)\)     figures/AffRel/surj2

\((4)\)     figures/AffRel/inj1        \((4)\)     figures/AffRel/surj1

§ GRAPHICAL LINEAR AND AFFINE LAGRANGIAN ALGEBRA

In this section, we refine graphical treatments of linear and affine algebra to the symplectic setting. To this end, we first review some of the basic notions in linear symplectic geometry:

§.§ Symplectic linear and affine algebra

A symplectic \(\K\)-vector space is a \(\K\)-vector space \(V\) endowed
with a bilinear map \(\omega_V: V \oplus V \to \K\) called the  symplectic form which is:

* Alternating: For all \(\vec v \in V\), \(\omega_V(\vec v,\vec v)=0\).

* Nondegenerate: Given some \(\vec v \in V\): if for all \(\vec u\in V\) \(\omega_V(\vec v,\vec u)=0\), then \(\vec v=\vec 0\).

A symplectic \(\K\)-linear map
between symplectic spaces \((V,\omega_V) \to (W, \omega_W)\) is a \(\K\)-linear
map \(S : V \to W\) that preserves the symplectic form, i.e. \(\omega_W(S\vec v,S\vec u)
= \omega_V(\vec v,\vec u)\) for all \(\vec v, \vec u\in V\). A
symplectomorphism is a symplectic isomorphism.
Similarly, a symplectic \(\K\)-affine map is a \(\K\)-affine map whose linear component is symplectic; and an affine symplectomorphism is an  symplectic \(\K\)-affine isomorphism.

The vector space \(\K^0\) has trivial symplectic structure.
The next most simple example of a symplectic vector space is
\(\K^2\) equipped with the symplectic form

\[
\omega_{1}\!\left(\begin{bmatrix}z_0\\ x_0\end{bmatrix}, \begin{bmatrix}z_1\\ x_1\end{bmatrix}\right)
\coloneqq  z_0x_1-x_0z_1
\]

Call the first component of \(\K^2\cong \K\oplus\K\) the \(Z\)-grading, and the second the \(X\)-grading.

The vector space \(\K^{2n}\) is also a symplectic vector space with the symplectic form:

\[\omega_n\!\left( \bigoplus_{j=0}^{n-1} \begin{bmatrix}z_j\\x_j\end{bmatrix}, \bigoplus_{j=0}^{n-1} \begin{bmatrix}z_j'\\x_j'\end{bmatrix} \right) \coloneqq  \sum_{j=0}^{n-1} \omega_1\!\left(\begin{bmatrix}z_j\\x_j\end{bmatrix} ,\begin{bmatrix}z_j'\\x_j'\end{bmatrix} \right)\]

Every finite-dimensional symplectic vector space \((V,\omega_V)\) is symplectomorphic to the symplectic vector space \((\K^{2n} , \omega_n)\).

There is an intuitive geometric interpretation of \(\omega_n\): it refines the measure of oriented volumes in \(\K^{2n}\), as \(\bigwedge_{j=1}^n \omega_1\) is a volume form. For \(n=1\), \(\omega_1\) captures the area of a parallelogram given by points \((z_0,x_0),(z_1,x_1)\in\K^2\). This is visualized as follows, where the vertical axis denotes the \(X\)-component, and the horizontal axis denotes the \(Z\)-component:

\begin{equation}
\label{eq:volume}
\tikzfig{figures/AffLagRel/symplectic_volume/volume}
\end{equation}

Therefore the  linear and affine symplectomorphisms are the linear and affine transformations which preserve oriented volume between the \(Z\) and \(X\)-gradings:

Using affine symplectomorphisms, the parallelogram from equation (<ref>) can be:

\begin{align*}
&\bullet\ \text{\em Squeezed:}
\quad
\xmapsto{
\begin{bmatrix}
a^{-1} & 0\\
0    & a
\end{bmatrix}
\tikzfig{figures/AffLagRel/symplectic_volume/squeezing}
\hfil
&\bullet\ \text{\em Sheared:}
\quad
\xmapsto{
\begin{bmatrix}
1 & a\\
0 & 1
\end{bmatrix}
\tikzfig{figures/AffLagRel/symplectic_volume/sheared}
\\
&\bullet\ \text{\em Rotated:}
\quad
\xmapsto{
\begin{bmatrix}
0  & 1\\
-1 & 0
\end{bmatrix}
\tikzfig{figures/AffLagRel/symplectic_volume/rotating}
\hfil
&\bullet\ \text{\em Shifted:}
\quad
\xmapsto{
\left(
\begin{bmatrix}
1 & 0\\
0 & 1
\end{bmatrix}
\begin{bmatrix}
\end{bmatrix}
\right)
\tikzfig{figures/AffLagRel/symplectic_volume/shifting}
\end{align*}

Notice that for $n=1$ the symplectic form is a volume form and hence the correspondence is perfect, however, for $n\geq 2$, symplectomorphisms are still volume preserving but there are volume preserving maps that are not symplectomorphisms.

Given a linear subspace \(S\) of a symplectic vector space \((V,\omega)\), its symplectic
complement is the linear subspace:

\[S^\omega \coloneqq \left\{\vec v \in V \,\middle|\,  \forall \vec s \in S: \omega(\vec v,\vec s)
= 0\right\}\subseteq V\]

A linear subspace \(S\) of a symplectic vector space \((V,\omega)\) is:

* isotropic if \(S \subseteq S^\omega\) (so that for all \(\vec s, \vec t \in S\), \(\omega(\vec{t}, \vec{s})= 0\));

* coisotropic if \(S^\omega \subseteq S\);

* Lagrangian if it is both isotropic and coisotropic (so that \(S = S^\omega\)).

Similarly, an affine subspace \((S,\vec a)\) of  a symplectic vector space \((V,\omega)\) is isotropic / coisotropic / Lagrangian when either \(S\) is isotropic / coisotropic / Lagrangian, or \(S\) is empty.

Any line in the affine plane is given by an affine Lagrangian subspace of \((\K^2,\omega_1)\).  These take of one of the two following forms, for some \(a,b\in \K\):

\[
\left\{\begin{bmatrix}z\\x\end{bmatrix} \in \K^2\ \middle| \ x=bz+a \right\}
\quad\text{visualized as}\quad
\tikzfig{figures/AffLagRel/symplectic_volume/line0}
\]

\[
\left\{ \begin{bmatrix}z\\x\end{bmatrix} \in \K^2\ \middle| \ z=bx+a \right\}
\quad\text{visualized as}\quad
\tikzfig{figures/AffLagRel/symplectic_volume/line1}
\]

Notice that the intersection of both classes of lines are the lines which pass through the origin and which are not completely vertical or horizontal.

The entire plane, however, is the coisotropic subspace
\(\K^2 \subseteq \K^2\)
whereas its orthogonal complement, the origin, is an isotropic  subspace
\(\K^0 \subset \K^2\).  An arbitrary single point on the plane is an affine coisotropic subspace.

From a geometric point of view, we see that the points and lines are affine isotropic subspaces of  \(\K^2\) because they have no volume; the line is affine Lagrangian subspace of \(\K^2\) because it has the largest possible dimension without having any volume; and the entire plane is a coisotropic subspace because it is dual to the isotropic subspace given by the origin.

An isotropic / coisotropic / Lagrangian, linear / affine relation \(m\to n\)
is an isotropic / coisotropic / Lagrangian, linear / affine subspace of:

\[(\K^{2m} \oplus \K^{2n},  (\vec v, \vec w) \mapsto \omega_{m}(\vec v)-\omega_{n}(\vec w))\]

We must introduce this twisted symplectic form, as opposed to \(\omega_{n+m}\), so that these notions of “relations” are really stable under relational composition as described in definition <ref>:

The \(\dagger\)-compact props of isotropic / coisotropic / Lagrangian, linear / affine relations, \(\IR\), \(\CR\),  \(\LR\),  \(\AIR\), \(\ACR\), \(\ALR\) have:

* Arrows are given by isotropic / coisotropic / Lagrangian, linear / affine relations.

* Composition is given by relational composition.

* Identity on \(1\) is given by the diagonal on \(\K^{1}\).

* The monoidal structure is given by the direct sum and \(0\).

* The symmetry on \(1\) is given by:

\begin{equation*}
\left\{\left( \begin{bmatrix} \vec v \\ \vec w \end{bmatrix}, \begin{bmatrix} \vec w \\ \vec v \end{bmatrix} \right) \,\middle|\,  \vec v, \vec w \in \K^2 \right\}:2\to 2
\end{equation*}

* The compact structure on \(1\) is given by

* The dagger of an arrow \(R:n\to m\) is given by:

\begin{equation*}
R^\dag \coloneqq
\left\{
\left(\bigoplus_{j=0}^{m-1} \begin{bmatrix} z_j \\ -x_j \end{bmatrix}, \bigoplus_{k=0}^{n-1} \begin{bmatrix} z_k' \\ -x_k' \end{bmatrix} \right)
\,\middle|\,
\left(\bigoplus_{k=0}^{n-1}\begin{bmatrix} z_k' \\ x_k'\end{bmatrix}, \bigoplus_{j=0}^{m-1} \begin{bmatrix} z_j \\ x_j \end{bmatrix}  \right)\in R
\right\} :m\to n
\end{equation*}

Our definition differs slightly from the way it is often stated in the literature, for example in the work of weinstein_symplectic_2009 and network.  This is because we have decided to work in the skeletal case, where all isomorphic objects are equal. However, both definitions are equivalent, so this difference is inconsequential.

We must be careful as the relationship between the props \(\lR\) / \(\AR\) and their symplectic counterparts is subtle. First, for example, the symmetric monoidal functor \(\interp{-}_{\abbralagr}^{\abbrar}:\ALR \to \AR \) which forgets the symplectic structure is not a prop morphism, as it sends \(n\mapsto 2n\). Furthermore the compact structure of \(\ALR\) is different from the compact structure we defined on \(\AR\) because the latter is not Lagrangian.

Remark that any (affine) symplectic map \(R: (\K^{2n},\omega_n) \to (\K^{2m},\omega_m)\) induces an (affine) Lagrangian relation via its graph

\[ \Gamma_R\coloneqq \{(\vec v, R \vec v) \ | \ \forall \vec  v \in \K^{2n} \}:n\to m\]

which is functorial, so these categories of symplectic relations strictly generalize (affine) symplectic maps.

It is helpful to get a geometric intuition for composition in these symplectic categories of relations:

Consider the affine Lagrangian relation \(R:0\to 1\) relating the point to the line \(x=bz+a\); and consider another affine Lagrangian relation \(S:1\to 0\) relating the line \(x=b'z+a'\) to the point.

* If \(b=b'\), so that both lines are parallel, but \(a\neq a'\) so that they never meet, then \(S\circ R\) is the empty set.

* On the other hand if \(b=b'\) and \(a=a'\), so that these are both the same lines then  \(S\circ R\)  is the identity.

* Even if these two lines intersect only once, then \(S\circ R\) is still the identity!

§.§ Generators and equations for affine Lagrangian relations

In order to give a graphical axiomatisation of \(\ALR\), we extend the phase group of \(\GAA\) (recalling definition <ref>):

Let  \(\ZX\) be the †-compact prop given by extending the phase groups of \(\GAA\); the grey spiders phase group extended along the group homorphism \(\K^0\hookrightarrow \K^2\) and the white spider along the group homorphism \(\K^1\hookrightarrow \K^2\):

\begin{equation}
\label{eq:symplecticspiders}
\tikzfig{figures/AffLagRel/lhsgrey} \longmapsto \tikzfig{figures/AffLagRel/rhsgrey}\quad\quad
\tikzfig{figures/AffLagRel/lhswhite} \longmapsto \tikzfig{figures/AffLagRel/rhswhite}
\end{equation}

Modulo the following equations for all \(a,b,c \in\K\) and \(d\in\K^*\):

\begin{equation}
\label{eq:ALR_axioms}
\tikzfig{figures/AffLagRel/axioms}
\end{equation}

Where there are derived generators, for all \(a \in\K \):

\begin{equation}
\label{eq:box-def}
\tikzfig{figures/AffLagRel/box-def}
\end{equation}

The †-structure is given by:

\begin{equation*}
\tikzfig{figures/AffLagRel/b-spider} \mapsto \tikzfig{figures/AffLagRel/b-spider-daggered}  \quad
\tikzfig{figures/AffLagRel/w-spider} \mapsto \tikzfig{figures/AffLagRel/w-spider-daggered}  \quad
\tikzfig{figures/AffLagRel/scalar} \mapsto \tikzfig{figures/AffLagRel/scalar_daggered} \quad
\tikzfig{figures/AffLagRel/box_undaggered} \mapsto \tikzfig{figures/AffLagRel/box_daggered}
\end{equation*}

Call the first component of the phase groups for the grey and white  spiders in equation (<ref>) the  affine phase, and the second component the
symplectic phase.

The derived generators in <ref> are called boxes.  The disinguished boxes with labels \(1\) and \(-1\) are respectively the symplectic Fourier transform and inverse symplectic Fourier transform.

Recalling the geometric intuition from example <ref>, lifting scalar multiplication along the embedding \(\GAA\hookrightarrow\ZX\) corresponds to squeezing.  Similarly, the affine phase for the white spider corresponds to shifting the \(X\)-gradient.  On the other hand, the affine phase for the grey spider corresponds to shifting the \(Z\)-gradient.  The symplectic phases for the white and grey spiders corresponding to shearing in the \(X\) and \(Z\) direction.  The symplectic Fourier transform corresponds to a \(\pi/2\)-rotation in the affine plane.

Following equation <ref>, we can actually define multipliers
from boxes: figures/AffLagRel/multiplier_from_box. From now on,
we will take the boxes as primary, rather than multiplication by scalars.
This is because:

The presentation  \(\ZX\)  of \(\ALR\) with generators

\begin{equation*}
\tikzfig{figures/AffLagRel/b-spider} : m \to n  \quad\quad\quad
\tikzfig{figures/AffLagRel/w-spider} : m \to n  \quad\quad\quad
\tikzfig{figures/AffLagRel/box} : 1 \to 1
\end{equation*}

is flexsymmetric.

See appendix <ref> for an explicit presentation of \(\ZX\).

Note that the symplectic setting is quite special: as discussed in remark <ref> \(\AR\) and \(\lR\) do not obviously admit flexsymmetric presentations.

There is an interpretation \(\interp{-}_\abbralagr^\zx: \ZX \to \ALR\) given by:

\begin{align*}
\coloneqq \left\{ \left(
\bigoplus_{j=0}^{m-1} \begin{bmatrix}
z_j \\ x
\end{bmatrix} ,
\bigoplus_{k=0}^{n-1} \begin{bmatrix}
z_k' \\ x
\end{bmatrix}
\right) \,\middle|\, \begin{aligned} &\vec z\in\K^m, \vec{z'} ; \in \K^n, x \in \K \qq{such that} \\ &\sum_{j=0}^{m-1} z_j - \sum_{k=0}^{n-1} z_k' + bx = a \end{aligned} \right\} \\
\coloneqq
\left\{ \left(
\bigoplus_{j=0}^{m-1}
\begin{bmatrix}
z \\ x_j
\end{bmatrix} ,
\bigoplus_{k=0}^{n-1}
\begin{bmatrix}
-z \\ x_k'
\end{bmatrix}
\right) \,\middle|\, \begin{aligned} & \vec x \in \K^m, \vec{x'}\in \K^n, z\in \K \qq{such that} \\ &\sum_{j=0}^{m-1} x_j + \sum_{k=0}^{n-1} x_k' - bz = a \end{aligned} \right\}
\end{align*}

\begin{align*}
\interp{\tikzfig{figures/AffLagRel/box_zero}}_\abbralagr^\zx
\coloneqq \left\{ \left(
\begin{bmatrix} 0 \\ x \end{bmatrix}, \begin{bmatrix} 0 \\ x' \end{bmatrix}
\right) \,\middle|\, x,x' \in \K \right\} & &
\interp{\tikzfig{figures/AffLagRel/box_invertible}}_\abbralagr^\zx
\coloneqq \left\{ \left(
\vec{v},
\begin{bmatrix}
\end{bmatrix},
\begin{bmatrix}
\end{bmatrix} \vec{v}
\right) \,\middle|\, z,x\in\K \right\}
\end{align*}

where \(m,n \in \N\), \(a,b \in \K\) and \(c \in \K^*\).

Translating this to string diagrams, following comfort_graphical_2021, we have a factorization of \(\interp{-}_\abbralagr^\zx: \ZX \to \ALR\) through $\GAA$ :

There is an interpretation
\(\interp{-}_\gaa^\zx : \ZX \to \GAA\), defined on objects
by \(\interp{m}_\mathsf{GAA}^\zx= 2m\) and on morphisms by:

\[
\interp{\tikzfig{figures/AffLagRel/b-spider-ind}}_\gaa^\zx
\hspace*{-.25cm}=
\tikzfig{figures/AffLagRel/GAA_b-spider}
\quad
\interp{\tikzfig{figures/AffLagRel/w-spider-ind}}_\gaa^\zx
\hspace*{-.25cm}=
\tikzfig{figures/AffLagRel/GAA_w-spider}
\]

\[
\interp{\tikzfig{figures/AffLagRel/box_invertible_whydidyouusethesamediagramwithalocalvariableinsideofit}}_\gaa^\zx =\tikzfig{figures/AffLagRel/GAA_box_invertible}
\]

The interpretations \(\interp{-}_\abbralagr^\zx
: \ZX \to \ALR\) and \(\interp{-}_{\gaa}^\zx : \ZX \to
\GAA\)  are †-symmetric monoidal functors, making the following diagram of †-compact closed categories commute:

\[
\xymatrix{%
\ZX \ar[rr]^{\interp{-}_{\gaa}^\zx} \ar[d]_{\interp{-}_\abbralagr^\zx}
&& \GAA \ar[d]^{\interp{-}_{\abbrar}^{\gaa}}\\
\ALR \ar[rr]_{\interp{-}_{\abbrar}^{\abbralagr}}
&& \AR
\]

Where the vertical arrows are morphisms of †-compact props.

§.§ Scalable notation for graphical symplectic algebra

In this subsection we extend the scalable notation for affine relations introduced in
section <ref> to the setting of affine Lagrangian relations.
First, note that the the matrix arrows in  \(\GAA\) lift along the embedding
\(\GAA\hookrightarrow\ZX\) given in definition <ref>.  However, now the  \([n]\)-coloured grey and white spiders both have phase groups \(\K^n \times
\Sym[n]\) (recalling definition <ref>), where  \(\Sym\) denotes the Abelian group of symmetric \(n \times n\) matrices over \(\K\) under addition.

Define scalable grey and white spiders in \(\ZX\) by induction on the colour of wires \(k\in\N\).
The base case is trivial.  For the inductive step, take, \(n,m\in \N\), \(a,b\in \K\), \(\vec v, \vec w \in \K^k\) and \(A\in\Sym[k]\), we define  \([k+1]\)-coloured spiders as:

\begin{equation}
\label{eq:thick_spider_def}
\tikzfig{figures/AffLagRel/scalable/b-spider-def}
\quad\quad\quad\quad
\tikzfig{figures/AffLagRel/scalable/w-spider-def}
\end{equation}

where the scaled box is also inductively defined.  The base case is trivial, and the inductive step is given by:

\begin{equation}
\label{eq:scalable_box}
\tikzfig{figures/AffLagRel/scalable/box-def}
\end{equation}

A \(k\)-coloured grey spider with \(n\) inputs and \(m\) outputs parametrizes an undirected open graph with edges coloured by \(\K\), vertices coloured by \(\K^2\), with \(n\) distinguished inputs and \(m\) distinguished outputs.

On the left hand side we have a graph state with \(n = 0\), \(m=1\) and \(k=3\).  On the right hand side, we have a spider with  \(m = 3\),  \(n = 2\) and \(k =

\begin{equation}
\tikzfig{figures/AffLagRel/scalable/b-spider-explicit-simple}
\quad\quad\quad
\tikzfig{figures/AffLagRel/scalable/b-spider-explicit}
\end{equation}

The axioms of \(\ZX\) admit very natural scalable generalizations which we have included in appendix <ref>.  This notation is very powerful, and makes the proof of completeness much more understandable and elegant.

§.§ Completeness and normal form

In this subsection, we show that the interpretation  \(\interp{-}^\zx_\abbralagr:\ZX \cong \ALR\)  is an isomorphism of †-compact props.  We have already proven that it is a †-compact functor in proposition <ref>.  Fullness follows immediately from the result of Comfort and Kissinger  <cit.>.
Therefore it remains to show that it is faithful.  To prove this, we establish a normal form.

If a diagram  has empty semantics, then a simple induction argument yields the following unique normal form:

For any \(m,n \in \N\) and \(D \in \ZX(m,n)\) and \(a \in \K^*\):

\begin{equation*}
\tikzfig{figures/AffLagRel/zero_normal_forms}
\end{equation*}

The normal form for diagrams with nonempty semantics takes more work.
To this end, we further expose the graph theoretical properties of \(\ZX\).
Consider a subclass of diagrams, which is inspired by that of duncan_graph-theoretic_2020 in the context of the qubit ZX-calculus:

A \(\ZX\)-diagram is graph-like when:

* All spiders are grey spiders.

* Grey spiders are only connected via edges containing a box.

* There are no self-loops.

* Every input or output is connected to a grey spider.

* Every grey spider is connected to at most one input or output.

Graph like diagrams induce undirected graph with edges coloured by \(\K\),  vertices coloured by \(\K^2\), with distinguished vertices corresponding to spiders which are connected to specific inputs and outputs.  Given a graph-like diagram:

* To each \((a,b)\)-phased grey spider, associate an \((a,b)\)-labelled vertex.

* To each wire between two spiders mediated by an \(a\)-labelled box, associate an \(a\)-labelled edge between the corresponding internal vertices.

* To each spider connected connected to an input/output, distinguish the corresponding edge as being associated to the specific input/output.  Call such a vertex a boundary vertex.  Call vertices not associated to inputs/outpus internal.

The following \(\ZX\)-diagram is graph-like:

\begin{equation}
\label{eq:graph-like-example}
\tikzfig{figures/AffLagRel/graph-like-example}\ \ \
\begin{tikzpicture}\draw [->, decorate, decoration=snake] (0,0) to (3.5,0);\end{tikzpicture}
\tikzfig{figures/AffLagRel/graph-like-example-graph}
\end{equation}

where the top three vertices are boundary vertices, and the bottom one is

Every \(\ZX\)-diagram can be rewritten to graph-like form.

Because \(\ZX\) is compact closed, we can bend the input wires of diagrams into output
wires. As long as we remember which outputs originally came from bending
inputs, we only need to work with states \(0
\to n\). Graph-like states take the following simple form in the scalable notation, for some \(m,n \in \N\), \(\vec x \in \K^{m+n}\) and \(X \in \Sym[m+n][\K]\):

\begin{equation}
\label{eq:scalable_graph-like}
\tikzfig{figures/AffLagRel/scalable/graph-like}
\end{equation}

This graph-like state has \(m\) internal vertices, and \(n\) outputs. As
before, \(X\)  encodes the adjacency matrix of the underlying
weighted graph with \(m+n\) vertices (compare with example <ref> and equations (<ref>) and (<ref>)).  It is
possible to simplify graph-like diagrams by reducing the number of internal
vertices using the following result.

For any invertible \(X \in \Sym[m][\K]\), \(Y \in
\Sym[n][\K]\), \(E \in \Matrices[m][n]\), \(\vec x \in \K^m\), and \(\vec y \in \K^n\):

\begin{equation*}
\tikzfig{figures/AffLagRel/scalable/symplectic_elimination}
\end{equation*}

This proposition encompasses both local complementation and pivoting
of graphs in bouchet_circle_1994, generalised to coloured graphs by kante_rank-width_2013.  This has been used in the context of the stabiliser fragment of the ZX-calculus, for example by
backens_zx-calculus_2014, duncan_graph-theoretic_2020, booth_complete_2022, poor_qupit_2023:

For any \(z \in \K^*\), \(a \in \K\), \(\vec{z}
\in \K^k\), \(E \in \Matrices[k][1]\), \(Z \in \Sym[k]\) where

\begin{equation*}
\tikzfig{figures/AffLagRel/local_complementation}
\end{equation*}

Where\(\gamma_i \coloneqq z_i + E_i a z^{\minu 1},\quad \delta_i \coloneqq Z_{i,i} - z^{\minu 1} E_i^2,\quad{\it and}\quad g_{i,j} \coloneqq Z_{i, j} - z^{\minu 1} E_i E_j.\)

The new edge weights \(g_{i,j}\) in the right-hand side are obtained from
the edge weights \(E_{i_j}\) of the left-hand side by performing a local
complementation (in the sense of kante_rank-width_2013) around the
vertex \(1\), which is then deleted.

For any \(\epsilon \in \K^*\), \(a,b \in \K\), \(\vec{z}
\in \K^k\), \(E \in \Matrices[n][2]\), \(Z \in \Sym[k]\) where

\begin{equation*}
\tikzfig{figures/AffLagRel/pivot}
\end{equation*}

\[\gamma_i \coloneqq z_i + \epsilon^{\minu 1} (a E_{2,i} + b E_{1,i}),\  \delta_i \coloneqq Z_{i,i} - 2 \epsilon^{\minu 1} E_{1,i} E_{2,i},\  {\it and}\  g_{i,j} \coloneqq - \epsilon^{\minu 1} (E_{1,i} E_{2,j} + E_{1,j} E_{2,i}).\]

The new edge weights \(g_{i,j}\) in the right-hand side are obtained from
the edge weights \(E_{i_j}\) of the left-hand side by performing a pivot
(in the sense of kante_rank-width_2013) around the edge weighted
by \(\epsilon\). The two vertices connected by this edge are then deleted.

Using proposition <ref>, it is clear that we can
eliminate any internal spider with phase \((x,z)\) where \(z \neq 0\). Having
done this, we then use proposition <ref> to eliminate any
remaining internal spiders that are connected. Therefore, we can refine
the notion of graph-like diagram:

A graph-like diagram is in Affine with Phases form
(AP-form) when:

* There are no inputs;

* The internal spiders have phases of the form \((x,0)\) for \(x \in \K\);

* Internal spiders are only connected to boundary spiders.

Every graph-like diagram \(0 \to n\) can be put into AP-form.

In the scalable notation, the AP-form  can be seen to be the following refinement of the graph-like form which was presented in equation (<ref>):

\begin{equation}
\label{eq:scalable-AP-form}
\tikzfig{figures/AffLagRel/scalable/AP-form}
\end{equation}

for \(m,n \in \N\), \(\vec{x} \in \K^m\), \(\vec{y} \in \K^n\),
\(E \in\Matrices[m][n][\K]\), and \(Y \in \Sym\). Here
there are \(m\) internal spiders with phases \((x_k,0)\), connected to \(n\)
boundary spiders via the matrix \(E\).

The AP-form also appeared in the completeness result of odd-prime-dimensional stabiliser ZX-calculus of  poor_qupit_2023. Our scalable presentation of the AP-formal form can be easily rewritten to more closely resemble their presentation:

\begin{equation}
\label{eq:scalable-AP-form-derivation}
\tikzfig{figures/AffLagRel/scalable/AP-form-derivation}
\end{equation}

The history of this form is rather complicated, and we will discuss the attribution and history at the end of this section.

The AP-form, can be row-reduced, which leads to the following refinement:

A diagram in AP-form defined by \((E,Y,\vec{x}, \vec{y})\) is in
reduced AP-form if its semantics are empty, or it satisfies the following:

* \(E\) is in reduced row echelon form;

* \(E\) is surjective (none of the rows of  \(E\) are zero);

* \(\im (E^\trans) \subseteq \ker (Y) \) (if the \(j^\text{th}\)  column of \(E\) is a pivot, then the \(j^\text{th}\)  column of \(Y\) is \(0_n\));

* \(\im (E^\trans) \subseteq \ker (\vec{y}^\trans)\) (if the \(j^\text{th}\)  column of \(E\) is a pivot, then the \(j^\text{th}\)  entry of \(\vec y\) is \(0\)).

In the scalable notation, the reduced AP-form can be stated graphically, for some \(m \leqslant n \in \N\), \(\vec{x} \in \K^m\), \(\vec{s} \in
\K^{n-m}\), \(F \in \Matrices[m][n-m]\) and \(S \in \Sym[n-m]\), up to a permutation matrix \(\varsigma\in \Matrices[n][n]\):

\begin{equation}
\label{eq:scalable-reduced-AP-form}
\tikzfig{figures/AffLagRel/scalable/reduced-AP-form}
\end{equation}

Note that the permutation \(\varsigma\) allows for the pivots \(1_m\) to be separated into a different block than \(F\), so that \(E=\begin{bmatrix} 1_m & F \end{bmatrix}\varsigma\), and similarly for \(\vec s\) and \(0_m\), so that \(y=\varsigma^\trans \begin{bmatrix} 0_m^\trans & \vec s^\trans \end{bmatrix}^\trans \). Therefore, pulling the permutation out to the right makes  the normal form easier to state diagrammatically.

Every \(\ZX\)-diagram can be put into reduced AP-form.

The reduced AP-form is unique:

For any nonempty affine Lagrangian state there is exactly one equivalent diagram in reduced-AP form.

Recall that \(\interp{-}^\zx_\abbralagr:\ZX \to \ALR\) is full.  Moreover, it faithful on diagrams with empty semantics by proposition <ref>.  Because, in addition,  every nonempty \(\ZX\) diagram can be rewritten to the reduced-AP form by proposition <ref>, which is unique by proposition <ref>, we have that:

The  interpretation \(\interp{-}^\zx_\abbralagr:\ZX \cong \ALR\) is a †-compact prop isomorphism.

This also gives a complete representation for Lagrangian relations as an immediate corollary:

There is an isomorphism of †-compact props \(\interp{-}^{\zx^0}_\abbralagr:\ZX^0 \cong \LR\), where \(\ZX^0\) obtained by restricting the affine phases of the white and grey spiders in \(\ZX\) to be 0 and dropping the axioms involving nonzero affine phase.

See appendix <ref> for an explicit presentation of \(\ZX^0\).

A note on the attribution of the (reduced) AP-form What we have called the “reduced AP-form” has a complicated history, originating from within the field of quantum information theory, which we review here in order to give correct attribution. A closely related form, called the “standard form” for qubit stabiliser codes seems to first appear in the work of Cleve1997.  When the stabiliser code is taken to have maximal dimension, the standard form for the stabiliser tableau is essentially the reduced AP-form for a linear Lagrangian subspace over the field \(\mathbb{F}_2\). The connection of this form for qubit stabiliser states to graphs was developed by Elliott2008; they decorate the graphs to recover the “phase-information” which is lost in the representation of a stabiliser state via its standard form.  hu_improved_2022 refined the results of Elliott2008, providing a unique graph-like representation of qubit stabiliser states which also accounted for phase information, in terms of its affine support and a phase-polynomial.  Note that the work of Elliott2008 was itself is directly inspired by that of van_den_nest_graphical_2004, where they showed that, modulo scalars, qubit stabiliser states can be represented, non-uniquely by “quantum graph states” up to the action of the local Clifford operators.

In the ZX-calculus community, backens_zx-calculus_2014 used Van den Nest et al.'s pseudonormal form of quantum graph states in order to give the first complete presentation of the qubit stabiliser ZX-calculus.
Later on, McElvaney and Backens reformulated  the unique normal form of  hu_improved_2022 in the context of the qubit ZX-calculus <cit.>. Because of the connection which they draw to phase-polynomials, they named this incarnation of the “canonical form” with phase information the  “phase-polynomial form” for a qubit stabiliser ZX-diagram, analagous to our AP-from. They further refine this form into the unique  “canonical phase-polynomial form” for qubit stabiliser ZX-diagrams.  This canonical phase-polynomial form is analagous to our reduced AP-form.

To make the connection between the “canonical phase-polynomial form” of  mcelvanney_complete_2022 and the AP-form as described in our paper, we must take a detour through odd-prime-dimensional quantum circuits. In the setting of odd-prime-dimensional quantum systems, Bahramgiri and Beigi <cit.> had already noted that local complementation of \(\mathbb{F}_p\)-coloured graphs, as defined in the work of kante_rank-width_2013, provides a suitable generalisation of the results of van_den_nest_graphical_2004.  booth_complete_2022 used this to prove completeness of a ZX-calculus for odd-prime-dimensional stabiliser quantum systems, using a proof method strongly inspired by <cit.>. On the other hand, inspired by the phase-polynomial form and the unique canonical  phase-polynomial form for qubit stabiliser states of mcelvanney_complete_2022, poor_qupit_2023 adapted these forms to  the odd-prime-dimensional qudit stabiliser fragment of the ZX-calculus.  They dubbed the qudit analogue of the canonical phase-polynomial form the “affine with phases form” (AP-form), and the analogue of the canonical phase-polynomial form the “reduced affine with phases form” (reduced AP-form). By contrast to the quantum graph-state approach, the uniqueness of the reduced AP-form provided a cleaner completeness proof for the odd-prime-dimensional qudit stabiliser ZX-calculus.
Since comfort_graphical_2021 proved that \(\ALR[\Zp]\)  is a projective representation for the odd-prime-dimensional qudit stabiliser ZX-calculus the year before (see section <ref>), our generalization of this normal form to \(\ALR\) was a natural next-step. Although, annoyingly. instead of representing qubit stabiliser circuits, \(\ALR[\mathbb{F}_2]\) is isomorphic to the prop of  “pure circuits in Spekken's toy model” which was axiomatized separately by spekzx; hence the difficulty in giving correct attribution.

In fact, cockett_categories_2022 had already remarked that any linear Lagrangian relation can be expressed in a manner analogous to the canonical form for a stabiliser state.  However,  their statement is purely semantic, and does not concern the completeness of a graphical language.

§ GRAPHICAL LINEAR AND AFFINE COISOTROPIC ALGEBRA

In this section, we extend the presentation \(\ZX\) of \(\ALR\) to one for  \(\ACR\).  We also obtain a presentation of \(\CR\cong\IR\) as an immediate corollary.

First, recall from subsection <ref> that we can not only take the images of matrices, but we can also take images of affine (resp. linear) relations.  Because affine (resp. linear) Lagrangian relations are structure preserving affine (resp. linear) relations, we can also ask for their images:

Given an affine Lagrangian relation \(L:k\to n\), the image of \(L\) is the image of the underlying affine relation \(2k\to 2n\):

\[\tikzfig{figures/AffCoisoRel/image}\]

And likewise, for the image of linear Lagrangian relations.

Recall the following result of Comfort <cit.>:

The set of nonempty affine (resp. linear) coisotropic subspaces of a symplectic vector space \((\K^{2n},\omega_n)\) of dimension \(n+k\) are in bijection with the set of the  images of isometries of type \(k\to n\) in \(\ALR\) (resp. \(\LR\)).

Therefore, we only need to add a single generator of type \(0\to 1\) to  \(\ZX\)  (resp. \(\ZX^0\)) to get a presentation for \(\ACR\) (resp. \(\CR\)).
Geometrically, this corresponds to the linear relation which relates the point to affine plane.  In fact, it will be slightly more convenient, but equivalent, to instead add its converse: the relation which discards the entire plane.

We  now must find which additional equations this generator satisfies.  To this end, we investigate more of the the structure of \(\ALR\) and \(\LR\).
First, we observe that there is an alternative presentation of affine/linear coisotropic subspaces due to [Theorem 4.5]comfort_algebra_2023:

Given  \(L:k\to n\) and \(K:m\to n\) in \(\ALR\) (or in \(\LR\)), then:

\[ \im(L)= \im(K) \iff L L^\dag     = K K^\dag  \]

Second, observe that linear and affine Lagrangian relations have the following bipartite decomposition:

Any affine (resp. linear) Lagrangian relation \(L:n\to m\) can be decomposed in the form:

\[\tikzfig{figures/AffCoisoRel/stdform}\]

where \(S:n\to n \) and \(T: m \to m\) are affine (resp. linear) symplectomorphisms.

Note that affine symplectomorphisms are precisely the isomorphisms which are precisely the unitaries in \(\ALR\), and similarly, for the linear symplectomorphisms in \(\LR\).
It seems that this decomposition is well-known, where it is related to “coisotropic reduction” as in [section 3.1]weinstein_symplectic_2009.
However, we arrived at this decomposition from a slightly different angle than it usually stated in the literature.
For this reason, it is evident that this decomposition is an instance of the “generalized compact singular value decomposition” in the context of dagger categories of [definition 3.5]MPI.  So in some sense, this a symplectic version of the singular value decomposition of complex matrices.  Because of this similarity to the singular value decomposition, we have a symplectic version of the “essential uniqueness of purification” of mixed quantum circuits:

Given (affine) Lagrangian relations \(L:n \to a\) and \(K:n \to b\) such that  \(L^\dagger  L = K^\dagger  K\), and \(b\leq a\) then there exist an (affine) symplectomorphism \(H: b+ (a-b)\to a\), such that:

\[\tikzfig{figures/AffCoisoRel/enoughiso}\]

Combining lemmas <ref> and <ref>, given two (affine) Lagrangian relations \(L\) and \(K\) with \(\im(L^\dag)=\im(K^\dag)\), then it follows that \(L\) and \(K\) differ only up to postcomposition by an isometry!
Recall the following definition from Carette et al. which quotients precisely by this congurence <cit.>:

Given a †-compact prop, \(\mathsf C\), the discard construction of \(\mathsf{C}^\disc\) is presented by freely adding a generator \(\tikzfig{figures/AffCoisoRel/discard}: 1\to 0\) to \(\mathsf C\) modulo the equations such that for all isometries  \(H:n\to m\) in \(\mathsf C\):

\[\tikzfig{figures/AffCoisoRel/discardconstruction}\]

In other words, in the language of  [definition 10]discard, it follows immediately from lemma <ref> that \(\ALR\) and \(\LR\) both have “enough isometries,” and thus:

\(\ZX^\disc\cong \ACR\) and \((\ZX^0)^\disc\cong\CR\).

Luckily, the generators for (affine) symplectomorphisms, and by immediate consequence, the  isometries are well-known; thus:

\(\ZX^\disc\cong\ACR\) is presented by the adding the generator \(\tikzfig{figures/AffCoisoRel/discard}: 1\to 0\)  to \(\ZX\) in addition to the equations discarding the generating isometries for all \(a,b\in\K\):

\[\tikzfig{figures/AffCoisoRel/eqdisc}\]

Where \((\ZX^0)^\disc\cong\CR\) is presented by adding the same generator to  \(\ZX^0\)  and restricting the grey and white phase groups to \(\K\) along the embeddings \(b \mapsto (0,b)\).

§ APPLICATIONS

In mechanics, the state of a system is often given by the configurations of positions, and the evolution of the system is described by how the positions change over time.  However, it is often useful to take a different perspective where states are determined by their abstract positions and momenta, ie. where they are elements of the phase space.  From this perspective, the evolution of the system is described by how the positions and momenta change over time; in other words, the evolution is determined by the Hamiltonian flow of particles through the system.

§.§ Classical mechanics

In classical mechanics, the only valid reversible transformations are those which preserve the oriented local volume between position and momentum: ie the (affine) symplectormorphisms.
In other words, symplectic geometry is the geometry of the phase space picture of classical mechanics.
Recall from theorem <ref> that a symplectic vector space can be decomposed into two parts: a \(Z\) and \(X\) grading. The elements of these gradings are interpreted respectively as abstract  configurations of positions and momenta. There are different notions of positions and momenta  in different classical mechanical settings (adapted from [page 23, table 2.1]bondgraph and thetable):

mechanics			         Z            \({d Z}/{d t}\)       \(X\)                                      \({d X}/{d t}\)

Translation                         position     velocity             momentum                          force

Electronic                          charge       current              flux linkage                          voltage

Hydraulic                           volume      flow                    pressure momentum          pressure

Thermal                             entropy     entropy flow      temperature momentum     temperature

The connection between affine Lagrangian relations and electrical circuits is well documented, therefore we focus on this example. Baez et al. use  linear Lagrangian relations to give a semantics for passive linear circuits: an idealized class of electrical circuits with linear behaviour  <cit.>.  We will review this work from a string diagrammatic perspective.
To this end, recall the physical laws respectively due to Ohm <cit.> and  Kirchhoff <cit.>:

Ohm's law:  The voltage around the node in a circuit is equal to the current multiplied by the resistance.

Kirchhoff's current law: The sum of currents flowing into a node is equal to the sum of currents flowing out of the node.

Given a resistor with resistance \(r\in \R^{+}\), by Kirchhoff's current  law the incoming current is equal to the outgoing current; and by By Ohm's law, the outgoing potential is equal to the current multiplied by \(r\) plus the incoming potential.  Therefore we can interpret electrical circuits composed of resistors in \(\zx_\R\):

\[
\interp{
\input{figures/Applications/electrical/resistor_symbol}
\tikzfig{figures/Applications/electrical/resistor_interpretation}
\]

White spider fusion entails that composing resistors in sequence adds resistance:

\begin{equation}
\tikzfig{figures/Applications/electrical/serie}
\end{equation}

Consider an ideal junction of \(n\) incoming wires connected to \(m\) outgoing wires with no resitance.  By Kirchhoff's current law, the sum of the currents of the incoming wires is equal to the sum of the currents of the outgoing wires.  Moreover, by Ohm's law, because resistance is zero, the   incoming and outgoing potentials are all made to be equal.  Therefore an ideal junction of \(n\) incoming wires and \(m\) outgoing wires is interpreted as the following Lagrangian relation:

\[
\interp{
\tikzfig{figures/Applications/electrical/junction_symbol}
\tikzfig{figures/Applications/electrical/junction_interpretation}
\]

A circuit of resistors with resistances \(r_0\) and \(r_1\) composed in parallel can therefore be simplified using pivoting:

\begin{align}
\tikzfig{figures/Applications/electrical/resistors_in_parallel/0}
\tikzfig{figures/Applications/electrical/resistors_in_parallel/0-1}
\stackeqmid{\minilemref{lem:antipode_spider}}
\tikzfig{figures/Applications/electrical/resistors_in_parallel/1}
\stackeqmid{\Bigebra}
\tikzfig{figures/Applications/electrical/resistors_in_parallel/2}\\
\stackeq{\minilemref{lem:symplectic_states}}
\tikzfig{figures/Applications/electrical/resistors_in_parallel/3}
\stackeqmid{\Fusion}
\tikzfig{figures/Applications/electrical/resistors_in_parallel/4}
\stackeqmid{\minilemref{lem:symplectic_states}}
\tikzfig{figures/Applications/electrical/resistors_in_parallel/5}
\stackeqmid{\Fusion}
\tikzfig{figures/Applications/electrical/resistors_in_parallel/6}
\end{align}

This fragment of eletrical circuits composed of circuits of resistors with junctions of wires has recently been given a complete equational theory by  amolakresistors; their completeness result relies on the “star-mesh” transformations, which are linear versions of the pivoting rule which we discussed in proposition <ref>.
However, we are working in a larger semantic domain,  therefore more generators can be expressed using our string diagrams.
For example, by working in affine Lagrangian relations, now we can nudge the position of momentum by a constant factor. Using results from  the subsequent work of Baez et al., voltage and current sources with voltage \(v \in \R^{+}\) and current \(\iota \in \R^{+}\) have the following interpretations <cit.>:

\[
\interp{
\input{figures/Applications/electrical/voltage_source_symbol}
\tikzfig{figures/Applications/electrical/voltage_source_interpretation}
\qquad\qquad
\interp{
\input{figures/Applications/electrical/current_source_symbol}
\tikzfig{figures/Applications/electrical/current_source_interpretation}
\]

We obtain an elegant proof that composing voltage sources in parallel with different voltages \(v_0\neq v_1\) leads to contradiction:

\begin{align}
\tikzfig{figures/Applications/electrical/voltage_sources_in_parallel/0}
\tikzfig{figures/Applications/electrical/voltage_sources_in_parallel/0-1}
\stackeqmid{\minilemref{lem:antipode_spider}}
\tikzfig{figures/Applications/electrical/voltage_sources_in_parallel/1}
\stackeqmid{\Bigebra}
\tikzfig{figures/Applications/electrical/voltage_sources_in_parallel/2}\\
\stackeq{\Copy}
\tikzfig{figures/Applications/electrical/voltage_sources_in_parallel/3}
\stackeqmid{\Fusion}
\tikzfig{figures/Applications/electrical/voltage_sources_in_parallel/4}
\stackeqmid{\minipropref{prop:zero_normal_forms}}
\tikzfig{figures/Applications/electrical/voltage_sources_in_parallel/6}
\end{align}

Our graphical simplifications of the parallel composition of resistors and voltage sources should be compared with the “doubled” proofs of Bonchi et al., where they represent the voltage and current gradings as separate wires  in \(\GAA[\R]\) <cit.>.

Baez et al. showed how discretized time-dependent electical circuits can be interepreted in affine Lagrangian relations over the real rational functions \(\R(s)\) <cit.>.  In this setting, the \(j^\text{th}\) element of the stream is encoded as the coefficient of the \(j^\text{th}\) power of the polynomial indeterminate \(s\).  Taking the derivative and integrating with respect to time are therefore represented by multiplication and division by the polynomial indeterminate \(s\).
Applying  Kirchhoff's current law and Ohm's law,  (linear) inductors with inductance  \(\ell \in \R^+\)  and  (linear) capacitors with capacitance \(c \in \R^+\)  can therefore be interpreted as follows:

\[
\interp{
\input{figures/Applications/electrical/inductor_symbol}
\tikzfig{figures/Applications/electrical/inductor_interpretation}
\qquad
\interp{
\input{figures/Applications/electrical/capacitor_symbol}
\tikzfig{figures/Applications/electrical/capacitor_interpretation}
\]

Unlike the previous approaches, the scalable notation for \(\ZX\) allows us to compactly represent electrical circuits.  Fore example, recall that an impedance matrix is an \(n\times n\) real matrix which describes the impedance between ports in an electrical network (see the textbook of [section 4.2]Pozar for reference).  An electrical network is said to be reciprocal, when the relation of impedance between nodes is symmetric: that is to say, when the  corresponding impedance matrix is an element of \(\Sym[n][\R]\).  In the scalable notation for \(\ZX[\R]\), an impedance matrix  is represented by a thickened, scalable version of the resistor, which is carries a symmetric matrix \(R\in \Sym[n][\R]\) as a phase, rather than a scalar \(r\in \R\):

\begin{equation}
\tikzfig{figures/Applications/electrical/impendance_interpretation}
\end{equation}

This raises the question if the constructions from Boisseau et al.'s  impedance calculus <cit.> such as “impedance boxes” can be represented succinctly in the scalable notation for \(\ZX\).

It is  important to reiterate that the electrical circuits semantics is only one example.  We could have just as easily chosen any row from the table as our semantics and.  For example, in fluid mechanics we would replace idealized wires with idealized pipes through which fluid flows, resistors with narrowing pipes and so on.  Or more conceptually, some linear/affine network through which tokens are flowing throughout.  For example, consider an idealized network of cars driving along roads, where the flow of cars is assumed to be linear/affine.  Introducing a bottlneck to the flow of traffic, such as reducing the number of lanes, would be analgous to a resistor.

§.§ Quantum mechanics

Classical mechanics can be quantized in two different, but connected ways.

§.§.§ Stabiliser quantum mechanics in odd-prime dimensions

Given an odd prime \(p\),  Comfort and Kissinger showed that the †-compact prop of affine Lagrangian relations over \(\Zp\) is isomorphic to the †-compact prop \(\Stab\) of odd-prime-dimensional pure qudit stabiliser circuits, modulo scalars <cit.>.  If one doesn't allow symplectic-phases, then \(\ZX[\mathbb{F}_2]\) restricts to a semantics for qubit “CSS-circuits.”
Here, the \(Z\) and \(X\) gradings correspond respectively to the Pauli \(Z\) and Pauli \(X\) observables, and the symplectic form captures the commutation of Pauli operators. Therefore, we can add another row to our table:

Quantum mechanics                         $Z$              ${d Z}/{d t}$                   $X$                                  ${d X}/{d t}$
Stabiliser circuits                                 Pauli $Z$     Pauli $Z$ flow             Pauli $X$                          Pauli $X$ flow

Denote the induced prop isomorphism by \(\interp{-}_{\zx_\Zp}^{\Stab}:\Stab\to\zx_\Zp\).
Following the convention of Gottesman <cit.>, the  controlled-\(\mathcal X\), Fourier,
phase, and Pauli \(\mathcal X\) gates correspond to the generators of the prop for the affine symplectic groupoid, or “general affine symplectic group”:

\begin{align}
\interp{\tikzfig{figures/Applications/stabiliser/cnot_circuit}}_{\zx_\Zp}^{\Stab} = \tikzfig{figures/Applications/stabiliser/cnot_ZX}
\qquad\qquad
&\interp{\tikzfig{figures/Applications/stabiliser/hadamard_circuit}}_{\zx_\Zp}^{\Stab} = \tikzfig{figures/Applications/stabiliser/hadamard_ZX}\\
\interp{\tikzfig{figures/Applications/stabiliser/phase_circuit}}_{\zx_\Zp}^{\Stab} = \tikzfig{figures/Applications/stabiliser/phase_ZX}
\qquad\qquad
&\interp{\tikzfig{figures/Applications/stabiliser/X_circuit}}_{\zx_\Zp}^{\Stab} = \tikzfig{figures/Applications/stabiliser/X_ZX}
\end{align}

Moreover, the ground state and effect have the following interpretations:

\begin{equation}
\interp{\tikzfig{figures/Applications/stabiliser/ketzero_circuit}}_{\zx_\Zp}^{\Stab} = \tikzfig{figures/Applications/stabiliser/ketzero_ZX}
\qquad\qquad
\interp{\tikzfig{figures/Applications/stabiliser/brazero_circuit}}_{\zx_\Zp}^{\Stab} = \tikzfig{figures/Applications/stabiliser/brazero_ZX}
\end{equation}

The dagger of \(\ZX[\Zp]\) corresponds to the Hermitian adjoint in \(\Stab\).
Therefore, we find that \(\ZX[\Zp]\) is essentially the same presentation given by Poór et al. for odd-prime-dimensional pure qudit stabiliser circuits, where we instead quotient by scalars <cit.>.  Note that our white spiders correspond to the red spiders of Poór et al. and our grey spiders correspond to their green spiders.

However, the symplectic perspective on stabiliser circuits which we take here gives a unique notational advantage over the traditional Hilbert spaces semantics which is used by poor_qupit_2023 .
the adjacency matrix \(G\) of an \(\Zp\)-edge-weighted
graph on \(n\) vertices, the associated quantum graph state
<cit.> is
\(\interp{\tikzfig{figures/Applications/stabiliser/graph_state}}\!{\substack{\Stab\\ \zx_\Zp}}\)
(up to a normalisation scalar). Therefore, it is very natural to work with graph states in \(\ZX\).  In our presentation one can simultanously exploit  the geometric nature of string diagrams as well as the algebraic representation of  adjacency matrices: here both the string diagrams are graphs, and graphs are string diagrams! Such a natural and integrated string diagrammatic representation of graph states is very important because of their widespread usage in the quantum computing literature <cit.>.

Comfort showed for odd prime \(p\),  the prop of affine coisotropic relations over  \(\Zp\) is isomorphic to odd-prime-dimensional qudit mixed stabiliser circuits modulo scalars, \(\stab_p^\disc\) <cit.>.  Here, the discard relation which we added to \(\ZX\) to obtain \(\ZXdisc\) corresponds to the quantum discarding map:

\begin{equation}
\interp{\tikzfig{figures/Applications/stabiliser/discard}}_{\zx_\Zp^\disc}^{\stab_p^\disc} = \tikzfig{figures/Applications/stabiliser/discard}
\end{equation}

The states in mixed stabiliser circuits correspond to stabiliser codes.  Stabiliser codes are used extensively in quantum error correction, as witnessed by the success of Gottesman's PhD thesis on the subject <cit.>.  Stabiliser codes are essentially stabiliser states which have been perturbed by measurement, which gives them extra redundancy to protect information against errors.

Combining our work with that of comfort_algebra_2023,  one obtains a presentation of the 2-coloured prop of stabiliser circuits with both quantum and classical types mediated by preparation and measurement maps. In fact, this has nothing to do with prime fields, and can be constructed by the coproduct of \(\ZX\) and \(\GAA\) along an isometry witnessing the embedding of †-compact props \(\GAA\hookrightarrow\ZX\) exhibited in definition <ref>.  In the stabiliser circuit semantics, this isometry corresponds to the “state preparation map,” and its adjoint to the “measurement map.” But more generally, this provides a syntax for mechanical systems with affine control.

§.§.§ Picturing quantum optics

The \(\LOv\)-calculus is a complete diagrammatic language for reasoning about
passive linear quantum optics <cit.>. It is
a prop defined on the following set of generators, for all \(\theta, \varphi\in\R\):

* phase shifter,  wave plate, beamsplitter, and polarising beamsplitter:

\begin{equation*}
\tikzfig{figures/Applications/lov/convtp-phase-shift}:1 \to 1
\qquad \tikzfig{figures/Applications/lov/pol-rot}:1 \to 1
\qquad \tikzfig{figures/Applications/lov/beamsplitter}:2 \to 2
\qquad \tikzfig{figures/Applications/lov/bs}:2 \to 2
\end{equation*}

* vacuum state and effect:

\begin{equation*}
\tikzfig{figures/Applications/lov/gene-0}:0 \to 1 \qquad \tikzfig{figures/Applications/lov/detector-0}:1 \to 0
\end{equation*}

We  can interpret a subset of the generators of
\(\LOv\) in \(\GAA[\R]\cong\AR[\R]\).  Let \(\LOv'\) denote the fragment \(\LOv\) generated only by the phase shifters, wave plates, beamsplitters and polarizing beamsplitters.
Identifing the generators
of \(\LOv'\) with elements of the affine orthogonal group

we obtain a symmetric monoidal functor \(\interp{-}_{\GAA[\R]}^{\LOv'}:{\LOv'}\to\GAA[\R] \).
On objects it is given by doubling \(\interp{n}_{\GAA[\R]}^{\LOv'}=2n\), and on the
generators by:

\[
\begin{array}{rlcrl}
\label{eq:optics}
\interp{\tikzfig{figures/Applications/lov/pol-rot}}_{\GAA[\R]}^{\LOv'}
=&\ \tikzfig{figures/Applications/lov/rotation_ZX} &\quad&
\interp{\tikzfig{figures/Applications/lov/convtp-phase-shift}}_{\GAA[\R]}^{\LOv'}
=&\ \tikzfig{figures/Applications/lov/phase_ZX} \\ \\
\interp{\tikzfig{figures/Applications/lov/bs}}_{\GAA[\R]}^{\LOv'}
=&\ \tikzfig{figures/Applications/lov/polarising_bs}&\quad&
\interp{\tikzfig{figures/Applications/lov/beamsplitter}}_{\GAA[\R]}^{\LOv'}
=&\ \tikzfig{figures/Applications/lov/beamsplitter_ZX}
\end{array}
\]

Here, there are some terminological clashes.
Passive optical components correspond to affine relations whereas the passive
electric circuits discussed in subsection <ref> are linear relations. Furthermore, the phase-shifter in this context of quantum optics should therefore not be confused with the phase-shift gate in the context of stabiliser circuits which we discussed in subsubsection <ref>.

By working in the image of the embedding \(\interp{n}_{\GAA[\R]}^{\LOv'}\) we already have the ability to model
additional quantum-optical components that are not present in
\(\mathsf{LOv}\). For instance, active squeezing of the vertical polarisation
mode is given, for \(\eta \in \R\), by:

\begin{equation}
\tikzfig{figures/Applications/lov/squeezing}
\end{equation}

Furthermore \(\GAA[\R]\) is compact closed, as opposed to the usual infinite dimensional Hilbert space semantics,  so by contrast we have much more freedom for rewriting in this setting.

Extending along the embedding \(\GAA[\R] \to\ZX[\R]\),
we can now also describe more components of Gaussian quantum optics,
since these correspond to elements of the affine symplectic group

In this setting, shearing between the position and momentum
operators takes the form:

\begin{equation}
\tikzfig{figures/Applications/lov/shear}
\end{equation}

However, one can not interpret the vacuum state in
\(\ALR[\R]\), because this only admits “infinitely-squeezed” states. In our forthcoming paper
<cit.>, we will also show that there is a symmetric monoidal embedding \(\interp{-}^\LOv_{\ZX[\C]} : \LOv
\to \ZX[\C]\). This interpretation extends the one above and is given
on the vacuum state and effect by:

\begin{align}
\interp{\tikzfig{figures/Applications/lov/gene-0}}^\LOv_{\ZX[\C]}
= \tikzfig{figures/Applications/lov/vacuum_state}
\qquad\qquad
\interp{\tikzfig{figures/Applications/lov/detector-0}}^\LOv_{\ZX[\C]}
= \tikzfig{figures/Applications/lov/vacuum_effect}
\end{align}

lifting the diagrammatic characterisation of quopit stabiliser quantum
mechanics given in <cit.> to the setting of Gaussian quantum
mechanics <cit.>.

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

journaltitleNew Journal of Physics
shortjournalNew J. Phys.
titleThe ZX-calculus is complete for stabilizer quantum mechanics
Quantum Physics

Springer Science
Business Media LLC

journaltitleFoundations of Physics
titleA Complete Graphical Calculus for Spekkens’ Toy Bit Theory

Open Publishing Association

journaltitleElectronic Proceedings in Theoretical Computer Science
titleZH: A Complete Graphical Calculus for Quantum Computations Involving Classical Non-linearity

titleNetwork Theory (Part 29)

journaltitleTheory and Applications of Categories
titleProps in network theory

journaltitleTheory and Applications of Categories
titleCategories in control

journaltitleTheory and Applications of Categories
titleA compositional framework for passive linear networks
pagespp 11581222

titleAn Efficient Algorithm to Recognize Locally Equivalent Graphs in Non-Binary Case
Computer Science - Data Structures and Algorithms

titleGraph States Under the Action of Local Clifford Group in Non-Binary Case
Quantum Physics

Open Publishing Association

journaltitleElectronic Proceedings in Theoretical Computer Science
titleTechniques to Reduce $\pi/4$-Parity-Phase Circuits, Motivated by the ZX Calculus

Florence, Italy

booktitleProceedings of the meeting "Geometry and Physics"
eventtitleGeometry and Phyiscs
titleThe category of symplectic reductions

booktitleSymplectic Geometry
titleLinear Symplectic Relations

Springer International Publishing

booktitleLecture Notes in Computer Science
titleGraphical Piecewise-Linear Algebra

Open Publishing Association

journaltitleElectronic Proceedings in Theoretical Computer Science
titleString Diagrammatic Electrical Circuit Theory

Schloss Dagstuhl - Leibniz-Zentrum für Informatik

booktitle41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021, December 15-17, 2021, Virtual Conference
titleDiagrammatic Polyhedral Algebra

Association for Computing Machinery (ACM)

journaltitleProceedings of the ACM on Programming Languages
titleDiagrammatic algebra: from linear to concurrent systems
ttps://www.ioc.ee/ pawel/papers/popl19.pdf

booktitle2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
titleGraphical affine algebra

Springer Berlin Heidelberg

booktitleLecture Notes in Computer Science
titleA Categorical Semantics of Signal Flow Graphs

journaltitleJournal of Pure and Applied Algebra
titleInteracting Hopf algebras

Elsevier BV

journaltitleInformation and Computation
titleThe Calculus of Signal Flow Diagrams I: Linear relations on streams
ttps://www.ioc.ee/ pawel/papers/sfg1.pdf

Dagstuhl, Germany

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

booktitle47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)
noteISSN: 1868-8969
seriesLeibniz International Proceedings in Informatics (LIPIcs)
titleComplete ZX-Calculi for the Stabiliser Fragment in Odd Prime Dimensions

titleA complete equational theory for Gaussian quantum mechanics with infinite squeezing

journaltitleJournal of Physics A: Mathematical and Theoretical
notePublisher: IOP Publishing
shortjournalJ. Phys. A: Math. Theor.
titleOutcome determinism in measurement-based quantum computation with qudits

journaltitleJournal of Combinatorial Theory, Series B
shortjournalJournal of Combinatorial Theory, Series B
titleCircle Graph Obstructions

journaltitleNew Journal of Physics
shortjournalNew J. Phys.
titleGeneralized Cluster States Based on Finite Groups
Quantum Physics

titleA note on diagonal gates in SZX-calculus
Quantum Physics

Université de Lorraine

titleWielding the ZX-calculus, Flexsymmetry, Mixed States, and Scalable Notations

Dagstuhl, Germany

Schloss Dagstuhl–Leibniz-Zentrum für Informatik

booktitle44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)
seriesLeibniz International Proceedings in Informatics (LIPIcs)
titleSZX-calculus: Scalable Graphical Quantum Reasoning
Quantum Physics

Association for Computing Machinery (ACM)

journaltitleACM Transactions on Quantum Computing
titleCompleteness of Graphical Languages for Mixed State Quantum Mechanics

Dagstuhl, Germany

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

booktitle47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)
noteISSN: 1868-8969
seriesLeibniz International Proceedings in Informatics (LIPIcs)
titleLOv-Calculus: A Graphical Language for Linear Optical Quantum Circuits
Completeness,Quantum Computing,Graphical Language,Linear Optical Circuits,Linear Optical Quantum Computing

American Physical Society (APS)

journaltitlePhysical Review A
titleEfficient computations of encodings for quantum error correction

noteNumber: arXiv:2205.05870
titleCategories of Kirchhoff relations
05.05870 [quant-ph]
Quantum Physics

journaltitleJournal of Pure and Applied Algebra
shortjournalJournal of Pure and Applied Algebra
titleWeakly distributive categories

Open Publishing Association

journaltitleElectronic Proceedings in Theoretical Computer Science
titleMoore-Penrose Dagger Categories

eventtitleApplied Category Theory 2023
titleNormalizing Resistor Networks

IOP Publishing

journaltitleNew Journal of Physics
titleInteracting quantum observables: categorical algebra and diagrammatics

Open Publishing Association

booktitleProceedings 17th International Conference on Quantum Physics and Logic, Paris, France, June 2 - 6, 2020
seriesElectronic Proceedings in Theoretical Computer Science
titleThe ZX&-calculus: A complete graphical calculus for classical circuits using spiders

titleThe Algebra for Stabilizer Codes

eventtitleApplied Category Theory 2021
titleA Graphical Calculus for Lagrangian Relations

Open Publishing Association

journaltitleElectronic Proceedings in Theoretical Computer Science
titlePhase Gadget Synthesis for Shallow Circuits

University of California Riverside

titleCircuits, bond graphs, and signal-flow diagrams: A categorical perspective

titleGraph-theoretic Simplification of Quantum Circuits with the ZX-calculus

American Physical Society (APS)

journaltitlePhysical Review A
titleGraphical description of the action of Clifford operators on stabilizer states

University of California Riverside

titleCategories in control: applied PROPs

California Institute of Technology

titleStabilizer Codes and Quantum Error Correction

journaltitleChaos, Solitons & Fractals
shortjournalChaos, Solitons & Fractals
titleFault-Tolerant Quantum Computation with Higher-Dimensional Systems
Quantum Physics

journaltitleAmerican Journal of Mathematics
shortjournalAmerican Journal of Mathematics
titleSome Problems in Integral Geometry and Some Related Problems in Micro-Local Analysis

Los Alamitos, CA, USA

IEEE Computer Society

booktitle2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
titleA Diagrammatic Axiomatisation for Qubit Entanglement

journaltitleQuantum Inf. Comput.
titleCluster state quantum computation for many-level systems

issn2469-9926, 2469-9934
journaltitlePhysical Review A
shortjournalPhys. Rev. A
titleImproved Graph Formalism for Quantum Circuit Simulation
10 [quant-ph]

journaltitleLogical Methods in Computer Science
titleCompleteness of the ZX-Calculus
volumeVolume 16, Issue 2
Quantum Physics ; Computer Science - Logic in Computer Science

journaltitleScientific Reports
noteNumber: 1 Publisher: Nature Publishing Group
shortjournalSci Rep
titleLogical measurement-based quantum computation in circuit-QED
Quantum information,Qubits

issn1432-4350, 1433-0490
journaltitleTheory of Computing Systems
shortjournalTheory Comput Syst
titleThe Rank-Width of Edge-Colored Graphs

issn1050-2947, 1094-1622
journaltitlePhysical Review A
shortjournalPhys. Rev. A
titleQuantum secret sharing with qudit graph states

Berlin, Heidelberg

seriesLecture Notes in Physics
titleA Symplectic Framework for Field Theories
dynamics,Feldtheorie,field theory,geometry,mechanics,Mechanik,Symplektische Geometrie
given=Student of,

journaltitleAnnalen der Physik
titleUeber den Durchgang eines elektrischen Stromes durch eine Ebene, insbesondere durch eine kreisförmige

American Physical Society (APS)

journaltitlePhysical Review A
titleReducing the number of non-Clifford gates in quantum circuits

Springer New York

journaltitleGraduate Texts in Mathematics
titleCategories for the Working Mathematician
ttp://www.mtm.ufsc.br/ ebatista/2016-2/maclanecat.pdf

journaltitleJournal of Differential Equations
shortjournalJournal of Differential Equations
titleSpecial symplectic spaces

Open Publishing Association

journaltitleElectronic Proceedings in Theoretical Computer Science
titleHypergraph Simplification: Linking the Path-sum Approach to the ZH-calculus

noteArtwork Size: 17 pages Medium: application/pdf Publisher: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany
titleAccess Structure in Graphs in High Dimension and Application to Secret Sharing
pages17 pages
000 Computer science,knowledge,general works,Computer Science

Open Publishing Association

journaltitleElectronic Proceedings in Theoretical Computer Science
titleComplete Flow-Preserving Rewrite Rules for MBQC Patterns with Pauli Measurements

titleA universal completion of the ZX-calculus

Bei T.H. Riemann

titleDie galvanische Kette

Paris, France

booktitleElectronic Proceedings in Theoretical Computer Science
eventtitleTwentieth International Conference on Quantum Physics and Logic
shorttitleThe Qupit Stabiliser ZX-travaganza
titleThe Qupit Stabiliser ZX-travaganza: Simplified Axioms, Normal Forms and Graph-Theoretic Simplification

Chichester, England

John Wiley & Sons

titleMicrowave Engineering

issn2469-9926, 2469-9934
journaltitlePhysical Review A
shortjournalPhys. Rev. A
titleAncilla-driven quantum computation for qudits and continuous variables

journaltitleNature Physics
noteNumber: 2 Publisher: Nature Publishing Group
shortjournalNature Phys
titleHigh-dimensional one-way quantum processing implemented on d-level cluster states

University of Glasgow

titleBond Graph Modelling of Physical Systems

journaltitleJournal of Geometry and Physics
shortjournalJournal of Geometry and Physics
titleThe category of Fresnel kernels
Fresnel Kernels,Morse Families,Symplectic Relations

journaltitleAtti della Accademia delle Scienze di Torino. Classe di Scienze Fisiche, Matematiche e Naturali
shortjournalAtti della Accademia delle Scienze di Torino. Classe di Scienze Fisiche, Matematiche e Naturali
titleThe structure of positive linear symplectic relations

journaltitlePhysical Review A
notePublisher: American Physical Society
shortjournalPhys. Rev. A
titleGraphical description of the action of local Clifford transformations on graph states

Open Publishing Association

booktitleProceedings 14th International Conference on Quantum Physics and Logic, Nijmegen, The Netherlands, 3-7 July 2017
seriesElectronic Proceedings in Theoretical Computer Science
titleQutrit ZX-calculus is Complete for Stabilizer Quantum Mechanics

issn0034-6861, 1539-0756
journaltitleReviews of Modern Physics
titleGaussian Quantum Information

Berlin, Heidelberg

Springer Berlin Heidelberg

isbn978-3-540-11197-9 978-3-540-39002-2
noteBook Title: Differential Geometric Methods in Mathematical Physics Series Title: Lecture Notes in Mathematics
titleThe symplectic “category”

titleSymplectic Categories

titleZX-calculus for the working quantum computer scientist

titleString diagrams for non-strict monoidal categories

Université de Lyon

titleInteracting Hopf Algebras: the theory of linear systems

issn1050-2947, 1094-1622
journaltitlePhysical Review A
shortjournalPhys. Rev. A
titleQuantum computation based on d-level cluster states
Quantum Physics

§ AXIOM TABLES

§.§ Axioms for GSA

Let \(\ZX\) denote the †-compact prop with:

* Objects natural numbers.

* Morphisms are presented by the following generators indexed by \(n,m \in \N\) and \(a,b\in \K\):

\begin{equation*}
\tikzfig{figures/AffLagRel/b-spider} : m \to n  \quad\quad\quad
\tikzfig{figures/AffLagRel/w-spider} : m \to n  \quad\quad\quad
\tikzfig{figures/AffLagRel/box} : 1 \to 1
\end{equation*}

Modulo the equations imposing flexsymmetry, in addition to the following equations for all \(a,b,c,d \in \mathbb{K}\) and \(z
\in \mathbb{K}^*\):

* Composition is given by horizontally connecting output wires
to input wires.

* The monoidal product is given on objects by addition,
and on morphisms by vertical juxtaposition.

* The compact structure is obtained from the grey Frobenius algebra:

\begin{equation*}
\tikzfig{figures/AffLagRel/cup} =  \tikzfig{figures/AffLagRel/cup_explicit}
\qand
\tikzfig{figures/AffLagRel/cap} =  \tikzfig{figures/AffLagRel/cap_explicit}
\end{equation*}

* The dagger is given by:

\begin{equation*}
\tikzfig{figures/AffLagRel/b-spider} \longmapsto \tikzfig{figures/AffLagRel/b-spider-daggered}  \quad\quad
\tikzfig{figures/AffLagRel/w-spider} \longmapsto \tikzfig{figures/AffLagRel/w-spider-daggered}  \quad\quad
\tikzfig{figures/AffLagRel/box} \longmapsto
\tikzfig{figures/AffLagRel/minusbox}
\end{equation*}

§.§ Axioms for linear GSA

Let \(\ZX^0\) denote the †-compact prop with:

* Objects natural numbers.

* Morphisms are presented by the following generators indexed by \(n,m \in \N\) and \(a\in \K\):

\begin{equation*}
\tikzfig{figures/AffLagRel/linear/b-spider} : m \to n  \quad\quad\quad
\tikzfig{figures/AffLagRel/linear/w-spider} : m \to n  \quad\quad\quad
\tikzfig{figures/AffLagRel/box} : 1 \to 1
\end{equation*}

Modulo the equations imposing flexsymmetry, in addition to the following equations for all \(a,b \in \mathbb{K}\) and \(z
\in \mathbb{K}^*\):

* Composition is given by horizontally connecting output wires
to input wires.

* The monoidal product is given on objects by addition,
and on morphisms by vertical juxtaposition.

* The compact structure is obtained from the grey Frobenius algebra:

\begin{equation*}
\tikzfig{figures/AffLagRel/cup} =  \tikzfig{figures/AffLagRel/cup_explicit}
\qand
\tikzfig{figures/AffLagRel/cap} =  \tikzfig{figures/AffLagRel/cap_explicit}
\end{equation*}

* The dagger is given by:

\begin{equation*}
\tikzfig{figures/AffLagRel/linear/b-spider} \longmapsto \tikzfig{figures/AffLagRel/linear/b-spider-daggered}  \quad\quad
\tikzfig{figures/AffLagRel/linear/w-spider} \longmapsto \tikzfig{figures/AffLagRel/linear/w-spider-daggered}  \quad\quad
\tikzfig{figures/AffLagRel/box} \longmapsto
\tikzfig{figures/AffLagRel/minusbox}
\end{equation*}

§.§ Scalable  GSA

The strictification \([\ZX]\) can be explicitly presented by generators
and relations:

* Objects are elements of  \(\operatorname{List}(\N)\).

* Morphisms are presented by the following generators indexed
by \(n,m,k, \ell \in \N\), \(\vec v \in \N^n\) and \(x,y\in \K\):

\begin{align*}
\tikzfig{figures/AffLagRel/scalable/b-spider} &: [k, \overset{m}{\cdots}, k] \to [k, \overset{n}{\cdots}, k]&
\quad\quad
\tikzfig{figures/AffLagRel/scalable/w-spider}  &: [k, \overset{m}{\cdots}, k] \to [k, \overset{n}{\cdots}, k] &
\\
\tikzfig{figures/AffLagRel/scalable/box} &: [k] \to [k] &
\quad\quad
\tikzfig{figures/AffLagRel/scalable/arrow} &: [k] \to [\ell] &
\\
\tikzfig{figures/AffLagRel/scalable/dividermonoid} &: \left[\sum_{i=0}^{n-1}v_i\right] \to [v_0,\cdots, v_{n-1}] &
\quad\quad
\tikzfig{figures/AffLagRel/scalable/gatherermonoid} &: [v_0,\cdots, v_{n-1}]   \to \left[\sum_{i=0}^{n-1}v_i \right] &
\end{align*}

modulo the equations that the phased spiders and boxes are flexsymmetric in addition to the following equations for all \(n,m,k \in \N\),  \(\vec x,\vec y \in \K^n\), \(\vec w \in \K^m\), \(X,Y\in\Sym[n][\K]\), \(W \in \Sym[m][\K]\),  \(A,B,Z\in \Matrices[m][n][\K]\), \(C\in \Matrices[k][n][\K]\), \(D\in \Matrices[m][\ell][\K]\), \(E\in \Matrices[k][\ell][\K]\),  with \(Z\) surjective:

* Composition is given by horizontally connecting output wires
to input wires.

* The monoidal product is given on objects by concatenation of lists,
and on morphisms by vertical juxtaposition.

* The compact structure is obtained from the grey Frobenius algebra:

\begin{equation*}
\tikzfig{figures/AffLagRel/thick/cup} =  \tikzfig{figures/AffLagRel/thick/cup_explicit}
\qand
\tikzfig{figures/AffLagRel/thick/cap} =  \tikzfig{figures/AffLagRel/thick/cap_explicit}
\end{equation*}

* The dagger is given by:

\begin{equation*}
\tikzfig{figures/AffLagRel/thick/b-spider} \mapsto \tikzfig{figures/AffLagRel/thick/b-spider-daggered}  \quad
\tikzfig{figures/AffLagRel/thick/w-spider} \mapsto \tikzfig{figures/AffLagRel/thick/w-spider-daggered}  \quad
\tikzfig{figures/AffLagRel/thick/box} \mapsto \tikzfig{figures/AffLagRel/thick/box-daggered} \quad
\tikzfig{figures/AffLagRel/thick/matrix} \mapsto \tikzfig{figures/AffLagRel/thick/matrix-daggered}
\end{equation*}

\begin{equation*}
\tikzfig{figures/AffLagRel/scalable/gatherermonoid} \longmapsto \tikzfig{figures/AffLagRel/scalable/dividermonoid} \quad\quad \tikzfig{figures/AffLagRel/scalable/dividermonoid}\longmapsto  \tikzfig{figures/AffLagRel/scalable/gatherermonoid}
\end{equation*}

We prove in lemma <ref> and in lemma <ref>.  All of the other axioms have already been proven, or follow by simple induction arguments.  In the thickened setting, remark by lemma <ref>, we don't need a thickened version of .

Note that we have not given a flexsymmetric presentation of the strictification of \(\ZX\) because the dividers and gathers can not be made to be symmetric!

§ PROOFS

§.§ Proofs of section <ref>

We start with the first set of proposition:

$(1)\Rightarrow (2)$ Taking the relational semantics, $(2)$ can be reformulated as: for all $x,y,z\in \K$, $Ax=Ay=z$ is equivalent to $x=y$ and $z=Ax=Ay$. Which is true if $A$ is injective.

$(2)\Rightarrow (3)$ figures/AffRel/inj2to3

$(3)\Rightarrow (4)$figures/AffRel/inj3to4

$(4)\Rightarrow (1)$ Taking the relational semantics, $(4)$ amounts to $\ker(A) = \{0\}$ which implies that $A$ is injective.

Then the second set of propositions:

$(1)\Rightarrow (2)$ Taking the relational semantics, $(2)$ can be reformulated as: for all $x,y,z\in \K$, $-Ax=y+z$ is equivalent to there exists $a,b\in\K$, such that $-x=a+b$, $y=Aa$ and $z=Ab$. Which is true if $A$ is surjective by taking premimages of $y$ and $z$.

$(2)\Rightarrow (3)$figures/AffRel/surj2to3

$(3)\Rightarrow (4)$figures/AffRel/surj3to4

$(4)\Rightarrow (1)$ Taking the relational semantics, $(4)$ amounts to $\Im(A)$ being equal to the full space, which implies that $A$ is surjective.

§.§ Proofs of section <ref>

\[\tikzfig{figures/soundness/lemmas/antipode}\]

This follows immediately from and the uniqueness of inverses.

\[\tikzfig{figures/soundness/lemmas/affinediscard}\]

\begin{equation}
\tikzfig{figures/soundness/lemmas/affinediscardproof}
\end{equation}

Given \(a \in \K^*\):

\[\tikzfig{figures/soundness/lemmas/inversetranspose}\]

\begin{equation}
\tikzfig{figures/soundness/lemmas/inversetransposeproof}
\end{equation}

\begin{equation}
\tikzfig{figures/soundness/lemmas/inversetransposeproofii}
\end{equation}

Given \(a \in \K^*\):

\[\tikzfig{figures/soundness/lemmas/cnotswap}\]

\[\tikzfig{figures/soundness/lemmas/cnotswapproof}\]

The only nontrivial thing to check is the functoriality of \(\interp{-}_{\gaa}^\zx\).  To this end, we show that al of the axioms of \(\ZX\) are sound:

\begin{align}\label{lem:fusion}
\interp{\tikzfig{figures/soundness/fusion/fusion_LHS}}_\gaa^\zx
\tikzfig{figures/soundness/fusion/fusion_1}
\stackeqmid{\GAAFusionB \\ \GAAFusionW}
\tikzfig{figures/soundness/fusion/fusion_2}\\
\stackeq{\GAAAdd}
\tikzfig{figures/soundness/fusion/fusion_3}
= \interp{\tikzfig{figures/soundness/fusion/fusion_RHS}}_\gaa^\zx
\end{align}

The white version of follows from an analagous argument.

\begin{align}\label{lem:bigebra}
\interp{\tikzfig{figures/soundness/bigebra/bigebra_LHS}}_\gaa^\zx
&= \tikzfig{figures/soundness/bigebra/bigebra_1}
\stackeqmid{\GAAidoneii\\ \minilemref{lem:antipode} } \tikzfig{figures/soundness/bigebra/bigebra_2} \\
\stackeq{\GAABigebra\\ \GAAidoneii\\ \minilemref{lem:antipode}} \tikzfig{figures/soundness/bigebra/bigebra_3}
\end{align}

\begin{align}\label{lem:copy}
\interp{\tikzfig{figures/soundness/copy/copy_LHS}}_\gaa^\zx
= \tikzfig{figures/soundness/copy/copy_1}
\stackeqmid{\GAACopyi \\ \GAACopyii }
\tikzfig{figures/soundness/copy/copy_4}
= \interp{\tikzfig{figures/soundness/copy/copy_RHS}}_\gaa^\zx
\end{align}

\begin{align}\label{lem:one}
\interp{\tikzfig{figures/soundness/one/one_LHS}}_\gaa^\zx
&= \tikzfig{figures/soundness/one/one_1}
\stackeqmid{\minilemref{lem:affinediscard}\\ \GAAdisciii \\ \GAACap}
\tikzfig{figures/soundness/one/one_2}
\stackeqmid{\GAAidzeroi}
\tikzfig{figures/soundness/one/one_MHS}
= \interp{\tikzfig{figures/soundness/one/one_MHS}}_\gaa^\zx\\
&= \interp{\tikzfig{figures/soundness/one/one_MHS}}_\gaa^\zx
= \tikzfig{figures/soundness/one/one_MHS}
\stackeqmid{\GAAidzeroii \\ \GAAidzeroiii}
\tikzfig{figures/soundness/one/one_3}
\interp{\tikzfig{figures/soundness/one/one_RHS}}_\gaa^\zx
\end{align}

\begin{align}\label{lem:zero}
\interp{\tikzfig{figures/soundness/zero/zero_LHS}}_\gaa^\zx
= \tikzfig{figures/soundness/zero/zero_1}
\stackeqmid{\GAAEmpty}
\tikzfig{figures/soundness/zero/zero_2}
= \interp{\tikzfig{figures/soundness/zero/zero_RHS}}_\gaa^\zx
\end{align}

\begin{align}\label{lem:id}
\interp{\tikzfig{figures/soundness/id/id_LHS}}_\gaa^\zx
= \tikzfig{figures/soundness/id/id_1}
\stackeqmid{\GAAidoneii \\ \GAAidoneiii}
\tikzfig{figures/soundness/id/id_2}
= \interp{\tikzfig{figures/soundness/id/id_RHS}}_\gaa^\zx
\end{align}

If \(a \neq 0\),

\begin{align}\label{lem:box}
\interp{\tikzfig{figures/soundness/box/box_RHS}}_\gaa^\zx
&= \tikzfig{figures/soundness/box/box_1}
\stackeqmid{\minilemref{lem:affinediscard}\\ \GAAidoneii} \tikzfig{figures/soundness/box/box_2} \\
\stackeq{\GAACopyiii \\ \GAACopyiv}
\tikzfig{figures/soundness/box/box_3} \\
\stackeq{\minilemref{lem:inversetranspose}} \tikzfig{figures/soundness/box/box_4} \\
\stackeq{\minilemref{lem:cnotswap}} \tikzfig{figures/soundness/box/box_5}
= \tikzfig{figures/soundness/box/box_6}
= \interp{\tikzfig{figures/soundness/box/box_LHS}}_\gaa^\zx
\end{align}

If \(a,b \neq 0\),

\begin{align}\label{lem:times}
\interp{\tikzfig{figures/soundness/times/times_LHS}}_\gaa^\zx
&= \tikzfig{figures/soundness/times/times_1} \\
&= \tikzfig{figures/soundness/times/times_2} \\
\stackeq{\minilemref{lem:antipode}\\ \GAAMult} \tikzfig{figures/soundness/times/times_3}
= \interp{\tikzfig{figures/soundness/times/times_RHS}}_\gaa^\zx
\end{align}

\begin{align}\label{lem:plus}
\interp{\tikzfig{figures/soundness/plus/plus_LHS}}_\gaa^\zx
&= \tikzfig{figures/soundness/plus/plus_1}\\
\stackeq{\GAAFusionW \\ \GAAidoneii} \tikzfig{figures/soundness/plus/plus_2} \\
\stackeq{\GAAAdd} \tikzfig{figures/soundness/plus/plus_3}
= \interp{\tikzfig{figures/soundness/plus/plus_RHS}}_\gaa^\zx
\end{align}

\begin{align}\label{lem:colour}
\stackeqmid{} \tikzfig{figures/soundness/colour/colour_1} \\
\stackeq{} \tikzfig{figures/soundness/colour/colour_1_1}
\stackeqmid{\GAAFusionW} \tikzfig{figures/soundness/colour/colour_1_2}\\
\stackeq{\minilemref{lem:inversetranspose} \\ \GAACopyiii \\ \GAACopyiv} \tikzfig{figures/soundness/colour/colour_1_3}
\stackeqmid{\minilemref{lem:antipode}} \tikzfig{figures/soundness/colour/colour_1_4}\\
\stackeq{\minilemref{lem:inversetranspose}} \tikzfig{figures/soundness/colour/colour_1_5}
\stackeqmid{\GAAMult} \tikzfig{figures/soundness/colour/colour_1_6}\\
\stackeq{\GAAMult} \tikzfig{figures/soundness/colour/colour_1_7}
\stackeqmid{\minilemref{lem:antipode}} \tikzfig{figures/soundness/colour/colour_1_8}\\
\stackeq{\GAAidonei} \tikzfig{figures/soundness/colour/colour_1_9}
\stackeqmid{\GAAdiscii} \tikzfig{figures/soundness/colour/colour_1_10} \\
\stackeq{\GAAFusionW} \tikzfig{figures/soundness/colour/colour_3}
\stackeqmid{ } \interp{\tikzfig{figures/soundness/colour/colour_RHS}}_\gaa^\zx
\end{align}

§.§ Proofs of section <ref>

Products of boxes are antipodes: for any \(z \in \K^*\)

\begin{equation*}
\tikzfig{figures/completeness/box_product}
\end{equation*}

\begin{equation}
\tikzfig{figures/completeness/box_product_proof}
\end{equation}

For any \(z \in \K^*\)

\begin{equation*}
\tikzfig{figures/completeness/box_identity}
\end{equation*}

\begin{equation}
\tikzfig{figures/completeness/box_identity_proof}
\end{equation}

\begin{equation*}
\tikzfig{figures/completeness/box_inverse}
\end{equation*}

\begin{equation}
\tikzfig{figures/completeness/box_inverse_proof}
\end{equation}

Boxes and antipodes commute: for any \(z \in \K^*\),

\begin{equation*}
\tikzfig{figures/completeness/box_antipode}
\end{equation*}

\begin{equation}
\tikzfig{figures/completeness/box_antipode_proof}
\end{equation}

The opposite-inverse box can be written as follows: for any \(z \in \K^*\),

\begin{equation*}
\tikzfig{figures/completeness/box_opposite_inverse}
\end{equation*}

\begin{equation}
\tikzfig{figures/completeness/box_opposite_inverse_proof}
\end{equation}

The “inverse” colour change rule is provable from the axioms: for any
\(z \in \K^*\),

\begin{equation*}
\tikzfig{figures/completeness/colour_inverted}
\end{equation*}

\begin{equation}
\tikzfig{figures/completeness/colour_inverted_proof}
\end{equation}

Spiders absorb antipodes:

\begin{equation*}
\tikzfig{figures/completeness/antipode_spider}
\end{equation*}

These follow straightforwardly from lemma <ref>, and lemma <ref>.

The “cut” rule for the zero box is derivable:

\begin{equation*}
\tikzfig{figures/completeness/box_zero}
\end{equation*}

\begin{equation}
\tikzfig{figures/completeness/box_zero_proof}
\end{equation}

A colour-swapped version of is derivable: for any \(a \in \K\),

\begin{equation*}
\tikzfig{figures/completeness/copy_swapped}
\end{equation*}

\begin{equation}
\tikzfig{figures/completeness/copy_swapped_proof}
\end{equation}

The Hopf identity is derivable:

\begin{equation*}
\tikzfig{figures/completeness/hopf}
\end{equation*}

\begin{equation}
\tikzfig{figures/completeness/hopf_proof}
\end{equation}

Strictly-affine white states absorb arbitrary phases and vice-versa:

\begin{equation*}
\tikzfig{figures/completeness/pauli_state_push}
\end{equation*}

\begin{align}
&\tikzfig{figures/completeness/pauli_state_push_proof} \\
\end{align}

For any \(a,b \in \K\),

\begin{equation*}
\tikzfig{figures/completeness/phase_inverses}
\end{equation*}

\begin{equation}
\tikzfig{figures/completeness/phase_inverses_proof}
\end{equation}

\begin{equation}
\tikzfig{figures/completeness/phase_inverses_proof_2}
\end{equation}

There are four (more or less equivalent) versions of : for any
\(z \in \K^*\),

\begin{equation*}
\tikzfig{figures/completeness/box_swapped}
\end{equation*}

The first two equations are also valid for \(z = 0\).

The first equation is just .

\begin{equation}
\tikzfig{figures/completeness/box_swapped_proof_1}
\end{equation}

\begin{equation}
\tikzfig{figures/completeness/box_swapped_proof_2}
\end{equation}

\begin{equation}
\tikzfig{figures/completeness/box_swapped_proof_3}
\end{equation}

States with non-zero symplectic part can all be represented using both
grey and white spiders: for any \(a \in \K\) and \(b \in \K^*\),

\begin{equation*}
\tikzfig{figures/completeness/symplectic_states}
\end{equation*}

\begin{equation}
\tikzfig{figures/completeness/symplectic_states_proof_green}
\end{equation}

The second equation follows once again using and
lemma <ref>.

For any \(m,n \in \N\) and \(A \in \Matrices\),

\begin{equation*}
\tikzfig{figures/completeness/scalable/arrow_transpose}
\end{equation*}

This follows from a straightforward induction on the type \(m \times n\)
of the matrix \(A\).

For any \(\vec{x} \in \K^n\) and \(X \in \Sym\),

\begin{equation*}
\tikzfig{figures/completeness/scalable/colour}
\end{equation*}

This follows straightforwardly by induction on the size \(n\) of the thick
wires, using lemma <ref>.

For any \(\vec{x},\vec{y} \in \K^n\) and \(X,Y \in \Sym\),

\begin{equation*}
\tikzfig{figures/completeness/scalable/fusion}
\end{equation*}

We prove thickened grey fusion by induction on the type \(n\in\N\) of the thick wires. The base case is trivial. Assume that the inductive claim holds for \(n=k\), and denote this assumption by  \(\textsc{Fusion}_k\) .
Suppose we have two black spiders as above, of type \(k+1\). Then:

\begin{equation}
\tikzfig{figures/completeness/scalable/fusion_proof}
\end{equation}

where we assume without loss of generality that

\begin{equation}
X = \begin{bmatrix} X_{1,1} & X_{1,\bullet}^\trans \\ X_{1,\bullet} & X' \end{bmatrix}
\qand
Y = \begin{bmatrix} Y_{1,1} & Y_{1,\bullet}^\trans \\ Y_{1,\bullet} & Y' \end{bmatrix}
\end{equation}

The white spider fusion follows from essentially the same argument.

For any \(n \in \N\) and \(A \in \Matrices[n][n]\),

\begin{equation*}
\tikzfig{figures/completeness/scalable/box_loop}
\end{equation*}

We proceed again by induction on the type \(n\) of the thick wires,
equivalently, the dimension of the matrix \(A\).  The base case is trivial.  Assume that the inductive claim holds for \(n=k\), and denote this by \((\textsc{Loop}_k)\),
Note that for any \(x \in \K\):

\begin{equation}
\label{eq:box_loop_thin}
\tikzfig{figures/completeness/scalable/box_loop_proof_1}
\end{equation}

Now, let \(A \in\Matrices[k+1][k+1]\), and assume without loss of
generality that it takes the following form for some \(a \in \K, B \in \Matrices[k][1], C \in
\Matrices[1][k] \qand D \in  \Matrices[k][k]\):

\begin{equation}
A =
\begin{bmatrix}
a & C \\ B & D
\end{bmatrix}
\end{equation}

\begin{equation}
\tikzfig{figures/completeness/scalable/box_loop_proof_2}
\end{equation}

where in the last step we have identified

\begin{equation}
A + A^\trans = \begin{bmatrix}
2a & C + B^\trans
\\ B + C^\trans & D + D^\trans
\end{bmatrix}
\end{equation}

For any \(m,n \in \N\), any \(A \in \Matrices\), any \(\vec x \in \K^m\)
and any \(X \in \Sym[m]\),

\begin{equation*}
\tikzfig{figures/completeness/scalable/arrow_phase}
\end{equation*}

The proof is by (double) induction on the shape \(m,n \in \N\) of the
matrix \(A\). The base case is trivial.

Now, fix \(m,n\) and assume the lemma is true for any matrix in
\(\Matrices[j][k]\) where either \(j \leqslant m\) or \(k
\leqslant n\), and let \(A \in  \Matrices[m+1][n]\). Then,
denoting the inductive step by \(\textsc{Ind}_{m,n}\),

\begin{equation}
\tikzfig{figures/completeness/scalable/arrow_phase_proof_2}
\end{equation}

where we have identified

\begin{equation}
\vec x = \begin{bmatrix} x_1 \\ \vec  x_\bullet \end{bmatrix}
\quad\quad\quad
X = \begin{bmatrix} X_{1,1} & X_{1,\bullet}^\trans \\ X_{1,\bullet} & X_{\bullet,\bullet} \end{bmatrix}
\quad\quad\quad
A = \begin{bmatrix} a \\ A_\bullet \end{bmatrix}
\end{equation}

so that \(Ax = ax_1 + A_\bullet \vec x_\bullet\) and \(A^\trans XA =
a^2 X_{1,1} + A_\bullet^\trans X_{\bullet,\bullet}A_\bullet +
aA_\bullet^\trans X_{1,\bullet} + aX_{1,\bullet}^\trans A_\bullet\).

Secondly, fix \(m \in \N\) and assume the lemma is true for all matrices
in \( \Matrices[j][k]\) such that \(j \leqslant m\). Pick
some \(A \in  \Matrices[1][n+1]\), then if \(A\) is zero, then

\begin{equation}
\tikzfig{figures/completeness/scalable/arrow_phase_proof_3}
\end{equation}

where the scalable version of is straightforwardly derivable by

Otherwise, some element of \(A\) is non-zero. For the sake of clarity,
we assume that this is the first element of \(A\), but since we can
write any permutation of the elements using the swap, there is no loss of
generality. Then,

\begin{equation}
\tikzfig{figures/completeness/scalable/arrow_phase_proof_4}
\end{equation}

where we have identified

\begin{equation}
\begin{bmatrix}
ya^2 & ya A_\bullet^\trans \\
ya A_\bullet & y A_\bullet^\trans A_\bullet
\end{bmatrix} = yA^\trans A
\end{equation}

This completes the induction.

For any \(m,n \in \N\), any injective \(A \in  \Matrices\), any \(\vec x \in \K^m\)
and any \(X \in \Sym\),

\begin{equation*}
\tikzfig{figures/completeness/scalable/arrow_label_black}
\end{equation*}

\begin{equation}
\tikzfig{figures/completeness/scalable/arrow_label_black_proof}
\end{equation}

For any \(m,n \in \N\), any surjective \(A \in \Matrices\), any \(\vec x \in \K^n\)
and any \(X \in \Sym\),

\begin{equation*}
\tikzfig{figures/completeness/scalable/arrow_label_white}
\end{equation*}

This follows from lemmas <ref>,
<ref> and <ref>, and the fact that
the transpose of a surjective matrix is injective.

\[\tikzfig{figures/completeness/scalable/colour}\]

This follows immediately by combining lemmas <ref> and <ref>.

For any \(X \in \Sym\),

\begin{equation*}
\tikzfig{figures/completeness/scalable/box}
\end{equation*}

If furthermore, \(X\) is invertible,

\begin{equation*}
\tikzfig{figures/completeness/scalable/box_invertible}
\end{equation*}

We start by proving the first equation. The proof is by induction on the
type \(n \in \N\) of the \(n \times n\) symmetric matrix \(X\).

The base case is trivial.

Assume the lemma is true for all \(j < n\) for some \(n
\in \N\), and pick \(X \in \Sym[n+1]\), which we assume takes the form for some \(X_{1,1} \in \K, X_{1,\bullet} \in \Matrices[n][1], \qand X_{\bullet,\bullet} \in \Matrices[n][n]\):

\begin{equation}
X = \begin{bmatrix} X_{1,1} & X_{1,\bullet}^\trans \\ X_{1,\bullet} & X_{\bullet,\bullet} \end{bmatrix}
\end{equation}

Now, if \(X_{1,\bullet} = 0\), we have

\begin{equation}
\tikzfig{figures/completeness/scalable/box_proof_1}
\end{equation}

Otherwise, \(X_{1,\bullet}\) is injective, so that, denoting the inductive
step by \(\textsc{Ind}_{m}\),

\begin{align}
\tikzfig{figures/completeness/scalable/box_proof_2/0}
\tikzfig{figures/completeness/scalable/box_proof_2/1}
\stackeqmid{\minieqref{eq:scalable_box}}
\tikzfig{figures/completeness/scalable/box_proof_2/2}\\
\stackeq{\HBox \\ \text{\tiny{$(\textsc{Ind}_n)$} }}
\tikzfig{figures/completeness/scalable/box_proof_2/3}
\stackeqmid{\minilemref{lem:scalable_fusion}}
\tikzfig{figures/completeness/scalable/box_proof_2/4}\\
\stackeq{\mini{\Bigebra}}
\tikzfig{figures/completeness/scalable/box_proof_2/5}
\stackeqmid{\minilemref{lem:scalable_colour}\\ \minilemref{lem:arrow_transpose}\\ \Fusion \\ \minilemref{lem:scalable_fusion}}
\tikzfig{figures/completeness/scalable/box_proof_2/6}\\
\stackeq{\minieqref{eq:thick_spider_def}}
\tikzfig{figures/completeness/scalable/box_proof_2/7}
\stackeqmid{\Bigebra}
\tikzfig{figures/completeness/scalable/box_proof_2/8}\\
\stackeq{\Bigebra}
\tikzfig{figures/completeness/scalable/box_proof_2/9}
\stackeqmid{\minilemref{lem:scalable_fusion}}
\tikzfig{figures/completeness/scalable/box_proof_2/10}\\
\stackeq{\tikzeqref{prop:matprop}}
\tikzfig{figures/completeness/scalable/box_proof_2/11}
\stackeqmid{\tikzeqref{prop:matprop}}
\tikzfig{figures/completeness/scalable/box_proof_2/12}\\
\stackeq{\GAAFusionB\\\GAAFusionW\\ \GAAAdd \\ \GAAZero\\ \GAAidonei\\ \GAAidoneii}
\tikzfig{figures/completeness/scalable/box_proof_2/13}
\stackeqmid{\minieqref{eq:thick_spider_def}}
\tikzfig{figures/completeness/scalable/box_proof_2/14}
\end{align}

This completes the induction.

The remaining equations follow from manipulations analogous to the proof
of lemma <ref>.

For any \(n \in \N\), \(\vec x \in \K^n\) and invertible \(X \in \Sym\),

\begin{equation*}
\tikzfig{figures/completeness/scalable/symplectic_states}
\end{equation*}

The proof is analogous to the proof of lemma <ref>.

Transform the diagram as follows:

* Use to change every white spider into a grey one,
surrounded by boxes. The resulting diagram consists of only grey
spiders and boxes.

* Use to add a grey spider between any two subsequent
boxes. The diagram now consists of only grey spiders, connected either
by plain edges or boxes.

* Use to fuse any two spiders connected by plain edges,
to eliminate any loops, and use lemma <ref> to eliminate
any “loops” carrying boxes. The resulting diagram contains no loops, and
furthermore spiders are connected only by edges carring boxes.

* Use to fuse all edges between two spiders into
a single weighted box or no edge (after a simple application of
lemma <ref> and ).

* Use and lemma <ref> to obtain

\begin{equation}
\tikzfig{figures/AffLagRel/spider_graph_split}\quad,
\end{equation}

which allows one to split any spider connected to more than one output into
several grey spiders, each connected to exactly one output.

The resulting diagram is in graph-like form.

\begin{equation}
\tikzfig{figures/completeness/scalable/symplectic_elimination_proof}
\end{equation}

\begin{equation}
\tikzfig{figures/completeness/local_complementation_old_proof}
\end{equation}

where \(E \in \Matrices[k][1]\) has components \(E_j\) and \(Z \in \Sym[k]\)
has components \(Z_{j,k}\). In the last diagram, we have
\(\gamma_i = z_i + E_i x z^{\minu 1}\),
\(\delta_i = Z_{i,i} - z^{\minu 1} E_i^2\),
and \(g_{i,j} = Z_{i j} - z^{\minu 1} E_i E_j\) as required.

\begin{equation}
\tikzfig{figures/completeness/pivot_proof}
\end{equation}

where we have applied proposiiton <ref> to the invertible submatrix

\begin{equation}
\begin{bmatrix} 0 & \epsilon \\ \epsilon & 0 \end{bmatrix}
\qq{whose inverse is}
\begin{bmatrix} 0 & \epsilon^{-1} \\ \epsilon^{-1} & 0 \end{bmatrix}.
\end{equation}

The matrix \(E \in \Matrices[k][2]\) has components \(E_{j,k}\) and \(Z
\in \Sym[k]\) has components \(Z_{j,k}\).  Here, we have
\(\gamma_i = z_i + \epsilon^{\minu 1} (a E_{2,i} + b E_{1,i})\),
\(\delta_i = Z_{i,i} - 2 \epsilon^{\minu 1} E_{1,i} E_{2,i}\),
and \(g_{i,j} = - \epsilon^{\minu 1} (E_{1,i} E_{2,j} + E_{1,j} E_{2,i})\) as requied.

Given a graph-like diagram, keep appling
propositions <ref> and <ref> to
the internal vertices of the diagram as long as it is possible. Every
application strictly reduces the number of internal vertices hence
the algorithm must halt. The result is a diagram in AP-form since
proposition <ref> eliminates all internal
vertices with non-zero symplectic phase, and proposition <ref>
eliminates all pairs of connected internal vertices.

White spiders with arbitrary phases copy affine grey spiders and vice-versa:

\begin{equation*}
\tikzfig{figures/completeness/extended-copy}
\qquad \qquad
\tikzfig{figures/completeness/extended-copy-compl}
\end{equation*}

First of all,

\begin{equation}
% \label{eq:pauli-commute-pf-1}
\tikzfig{figures/completeness/extended-copy-proof-1}
\end{equation}

Then, we separate the equation into two cases based on whether the grey spider
is affine or not.
In case $d = 0$, the grey spider is affine and therefore:

\begin{equation}
% \label{eq:pauli-commute-pf-2}
\tikzfig{figures/completeness/extended-copy-proof-2}
\end{equation}

Note that if \(d = 0\), then \(ad - c = -c\) and so the lemma holds.
Otherwise, \(d \neq 0\) and therefore \(d^{\minu 1}\) exists, so we can apply
the state-change lemma:

\begin{equation}
% \label{eq:pauli-commute-pf-3}
\tikzfig{figures/completeness/extended-copy-proof-3}
\end{equation}

Note that the phases after the application of the second state-change
follow from:

\begin{equation}
% \label{eq:pauli-commute-part}
-(a - c d^{\minu 1})(\minu d^{\minu 1})^{\minu 1},
\,  \minu(\minu d^{\minu 1})^{\minu 1}
= -(a - c d^{\minu 1}) (\minu d), \,  d
= ad - c, \, d
\end{equation}

We can prove the second equation of the lemma using Hadamard-boxes as

\begin{equation}
% \label{eq:pauli-commute-compl-pf}
\tikzfig{figures/completeness/extended-copy-compl-proof}
\end{equation}

For any \(x,y \in \K^n\) and \(X \in \Sym[m]\),

\begin{equation*}
\tikzfig{figures/completeness/scalable/affine_symplectomorphisms}
\end{equation*}

We prove the claim by induction on the thickness of scalable spiders.  The base case is trivial.  For the inductive step:

\begin{equation}
\tikzfig{figures/completeness/scalable/affine_symplectomorphisms_proof}
\end{equation}

We can perform row operations on the matrix \(E\) of a
in AP-form without changing the semantics.  However, applying these row operations can change the affine phases
\(\vec{x}\) of the internal spiders:

Given a diagram in AP-form and an invertible matrix \(A \in
\Matrices[m][m][\K]\),

\[
\tikzfig{figures/AffLagRel/scalable/AP-form_GaussianElimination}
\]

\begin{equation}
\tikzfig{figures/completeness/scalable/AP-form_GaussianElimination_proof}
\end{equation}

Consider a diagram in AP-form described by the quadruplet
\((E,Y,\vec{x},\vec{y})\). Then, by lemma <ref>
we can act on \(E\) on the left by by an invertible matrix \(A\). Thus,
we can run a Gaussian elimination on \(E\). During this procedure,
if at any point the resulting matrix \(AE\) has a zero row,
this means that one of the internal vertices has no neighbours in
the graph. This disconnected internal vertex then takes the form
figures/completeness/scalable/AP-form_reduction_scalar. If
\(x \neq 0\)  then the diagram has empty semantics and we can use
lemma <ref> to rewrite the diagram to normal
form. Otherwise, \(x=0\) and we can eliminate the disconnected vertex
using .

The resulting row reduced echelon form of \(E\), with zero rows removed,
is of the form \(\begin{bmatrix} 1_m & F \end{bmatrix}\), up to a permutation
of its columns. Denoting this permutation by \(\varsigma\), we have

\begin{equation}
\tikzfig{figures/completeness/scalable/AP-form_reduction_proof_1}
\end{equation}

for matrices \(A,B,C,F\) and vectors \(\vec{a},\vec{b}\) of suitable
dimensions. Let's ignore the permutation for now, then following
equation <ref> we have

\begin{equation}
\tikzfig{figures/completeness/scalable/AP-form_reduction_proof_2}
\end{equation}

where we have set \(\vec{s} \coloneqq F^\mathsf{T}\vec{a} +
\vec{b} -  (A+B) \vec{x}\) and \(S \coloneqq F^\mathsf{T}AF + B -
BF - F^\mathsf{T}B^\mathsf{T}\).  Reintroducing the permutation,
we see that this final diagram is exactly the form described in
remark <ref>, which is easily seen to verify the
conditions of definition <ref>. The diagram is therefore
in reduced AP-form.

The thick scalable version of lemma <ref> holds:

\begin{equation*}
\tikzfig{figures/completeness/scalable/pauli_state_push}
\end{equation*}

The proof is essentially the same as that of lemma <ref>

Up to permutation the proof of proposition <ref>, entails that the the AP-form can be rewritten to:

\begin{equation}
\tikzfig{figures/completeness/scalable/reduced_ap_form_uniqueness_1}
\end{equation}