English
There exists a canonical lift from the direct limit to any target C given a compatible family ih: i ↦ F_i → C; this lift is well-defined and respects the component-wise definitions.
Русский
Существуют канонические отображения-«поднятия» из прямого предела в произвольную цель C, заданные совместимой семейкой ih: i → F_i → C; они корректно определяются на пределе.
LaTeX
$$$\\mathrm{DirectLimit.lift}\\; f\\; ih\\; compat : \\mathrm{DirectLimit}(F,f)\\to C$$
Lean4
/-- To define a function from the direct limit, it suffices to provide one function from each
component subject to a compatibility condition. -/
protected def lift (z : DirectLimit F f) : C :=
z.recOn (fun x ↦ ih x.1 x.2) fun x y ⟨k, hxk, hyk, eq⟩ ↦ by
simp_rw [eq_rec_constant, compat _ _ hxk, compat _ _ hyk, eq]
