English
Let (G_i) be a directed system of commutative rings with bonding maps f_{i j}, and let P be a commutative ring. If g_i: G_i → P is a compatible family (g_j ∘ f_{i j} = g_i), then the induced map from the direct limit DirectLimit(G,f) to P is uniquely determined by its restrictions to each G_i; equivalently, for every x in the direct limit, F(x) equals the universal lift of the family (g_i) applied to x.
Русский
Пусть (G_i) — направленная система колмитов коммутативных колец с связующими отображениями f_{i j}, и P — коммутативное кольцо. Если g_i: G_i → P образуют совместную семью (совместимую: g_j ∘ f_{i j} = g_i), то полученная каноническая связка DirectLimit(G,f) → P уникальна и определяется своими ограничениями на каждом G_i; то есть для каждого элемента x в прямом пределе выполняется F(x) = lift(коэффициенты) x, т.е. F(x) определяется единственным Линейным отображением, совместимым с g_i.
LaTeX
$$$\\exists!\\ F: \\mathrm{DirectLimit}(G,f) \\to P\\quad\\text{such that}\\quad F \\circ (\\mathrm{of}\\ G f i) = g_i\\ \\text{for all } i.$$$
Lean4
@[deprecated lift_comp_of (since := "2025-08-11")]
theorem lift_unique (F : DirectLimit G f →+* P) (x) :
F x = lift G f P (fun i ↦ F.comp <| of G f i) (fun i j hij x ↦ by simp) x := by rw [lift_comp_of]
