π_desc — Mathlib

English

Let f,g: X → Y be a parallel pair and s a colimit Cofork for (f,g). For any Cofork t for (f,g) and the IsColimit hs, we have s.π ≫ hs.desc t = t.π; hs.desc t is the mediating morphism t.pt → s.pt.

Русский

Пусть f,g: X → Y образуют параллельную пару и s является колимитным кофором для (f,g). Для любого кофора t и изотримимности hs верно s.π ≫ hs.desc t = t.π; desc является медиатором.

LaTeX

$$$\operatorname{IsColimit}(s) \Rightarrow \forall t:\, \mathrm{Cofork}(f,g),\ s.\pi \;\gg\; \operatorname{desc}_{hs}(t) = t.\pi$$$

Lean4

@[reassoc (attr := simp)]
theorem π_desc {s t : Cofork f g} (hs : IsColimit s) : s.π ≫ hs.desc t = t.π :=
  hs.fac _ _

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