English
There is a universal lift: given a family of monoid homomorphisms f_i: G_i → K and k: H → K with f_i ∘ φ_i = k, there exists a unique MonoidHom PushoutI φ → K extending them.
Русский
Существует единственный отображение из PushoutI φ в K, который на каждой G_i действует как f_i и согласуется с k на H, если f_i ∘ φ_i = k для всех i.
LaTeX
$$$lift(f,k,hf) : PushoutI(\varphi) →^* K$ с условием ∀ i, (f_i) ∘ φ_i = k$$
Lean4
/-- Define a homomorphism out of the pushout of monoids be defining it on each object in the
diagram -/
def lift (f : ∀ i, G i →* K) (k : H →* K) (hf : ∀ i, (f i).comp (φ i) = k) : PushoutI φ →* K :=
Con.lift _ (Coprod.lift (CoprodI.lift f) k) <|
by
apply Con.conGen_le fun x y => ?_
rintro ⟨i, x', rfl, rfl⟩
simp only [DFunLike.ext_iff, MonoidHom.coe_comp, comp_apply] at hf
simp [hf]
