π_desc — Mathlib

English

For W, a family k of arrows from I.right b to W satisfying the compatibility, the map π I b composed with desc gives k b.

Русский

Для W и семейства стрелок k: I.right b → W, удовлетворяющего совместимости, композиция π I b с desc дает k b.

LaTeX

$$$\forall W\, k,\; (\forall b, I.right b \to W),\; (K.π b) \circ (\text{Multiequalizer.desc } I \; \_\; k \; h) = k b$$$

Lean4

@[reassoc]
theorem π_desc (W : C) (k : ∀ b, I.right b ⟶ W) (h : ∀ a, I.fst a ≫ k (J.fst a) = I.snd a ≫ k (J.snd a)) (b) :
    Multicoequalizer.π I b ≫ Multicoequalizer.desc I _ k h = k _ :=
  colimit.ι_desc _ _

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