No continuous, injective maps `Circle → ℝ `

Stream: Is there code for X?

[Geoffrey Irving]

Do we have either exactly this result, or a brief way to show it? I can do it with case analysis, but I'd prefer not to:

import Mathlib

lemma Circle.not_continuous_or_not_injective {f : Circle → ℝ} :
    ¬Continuous f ∨ ¬f.Injective := by sorry

[Aaron Liu]

oh I did this once before

[Aaron Liu]

I don't have the proof on me now but I can pull it up when I get home

[Aaron Liu]

it's a very bad proof

[Aaron Liu]

I don't think it's in mathlib

[Geoffrey Irving]

Aaron Liu said:

it's a very bad proof

Yes, this is what I am afraid of. :)

[Geoffrey Irving]

Simple to state though. :)

[Geoffrey Irving]

Actually there is a nice argument in terms of connectivity (courtesy of GPT-5). I will write it down.

[Yaël Dillies]

Is this not basically IVT twice?

[Geoffrey Irving]

Yes, but the direct IVT version has to deal with wraparounds and such. The direct connectivity argument is cleaner: you just need that the circle minus a point is connected.

[Aaron Liu]

ok I actually have the proof right here on my phone but the phone is not connected to the internet and I have no way of transferring it to the macbook

[Aaron Liu]

or I thought I did but I can't find it anymore

[Aaron Liu]

I'll just pull it up when I get home

[Yaël Dillies]

Aaron Liu said:

the phone is not connected

Is this because you removed a point?

[Geoffrey Irving]

Indeed, removing any countable number of points leaves a phone connected.

[Aaron Liu]

here's roughly the argument I used to show that a continuous function from the circle to the reals is not injective

• assume it is injective, want to derive a contradiction
• the circle is compact, so its image under a continuous function is compact
• the circle is connected, so its image under a continuous function is connected
• heine-borel says the image is closed and bounded, and closed bounded sets in the real numbers are intervals
• by precomposing with docs#AddCircle.continuous_equivIco_symm we get a continuous function from a closed-open real interval to a closed real interval
• docs#Continuous.strictMono_of_inj says this is strct mono or strict anti
• ???
• image of endpoint is strictly less than itself

[Geoffrey Irving]

Screenshot 2025-08-12 at 5.59.22 PM.png

I think I'll formalise this connectivity version, since I don't need to construct those functions. I do need a bunch of little facts about the Circle, but those seem clean.

[Junyan Xu]

I think you can use Continuous.isClosedEmbedding and Topology.IsEmbedding.toHomeomorph to get a homeomorphism between the circle and some subset of the reals. As noted, the former remains connected while the latter becomes disconnected after removing a point.

[Jireh Loreaux]

(deleted) nevermind, you can choose a different point.

[Junyan Xu]

I should have said the former remains connected after removing any point, and the latter becomes disconnected after removing some point :) The image is uncountable by virtue of injectivity so of course you can find three distinct points.

[Geoffrey Irving]

instance : Infinite Circle := by
  rw [Circle.argEquiv.infinite_iff]
  apply Set.Infinite.to_subtype
  exact Ioc_infinite (by linarith [Real.pi_pos])

lemma Circle.connected_compl_singleton (s : Circle) : IsConnected {s}ᶜ := by
  have e : {s}ᶜ = (fun t ↦ -s * Circle.exp t) '' Ioo (-π) π := by
    ext z
    simp only [mem_compl_iff, mem_singleton_iff, neg_mul, mem_image, mem_Ioo]
    constructor
    · intro zs
      refine ⟨(z / -s).val.arg, ?_⟩
      simp only [Complex.neg_pi_lt_arg, true_and, (Complex.arg_le_pi _).lt_iff_ne,
        Circle.exp_arg]
      simp only [← Circle.arg_neg_one, ne_eq, Circle.arg_eq_arg]
      simpa only [div_neg, neg_inj, mul_neg, mul_div_cancel, neg_neg, and_true, div_eq_one]
    · intro ⟨t,⟨lo,hi⟩,e⟩
      simp only [← e, neg_mul_eq_mul_neg, mul_eq_left]
      simp only [neg_eq_iff_eq_neg, Circle.ext_iff, coe_exp, coe_neg, OneMemClass.coe_one, ne_eq]
      rw [← Complex.exp_pi_mul_I]
      by_contra h
      replace h := Complex.exp_inj_of_neg_pi_lt_of_le_pi ?_ ?_ ?_ ?_ h
      · simp only [mul_eq_mul_right_iff, Complex.ofReal_inj, Complex.I_ne_zero, or_false] at h
        simp only [h, lt_self_iff_false] at hi
      · simp [lo]
      · simp [hi.le]
      · simp [Real.pi_pos]
      · simp
  rw [e]
  apply IsConnected.image
  · exact isConnected_Ioo (by linarith [Real.pi_pos])
  · fun_prop

