hom_ext — Mathlib

English

The basic compatibility condition for a multiequalizer: for each a in J.L, the left and right composites I.fst a and I.snd a with the corresponding π-maps agree after postcomposition with I.π components.

Русский

Основное условие совместимости мультиравнопорядка: для каждого a из J.L, левая и правая композиции I.fst a и I.snd a с соответствующими π-образами согласуются после композиции с соответствующими компонентами I.

LaTeX

$$$\forall a:\, J.L,\ I.fst a \;\gg\; \text{Multiequalizer.π } I (J.fst a) = I.snd a \;\gg\; \text{Multiequalizer.π } I (J.snd a)$$$

Lean4

theorem hom_ext (hK : IsColimit K) {T : C} {f g : K.pt ⟶ T} (h : ∀ a, K.π a ≫ f = K.π a ≫ g) : f = g :=
  by
  apply hK.hom_ext
  rintro (_ | _) <;> simp [h]

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