Oriented structures with a partially defined multiplication and having one as the neutral element of the multiplication. An entity of a Multiplicative structure will be called a factor.

Properties Let c be a type instance of the class Multiplicative, then holds:

1. For all p in Point c holds: orientation (one p) == p :> p.

2. For all f and g in c holds:

   1. if start f == end g then f * g is valid and start (f * g) == start g and end (f * g) == end f.
   2. if start f /= end g then f * g is not valid and its evaluation will end up in a NotMultiplicable exception.
3. For all f in c holds: one (end f) * f == f and f * one (start f) == f.
4. For all f, g and h in c with start g == end h and start f == end g holds: (f * g) * h == f * (g * h).

5. For all f in c holds:

   1. npower f 1 == f.
   2. If f is a endo than npower f 0 == one (start f) and For all n in N holds: npower f (succ n) == f * npower f n.

Such a c will be called a multiplicative structure and an entity f of c will be called factor. The associated factor one p to a p in Point c will be called the one at p.

Note If the types c and Point c are interpreted as sets M and O and * as a partially defined function from M x M -> M then this forms a small category with objects in O and morphisms in M.

the one to a given point. The type p c serves only as proxy and one' is lazy in it.

Note As Point may be a non-injective type family, the type checker needs some times a little bit more information to pic the right one.

check for being equal to one.

type representing the class of Multiplicative structures.

transformable to Multiplicative structure.

transposable Multiplicative structures.

Property Let c be a TransposableMultiplicative structure, then holds:

1. For all p in Point c holds: transpose (one p) = one p.
2. For all f, g in c with start f == end g holds: transpose (f * g) == transpose g * transpose f.

commutative multiplicative structures.

Property Let c be a Commutative structure, then holds: For all f and g in c with start f == end f, start g == end g and start f == end g holds: f * g == g * f.

multiplicative structures having a multiplicative inverse.

Definition Let f and g be two factors in a Multiplicative structure _c then we call g a multiplicative inverse to f (or short inverse) if and only if the following hold:

1. start g == end f and end g == start f.
2. f * g = one (end f) and g * f == one (start f).

Properties For all f in a Invertible structure c holds:

1. isInvertible f is equivalent to solvable (tryToInvert f).
2. if isInvertible f holds, then invert f is valid and it is the multiplicative inverse of f. Furthermore invert f == solve (tryToInvert m).
3. if not isInvertible f holds, then invert f is not valid and evaluating it will end up in a NotInvertible-exception.

Note

1. It is not required that every factor has a multiplicative inverse (see Cayleyan for such structures).
2. This structure is intended for multiplicative structures having a known algorithm to evaluate for every invertible f its inverse.

invertible factors within a Multiplicative structures c, which forms a sub Multiplicative structure on c, given by the canonical inclusion inj which is given by \Inv f _ -> f.

Property Let Inv f f' be in Inv c where c is a Multiplicative structure, then holds:

1. orientation f' == opposite (orientation f).
2. f' * f == one (start f).
3. f * f' == one (end f).

Note The canonical inclusion is obviously not injective on the set of all values of type Inv c to c. But restricted to the valid ones it is injective, because the inverses of a f in c are uniquely determined by f.

Invertible structures where every element is invertible.

Property Let c be a Cayleyan structure, then holds: For all f in c holds: isInvertible f == True.

Note

1. If the type Point c is singleton, then the mathematical interpretation of c is a group.
2. The name of this structures is given by Arthur Cayley who introduced the concept (and the name) of an abstract group in 1854 (https://en.wikipedia.org/wiki/Arthur_Cayley).
3. Usually in mathematics such a structure is called a groupoid.

random variable of paths at the given point and the given length (see xosPathMaxAt and as c is Multiplicative, the underlying random variable for factors for a given point is not empty).

random variable of paths with the given length.

the induced random variable for paths.