π_desc' — Mathlib

English

For a colimit Cofork s of f,g and a cocone t with k: Y → W and h: f ≫ k = g ≫ k, the equation s.π ≫ hs.desc t k h = k holds, expressing the dual universal property.

Русский

Для колимитного кофора s пар f,g и кокона t с k: Y → W и h: f ≫ k = g ≫ k, выполнено s.π ≫ hs.desc t k h = k.

LaTeX

$$$\forall t:\, \mathrm{Cofork}(f,g),\ (hs: IsColimit(s))\, (W:\,\mathrm{C})\, (k : Y \to W)(h : f \circ k = g \circ k) \Rightarrow s.\pi \circ (\operatorname{desc}_{hs} t k h) = k$$$

Lean4

@[reassoc (attr := simp)]
theorem π_desc' {s : Cofork f g} (hs : IsColimit s) {W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) :
    Cofork.π s ≫ Cofork.IsColimit.desc hs k h = k :=
  hs.fac _ _

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