hom_ext — Mathlib

English

If two morphisms m1, m2: B → W agree after composing with every π a, they are equal.

Русский

Если два морфизма m1, m2: B → W совпадают после композиции с каждым π a, то они равны.

LaTeX

$$m1 = m2$$

Lean4

theorem hom_ext {B W : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) [EffectiveEpiFamily X π] (m₁ m₂ : B ⟶ W)
    (h : ∀ a, π a ≫ m₁ = π a ≫ m₂) : m₁ = m₂ :=
  by
  have :
    m₂ = EffectiveEpiFamily.desc X π (fun a => π a ≫ m₂) (fun a₁ a₂ g₁ g₂ h => by simp only [← Category.assoc, h]) := by
    apply EffectiveEpiFamily.uniq; intro; rfl
  rw [this]
  exact EffectiveEpiFamily.uniq _ _ _ _ _ h

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