English
In a directed system, if the image of an element x ∈ G_i in the direct limit is zero, then there exists a later stage j ≥ i such that the transition map sends x to zero in G_j.
Русский
В направленной системе, если образ элемента x ∈ G_i в прямом пределе равен нулю, то существует поздний этап j ≥ i, такой что переходная карта отправляет x в ноль в G_j.
LaTeX
$$$\exists j\ hij:\; f_{i,j}^{h}(x)=0$ when $\text{of}(i,x)=0$$$
Lean4
/-- A component that corresponds to zero in the direct limit is already zero in some
bigger module in the directed system. -/
theorem zero_exact {i x} (H : of R ι G f i x = 0) : ∃ j hij, f i j hij x = (0 : G j) :=
by
convert exists_eq_of_of_eq (H.trans (map_zero <| _).symm)
rw [map_zero]
