Function Repository Resource:

AbstractStrictMonoidalCategory

Make an abstract model of a category equipped with a strictly associative and unital tensor product structure

Contributed by: Jonathan Gorard

ResourceFunction["AbstractStrictMonoidalCategory"][cat,map_ob,map_arr,tens,unit,eq_ob,eq_mor]

makes an abstract strict monoidal category based on the underlying abstract category cat, using the association of mappings between objects map_ob, the association of mappings between arrows map_arr, the tensor product symbol tens, the distinguished unit object unit, the list of new object equivalences eq_ob and the list of new morphism equivalences eq_mor.

ResourceFunction["AbstractStrictMonoidalCategory"][assoc]

makes an abstract strict monoidal category using the association of underlying abstract category, object mappings, arrow mappings, tensor product symbol, distinguished unit object, new object equivalences and new morphism equivalences assoc.

ResourceFunction["AbstractStrictMonoidalCategory"][ResourceFunction["AbstractStrictMonoidalCategory"][…],tens,unit,eq_ob,eq_mor]

makes a new abstract strict monoidal category from an old monoidal category by imposing new tensor product symbol tens, new distinguished unit object unit, new object equivalences eq_ob and new morphism equivalences eq_mor.

Details and Options

A monoidal category is a category that is equipped with a tensor product structure on its objects and morphisms, conventionally formalized as a bifunctor (i.e. a functor whose domain is a product category) that maps pairs of objects to objects and pairs of morphisms to morphisms, in such a way that this tensor product structure is both associative and unital on objects (i.e. there exists a distinguished object that acts as both a left and right identity for the tensor product structure). A generic category will often permit many different possible tensor product structures, and thus there are often many different monoidal categories that are consistent with a given underlying "base" category.

In a general monoidal category, the tensor product structure need only be associative and unital up to natural isomorphisms (with components known as the associator isomorphisms and left/right unitor isomorphisms, respectively). Strict monoidal categories correspond to a special case of general monoidal categories in which the associator isomorphisms and left/right unitor isomorphisms are all identities, and hence in which the tensor product structure is associative and unital up to strict equality of objects (and morphisms). Despite apparently constituting a special case, Mac Lane's coherence theorem for monoidal categories implies that every general monoidal category is monoidally equivalent to a corresponding strict monoidal category (i.e. there exists a monoidal equivalence functor from one to the other) via a procedure known as "strictification".

Monoidal categories capture many familiar constructions from mathematics such as Cartesian products of sets (in the monoidal category of sets), tensor products of vector spaces/modules/algebras (in the monoidal categories of vector spaces over a field, modules over a commutative ring and algebras over a commutative ring, respectively), smash products of pointed topological spaces (in the category of pointed spaces), etc., and generalize them to a much larger class of categories.

Moreover, monoidal categories appear in many of the standard applications of category theory to areas such as logic, theoretical computer science, condensed matter physics, quantum information theory and quantum field theory. For instance, Girard's linear logic can be formalized as a logic internal to any non-Cartesian symmetric closed monoidal category, Petri nets in theoretical computer science can be thought of as being computational descriptions of monoidal categories (with collections of tokens forming objects and their transitions forming morphisms), 2+1-dimensional bosonic and fermionic topological orders in condensed matter physics can be classified using monoidal categories (usually using fusion categories that are enriched over the category of vector spaces), arbitrary quantum computations in categorical quantum mechanics can be formalized in terms of compact-closed symmetric monoidal categories equipped with an involutive "dagger" structure, and functorial quantum field theories (including both topological and conformal field theories) can be formalized as symmetric monoidal functors from a monoidal category of cobordisms to a monoidal category of vector spaces, etc.

The tensor product structure of morphisms in a monoidal category can be represented using directed graphs known as "string diagrams", in which the directed edges (known as "wires" or "strings") represent the objects, the vertices (known as "boxes" or "spiders") represent the morphisms, wiring boxes together corresponds to composing the corresponding morphisms and stacking strings/boxes next to each other corresponds to taking tensor products of the corresponding objects/morphisms. String diagrams are thus dual (via Poincaré duality) to ordinary category-theoretic diagrams. String diagrams represent an abstract generalization of Penrose's graphical notation for tensor networks, Cvitanovic's birdtrack notation in algebra, circuit diagrams/ZX-diagrams for quantum circuits in categorical quantum information theory, Feynman diagrams for scattering amplitudes in functorial quantum field theories and proof nets for proofs in intuitionistic linear logic.

