The linear map to build a pure imaginary number

Stream: Is there code for X?

[Eric Wieser]

Do we have this?

noncomputable def complex.of_imag : ℝ →ₗ[ℝ] ℂ :=
{ to_fun := λ r, ⟨0, r⟩, map_add' := sorry, map_smul' := sorry }

[Eric Wieser]

I can get there with linear_map.to_span_singleton ℝ _ complex.I, but the definitional unfolding is worse.

[Heather Macbeth]

Can you compose docs#complex.of_real_am with the restrict_scalars of the multiplication-by-I linear map?

[Eric Wieser]

I'm not sure that really ends up much better. Maybe there's no reason to want ⟨0, r⟩ definitionally anyway.

[Heather Macbeth]

What do you want it for?

[Eric Wieser]

As an argument to docs#clifford_algebra.lift to construct clifford_algebra Q ≃ₐ[ℝ] ℂ where Q = -quadratic_form.lin_mul_lin linear_map.id linear_map.id

[Eric Wieser]

I don't have a particular reason for needing the definitional equality, I just thought it might help

[Eric Wieser]

So far I have:

import linear_algebra.clifford_algebra.basic
import data.complex.basic

noncomputable def clifford_algebra_complex.Q : quadratic_form ℝ ℝ :=
-quadratic_form.lin_mul_lin linear_map.id linear_map.id

@[simp]
lemma clifford_algebra_complex.Q_apply (r : ℝ) : clifford_algebra_complex.Q r = - (r * r) := rfl

open clifford_algebra_complex

noncomputable def clifford_algebra_complex : clifford_algebra clifford_algebra_complex.Q ≃ₐ[ℝ] ℂ :=
let to_fun : clifford_algebra Q →ₐ[ℝ] ℂ :=
  clifford_algebra.lift Q ⟨linear_map.to_span_singleton _ _ complex.I, λ r, begin
    dsimp [linear_map.to_span_singleton, linear_map.id],
    rw smul_mul_smul,
    simp,
  end⟩ in
{ to_fun := to_fun,
  inv_fun := λ z, algebra_map ℝ _ z.re + clifford_algebra.ι Q z.im,
  left_inv := λ x, by { simp [to_fun, linear_map.to_span_singleton], sorry },
  right_inv := λ z, by { ext, simp [to_fun, linear_map.to_span_singleton], sorry },
  ..to_fun, }

[Eric Wieser]

I guess my question is, which is the most canonical spelling: ↑r * complex.I, r • complex.I, or ⟨0, r⟩?