English
For a fixed i, g in G_i, the ring equivalence evaluated at the canonical element agrees with the canonical inclusion applied to g.
Русский
Для фиксированного i и элемента g∈G_i эквивалентность по прямому пределу согласуется с каноническим вложением g в прямой предел.
LaTeX
$$$\\mathrm{ringEquiv}(G,f')(\\mathrm{of}\\;G\\;i\\;g) = ⟦⟨i,g⟩⟧.$$$
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} (hix : of G (f' · · ·) i x = 0) : ∃ (j : _) (hij : i ≤ j), f' i j hij x = 0 :=
by
have := Nonempty.intro i
apply_fun ringEquiv _ _ at hix
rwa [map_zero, ringEquiv_of, DirectLimit.exists_eq_zero] at hix
