English
Let (G_i) be a directed system of L-structures with embeddings f, and maps g_i : G_i ↪[L] P into some P, commuting with the system via Hg. Then for every i and every x ∈ G_i, the canonical lift from the direct limit sends the image of x from G_i to g_i(x); i.e., the element ⟦.mk f i x⟧ in the direct limit maps to g_i(x) in P.
Русский
Пусть имеется направленная система структур L с вложениями f и карты g_i: G_i ↪[L] P в некоторую структуру P, которые согласованы через Hg. Тогда для каждого i и каждого x ∈ G_i отображение лифта из прямого предела отправляет образ x в G_i на g_i(x); то есть элемент ⟦.mk f i x⟧ прямого предела отображается в g_i(x) в P.
LaTeX
$$$\operatorname{lift}_{L,\iota,G,f,g,Hg}\big(\llbracket \mathrm{mk} f\, i\, x \rrbracket\big) = g_i(x).$$$
Lean4
@[simp]
theorem lift_quotient_mk'_sigma_mk' {i} (x : G i) : lift L ι G f g Hg ⟦.mk f i x⟧ = (g i) x :=
by
change (lift L ι G f g Hg).toFun ⟦.mk f i x⟧ = _
simp only [lift, Quotient.lift_mk]
