rigid

The free rigid category, i.e. diagrams with cups and caps.

Summary

Ob	A rigid object has adjoints Ob.l() and Ob.r().
Ty	A rigid type is a biclosed type with rigid objects inside.
PRO	A rigid PRO is a natural number n seen as a rigid type of length n.
Diagram	A rigid diagram is a biclosed diagram with Cup and Cap boxes.
Box	A rigid box is a biclosed box in a rigid diagram.
Cup	The counit of the adjunction for an atomic type.
Cap	The unit of the adjunction for an atomic type.
Sum	A rigid sum is a biclosed sum that can be transposed.
Functor	A rigid functor is a biclosed functor that preserves cups and caps.

Axioms

>>> unit, s, n = Ty(), Ty('s'), Ty('n')
>>> t = n.r @ s @ n.l
>>> assert t @ unit == t == unit @ t
>>> assert t.l.r == t == t.r.l
>>> left_snake, right_snake = Id(n.r).transpose(left=True), Id(n.l).transpose()
>>> assert left_snake.normal_form() == Id(n) == right_snake.normal_form()

>>> Equation(left_snake, Id(n), right_snake).draw(
...     figsize=(4, 1), path='docs/_static/rigid/typed-snake-equation.svg')

Objects may be coloured on both sides, i.e. an object F : a -> b is a wire separating a region a on its left from a region b on its right. Taking an adjoint reverses the direction of the wire, hence it swaps the two regions: G = F.r : b -> a. The unit and counit of the adjunction, i.e. eta = Cap(G, F) and epsilon = Cup(F, G), then satisfy the snake equations, one for F and one for G, for any colours a and b:

>>> from discopy.monoidal import Colour
>>> a = Colour('cornflowerblue', label='Function')
>>> b = Colour('palegreen', label='Morphism')
>>> F = Ty(Ob('F', dom=a, cod=b))
>>> G = F.r
>>> eta, epsilon = Cap(G, F), Cup(F, G)
>>> left_snake = Id(F) @ eta >> epsilon @ Id(F)
>>> right_snake = eta @ Id(G) >> Id(G) @ epsilon
>>> assert left_snake.normal_form() == Id(F)
>>> assert right_snake.normal_form() == Id(G)

>>> from discopy.monoidal import Equation
>>> Equation(left_snake, Id(F)).draw(
...     figsize=(3, 2), legend=True,
...     path='docs/_static/rigid/coloured-snake-equation.svg')
>>> Equation(right_snake, Id(G)).draw(
...     figsize=(3, 2), legend=True,
...     path='docs/_static/rigid/coloured-snake-equation-G.svg')

This is an instance of the free-forgetful adjunction between sets and monoids, with F the free monoid functor, sending a set of generators to the monoid of words over it, and G the forgetful functor, sending a monoid to its underlying set. The unit eta sends a generator to the length-one word on it, while the counit epsilon evaluates a word of elements of a monoid as their product:

>>> from functools import lru_cache
>>> from discopy.abc import ColouredMonoid
>>> from discopy.python.function import Function
>>> from discopy.cat import Ob as CatOb, Functor, Transformation

>>> class Z3(ColouredMonoid):
...     ''' The monoid of integers modulo three, with addition. '''
...     ob, dom, cod = type(None), None, None
...     def __init__(self, n):
...         self.n = n % 3
...     def __eq__(self, other):
...         return isinstance(other, Z3) and self.n == other.n
...     def __repr__(self):
...         return f"Z3({self.n})"
...     @classmethod
...     def id(cls, dom=None):
...         return cls(0)
...     def tensor(self, *others):
...         return Z3(self.n + sum(other.n for other in others))

>>> @lru_cache
... def Free(X):
...     ''' The free monoid on a set ``X``, i.e. words over ``X``. '''
...     class Word(ColouredMonoid):
...         ob, dom, cod = type(None), None, None
...         def __init__(self, xs=()):
...             self.xs = list(xs)
...         def __eq__(self, other):
...             return isinstance(other, Word) and self.xs == other.xs
...         def __repr__(self):
...             return f"Word({self.xs})"
...         @classmethod
...         def id(cls, dom=None):
...             return cls()
...         def tensor(self, *others):
...             return Word(self.xs + sum((other.xs for other in others), []))
...     return Word

>>> class Morphism(Function):
...     ''' A morphism of monoids; homomorphism not enforced. '''

The forgetful functor G does nothing to objects, it just views a monoid as a set, while the free functor F sends a set to its words. We spell out the two objects needed below as cat.Ob instances so that Transformation can validate the domains and codomains of its components:

>>> X_, M_ = CatOb('X'), CatOb('M')
>>> Id_set = Functor({X_: str, M_: Z3}, {}, cod=Function)
>>> GF = Functor({X_: Free(str), M_: Free(Z3)}, {}, cod=Function)
>>> Id_monoid = Functor({M_: Z3}, {}, cod=Morphism)
>>> FG = Functor({M_: Free(Z3)}, {}, cod=Morphism)

>>> eta = Transformation(
...     lambda obj: Function(
...         lambda x: Free(Id_set(obj)[0])([x]), Id_set(obj), GF(obj)),
...     Id_set, GF)
>>> epsilon = Transformation(
...     lambda obj: Morphism(
...         lambda w: Id_monoid(obj)[0].id().tensor(*w.xs),
...         FG(obj), Id_monoid(obj)),
...     FG, Id_monoid)

>>> X, M = str, Z3
>>> assert all(eta(X_)(x) == Free(X)([x]) for x in ('a', 'b'))
>>> assert epsilon(M_)(Free(M)([Z3(1), Z3(1), Z3(2)])) == Z3(1 + 1 + 2)
>>> assert all(epsilon(M_)(eta(M_)(x)) == x for x in (Z3(0), Z3(1), Z3(2)))