Abrupt categories induced by categories with star-morphisms

In this blog post I introduced the notion of category with star-morphisms, a generalization of categories which have aroused in my research.

Each star category gives rise to a category (abrupt category, see a remark below why I call it “abrupt”), as described below. Below for simplicity I assume that the set $latex {M}&fg=000000$ and the set of our indexed families of functions are disjoint. The general case (when they are not necessarily disjoint) may be easily elaborated by the reader.

• Objects are indexed (by $latex {\mathrm{arity}m}&fg=000000$ for some $latex {m \in M}&fg=000000$) families of objects of the category $latex {C}&fg=000000$ and an (arbitrarily choosen) object $latex {\mathrm{None}}&fg=000000$ not in this set
• There are the following disjoint sets of morphims:
  1. indexed (by $latex {\mathrm{arity} m}&fg=000000$ for some $latex {m \in M}&fg=000000$) families of morphisms of $latex {C}&fg=000000$
  2. elements of $latex {M}&fg=000000$
  3. the identity morphism $latex {\mathrm{id}_{\mathrm{None}}}&fg=000000$ on $latex {\mathrm{None}}&fg=000000$
• Source and destination of morphims are defined by the formulas:
  • $latex {\mathrm{Src}f = \lambda i \in \mathrm{dom}f : \mathrm{Src}f_i}&fg=000000$
  • $latex {\mathrm{Dst}f = \lambda i \in \mathrm{dom}f : \mathrm{Dst}f_i}&fg=000000$
  • $latex {\mathrm{Src}m =\mathrm{None}}&fg=000000$
  • $latex {\mathrm{Dst}m =\mathrm{Obj}_m}&fg=000000$.
• Compositions of morphisms are defined by the formulas:
  • $latex {g \circ f = \lambda i \in \mathrm{dom}f : g_i \circ f_i}&fg=000000$
  • $latex {f \circ m =\mathrm{StarProd} \left( m ; f \right)}&fg=000000$
  • $latex {m \circ \mathrm{id}_{\mathrm{None}} = m}&fg=000000$
• Identity morphisms for an object $latex {X}&fg=000000$ are:
  • $latex {\lambda i \in X : \mathrm{id}_{X_i}}&fg=000000$ if $latex {X \neq \mathrm{None}}&fg=000000$
  • $latex {\mathrm{id}_{\mathrm{None}}}&fg=000000$ if $latex {X =\mathrm{None}}&fg=000000$

We need to prove it is really a category.

Proof We need to prove:

1. Composition is associative
2. Composition with identities complies with the identity law.

Really:

1. $latex {\left( h \circ g \right) \circ f = \lambda i \in \mathrm{dom} f : \left( h_i \circ g_i \right) \circ f_i = \lambda i \in \mathrm{dom} f : h_i \circ \left( g_i \circ f_i \right) = h \circ \left( g \circ f \right)}&fg=000000$; $latex g \circ \left( f \circ m \right) = \mathrm{StarComp} \left( \mathrm{StarComp} \left( m ; f \right) ; g \right) = \\
   \mathrm{StarComp} \left( m ; \lambda i \in \mathrm{arity} m : g_i \circ f_i \right) = \mathrm{StarComp} \left( m ; g \circ f \right) = \left( g \circ f \right) \circ m &fg=000000$; $latex {f \circ \left( m \circ \mathrm{id}_{\mathrm{None}} \right) = f \circ m = \left( f \circ m \right) \circ \mathrm{id}_{\mathrm{None}}}&fg=000000$.

2. $latex {m \circ \mathrm{id}_{\mathrm{None}} = m}&fg=000000$; $latex {\mathrm{id}_{\mathrm{Dst} m} \circ m = \mathrm{StarComp} \left( m ; \lambda i \in \mathrm{arity} m : \mathrm{id}_{\mathrm{Obj}_m i} \right) = m}&fg=000000$.

Remark I call the above defined category abrupt category because (excluding identity morphisms) it allows composition with an $latex m\in M$ only on the left (not on the right) so that the morphism $latex m$ is “abrupt” on the right.