lift — Mathlib

English

Given a compatible family f_j: X → (F.obj(op j)).obj j, there exists a unique arrow X → end F whose compositions with π F j give f_j for all j.

Русский

Пусть имеется совместимая семейство f_j: X → (F.obj(op j)).obj j; существует единственная стрелка X → end F, чья композиция с π_F j равна f_j для всех j.

LaTeX

$$$\exists!\,\ell:\, X \to End(F)\quad\text{such that }\forall j,\; \ell;\pi F j = f_j$$$

Lean4

/-- Constructor for morphisms to the end of a functor. -/
noncomputable def lift : X ⟶ end_ F :=
  Wedge.IsLimit.lift (limit.isLimit _) f hf

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