lift_of' — Mathlib

English

The lift construction with the canonical injections, when applied to the direct limit, yields the identity map on the direct limit.

Русский

Лифт-операция, применённая к каноническим вложениям, даёт тождественное отображение на прямом пределе.

LaTeX

$$$\\operatorname{lift}(G,f,\\,\\_,\\,\\text{of})\\;\\big(\\,\\text{fun } i \\mapsto \\text{of }G f i\\,\\big)\\; (\\text{coherence}) = \\mathrm{id}_{\\mathrm{DirectLimit}(G,f)}.$$$

Lean4

@[simp]
theorem lift_of' : lift G f _ (of G f) (fun i j hij x ↦ by simp) = .id _ := by ext; simp

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