English
A class K has the amalgamation property when for any M ∈ K and embeddings M → N, M → P with N,P ∈ K, there exists a Q ∈ K and embeddings N → Q, P → Q making the square commute.
Русский
Класс K обладает свойством амальгамирования: для любых M ∈ K и вложений M → N, M → P с N,P ∈ K существует Q ∈ K и вложения N → Q, P → Q, образующие коммутативный квадрат.
LaTeX
$$$\text{Amalgamation}(K) \;:=\; \forall M,N,P, MN: M \hookrightarrow N, MP: M \hookrightarrow P, M,N,P \in K \rightarrow \exists Q \in K, NQ: N \hookrightarrow Q, PQ: P \hookrightarrow Q, Q \in K \land NQ \circ MN = PQ \circ MP$$$
Lean4
/-- A class `K` has the amalgamation property when for any pair of embeddings of a structure `M` in
`K` into other structures in `K`, those two structures can be embedded into a fourth structure in
`K` such that the resulting square of embeddings commutes. -/
def Amalgamation : Prop :=
∀ (M N P : Bundled.{w} L.Structure) (MN : M ↪[L] N) (MP : M ↪[L] P),
M ∈ K →
N ∈ K → P ∈ K → ∃ (Q : Bundled.{w} L.Structure) (NQ : N ↪[L] Q) (PQ : P ↪[L] Q), Q ∈ K ∧ NQ.comp MN = PQ.comp MP
