lift_unique — Mathlib

English

The map from the direct limit obtained by sending each component through the identity is the identity map on the direct limit.

Русский

Отображение прямого предела, которое инициируется через тождественные отображения на каждом компоненте, есть тождественность на пределе.

LaTeX

$$$\\mathrm{DirectLimit}.map (\\lambda i. \\mathrm{id}) (\\lambda i j h. \\mathrm{id}) = \\mathrm{LinearMap.id}$$$

Lean4

@[deprecated lift_comp_of (since := "2025-08-11")]
theorem lift_unique (F : DirectLimit G f →ₗ[R] P) (x) :
    F x = lift R ι G f (fun i ↦ F.comp <| of R ι G f i) (fun i j hij x ↦ by simp) x := by rw [lift_comp_of]

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