PathConnectedSpace ℂˣ

Stream: Is there code for X?

[Andrew Yang]

Do we have this? If not, where should this go?
Is there a better proof that avoids such a large import?
Or is there something more general that I should be proving instead?

import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.NormedSpace.Connected
import Mathlib.LinearAlgebra.Complex.FiniteDimensional

instance : PathConnectedSpace ℂˣ :=
  have : PathConnectedSpace { z : ℂ // z ≠ 0 } :=
    isPathConnected_iff_pathConnectedSpace (F := { z : ℂ | z ≠ 0 }).mp
    (isPathConnected_compl_singleton_of_one_lt_rank (by simp) _)
  let e := unitsHomeomorphNeZero (G₀ := ℂ)
  e.symm.surjective.pathConnectedSpace e.symm.continuous

[Yury G. Kudryashov]

Removing a point from a tvs of dimension larger than one gives you a path connected space

[Jireh Loreaux]

That's the result Andrew used already.

[Kenny Lau]

exp is surjective, C is path connected

[Andrew Yang]

That sounds like more import but I could try.

[Andrew Yang]

@loogle Complex.exp, Function.Surjective

[Andrew Yang]

@loogle Complex.exp, Function.Surjective

Edit: It should be docs#Complex.range_exp

[loogle]

:shrug: nothing found

[Andrew Yang]

Would people prefer this set of imports more?

import Mathlib.Analysis.Convex.PathConnected
import Mathlib.Analysis.SpecialFunctions.Complex.Log

instance : PathConnectedSpace ℂ :=
  IsTopologicalAddGroup.pathConnectedSpace

instance : PathConnectedSpace ℂˣ :=
  have : PathConnectedSpace { z : ℂ // z ≠ 0 } :=
    isPathConnected_iff_pathConnectedSpace (F := {0}ᶜ).mp
    (by rw [← Complex.range_exp]; exact isPathConnected_range Complex.continuous_exp)
  let e := unitsHomeomorphNeZero (G₀ := ℂ)
  e.symm.surjective.pathConnectedSpace e.symm.continuous

Perhaps I can import the former into the latter and put it there?

[Kenny Lau]

I tried it myself (unfortunately my attempt is much longer) and found some holes in the API:

import Mathlib.Analysis.CStarAlgebra.Classes
import Mathlib.Analysis.Calculus.MeanValue
import Mathlib.Analysis.SpecialFunctions.Complex.Log

open Complex

noncomputable def cexp' (z : ℂ) : ℂˣ :=
  Units.mk0 (cexp z) (by simp)

theorem cexp'_surjective : cexp'.Surjective :=
  fun z ↦ ⟨log z, Units.ext <| exp_log z.ne_zero⟩

@[simp] lemma unitsHomeomorphNeZero_apply_coe
    {G₀ : Type*} [GroupWithZero G₀] [TopologicalSpace G₀] [ContinuousInv₀ G₀] (x : G₀ˣ) :
    (unitsHomeomorphNeZero (G₀ := G₀)) x = (x : G₀) :=
  rfl

@[simp] lemma unitsHomeomorphNeZero_symm_apply
    {G₀ : Type*} [GroupWithZero G₀] [TopologicalSpace G₀] [ContinuousInv₀ G₀]
    (x : {x : G₀ // x ≠ 0}) :
    (unitsHomeomorphNeZero (G₀ := G₀)).symm x = .mk0 x x.2 :=
  (Equiv.symm_apply_eq _).mpr rfl

theorem cexp'_eq : cexp' =
    unitsHomeomorphNeZero.symm ∘ Equiv.setCongr (by ext; aesop) ∘ Set.rangeFactorization cexp :=
  by ext; unfold cexp'; simp

#check Homeomorph.subtype

@[fun_prop] theorem cexp'_continuous : Continuous cexp' := by
  rw [cexp'_eq]; sorry

instance : PathConnectedSpace ℂˣ :=
  cexp'_surjective.pathConnectedSpace cexp'_continuous

#min_imports

[Kenny Lau]

Andrew Yang said:

Would people prefer this set of imports more?

... yeah... i think we can consider "exp" to be basic knowledge...

[Kenny Lau]

@Andrew Yang $(t,r) \mapsto (\frac{2tr}{t^{2}+1},\frac{(t^{2}-1)r}{t^{2}+1})$ defines a surjection $\mathbb{R} \times \mathbb{R}_{>0} \to \mathbb{C}^\times$

[Kenny Lau]

(i basically drew a unit circle using the AG trick and then multiplied by r)

[Kenny Lau]

oh wait, no, the AG trick doesn't produce a circle lol

[Aaron Liu]

what's AG

[Aaron Liu]

algebraic geometry?

[Kenny Lau]

algebraic geometry

[Kenny Lau]

(-1,0) is on the unit circle, and any line through it has to intersect the circle at exactly one other point, and this defines a rational parametrisation of the circle

[Aaron Liu]

is that the stereographic projection?

[Aaron Liu]

maybe not quite

[Kenny Lau]

yeah

[Aaron Liu]

has stereographic projection been reduced to an "AG trick" now

[Kenny Lau]

I think the amount of effort to find a "shorter" proof might be the same amount of effort to just draw a path between any two points, lol

[Aaron Liu]

yeah just draw a path it's not that hard

[Aaron Liu]

although I don't think the path can depend continuously on the desired endpoints

[Andrew Yang]

Here's a PR with a stupid proof: #30418. Do people prefer this or a better proof in a later file?

[Kenny Lau]

nice proof!