English
There is a canonical equivalence between { I' : A | I'^2 = -1 } and ℂ →ₐ[ℝ] A.
Русский
Существует каноническое соответствие между { I' ∈ A | I'^2 = -1 } и ℂ →ₐ[ℝ] A.
LaTeX
$$$ lift : \{ I' : A \mid I'^2 = -1 \} \simeq (\mathbb{C} \to_{\mathbb{R}} A). $$$
Lean4
/-- There is an alg_hom from `ℂ` to any `ℝ`-algebra with an element that squares to `-1`.
See `Complex.lift` for this as an equiv. -/
def liftAux (I' : A) (hf : I' * I' = -1) : ℂ →ₐ[ℝ] A :=
AlgHom.ofLinearMap ((Algebra.linearMap ℝ A).comp reLm + (LinearMap.toSpanSingleton _ _ I').comp imLm)
(show algebraMap ℝ A 1 + (0 : ℝ) • I' = 1 by rw [RingHom.map_one, zero_smul, add_zero]) fun ⟨x₁, y₁⟩ ⟨x₂, y₂⟩ =>
show
algebraMap ℝ A (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
(algebraMap ℝ A x₁ + y₁ • I') * (algebraMap ℝ A x₂ + y₂ • I')
by
rw [add_mul, mul_add, mul_add, add_comm _ (y₁ • I' * y₂ • I'), add_add_add_comm]
congr 1
-- equate "real" and "imaginary" parts
·
rw [smul_mul_smul_comm, hf, smul_neg, ← Algebra.algebraMap_eq_smul_one, ← sub_eq_add_neg, ← RingHom.map_mul, ←
RingHom.map_sub]
·
rw [Algebra.smul_def, Algebra.smul_def, Algebra.smul_def, ← Algebra.right_comm _ x₂, ← mul_assoc, ← add_mul, ←
RingHom.map_mul, ← RingHom.map_mul, ← RingHom.map_add]