An abstract presentation of a strict monoidal category can therefore be given in terms of an underlying abstract category (the "base" category), collections of mappings between objects and arrows in the underlying abstract quiver, a tensor product symbol, a distinguished unit object, and collections of new relations between objects and morphisms (effectively specifying which objects and morphisms in the codomain category of the abstract bifunctor may be treated as equivalent).

ResourceFunction["AbstractStrictMonoidalCategory"] supports the specification of abstract strict monoidal categories either by an underlying abstract category together with six lists/associations/symbols (an association of mappings between objects map_ob, an association of mappings between arrows map_arr, a tensor product symbol tens, a distinguished unit object unit, a list of new object equivalences eq_ob and a list of new morphism equivalences eq_mor) or by an explicit association of the form <|"Category"→cat,"ObjectMappings"→map_ob,"ArrowMappings"→map_arr,"TensorProductSymbol"→tens,"UnitObject"→unit,"ObjectEquivalences"→eq_ob,"MorphismEquivalences"→eq_mor|>.

An abstract category object can be generated using the resource function AbstractCategory.

Where specified, the tensor product symbol tens should be a binary operator.

When specifying an abstract strict monoidal category by a collection of lists/associations/symbols, ResourceFunction["AbstractStrictMonoidalCategory"] allows one to omit either the association of object mappings, the association of arrow mappings, the tensor product symbol, the distinguished unit object, the list of new object equivalences or the list of new morphism equivalences (or some combination of the above). When the object mappings association is omitted, every object in the domain category of the abstract bifunctor is assumed to map to itself; likewise, when the arrow mappings association is omitted, every arrow in the underlying quiver of the domain category of the abstract bifunctor is assumed to map to itself. When the tensor product symbol is omitted, CircleTimes (⊗) is assumed by default. When the distinguished unit object is omitted, it is assumed to be the canonically first object in the list of objects in the underlying abstract quiver. When lists of either new object equivalences or new morphism equivalences are omitted, they are assumed to be empty (i.e. no additional equivalences are imposed between objects/morphisms in the codomain category).

Note that, just as with AbstractFunctor, ResourceFunction["AbstractStrictMonoidalCategory"] specifies mappings at the level of arrows in the underlying quiver, rather than mappings between the morphisms of the categories themselves; this is because the specification of mappings between the underlying arrows is sufficient to determine the bifunctor fully, since all other mappings between morphisms can subsequently be deduced from the properties of composition and identity in the underlying category (which are necessarily preserved by virtue of functoriality).

By default, all object and morphism equivalences in the underlying "base" category will be incorporated as part of the abstract bifunctor (i.e. equivalences between objects and morphisms in the "base" category will be mapped to equivalences between corresponding objects and morphisms in the product/domain category, as well as to the images of those objects and morphisms in the codomain category under the abstract bifunctor).

Any equivalences between objects and morphisms that follow directly from the strict associativity and strict left/right unitality of the tensor product structure are automatically added to the lists of object and morphism equivalences imposed by ResourceFunction["AbstractStrictMonoidalCategory"].

Note that a strict monoidal category is only "valid" if the codomain of the abstract bifunctor is equal to the underlying "base" category (after all object and morphism equivalences have been imposed). ResourceFunction["AbstractStrictMonoidalCategory"] allows one to check automatically whether or not this is the case.

If the function succeeds in constructing the specified abstract strict monoidal category, it will return an ResourceFunction["AbstractStrictMonoidalCategory"] expression.

In ResourceFunction["AbstractStrictMonoidalCategory"], the following properties are supported:

"ObjectCount"

number of objects in the domain category vs. the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category

"MorphismCount"

number of morphisms in the domain category vs. the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category

"ObjectEquivalences"

list of equivalences between objects in the codomain category imposed by the abstract bifunctor characterizing the abstract strict monoidal category

"ObjectEquivalenceCount"

number of equivalences between objects in the codomain category imposed by the abstract bifunctor characterizing the abstract strict monoidal category

"MorphismEquivalences"

list of equivalences between morphisms in the codomain category imposed by the abstract bifunctor characterizing the abstract strict monoidal category

"MorphismEquivalenceCount"

number of equivalences between morphisms in the codomain category imposed by the abstract bifunctor characterizing the abstract strict monoidal category

"ReducedObjectCount"

number of objects in the domain category vs. the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category modulo all object equivalences

