Olivier Laurent: Quantifiers added

2013-10-27T21:43:51Z

Quantifiers added

Olivier Laurent: First list

2013-04-25T19:48:16Z

First list

New page

== Linear negation ==

<math>
\begin{array}{rclcrcl}
A\biorth &\cong& A\\
(A\tens B)\orth &\cong& A\orth\parr B\orth &\quad& \one\orth &\cong& \bot\\
(A\parr B)\orth &\cong& A\orth\tens B\orth &\quad& \bot\orth &\cong& \one\\
(A\with B)\orth &\cong& A\orth\plus B\orth &\quad& \top\orth &\cong& \zero\\
(A\plus B)\orth &\cong& A\orth\with B\orth &\quad& \zero\orth &\cong& \top\\
(\oc A)\orth &\cong& \wn A\orth\\
(\wn A)\orth &\cong& \oc A\orth\\
\end{array}
</math>

== Neutrals ==

<math>
\begin{array}{rcl}
A\tens\one &\cong& \one\tens A\cong A\\
A\parr\bot &\cong& \bot\parr A\cong A\\
A\with\top &\cong& \top\with A\cong A\\
A\plus\zero &\cong&\zero\plus A\cong A\\
\end{array}
</math>

== Commutativity ==

<math>
\begin{array}{rcl}
A\tens B &\cong& B\tens A\\
A\parr B &\cong& B\parr A\\
A\with B &\cong& B\with A\\
A\plus B &\cong& B\plus A\\
\end{array}
</math>

== Associativity ==

<math>
\begin{array}{rcl}
(A\tens B)\tens C &\cong& A\tens(B\tens C)\\
(A\parr B)\parr C &\cong& A\parr(B\parr C)\\
(A\with B)\with C &\cong& A\with(B\with C)\\
(A\plus B)\plus C &\cong& A\plus(B\plus C)\\
\end{array}
</math>

== Multiplicative-additive distributivity ==

<math>
\begin{array}{rclcrcl}
A\tens(B\plus C) &\cong& (A\tens B)\plus(A\tens C) &\quad&
A\tens\zero &\cong& \zero\\
A\parr(B\with C) &\cong& (A\parr B)\with(A\parr C) &\quad&
A\parr\top &\cong& \top\\
\end{array}
</math>

== Linear implication ==

<math>
\begin{array}{rclcrcl}
A\limp B &\cong& A\orth\parr B\\
A\limp B &\cong& B\orth\limp A\orth\\
A\tens B \limp C &\cong& A\limp B \limp C\\
\end{array}
</math>

== The exponential isomorphisms ==

<math>
\begin{array}{rclcrcl}
\oc(A\with B) &\cong& \oc A\tens\oc B &\quad& \oc\top &\cong& \one\\
\wn(A\plus B) &\cong& \wn A\parr\wn B &\quad& \wn\zero &\cong& \bot\\
\end{array}
</math>

@@ Line 73: / Line 73: @@
   \oc(A\with B) &\cong& \oc A\tens\oc B &\quad& \oc\top &\cong& \one\\
   \wn(A\plus B) &\cong& \wn A\parr\wn B &\quad& \wn\zero &\cong& \bot\\
 \end{array}
 </math>

List of isomorphisms - Revision history

Olivier Laurent: Quantifiers added

Olivier Laurent: First list