Let $H$ be a multiplicative, commutative monoid, and denote by $H^\times$ the group of units of $H$, by $\mathcal A(H)$ the set of atoms (or irreducible elements) of $H$, by $\mathscr{F}^\ast(\mathcal A(H))$ the free monoid with basis $\mathcal A(H)$, which I will also write multiplicatively, and by $\pi_H$ the unique homomorphism $\mathscr{F}^\ast(\mathcal A(H)) \to H$ such that $\pi_H(a) = a$ for every $a \in \mathcal A(H)$, where I'm tacitly assuming, as usual, that $\mathscr{F}^\ast(\mathcal A(H))$ has been realized in a way that $\mathcal A(H) \subseteq \mathscr{F}^\ast(\mathcal A(H))$ as sets. Lastly, let $\mathscr{C}_{\rm red}$ (respectively, $\mathscr{C}_H$) be the smallest (monoid) congruence on $\mathscr{F}^\ast(\mathcal A(H))$ for which the following condition holds:

For all non-empty words $\mathfrak a = a_1 \cdots a_m$ and $\mathfrak b = b_1 \cdots b_n$ in $\mathscr{F}^\ast(\mathcal A(H))$, we have $(\mathfrak a, \mathfrak b) \in \mathscr{C}_H$ if and only if $m = n$ and there is a permutation $\sigma \in \mathfrak S_n$ such that $b_{\sigma(i)} \in a_i H^\times$ for each $i \in [\![1, n ]\!]$ (respectively, $\pi_H(\mathfrak a) = \pi_H(\mathfrak b)$, $m = n$, and there is a permutation $\sigma \in \mathfrak S_n$ such that $b_{\sigma(i)} \in a_i H^\times$ for each $i \in [\![1, n ]\!]$).

In ZFC, $\mathscr{F}^\ast(\mathcal A(H))/\mathscr{C}_{\rm red}$ embeds (as a monoid) in $\mathscr{F}^\ast(\mathcal A(H))/\mathscr{C}_H$, and the embedding is an isomorphism if and only if $H$ is reduced (i.e., $H = H^\times$). My question is:

Q.What about acanonicalembedding $\mathscr{F}^\ast(\mathcal A(H))/\mathscr{C}_{\rm red} \hookrightarrow \mathscr{F}^\ast(\mathcal A(H))/\mathscr{C}_H$?

I trust in your discernment to formalize my request. But if anyone insists that I should be clear about the actual meaning of the term "canonical", then I will ask whether the existence of the above embedding can be proved in ZF.

Let me recall that an element $a \in H$ is an atom if (i) $a$ is not a unit and (ii) $a = xy$ for some $x, y \in H$ only if $x \in H^\times$ or $y \in H^\times$.

P.S.: Since $H$ is commutative, I could have phrased my question in terms of the free *abelian* monoid with basis $\mathcal A(H)$. However, there are good reasons for doing otherwise.