English
If the index category is nonempty and directed, and each component map g_i is injective, then the lift map from the direct limit to P is injective.
Русский
Если система направлена и индексы непусты, и каждый отображатель g_i инективен, то лифт-переносник прямого предела в P инъективен.
LaTeX
$$$\\text{If } \\forall i,\\ \\operatorname{Injective}(g_i)\\text{ and directed conditions hold, then } \\operatorname{Injective}(\\mathrm{lift}\\ G f P g Hg).$$$
Lean4
theorem lift_injective [Nonempty ι] [IsDirected ι (· ≤ ·)] (injective : ∀ i, Function.Injective <| g i) :
Function.Injective (lift G f P g Hg) :=
by
simp_rw [injective_iff_map_eq_zero] at injective ⊢
intro z hz
induction z using DirectLimit.induction_on with
| ih _ g => rw [lift_of] at hz; rw [injective _ g hz, map_zero]
