Mazzola, Guerino / Noll, Thomas / Lluis-Puebla, Emilio: Perspectives in Mathematical and Computational Music Theory

Definition 4 A local composition is a denotator $D : A ~> F (y)$ , with $A (- Mod$ , whose form $F$ is of Power type. The coordinator $CF$ of $F$ is called the ambient space of $D,$ and its coordinates $y$ are called its support.

Definition 5 A local composition $D$ is called objective if $y (- 2Fun(CF )$ , that is, if there exists $Y < A@F un(CF )$ with $y = Y < @A × F un(CF )$ . $33 y isasubfunctorof@A ×Fun(CF).We haveseen thaty = Y isthesubsetY < A@F un(CF ) »made functor«.$ In this case $Y$ will also be called the support of $D$ . The $Card(D)$ of an objective denotator is the cardinality of its coordinates set $Y$ .

Here we should recall that: $Y < @A × F un(CF ),$ for $Y < A@2F un(CF)$ and, for another module $B$ ,

B@Y = {(u (- B@A, v (- B@F un(CF )) : v (- (u@F un(CF ))(Y )}.

Definition 6 A local composition that is not objective, is called functorial.

Then a local functorial composition is a subfunctor:

Z --> @A ×F un(CF ),

and a local objective composition is a subset:

Y --> A@F un(CF ))

An objective denotator $Y --> A@F$ (with $Y$ a local composition, $A (- Mod,$ and $F$ a functor) can be identified with its functorial version $Y --> @A × F$ . The same way, associated to each local functorial composition is its objective trace.

Definition 7 Let $Y --> @A × F$ be a local functorial composition, $A (- Mod,$ and $F$ its ambient space. Its objective trace is defined as the local composition:

S = {s (- A@F : (IdA,s) (- A@S},

that is, $S = 1A@S$ and, this way, a local functorial composition can be »frozen« to its objective trace.

On the other hand, the functorial version corresponding to $S$ (which is the local functorial composition $S$ »objectivized«) will be denoted as $<> S = S$

Proposition: Let $S --> @A × F$ be a local composition, $A (- Mod$ and ambient space $F$ . Then $<> S < S$ and $<> S = S$ if and only if $S$ is objective.

Proof : Let $<> (u,v) (- B@S = {u (- B@A, v (- B@F : v (- (u@F )(S)}$ . Then, $u : B --> A$ and $v (- (u@F )(S)$ and there exists $s (- S$ such that $(u@F )(s) = v$ . We also have $(IdA,s) (- A@S < A@A × A@F$ . Then we should show that $(u,v) (- B@S < B@A × B@F$ . However $u@S : A@S --> B@S, (IdA,s) '---> (u,v)$ , because

u@S : A@A ×A@F --> B@A × B@F, (IdA,s) '--> (u,u@F (s)) = (u,v).