The unique `ℂ →ₐ[ℝ] A` given a square root of -1

Stream: Is there code for X?

[Eric Wieser]

docs#complex.lift doesn't exist

[Filippo A. E. Nuccio]

But does this really exist? You can chose both I and -I, no? I mean, if you take $A=\mathbb{C}$, is the canonical map the identity or its opposite?

[Eric Wieser]

I've replaced the word "canonical" with "unique"

[Eric Wieser]

For a given I' there is a unique map

[Filippo A. E. Nuccio]

Ah sure, once the I' is chosen I agree.

[Eric Wieser]

I was able to define this as:

noncomputable def complex.lift (I' : A) (hf : I' * I' = -1) : ℂ →ₐ[ℝ] A :=
alg_hom.mk'
  { to_fun := ⇑((algebra.of_id ℝ A).to_linear_map.comp complex.re_lm +
                (linear_map.to_span_singleton _ _ I').comp complex.im_lm),
    map_zero' := linear_map.map_zero _,
    map_add' := linear_map.map_add _,
    map_mul' := λ ⟨x₁, y₁⟩ ⟨x₂, y₂⟩, by {
      change algebra_map ℝ A (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
             (algebra_map ℝ A x₁ + y₁ • I') * (algebra_map ℝ A x₂ + y₂ • I'),
      rw [mul_add, add_mul, add_mul],
      rw [smul_mul_smul, hf, smul_neg, ←algebra.algebra_map_eq_smul_one, ←sub_eq_add_neg],
      simp only [←algebra.commutes x₂, ←ring_hom.map_mul],
      simp only [←algebra.smul_def],
      simp only [add_smul, smul_smul, ring_hom.map_sub, mul_comm y₁ x₂],
      abel, },
    map_one' := show algebra_map ℝ A 1 + (0 : ℝ) • I' = 1,
      by rw [ring_hom.map_one, zero_smul, add_zero], }
  (linear_map.map_smul _)

but I suspect there's a shorter way

[Filippo A. E. Nuccio]

Have you looked around https://leanprover-community.github.io/mathlib_docs/field_theory/minpoly?

[Filippo A. E. Nuccio]

I can't find lifts of morphisms, though.

[Anne Baanen]

You could define a docs#power_basis on the complex numbers, then you can use docs#power_basis.lift :P

[Johan Commelin]

Something with splitting_field.lift maybe also works?

[Anne Baanen]

(Not sure how seriously to take my suggestion.)

[Oliver Nash]

You should be able to do this with extension of scalars, though you might need to fill in some gaps to get it to work. Wait sorry, that's not what you want.

[Filippo A. E. Nuccio]

Well, I really think it is a good suggestion, after all the setting is very much field-extension-ish.

[Eric Wieser]

My suspicion is that we probably do already have this somewhere, but inside some other construction that needed it

[Eric Wieser]

It's very similar to the docs#zsqrtd.lift that we already have

[Eric Wieser]

PR'd as #8107, would appreciate any golfing suggestions

[Anne Baanen]

I think the morally correct way to do #8107 is to use a more general construction, i.e. docs#power_basis.lift (viewing ℂ as adjoin ℝ I) or docs#splitting_field.lift (viewing ℂ as splitting_field (X * X + 1 : polynomial R)). I am quite sure though that we don't have the equiv form anywhere.

[Anne Baanen]

Do we have a proof that minpoly ℝ (I : ℂ) = X * X + 1?

[Anne Baanen]

Once we have the value of minpoly ℝ I, then power_basis.lift_equiv from #8110 is exactly what we're looking for.

[Eric Wieser]

Those definitions sound like they won't unfold nearly as cleanly

[Anne Baanen]

True, unfolding power_basis.lift will give you some ugly term involving basis.constr. But it should pass very well through simp, or at least once you add a simp lemma stating complex.lift I' hI I = I'. (After all, the alg_hom is uniquely specified by what it does on I = pb.gen.)

[Eric Wieser]

Would you argue that docs#zsqrtd.lift should be implemented using that machinery too?

[Anne Baanen]

Looking at it mathematically, yes, I would prefer that. There is nothing in zsqrtd.lift that does not work for adjoin_root or algebra.adjoin. Implementation-wise, there might be an argument that we should try and keep zsqrtd-based definitions computable. For complex numbers that's counterargument is not so convincing though :)

[Eric Wieser]

Playing devil's advocate, perhaps we should have a power_basis API for taking this style of "universal property" over a single generator and constructing a power basis

[Eric Wieser]

At any rate, I'll try to golf the proofs in #8107 with the lemma in #8109 so that I can more convincingly try to argue "it's shorter to just prove it directly".

[Anne Baanen]

Eric Wieser said:

Playing devil's advocate, perhaps we should have a power_basis API for taking this style of "universal property" over a single generator and constructing a power basis

Hmm, that sounds like a good idea actually. I'll have to think if "lift given by one element ↔ power basis" is true in full generality, but that should definitely be morally correct.

[Eric Wieser]

Here's level 2 of this game:

import algebra.quaternion

open_locale quaternion
namespace quaternion_algebra

variables {R : Type*} {A : Type*} [comm_ring R] [ring A] [algebra R A](c₁ c₂ : R)

def lift_aux (i : A) (hi : i * i = algebra_map R _ c₁) (j : A) (hj : j * j = algebra_map R _ c₂)
  (hij : i * j = -(j * i)) :
  ℍ[R,c₁,c₂] →ₐ[R] A :=
{ to_fun := λ q, algebra_map R _ q.re + q.im_i • i + q.im_j • j + q.im_k • (i * j),
  map_one' := by simp,
  map_mul' := λ q₁ q₂, begin
    simp [add_mul, mul_add],
    sorry
  end,
  map_zero' := by simp,
  map_add' := λ q₁ q₂, by { simp [add_smul], abel },
  commutes' := λ r, by simp }

That sorry looks very nasty, especially since all the surrounding simps use up lots of time

[Eric Wieser]

I solved this in https://github.com/pygae/lean-ga/blob/46e5be3c97c4f99085a8452ca2213f53d2f17bf9/src/for_mathlib/data/quaternion.lean#L144-L159, but I needed a substantial number of helper lemmas