π_desc — Mathlib

English

Let f, g: X → Y have a coequalizer with π: Y → Q and coequalizer.desc k h: Q → W, where h: Y → W and f ≫ k = g ≫ k. Then composing π with desc yields k: π f g ≫ desc k h = k. This expresses the universal property of the coequalizer.

Русский

Пусть f, g: X → Y имеют коэквалайзер с π: Y → Q и coequalizer.desc k h: Q → W, где h: Y → W и f ≫ k = g ≫ k. Тогда композиция π с desc дает k: π f g ≫ desc k h = k. Это выражает универсальное свойство коэквалайзера.

LaTeX

$$$ f \\circ k = g \\circ k \\; \\Rightarrow\\; \\operatorname{coequalizer}.\\pi f g \\circ \\operatorname{coequalizer}.desc k h = k $$$

Lean4

@[reassoc]
theorem π_desc {W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) : coequalizer.π f g ≫ coequalizer.desc k h = k :=
  colimit.ι_desc _ _

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