Amalgamation over the trivial group is the ordinary free product

Given: The objects and hypotheses in the statement.

If $f:K\to G$ and $h:K\to H$ are injective homomorphisms, their pushout is called the free product with amalgamation and is denoted $G\ast_KH$. The quotient construction is thm-group-pushout-as-an-amalgamated-quotient, and injectivity means the trivial-kernel condition of thm-group-homomorphism-injective-iff-trivial-kernel. The notation anticipates identifying $K$ with its two images, but injectivity of the canonical maps $G,H\to G\ast_KH$ is a theorem, not part of this definition. (Free products with amalgamation along monomorphisms).

For a family $(G_i)_{i\in I}$, a free product is a group $F$ with homomorphisms $\iota_i:G_i\to F$ in the sense of def-group-homomorphism, such that for every group $H$ and every family of homomorphisms $f_i:G_i\to H$, there is a unique homomorphism $f:F\to H$ satisfying $f\circ\iota_i=f_i$ for all $i$. It is denoted $\ast_{i\in I}G_i$. Injectivity of the maps $\iota_i$ is not part of this definition. (The free product of an arbitrary family of groups).

Any two free products of the same family are connected by a unique isomorphism commuting with every canonical factor map. (Free products are unique up to a unique factor-compatible isomorphism).