English
Let f: β → C be a family of objects with coproduct ∐ f and injections ι_b: f(b) → ∐ f. For any X and arrows g1, g2: ∐ f → X, if g1 ∘ ι_b = g2 ∘ ι_b for all b ∈ β, then g1 = g2.
Русский
Пусть f: β → C образует семейство объектов и их копроизведение ⨿ f с инъекциями ι_b: f(b) → ⨿ f. Пусть g1, g2: ⨿ f → X. Если для всех b ∈ β выполняется g1 ∘ ι_b = g2 ∘ ι_b, то g1 = g2.
LaTeX
$$$\forall g_1,g_2: \coprod_{b\in \beta} f(b) \to X, \quad (\forall b\in \beta)\ g_1 \circ \iota_b = g_2 \circ \iota_b \Rightarrow g_1 = g_2.$$$
Lean4
/-- Without this lemma, `limit.hom_ext` would be applied, but the goal would involve terms
in `Discrete β` rather than `β` itself. -/
@[ext 1050]
theorem hom_ext {f : β → C} [HasCoproduct f] {X : C} (g₁ g₂ : ∐ f ⟶ X)
(h : ∀ (b : β), Sigma.ι f b ≫ g₁ = Sigma.ι f b ≫ g₂) : g₁ = g₂ :=
colimit.hom_ext (fun ⟨j⟩ => h j)
