English
There is a natural correspondence between elements r of a ring R with r^2 = d and ring homomorphisms from Z[√d] to R; equivalently, a ring homomorphism is determined by the image of √d.
Русский
Существует естественное соответствие между элементами r в кольце R, удовлетворяющими r^2 = d, и кольцевыми гомоморфизмами из Z[√d] в R; гомоморфизм полностью определяется образом √d.
LaTeX
$$$d\\in\\mathbb{Z}\\;\\Rightarrow\\;\\{r\\in R\\mid r^{2}=d\\}\\simeq (\\mathbb{Z}[\\sqrt{d}]\\to^+_*R).$$$
Lean4
/-- The unique `RingHom` from `ℤ√d` to a ring `R`, constructed by replacing `√d` with the provided
root. Conversely, this associates to every mapping `ℤ√d →+* R` a value of `√d` in `R`. -/
@[simps]
def lift {d : ℤ} : { r : R // r * r = ↑d } ≃ (ℤ√d →+* R)
where
toFun
r :=
{ toFun := fun a => a.1 + a.2 * (r : R)
map_zero' := by simp
map_add' := fun a b => by
simp only [re_add, Int.cast_add, im_add]
ring
map_one' := by simp
map_mul' := fun a b =>
by
have :
(a.re + a.im * r : R) * (b.re + b.im * r) =
a.re * b.re + (a.re * b.im + a.im * b.re) * r + a.im * b.im * (r * r) :=
by ring
simp only [re_mul, Int.cast_add, Int.cast_mul, im_mul, this, r.prop]
ring }
invFun f := ⟨f sqrtd, by rw [← f.map_mul, dmuld, map_intCast]⟩
left_inv r := by simp
right_inv
f := by
ext
simp