"ReducedMorphismCount"

number of morphisms in the domain category vs. the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category modulo all morphism/object equivalences

"TensorProductSymbol"

symbol used to denote the tensor product of objects/morphisms in the abstract strict monoidal category

"UnitObject"

designated object that acts as a unit/identity for the tensor product structure in the abstract strict monoidal category

"Category"

underlying "base" abstract category of the abstract strict monoidal category

"DualStrictMonoidalCategory"

dual/opposite strict monoidal category (i.e. the abstract strict monoidal category obtained by swapping the source and target objects of all the morphisms and reversing the direction of morphism composition)

"ObjectMappings"

association of mappings between objects in the domain category and corresponding objects in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category

"ObjectMappingCount"

number of mappings between objects in the domain category and corresponding objects in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category

"ReducedObjectMappings"

association of mappings between objects in the domain category and corresponding objects in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category, modulo all object equivalences

"ReducedObjectMappingCount"

number of mappings between objects in the domain category and corresponding objects in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category, modulo all object equivalences

"ArrowMappings"

association of mappings between arrows in the underlying quiver of the domain category and corresponding arrows in the underlying quiver of the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category

"ArrowMappingCount"

number of mappings between arrows in the underlying quiver of the domain category and corresponding arrows in the underlying quiver of the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category

"MorphismMappings"

association of mappings between morphisms in the domain category and corresponding morphisms in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category

"MorphismMappingCount"

number of mappings between morphisms in the domain category and corresponding morphisms in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category

"ReducedMorphismMappings"

association of mappings between morphisms in the domain category and corresponding morphisms in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category, modulo all morphism/object equivalences

"ReducedMorphismMappingCount"

number of mappings between morphisms in the domain category and corresponding morphisms in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category, modulo all morphism/object equivalences

"ValidStrictMonoidalCategoryQ"

whether the abstract strict monoidal category is "valid" (i.e. whether the codomain of the abstract bifunctor characterizing the abstract strict monoidal category matches the underlying "base" abstract category)

"FullLabeledStringDiagrams"

association mapping morphisms in the abstract strict monoidal category to their corresponding representations as monoidal string diagrams, with labels on the wires and boxes

"FullUnlabeledStringDiagrams"

association mapping morphisms in the abstract strict monoidal category to their corresponding representations as monoidal string diagrams, with no labels on the wires and boxes

"ReducedLabeledStringDiagrams"

association mapping morphisms in the abstract strict monoidal category to their corresponding representations as monoidal string diagrams, modulo the lists of morphism/object equivalences, with labels on the wires and boxes

"ReducedUnlabeledStringDiagrams"

association mapping morphisms in the abstract strict monoidal category to their correpsonding representations as monoidal string diagrams, modulo the lists of morphism/object equivalences, with no labels on the wires and boxes

"AssociatorEquations"

list of associator equations (i.e. equations characterizing the strict associativity of the tensor product structure) for the abstract strict monoidal category

"ReducedAssociatorEquations"

list of associator equations (i.e. equations characterizing the strict associativity of the tensor product structure) for the abstract strict monoidal category, modulo the lists of morphism/object equivalences

"LeftUnitorEquations"

list of left unitor equations (i.e. equations characterizing the fact that the distinguished unit object acts as a strict left identity for the tensor product structure) for the abstract strict monoidal category

"ReducedLeftUnitorEquations"

"RightUnitorEquations"

list of right unitor equations (i.e. equations characterizing the fact that the distinguished unit object acts as a strict right identity for the tensor product structure) for the abstract strict monoidal category

"ReducedRightUnitorEquations"

"CommutativeDiagramQ"

whether the abstract strict monoidal category forms a commutative diagram (i.e. all directed paths with the same source and target object yield the same result)

"CommutativityEquations"

list of equations required to force the abstract strict monoidal category to be a commutative diagram

"ReducedCommutativityEquations"

list of equations required to force the abstract strict monoidal category to be a commutative diagram, modulo the lists of morphism/object equivalences

"StrictSymmetricMonoidalCategoryQ"

whether the abstract strict monoidal category is strictly symmetric (i.e. the tensor product is strictly commutative)

"SymmetryEquations"

list of equations required to force the abstract strict monoidal category to be strictly symmetric

"ReducedSymmetryEquations"

list of equations required to force the abstract strict monoidal category to be strictly symmteric, modulo the lists of morphism/object equivalences

"FullLabeledGraph"

