hom_ext — Mathlib

English

Let f : β → C be a HasProduct diagram and g1,g2 : X ⟶ ∏ᶜ f two morphisms. If for all b ∈ β we have g1 ≫ π_f b = g2 ≫ π_f b, then g1 = g2.

Русский

Пусть f : β → C задаёт произведение; g1,g2: X ⟶ ∏ᶜ f; если для каждого b верно g1 ≫ π_b = g2 ≫ π_b, то g1=g2.

LaTeX

$$$\\forall b,\\; g_1 \\;\\text{π}_b = g_2 \\;\\text{π}_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} [HasProduct f] {X : C} (g₁ g₂ : X ⟶ ∏ᶜ f) (h : ∀ (b : β), g₁ ≫ Pi.π f b = g₂ ≫ Pi.π f b) :
    g₁ = g₂ :=
  limit.hom_ext (fun ⟨j⟩ => h j)

Похожие утверждения