English
If d is non-square and R has characteristic zero, then the map r ↦ lift r is injective, i.e., distinct choices of r with r^2 = d give distinct ring isomorphisms from Z[√d] to R.
Русский
Если d не является квадратом и характеристика R равна нулю, то отображение r↦lift r инъективно; разные значения r с r^2 = d давали бы разные изоморфизмы.
LaTeX
$$$[CharZero\\,R]\\;{d:\\mathbb{Z}}\\; (r_1,r_2\\in\\{r\\in R\\mid r^2=d\\})\\:lift\\,r_1=lift\\,r_2\\Rightarrow r_1=r_2.$$$
Lean4
/-- `lift r` is injective if `d` is non-square, and R has characteristic zero (that is, the map from
`ℤ` into `R` is injective). -/
theorem lift_injective [CharZero R] {d : ℤ} (r : { r : R // r * r = ↑d }) (hd : ∀ n : ℤ, d ≠ n * n) :
Function.Injective (lift r) :=
(injective_iff_map_eq_zero (lift r)).mpr fun a ha =>
by
have h_inj : Function.Injective ((↑) : ℤ → R) := Int.cast_injective
suffices lift r a.norm = 0
by
simp only [re_intCast, add_zero, lift_apply_apply, im_intCast, Int.cast_zero, zero_mul] at this
rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this
rw [norm_eq_mul_conj, RingHom.map_mul, ha, zero_mul]
