lift_of — Mathlib

English

Given a compatible family of maps g_i from G_i to P into a common target, there is a unique map from the direct limit to P that agrees with all g_i on the injections.

Русский

Существует единственный отображение из прямого предела в P, которое согласуется с каждой g_i на инъекциях.

LaTeX

$$$\mathrm{lift}(G,f,P,g,Hg):\; \iota_i(x) \mapsto g_i(x)$ and uniqueness holds.$$

Lean4

@[simp]
theorem lift_of (i x) : lift G f P g Hg (of G f i x) = g i x :=
  Module.DirectLimit.lift_of (f := fun i j hij ↦ (f i j hij).toNatLinearMap) (fun i ↦ (g i).toNatLinearMap) Hg x

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