abstract bifunctor characterizing the abstract strict monoidal category, represented as a map between directed graphs with labels on the morphisms

"FullUnlabeledGraph"

abstract bifunctor characterizing the abstract strict monoidal category, represented as a map between directed graphs with no labels on the morphisms

"ReducedLabeledGraph"

abstract bifunctor characterizing the abstract strict monoidal category, represented as a map between directed graphs, modulo the lists of morphism/object equivalences, with labels on the morphisms

"ReducedUnlabeledGraph"

abstract bifunctor characterizing the abstract strict monoidal category, represented as a map between directed graphs, modulo the lists of morphism/object equivalences, with no labels on the morphisms

"SimpleLabeledGraph"

abstract bifunctor characterizing the abstract strict monoidal category, represented as a map between directed graphs, with self-loops and multiedges removed, with labels on the morphisms

"SimpleUnlabeledGraph"

abstract bifunctor characterizing the abstract strict monoidal category, represented as a map between directed graphs, with self-loops and multiedges removed, with no labels on the morphisms

"ReducedSimpleLabeledGraph"

abstract bifunctor characterizing the abstract strict monoidal category, represented as a map between directed graphs, with self-loops and multiedges removed, modulo the lists of morphism/object equivalences, with labels on the morphisms

"ReducedSimpleUnlabeledGraph"

"AssociationForm"

abstract strict monoidal category represented as an association of underlying "base" abstract category, object mappings, arrow mappings, tensor product symbol, distinguished unit object, new object equivalences and new morphism equivalences

"Properties"

list of properties

Examples

Basic Examples (3)

Construct a simple abstract strict monoidal category from a trivial abstract category generated by a single arrow (with X being the distinguished unit object by default):

In[1]:=

Out[1]=

In[2]:=

Out[2]=

In[3]:=

Out[3]=

Show the full directed graph representation of the abstract bifunctor, with labels on the morphisms:

In[4]:=

Out[4]=

Show the full directed graphs without labels on the morphisms:

In[5]:=

Out[5]=

Show the list of associator equations (i.e. the equations characterizing the strict associativity of the tensor product structure):

In[6]:=

Out[6]=

Show the list of left and right unitor equations (i.e. the equations characterizing the fact that the distinguished unit object, namely X, acts as both a strict left identity and a strict right identity for the tensor product structure):

In[7]:=

Out[7]=

In[8]:=

Out[8]=

Show the reduced directed graph representation the abstract bifunctor, with all equivalences between objects and morphisms imposed and with labels on the morphisms:

In[9]:=

Out[9]=

Show the reduced directed graphs without labels on the morphisms:

In[10]:=

Out[10]=

Construct a new abstract strict monoidal category, but now with a pair of associations designating object/arrow mappings, and with tensor product symbol ⊕ and distinguished unit object Y:

In[11]:=

Out[11]=

In[12]:=

Out[12]=

Show that the resulting diagram is not commutative:

In[13]:=

Out[13]=

Compute the list of equations between morphisms that must hold for the diagram to be commutative (after all equivalences between objects and morphisms are imposed):

In[14]:=

Out[14]=

Construct a new abstract strict monoidal category with these new equations between morphisms imposed (and no corresponding equations between objects enforced):

In[15]:=

Out[15]=

In[16]:=

Out[16]=

Show that the resulting diagram is now commutative:

In[17]:=

Out[17]=

Show that the abstract strict monoidal category is not yet "valid" (i.e. the codomain of the abstract bifunctor does not yet match the underlying "base" category):

In[18]:=

Out[18]=

Construct a new abstract strict monoidal category with an additional equivalence between morphisms imposed in order to force validity:

In[19]:=

Out[19]=

In[20]:=

Out[20]=

Show that the abstract strict monoidal category is now valid:

In[21]:=

Out[21]=

Construct an abstract strict monoidal category from a simple abstract category in which object Y⊗Y is mapped to Y and object Z⊗Z is mapped to Z (with X being the distinguished unit object by default):

In[22]:=

Out[22]=

In[23]:=

Out[23]=

In[24]:=

Out[24]=

In[25]:=

Out[25]=

Show the association of monoidal string diagrams representing the (currently trivial) tensor product structure of each morphism, with labels on the wires and boxes:

In[26]:=

Out[26]=

Show the association of monoidal string diagrams without labels on the wires and boxes:

In[27]:=

Out[27]=

