English
There is a natural equivalence between the subtype of integer-to-A homomorphisms that vanish on n and the type of ring homomorphisms ZMod n →+ A; i.e., lift : { f : ℤ →+ A // f n = 0 } ≃ (ZMod n →+ A).
Русский
Существует естественная эквивалентность между подмножеством гомоморфизмов ℤ →+ A, которые ноль на n, и гомоморфизмами ZMod n →+ A; то есть lift : { f : ℤ →+ A // f n = 0 } ≃ (ZMod n →+ A).
LaTeX
$$$\text{lift} : \{ f : \mathbb{Z} \to+* A \mid f(n) = 0 \} \simeq (\mathbb{Z}/n\mathbb{Z} \to+* A)$$$
Lean4
/-- The map from `ZMod n` induced by `f : ℤ →+ A` that maps `n` to `0`. -/
def lift : { f : ℤ →+ A // f n = 0 } ≃ (ZMod n →+ A) :=
(Equiv.subtypeEquivRight <| by
intro f
rw [ker_intCastAddHom]
constructor
· rintro hf _ ⟨x, rfl⟩
simp only [f.map_zsmul, zsmul_zero, f.mem_ker, hf]
· intro h
exact h (AddSubgroup.mem_zmultiples _)).trans <|
(Int.castAddHom (ZMod n)).liftOfRightInverse cast intCast_zmod_cast
