Roots of unity of Circle

Stream: mathlib4

[Michael Stoll]

With a view of adding a docs#HasEnoughRootsOfUnity instance for docs#Circle, I was trying to define the obvious isomorphism between the docs#rootsOfUnity of Circle and those of the complex numbers, and I found it rather painful:

noncomputable
def Circle.rootsOfUnityMulEquiv {n : ℕ} [NeZero n] : rootsOfUnity n Circle ≃* rootsOfUnity n ℂ := by
  refine MulEquiv.ofBijective (restrictRootsOfUnity coeHom n) ⟨?_, fun ζ ↦ ?_⟩
  · refine (injective_iff_map_eq_one _).mpr fun ζ hζ ↦ Subtype.ext ?_
    rw [Subgroup.coe_one]
    simp only [restrictRootsOfUnity, MonoidHom.coe_mk, OneHom.coe_mk, Subgroup.mk_eq_one,
      ← map_one (Units.map ↑coeHom)] at hζ
    exact (Units.map_injective <| (Set.injective_codRestrict Subtype.property).mp
      fun ⦃_ _⦄ a ↦ a) hζ
  · let z := ζ.val
    have hz : z.val ^ n = 1 := by
      norm_cast
      rw [show z ^ n = 1 from ζ.prop, Units.val_eq_one]
    have hz' : z.val ∈ Submonoid.unitSphere ℂ := by
      simp only [Submonoid.unitSphere, Submonoid.mem_mk, Subsemigroup.mem_mk, mem_sphere_iff_norm,
        sub_zero, Complex.norm_eq_abs]
      apply_fun Complex.abs at hz
      simp only [AbsoluteValue.map_pow, AbsoluteValue.map_one] at hz
      exact (pow_eq_one_iff_of_nonneg (AbsoluteValue.nonneg Complex.abs ↑z) (NeZero.ne n)).mp hz
    let zz : Circle := ⟨z.val, hz'⟩
    have hzz : zz ^ n = 1 := by
      ext
      rw [SubmonoidClass.coe_pow]
      simp only [hz, OneMemClass.coe_one]
    use rootsOfUnity.mkOfPowEq zz hzz
    ext
    simp only [restrictRootsOfUnity_coe_apply, rootsOfUnity.val_mkOfPowEq_coe, coeHom_apply]

I'm feeling that I must have missed a couple tricks here. Any pointers?

[Bhavik Mehta]

@[simp, norm_cast] lemma Circle.coe_pow (z : Circle) (n : ℕ) : (↑(z ^ n) : ℂ) = z ^ n := rfl

@[simp] lemma mem_unitSphere {R} {x} [NormedDivisionRing R] :
    x ∈ Submonoid.unitSphere R ↔ ‖x‖ = 1 := by simp [Submonoid.unitSphere]

noncomputable def Circle.rootsOfUnityMulEquiv {n : ℕ} [NeZero n] :
    rootsOfUnity n Circle ≃* rootsOfUnity n ℂ := by
  refine MulEquiv.ofBijective (restrictRootsOfUnity coeHom n) ⟨?_, ?_⟩
  · refine (Set.injective_codRestrict ?_).2 ?_
    exact (Units.map_injective coe_injective).comp Subtype.coe_injective
  · rintro ⟨ζ, hζ⟩
    suffices ∃ a : Circleˣ, (a : Circle) ^ n = 1 ∧ ((a : Circle) : ℂ) = ζ by
      simpa [Subtype.ext_iff, Units.ext_iff]
    have hζ' : (ζ : ℂ) ∈ Submonoid.unitSphere ℂ := by
      simpa using Complex.norm_eq_one_of_mem_rootsOfUnity hζ
    refine ⟨_root_.toUnits ⟨ζ, hζ'⟩, ?_, by simp⟩
    simpa [Units.ext_iff, Circle.ext_iff, coe_pow] using hζ

Here's my attempt; it seems like those two at the top are missing simp lemmas

