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

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. {\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)}; 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 ; {f \circ \left( m \circ \mathrm{id}_{\mathrm{None}} \right) = f \circ m = \left( f \circ m \right) \circ \mathrm{id}_{\mathrm{None}}}.
  2. {m \circ \mathrm{id}_{\mathrm{None}} = m}; {\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}.

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

Leave a Reply