lemma Circle.not_continuous_or_not_injective {f : Circle → ℝ} (cont : Continuous f)
    (inj : f.Injective) : False := by
  obtain ⟨a,_,lo⟩ := isCompact_univ.exists_isMinOn univ_nonempty cont.continuousOn
  obtain ⟨b,_,hi⟩ := isCompact_univ.exists_isMaxOn univ_nonempty cont.continuousOn
  simp only [isMinOn_iff, mem_univ, forall_const, isMaxOn_iff] at lo hi
  by_cases ab : f a = f b
  · have e : ∀ x y, f x = f y := by intro x y; linarith [lo x, hi x, lo y, hi y]
    specialize e (-1) 1
    simp only [inj.eq_iff, neg_ne] at e
  · replace ab : f a < f b := Ne.lt_of_le ab (lo b)
    obtain ⟨x,m⟩ := Infinite.exists_notMem_finset {a, b}
    simp only [Finset.mem_insert, Finset.mem_singleton, not_or, ← ne_eq] at m
    have ax : f a < f x := (inj.ne_iff.mpr m.1).symm.lt_of_le (lo x)
    have xb : f x < f b := (inj.ne_iff.mpr m.2).lt_of_le (hi x)
    have connect : (f '' {x}ᶜ).OrdConnected :=
      ((Circle.connected_compl_singleton x).image _ cont.continuousOn).isPreconnected.ordConnected
    have mem := connect.out (x := f a) (y := f b) (by aesop) (by aesop) ⟨ax.le, xb.le⟩
    simp only [mem_image, mem_compl_iff, mem_singleton_iff, inj.eq_iff, not_and_self,
      exists_const] at mem

[Geoffrey Irving]

I'll package up the other dependencies momentarily (little facts about Circle).

[Geoffrey Irving]

Here's a standalone file with all the little Circle facts, and only Mathlib dependencies otherwise:

https://github.com/girving/ray/blob/e1fb4aa33a5c78735ab8aeeebb11c77eb8b3ecb0/Ray/Misc/Circle.lean#L88

[Geoffrey Irving]

And the corollary I wanted:

/-- If `f : Circle → Circle` is continuous and injective, it is bijective -/
lemma Circle.bijective_of_injective {f : Circle → Circle} (cont : Continuous f)
    (inj : f.Injective) : f.Bijective := by
  refine ⟨inj, ?_⟩
  intro c
  by_contra s
  simp only [not_exists] at s
  set g : Circle → ℝ := fun z ↦ arg (f z / -c : Circle)
  have gc : Continuous g := by
    rw [continuous_iff_continuousAt]
    intro x
    refine (Complex.continuousAt_arg ?_).comp (by fun_prop)
    simp only [Circle.mem_slitPlane, ne_eq, div_eq_iff_eq_mul', neg_mul_neg, mul_one, s,
      not_false_eq_true]
  have gi : g.Injective := Circle.injective_arg.comp (div_left_injective.comp inj)
  exact Circle.not_continuous_or_not_injective gc gi

[Junyan Xu]

AddCircle has more APIs that makes isConnected_compl_singleton easy:

import Mathlib.Analysis.SpecialFunctions.Complex.Circle

lemma AddCircle.isConnected_compl_singleton {T : ℝ} [h : Fact (0 < T)]
    (s : AddCircle T) : IsConnected {s}ᶜ := by
  obtain ⟨s⟩ := s
  have := isConnected_iff_connectedSpace.mp
    (isConnected_Ioo <| show s < s + T by linarith [h.out])
  have : Set.Ioo s (s + T) ≃ₜ _ :=
    (AddCircle.partialHomeomorphCoe T s).toHomeomorphSourceTarget
  exact isConnected_iff_connectedSpace.mpr <|
    this.surjective.connectedSpace this.continuous

lemma Circle.isConnected_compl_singleton (s : Circle) : IsConnected {s}ᶜ := by
  have e := AddCircle.homeomorphCircle'
  have : Fact (0 < 2 * Real.pi) := ⟨by simp [Real.pi_pos]⟩
  rw [← e.isConnected_preimage]
  convert AddCircle.isConnected_compl_singleton (e.symm s)
  aesop