lift_comp_of — Mathlib

English

The equivalence between the direct limit and the module sends the canonical element from the i-th component to the component representative in M.

Русский

Эквиваленция между пределом и модулем отправляет канонический элемент из i-й компоненты в представление в M.

LaTeX

$$$\\mathrm{equiv}(\\text{DirectLimit}) \\bigl( \\text{of}(i,x) \\bigr) = x\\; \\text{in } M$$$

Lean4

@[simp]
theorem lift_comp_of (F : DirectLimit G f →ₗ[R] P) :
    lift R ι G f (fun i ↦ F.comp <| of R ι G f i) (fun i j hij x ↦ by simp) = F := by ext; simp

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