lift_of — Mathlib

English

If g is a family of ring homomorphisms from G_i into P compatible with the directed system, then the universal lift from the direct limit sends the image of i, x to g_i(x).

Русский

Пусть g_i: G_i → P — семейство кольцевых гомоморфизмов, совместимо с системой; тогда канонический взвод по пределу отправляет (i, x) на g_i(x).

LaTeX

$$$\\text{lift}(G, f, P, g, \\mathrm{Hg})(\\text{of}(i, x)) = g_i(x).$$$

Lean4

@[simp]
theorem lift_of (i x) : lift G f P g Hg (of G f i x) = g i x :=
  rfl

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