English
If the directed system maps f' i j h are injective for all i ≤ j, then each canonical map from G_i into the direct limit is injective.
Русский
Если переходные отображения системы направлены инъективны, то каждое каноническое вложение G_i в прямой предел инъективно.
LaTeX
$$$\\forall i,\\; \\mathrm{of}_{G,f,i}: G_i \\to \\mathrm{DirectLimit}(G,f)\\; \\text{injective}.$$$
Lean4
/-- If the maps in the directed system are injective, then the canonical maps
from the components to the direct limits are injective. -/
theorem of_injective [IsDirected ι (· ≤ ·)] [DirectedSystem G fun i j h ↦ f' i j h]
(hf : ∀ i j hij, Function.Injective (f' i j hij)) (i) : Function.Injective (of G (fun i j h ↦ f' i j h) i) :=
have := Nonempty.intro i
((ringEquiv _ _).comp_injective _).mp fun _ _ eq ↦ DirectLimit.mk_injective f' hf _ (by simpa only [← ringEquiv_of])