Construct a new abstract strict monoidal category in which morphism f⊗f is mapped to F, morphism g⊗g is mapped to G, etc.:

In[28]:=

monoidalCategory2 = ResourceFunction["AbstractStrictMonoidalCategory"][
category, <|CircleTimes[Y, Y] -> Y, CircleTimes[Z, Z] -> Z|>, <|
CircleTimes[f, f] -> F, CircleTimes[g, g] -> G, CircleTimes[f, OverTilde[X]] -> fX, CircleTimes[OverTilde[Y], g] -> Yg|>]

Out[28]=

In[29]:=

Out[29]=

Show the association of monoidal string diagrams representing the (now non-trivial) tensor product structure of each morphism, with labels on the wires and boxes:

In[30]:=

Out[30]=

Show the association of monoidal string diagrams without labels on the wires and boxes:

In[31]:=

Out[31]=

Show the association of object mappings:

In[32]:=

Out[32]=

Show the association of object mappings, with all equivalences between objects imposed:

In[33]:=

Out[33]=

Show the association of morphism mappings, with all equivalences between objects/morphisms imposed:

In[34]:=

Out[34]=

Compute the list of equations between morphisms that must hold for the diagram to be commutative (after all equivalences between objects and morphisms are imposed):

In[35]:=

Out[35]=

Construct a new abstract strict monoidal category in which, in addition to the object mappings above, objects (Z⊗Y)⊗Y and (Y⊗Z)⊗Z are both mapped to Z (with no corresponding morphism mappings):

In[36]:=

monoidalCategory3 = ResourceFunction["AbstractStrictMonoidalCategory"][
category, <|CircleTimes[Y, Y] -> Y, CircleTimes[Z, Z] -> Z, CircleTimes[CircleTimes[Z, Y], Y] -> Z, CircleTimes[CircleTimes[Y, Z], Z] -> Z|>, <||>]

Out[36]=

In[37]:=

Out[37]=

Compute the list of equations between morphisms that must hold for the diagram to be commutative (after all equivalences between objects and morphisms are imposed):

In[38]:=

Out[38]=

Construct a new abstract strict monoidal category with these new equations between morphisms imposed (and no corresponding equations between objects enforced), plus three additional equivalences required to force validity:

In[39]:=

monoidalCategory4 = ResourceFunction["AbstractStrictMonoidalCategory"][
category, <|CircleTimes[Y, Y] -> Y, CircleTimes[Z, Z] -> Z, CircleTimes[CircleTimes[Z, Y], Y] -> Z, CircleTimes[CircleTimes[Y, Z], Z] -> Z|>, <||>, {}, Join[equations, {CircleTimes[OverTilde[X], f] == f, CircleTimes[OverTilde[Y], CircleDot[g, f]] == g, CircleTimes[OverTilde[X], CircleDot[g, f]] == CircleDot[g, f]}]]

Out[39]=

In[40]:=

Out[40]=

Show that the resulting diagram is now commutative:

In[41]:=

Out[41]=

Show that the abstract strict monoidal category is now valid:

In[42]:=

Out[42]=

Show the association of monoidal string diagrams representing the tensor product structure of each morphism, with all equivalences between objects and morphisms imposed and with labels on the wires and boxes:

In[43]:=

Out[43]=

In[44]:=

Out[44]=

Construct an abstract strict monoidal category from a simple abstract category with equivalences between objects and morphisms, and show that these equivalences are subsequently inherited by the strict monoidal category by default:

In[45]:=

Out[45]=

In[46]:=

Out[46]=

In[47]:=

Out[47]=

In[48]:=

Out[48]=

Show the list of equivalences between objects:

In[49]:=

Out[49]=

Show the list of equivalences between morphisms:

In[50]:=

Out[50]=

Show the list of associator equations (i.e. the equations characterizing the strict associativity of the tensor product structure) after all equivalences between objects and morphisms are imposed:

In[51]:=

Out[51]=

In[52]:=

Out[52]=

In[53]:=

Out[53]=

Show the association of object mappings, with all equivalences between objects imposed:

In[54]:=

Out[54]=

Show the association of morphism mappings, with all equivalences between objects imposed:

In[55]:=

Out[55]=

Show the association of monoidal string diagrams representing the (non-trivial) tensor product structure of each morphism, with all equivalences between objects and morphisms imposed and with labels on the wires and boxes:

In[56]:=

Out[56]=

In[57]:=

Out[57]=

Show that the abstract strict monoidal category is (strictly) symmetric:

