English
The lift map (ZMod.lift n f) is injective if and only if the kernel condition on f holds: whenever f(m) = 0 for an integer m, then m maps to 0 in ZMod n.
Русский
Лифт (ZMod.lift n f) инъективен тогда и только тогда, когда ядро f удовлетворяет условию: если f(m) = 0 для некоторого целого m, то m эквивалентен 0 по модулю n.
LaTeX
$$$\\operatorname{Injective} (ZMod.lift n f) \\iff \\forall m \\in \\mathbb{Z},\\, f.m = 0 \\Rightarrow (m : \\mathbb{Z}/n\\mathbb{Z}) = 0$$$
Lean4
theorem lift_injective {f : { f : ℤ →+ A // f n = 0 }} : Injective (lift n f) ↔ ∀ m, f.1 m = 0 → (m : ZMod n) = 0 := by
simp only [← AddMonoidHom.ker_eq_bot_iff, eq_bot_iff, SetLike.le_def, ZMod.intCast_surjective.forall, ZMod.lift_coe,
AddMonoidHom.mem_ker, AddSubgroup.mem_bot]
