coequalizer_ext — Mathlib

English

If s.π ≫ k = s.π ≫ l then for every j, s.ι.app j ≫ k = s.ι.app j ≫ l.

Русский

Если s.π ≫ k = s.π ≫ l, то для каждого j выполняется s.ι.app j ≫ k = s.ι.app j ≫ l.

LaTeX

$$$s.\ι_{j} \;\gg\; k = s.\ι_{j} \;\gg\; l\quad\text{for all } j$$$

Lean4

/-- To check whether two maps are coequalized by both maps of a cotrident, it suffices to check it
for the second map -/
theorem coequalizer_ext [Nonempty J] (s : Cotrident f) {W : C} {k l : s.pt ⟶ W} (h : s.π ≫ k = s.π ≫ l) :
    ∀ j : WalkingParallelFamily J, s.ι.app j ≫ k = s.ι.app j ≫ l
  | zero => by rw [← s.app_one (Classical.arbitrary J), Category.assoc, Category.assoc, h]
  | one => h

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