English
lift provides an equivalence between the set of elements I' with I'^2 = -1 in A and ℂ-algebra homomorphisms ℂ →ₐ[ℝ] A.
Русский
lift устанавливает эквиваленцию между элементами I' из A с I'^2 = -1 и ℂ-алгебра-гомоморфизмами ℂ →ₐ[ℝ] A.
LaTeX
$$$ lift : \{ I' : A \mid I'^2 = -1 \} \simeq (\mathbb{C} \to_{\mathbb{R}} A). $$$
Lean4
/-- A universal property of the complex numbers, providing a unique `ℂ →ₐ[ℝ] A` for every element
of `A` which squares to `-1`.
This can be used to embed the complex numbers in the `Quaternion`s.
This isomorphism is named to match the very similar `Zsqrtd.lift`. -/
@[simps +simpRhs]
def lift : { I' : A // I' * I' = -1 } ≃ (ℂ →ₐ[ℝ] A)
where
toFun I' := liftAux I' I'.prop
invFun F := ⟨F I, by rw [← map_mul, I_mul_I, map_neg, map_one]⟩
left_inv I' := Subtype.ext <| liftAux_apply_I (I' : A) I'.prop
right_inv
_ :=
algHom_ext <|
liftAux_apply_I _
_
-- When applied to `Complex.I` itself, `lift` is the identity.
