fac — Mathlib

English

If c is a limit for a diagram F : β → C and f is a family of arrows A ⟶ F i, then the canonical map Desc hc f, followed by c.proj i, equals f i.

Русский

Пусть c является пределом диаграммы F: β → C, и f_i: A → F i; тогда композиция Desc hc f с проекцией c на i-ю вершину равна f_i.

LaTeX

$$$\\text{IsLimit } c \\implies c_{\\text{proj}_i} \\circ \\mathrm{desc}_{hc} f = f_i$$$

Lean4

@[reassoc (attr := simp)]
theorem fac {F : β → C} {c : Fan F} (hc : IsLimit c) {A : C} (f : ∀ i, A ⟶ F i) (i : β) :
    Fan.IsLimit.desc hc f ≫ c.proj i = f i :=
  hc.fac (Fan.mk A f) ⟨i⟩

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