I'm studying a special sort of homomorphisms between partial group-like structures, of the property below, $$\forall a' b c.\ \ a' \cdot \psi(b) = \psi(c) \to (\exists a.\ \ a' = \psi(a) \land a \cdot b = c)$$
Does this property has a known name? Thank you.
This is a property abstracted from separation algebra, and I find I'm using it everywere in my work so I feel there should be a name or some existing research for it. Bellow is my breif interpretaion about the property (can be misleading!):
It first gives me a sense of 'embedding'. For $\psi: A \rightarrow B$, the $A$ is embedded in a larger $B$. If $\psi(b)$ combined with some $a'$ still falls in $A$, then $a'$ must be some element in $A$ without any 'noise' from outside. It sounds like, elements from outside cannot make elements in $A$ by applying with elements in $A$. In my work, I use $B$ like a big container (a finite product), and inject several such $A$ into it. By this property, I can recover an injected element back.
Maybe another similar (but weaker) form can be more intuitive, $$\forall a\,a'\,b' c'.\ \ a' \cdot b' = c' \land a' = \psi(a) \land (\not\exists b.\ b' = \psi(b)) \to (\not \exists c.\ c' = \psi(c))$$ If the image $a' = \psi(a)$ is applied with another element that is not an image of $A$, the result will not fall in the image of $A$. It shows the homomorphism has some 'orthogonal' sense. $b'$ brings some elements not belonging to $A$, the application of $a' \cdot b'$ still contains those external elements so it cannot fall in the image of $A$.
Perhaps I find an answer but not sure, so please correct me if I am wrong.
It is an orthogonality between the group actions and the homomorphism.
First, we consider total monoid, and construct a category embedding the monoids and the homomorphism. It consists of two objects $A,B$ which are carrier sets of monoids $\mathcal{A}$ and $\mathcal{B}$, and their endomorphisms are the group actions of the monoids respectively. The only arrow from $A$ to $B$ is the homomorphism $\psi$.
The property $a' \cdot \psi(b) = \psi(c) \longrightarrow (\exists a.\ a' = \psi(a) \land a \cdot b = c)$ is characterized by the following commute diagram (ignore the red arrow for now). We use bold-face $\mathbf{a}(x) \triangleq a \cdot x$ to differentiate a left group action and the group element.
The existence of group element $a$ implies the existence of an arrow $\mathbf{a}$ that commutes.
The red arrow denotes $\mathbf{a}' \circ \psi$. We rearrange $\mathbf{b}, \mathbf{a}, \psi$ and the red arrow,
then we get the standard diagram for orthogonality.
If the property $a' \cdot \psi(b) = \psi(c) \longrightarrow (\exists a.\ a' = \psi(a) \land a \cdot b = c)$ is held, the arrow $\mathbf{a}$ exists and commutes in each triangles (note $\psi \circ \mathbf{a} = \lambda x. \psi(a \cdot x) = \mathbf{a}' \circ \psi$). According to the definition of orthogonality, $\mathbf{b} \perp \psi$, the group action of $b$ is orthogonal to the homomorphism $\psi$.
Reversely, it is also true. From the existence of $\mathbf{a}$, we can show the corresponding $a$ is the witness of the existence in the property. So the orthogonality also implies the property.
The conclusion can be extended to partial monoids if we change the way to construct the category (I am not sure if there is a standard approach embedding partial algebras into categories).
The objects are the elements of the two algebras, the morphisms are still group actions. There is an arrow $\mathbf{a}$ from $b$ to $c$ iff $a \cdot b = c$. Between the objects of $\mathcal{A}$'s elements and that of $\mathcal{B}$, there is an arrow $\psi$ from $a$ to $a'$ iff $a' = \psi(a)$. By this setting, the conclusion should be extended.
To handle non-unital and non-associative algberas, we only need to add a special initial object from which morphisms are constant functions returning the group elements, and let the two left-most objects in the second diagram be the initial object.