lift_of — Mathlib

English

Given a family of linear maps g i : G_i → P compatible with the system, the universal lift from the direct limit sends the canonical image of i, x to g_i x.

Русский

Имея совместимую семью линейных отображений g_i : G_i → P, каноническое вложение прямого предела отображает x ∈ G_i в g_i x.

LaTeX

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

Lean4

@[simp]
theorem lift_of {i} (x) : lift R ι G f g Hg (of R ι G f i x) = g i x :=
  rfl

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