In[58]:=

Out[58]=

Show the list of equations between objects that must hold for the abstract strict monoidal category to be strictly symmetric:

In[59]:=

Out[59]=

Show the list of equations between objects that must hold for the abstract strict monoidal category to be strictly symmetric, with all equivalences between objects imposed:

In[60]:=

Out[60]=

Scope (2)

If AbstractStrictMonoidalCategory is given only an abstract category object, then its default behaviour is to construct an identity bifunctor on that category as the tensor product structure:

In[61]:=

Out[61]=

In[62]:=

Out[62]=

In[63]:=

Out[63]=

In[64]:=

Out[64]=

Additional arguments can be used to specify object and arrow mappings:

In[65]:=

monoidalCategory2 = ResourceFunction["AbstractStrictMonoidalCategory"][
category, <|CircleTimes[Y, Z] -> Y, CircleTimes[Z, Y] -> Z|>, <|
CircleTimes[f, g] -> f, CircleTimes[g, f] -> g|>]

Out[65]=

In[66]:=

Out[66]=

In[67]:=

Out[67]=

Further arguments can be used to specify the tensor product symbol and the distinguished unit object:

In[68]:=

monoidalCategory3 = ResourceFunction["AbstractStrictMonoidalCategory"][
category, <|CirclePlus[Y, X] -> Y, CirclePlus[X, Y] -> X|>, <|
CirclePlus[f, g] -> f, CirclePlus[g, f] -> g|>, CirclePlus, Z]

Out[68]=

In[69]:=

Out[69]=

In[70]:=

Out[70]=

In[71]:=

Out[71]=

Further arguments can finally be used to specify new equivalences between objects and morphisms in the codomain category of the abstract bifunctor characterizing the strict monoidal category:

In[72]:=

monoidalCategory4 = ResourceFunction["AbstractStrictMonoidalCategory"][
category, <|CirclePlus[Y, X] -> Y, CirclePlus[X, Y] -> X|>, <|
CirclePlus[f, g] -> f, CirclePlus[g, f] -> g|>, CirclePlus, Z, {CirclePlus[CirclePlus[X, X], Y] == Y}, {CirclePlus[g, OverTilde[Y]] == CirclePlus[OverTilde[Y], g]}]

Out[72]=

In[73]:=

Out[73]=

In[74]:=

Out[74]=

If the tensor product symbol is omitted, it is assumed to be ⊗ by default. If the distinguished unit object is omitted, it is assumed to be the canonically first object in the list of objects in the underlying abstract category by default:

In[75]:=

monoidalCategory5 = ResourceFunction["AbstractStrictMonoidalCategory"][
category, <|CircleTimes[Y, Z] -> Y, CircleTimes[Z, Y] -> Z|>, <|
CircleTimes[f, g] -> f, CirclePlus[g, f] -> g|>, {CircleTimes[CircleTimes[Z, Z], Y] == Y}, {CircleTimes[g, OverTilde[Y]] == CircleTimes[OverTilde[Y], g]}]

Out[75]=

In[76]:=

Out[76]=

New tensor product symbols and distinguished unit objects can be specified for any existing abstract strict monoidal category:

In[77]:=

Out[77]=

In[78]:=

Out[78]=

Likewise for new object and morphism equivalences:

In[79]:=

monoidalCategory7 = ResourceFunction["AbstractStrictMonoidalCategory"][
monoidalCategory5, {CircleTimes[CircleTimes[Z, Z], Y] == Y, CircleTimes[CircleTimes[Y, Y], Z] == Y}, {CircleTimes[g, OverTilde[Y]] == CircleTimes[OverTilde[Y], g],
CircleTimes[CircleDot[g, f], f] == CircleTimes[CircleDot[g, f], OverTilde[X]]}]

Out[79]=

In[80]:=

Out[80]=

All four properties (new tensor product symbol, new distinguished unit object, new object equivalences and new morphism equivalences) may be specified simultaneously:

In[81]:=

monoidalCategory8 = ResourceFunction["AbstractStrictMonoidalCategory"][monoidalCategory5,
CirclePlus, Z, {CirclePlus[X, X] == X, CirclePlus[Y, Y] == Y}, {CirclePlus[CircleDot[g, f], CircleDot[g, f]] == CirclePlus[CircleDot[g, f], OverTilde[Z]]}]

Out[81]=

In[82]:=

Out[82]=

In[83]:=

Out[83]=