[Bhavik Mehta]

Perhaps docs#Complex.norm_eq_one_of_mem_rootsOfUnity was the trick you missed?

[Bhavik Mehta]

now that I look at your code again, I realised I missed the trick of rootsOfUnity.mkOfPowEq:

noncomputable def Circle.rootsOfUnityMulEquiv {n : ℕ} [NeZero n] :
    rootsOfUnity n Circle ≃* rootsOfUnity n ℂ := by
  refine MulEquiv.ofBijective (restrictRootsOfUnity coeHom n) ⟨?_, ?_⟩
  · refine (Set.injective_codRestrict ?_).2 ?_
    exact (Units.map_injective coe_injective).comp Subtype.coe_injective
  · rintro ⟨ζ, hζ⟩
    have hζ' : (ζ : ℂ) ∈ Submonoid.unitSphere ℂ := by
      simpa using Complex.norm_eq_one_of_mem_rootsOfUnity hζ
    exact ⟨rootsOfUnity.mkOfPowEq ⟨ζ, hζ'⟩ (by aesop (add simp Units.ext_iff)), by aesop⟩

[Michael Stoll]

With import Mathlib, your code gives two errors in the playground.

[Junyan Xu]

This shouldn't be noncomputable, right?

[Michael Stoll]

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Circle.instCommGroup', and it does not have executable code

[Michael Stoll]

Complex numbers are not really computable anyway...

[Bhavik Mehta]

Michael Stoll said:

With import Mathlib, your code gives two errors in the playground.

It works fine for me in the playground on latest mathlib. Make sure to include the two lemmas at the beginning of the earlier message.

[Junyan Xu]

I mean you can make it computable using something other than MulEquiv.ofBijective. The backwards map doesn't have good defeq property with it.

[Michael Stoll]

I don't think this would get rid of the noncomputable semigroup instance.

[Bhavik Mehta]

Indeed it doesn't, but you end up with something shorter and with better defeqs for the inverse:

import Mathlib

@[simp, norm_cast] lemma Circle.coe_pow (z : Circle) (n : ℕ) : (↑(z ^ n) : ℂ) = z ^ n := rfl

@[simp] lemma mem_unitSphere {R} {x} [NormedDivisionRing R] :
    x ∈ Submonoid.unitSphere R ↔ ‖x‖ = 1 := by simp [Submonoid.unitSphere]

noncomputable def Circle.rootsOfUnityMulEquiv {n : ℕ} [NeZero n] :
    rootsOfUnity n Circle ≃* rootsOfUnity n ℂ where
  __ := restrictRootsOfUnity coeHom n
  invFun ζ := rootsOfUnity.mkOfPowEq ⟨(ζ : ℂˣ),
      mem_unitSphere.2 (Complex.norm_eq_one_of_mem_rootsOfUnity ζ.2)⟩
      (by aesop (add simp Units.ext_iff))
  left_inv ζ := by ext; simp
  right_inv ζ := by ext; simp

[Junyan Xu]

Interesting, even if I do

def Circle.rootsOfUnityMulEquiv {n : ℕ} [NeZero n] :
    rootsOfUnity n Circle ≃* rootsOfUnity n ℂ where
  toFun x := ⟨⟨x.1, x.1.inv, sorry, sorry⟩, sorry⟩
  invFun x := ⟨⟨⟨x.1, sorry⟩, ⟨x.1.inv, sorry⟩, sorry, sorry⟩, sorry⟩
  left_inv := sorry
  right_inv := sorry
  map_mul' := sorry

Lean still complains

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Circle.instCommGroup', and it does not have executable code

[Yuyang Zhao]

This may be because docs#CauSeq.Completion.instInvCauchy is not computable. It may be possible to define computable inv that require a non-zero proof, and thus obtain computable docs#Circle.instCommGroup.

[Junyan Xu]

The inv I use is docs#Units.inv which should absolutely be computable ... And the ⁻¹ on Units should also be computable.