lift_of' — Mathlib

English

The functorial lift with the canonical of' maps yields the identity on the target when g is the identity on each component.

Русский

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

LaTeX

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

Lean4

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

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