From an explicit association:

In[84]:=

monoidalCategory9 = ResourceFunction[
"AbstractStrictMonoidalCategory"][<|"Category" -> category, "ObjectMappings" -> <|CirclePlus[Y, Z] -> Y, CirclePlus[Z, Y] -> Z|>,
"ArrowMappings" -> <|CirclePlus[f, g] -> f, CirclePlus[g, f] -> g|>,
"TensorProductSymbol" -> CirclePlus, "UnitObject" -> Z, "ObjectEquivalences" -> {CirclePlus[X, X] == X, CirclePlus[Y, Y] == Y}, "MorphismEquivalences" -> {CirclePlus[CircleDot[g, f], CircleDot[g, f]] == CirclePlus[CircleDot[g, f], OverTilde[Z]]}|>]

Out[84]=

In[85]:=

Out[85]=

Construct an abstract strict monoidal category from an abstract category and associations of object/arrow mappings, a tensor product symbol, a designated unit object and lists of new object/morphism equivalences:

In[86]:=

Out[86]=

In[87]:=

monoidalCategory = ResourceFunction["AbstractStrictMonoidalCategory"][
category, <|CirclePlus[W, W] -> W, CirclePlus[W, X] -> Y|>, <|
CirclePlus[f, f] -> f|>, CirclePlus, Z, {CirclePlus[W, X] == W, Y == CirclePlus[X, X], CirclePlus[CirclePlus[X, W], W] == W}, {CirclePlus[f, f] == f}]

Out[87]=

Show the list of properties:

In[88]:=

Out[88]=

Show the number of objects in the domain category vs. the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[89]:=

Out[89]=

Show the number of morphisms in the domain category vs. the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[90]:=

Out[90]=

Show the list of equivalences between objects in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[91]:=

Out[91]=

Show the number of equivalences between objects in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[92]:=

Out[92]=

Show the list of equivalences between morphisms in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[93]:=

Out[93]=

Show the number of equivalences between morphisms in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[94]:=

Out[94]=

Show the number of reduced objects (modded out by all object equivalences) in the domain category vs. the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[95]:=

Out[95]=

Show the number of reduced morphisms (modded out by all object and morphism equivalences) in the domain category vs. the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[96]:=

Out[96]=

Show the (binary) symbol used to denote the tensor product structure in the abstract strict monoidal category:

In[97]:=

Out[97]=

Show the distinguished unit object in the abstract strict monoidal category:

In[98]:=

Out[98]=

Show the underlying "base" abstract category of the abstract strict monoidal category:

In[99]:=

Out[99]=

Compute the dual (obtained by swapping the source and target objects of each morphism and reversing the direction of morphism composition) of the abstract strict monoidal category:

In[100]:=

Out[100]=

Show the association of mappings between objects in the domain category and corresponding objects in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[101]:=

Out[101]=

Show the number of mappings between objects in the domain category and corresponding objects in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[102]:=

Out[102]=

Show the reduced association of mappings (modded out by all object equivalences) between objects in the domain category and corresponding objects in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[103]:=

Out[103]=

Show the number of reduced mappings (modded out by all object equivalences) between objects in the domain category and corresponding objects in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[104]:=

Out[104]=

Show the association of mappings between arrows in the underlying quiver of the domain category and corresponding arrows in the underlying quiver of the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[105]:=

Out[105]=

Show the number of mappings between arrows in the underlying quiver of the domain category and corresponding arrows in the underlying quiver of the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[106]:=

Out[106]=

Show the association of mappings between morphisms in the domain category and corresponding morphisms in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[107]:=

Out[107]=

Show the number of mappings between morphisms in the domain category and corresponding morphisms in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[108]:=

Out[108]=

Show the reduced association of mappings (modded out by all object and morphism equivalences) between morphisms in the domain category and corresponding morphisms in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[109]:=

Out[109]=

Show the number of reduced mappings (modded out by all object and morphism equivalences) between morphisms in the domain category and corresponding morphisms in the codomain category of the abstract bifunctor characterizing the abstract strict monoidal category:

In[110]:=

Out[110]=

Determine whether the abstract strict monoidal category is "valid" (i.e. the codomain of the abstract bifunctor characterizing the abstract strict monoidal category matches the underlying "base"abstract category):

In[111]:=

Out[111]=

Compute the association mapping morphisms in the abstract strict monoidal category to their corresponding monoidal string diagram representations, with labels on the wires and boxes:

