hom_ext — Mathlib

English

Let t be a PushoutCocone f g. To check whether a morphism is coequalized by t.ι, it suffices to check two generating arrows: inl t and inr t.

Русский

Пусть t — PushoutCocone f g. Чтобы проверить, тождественно ли коселено стрелы t.ι, достаточно проверить две базовые стрелы inl t и inr t.

LaTeX

$$$\\forall j:\\ WalkingSpan, t.ι.app j \\;\\text{coequalizes}\\; k,l$$$

Lean4

theorem hom_ext {t : PushoutCocone f g} (ht : IsColimit t) {W : C} {k l : t.pt ⟶ W} (h₀ : inl t ≫ k = inl t ≫ l)
    (h₁ : inr t ≫ k = inr t ≫ l) : k = l :=
  ht.hom_ext <| coequalizer_ext _ h₀ h₁

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