lift_ι — Mathlib

English

The lifted morphism composed with each projection equals the given f_j.

Русский

Полученный при подъёме морфизм при композиции с каждой проекцией равен заданной f_j.

LaTeX

$$$\\mathrm{lift}\\ hc\\ f hf \\;\\circ\\; \\mathrm{c.ι}_j = f_j$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_ι (hc : IsLimit c) {X : C} (f : ∀ j, X ⟶ (F.obj (op j)).obj j)
    (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f i ≫ (F.obj (op i)).map g = f j ≫ (F.map g.op).app j) (j : J) :
    lift hc f hf ≫ c.ι j = f j := by apply IsLimit.fac

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