English
There is a canonical homomorphism from the coproduct CoprodI G to PushoutI φ
Русский
Существует канонический гомоморфизм из копрода CoprodI G в PushoutI φ.
LaTeX
$$$ofCoprodI : CoprodI G \to^* PushoutI(\varphi)$$$
Lean4
/-- The equivalence that is part of the universal property of the pushout. A hom out of
the pushout is just a morphism out of all groups in the pushout that satisfies a commutativity
condition. -/
@[simps]
def homEquiv : (PushoutI φ →* K) ≃ { f : (Π i, G i →* K) × (H →* K) // ∀ i, (f.1 i).comp (φ i) = f.2 } :=
{ toFun := fun f =>
⟨(fun i => f.comp (of i), f.comp (base φ)), fun i => by rw [MonoidHom.comp_assoc, of_comp_eq_base]⟩
invFun := fun f => lift f.1.1 f.1.2 f.2,
left_inv := fun _ => hom_ext (by simp [DFunLike.ext_iff]) (by simp [DFunLike.ext_iff])
right_inv := fun ⟨⟨_, _⟩, _⟩ => by simp [DFunLike.ext_iff, funext_iff] }