In[112]:=

Out[112]=

Compute the association mapping morphisms in the abstract strict monoidal category to their corresponding monoidal string diagram representations, without labels on the wires and boxes:

In[113]:=

Out[113]=

Compute the association mapping morphisms in the abstract strict monoidal category to their corresponding monoidal string diagram representations, with all equivalences between objects and morphisms imposed and with labels on the wires and boxes:

In[114]:=

Out[114]=

In[115]:=

Out[115]=

Show the list of equations between objects in the abstract strict monoidal category implicitly imposed by the constraint that the tensor product structure must be strictly associative:

In[116]:=

Out[116]=

Show the list of equations between objects in the abstract strict monoidal category implicitly imposed by the constraint that the tensor product structure must be strictly associative, modulo all object and morphism equivalences:

In[117]:=

Out[117]=

Show the list of equations between objects in the abstract strict monoidal category implicitly imposed by the constraint that the distinguished unit object must act as a strict left identity for the tensor product structure:

In[118]:=

Out[118]=

In[119]:=

Out[119]=

Show the list of equations between objects in the abstract strict monoidal category implicitly imposed by the constraint that the distinguished unit object must act as a strict right identity for the tensor product structure:

In[120]:=

Out[120]=

In[121]:=

Out[121]=

Determine whether the abstract strict monoidal category is a commutative diagram (i.e. all directed paths through the graph with the same source and target object yield the same morphism):

In[122]:=

Out[122]=

Show the list of equations between morphisms required to force the abstract strict monoidal category to be a commutative diagram:

In[123]:=

Out[123]=

Show the list of equations between morphisms required to force the abstract strict monoidal category to be a commutative diagram, modulo all equivalences between objects and morphisms:

In[124]:=

Out[124]=

Determine whether the abstract strict monoidal category is strictly symmetric (i.e. the tensor product structure is strictly commutative):

In[125]:=

Out[125]=

Show the list of equations between objects required to force the abstract strict monoidal category to be strictly symmetric:

In[126]:=

Out[126]=

Show the list of equations between objects required to force the abstract strict monoidal category to be strictly symmetric, modulo all equivalences between objects and morphisms:

In[127]:=

Out[127]=

Show the abstract bifunctor characterizing the abstract strict monoidal category, represented as a map between full directed graphs with labels on the morphisms:

In[128]:=

Out[128]=

Show the abstract bifunctor characterizing the abstract strict monoidal category, represented as a map between full directed graphs without labels on the morphisms:

In[129]:=

Out[129]=

Show the abstract bifunctor characterizing the abstract strict monoidal category, represented as a map between reduced directed graphs, with all equivalences between objects and morphisms imposed and with labels on the morphisms:

In[130]:=

Out[130]=

In[131]:=

Out[131]=

Show the abstract bifunctor characterizing the abstract strict monoidal category, represented as a map between simple directed graphs, with all self-loops and multiedges removed and with labels on the morphisms:

In[132]:=

Out[132]=

In[133]:=

Out[133]=

Show the abstract bifunctor characterizing the abstract strict monoidal category, represented as a map between reduced simple directed graphs, with all self-loops and multiedges removed, plus all object and morphism equivalences modded out and with labels on the morphisms:

In[134]:=

Out[134]=

In[135]:=

Out[135]=

Show the explicit association form of the abstract strict monoidal category:

In[136]:=

Out[136]=

Publisher

Jonathan Gorard

Version History

1.0.0 – 06 June 2022

Source Metadata

Citation:
- Saunders Mac Lane (1971), Categories for the Working Mathematician
- Stephen Wolfram (2002), A New Kind of Science
- Stephen Wolfram (2020), "A Class of Models with Potential to Represent Fundamental Physics"
- Jonathan Gorard (2020), "Some Relativistic and Gravitational Properties of the Wolfram Model"
- Jonathan Gorard (2020), "Some Quantum Mechanical Properties of the Wolfram Model"

Related Resources

License Information

This work is licensed under a Creative Commons Attribution 4.0 International License

Wolfram Function Repository

AbstractStrictMonoidalCategory

Details and Options

Examples

Basic Examples (3)

Scope (2)

Publisher

Related Links

Version History

Source Metadata

Related Resources

License Information

AbstractStrictMonoidalCategory

Details and Options

Examples

Basic Examples (3)

Scope (2)

Publisher

Related Links

Version History

Source Metadata

Related Resources

Related Symbols

License Information