lift_comp_of — Mathlib

English

If each component map g_i is injective and the system is directed, then the lift from the direct limit is injective.

Русский

Если каждое отображение g_i инъективно и система направлена, то отображение lift инъективно.

LaTeX

$$$\text{lift}: \varinjlim G_i \to P$ is injective if all g_i$ are injective and the system is directed.$$

Lean4

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

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