3
$\begingroup$

First of all, my question is in the context of formalising proofs in the proof assistant Isabelle/HOL, so my questions are a bit guided by what material we have in the complex analysis library there.

Apostol's ‘Modular Functions and Dirichlet Series in Number Theory’ has a short proof of Picard's Little Theorem based on Klein's $J$ function (Theorem 2.10, end of Chapter 2). It starts like this:

If $g(z)$ is an entire function that never attains the values 0 and 1. Then $J'(z) \neq 0$ for all values in the image of $g$, and thus there exists an entire function $h$ such that $J(h(z)) = g(z)$.

It is clear that such a function $h$ exists locally at every $z$. Apostol says that it then also exists globally due to the Monodromy Theorem, but he does not give any details.

Now, what I have been able to do is the following:

  1. Prove that $J$ is a covering map from $\{z\mid \text{Im}(z)>0,\ J(z)\notin\{0,1\}\}$ to $\mathbb{C}\setminus\{0,1\}$
  2. Use a theorem that states that if $f : C \to S$ is a holomorphic covering map and $g : U\to S$ is holomorphic with $U$ simply connected then there exists a holomorphic map $h : U\to C$ with $f(h(z)) = g(z)$.

Now the problem with this is that the proof for 1. was fairly tedious – much more so than what Apostol's style would suggest. Am I making my life more difficult than necessary here? Is there an easier way to prove that $J$ is a covering map than unfolding the definition of ‘covering map’ and proving away? Is there a way to do this without proving that $J$ is a covering map at all?

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ Definitely you need something more than there being no critical values in order to know that the map is a covering map; you also need to know that there are no asymptotic values. Without having looked at Apostol's book, it seems that this proof does indeed omit some important details. As mentioned by Alex, it would be easier to use a universal covering, and there are other proofs available - how feasible these are depends on what you have already available in the complex analysis library, of course! $\endgroup$
    – Lasse Rempe
    Commented Apr 25, 2022 at 10:40
  • $\begingroup$ We actually already had Little Picard (and even Big Picard). The purpose of this exercise was really more to see if we can formalise Apostol's "simple" proof as it is written in the book as well. Alas, it seems that it is not quite as simple as he makes it out to be. But I did manage to formalise it just fine, I was just very perplexed at having to prove the covering map thing. Thanks for the context! $\endgroup$
    – Manuel Eberl
    Commented Apr 26, 2022 at 22:33
  • $\begingroup$ I think the point of the proof is that, once you know that there is a covering map from the disc to the doubly-punctured plane, the proof is rather simple. The fact that the doubly-punctured plane is covered by the disc is important in itself (it is a special case of the Uniformisation Theorem, and once you know it you can prove that theorem for the case of any plane domain with arguments using normal families), and it is classical. $\endgroup$
    – Lasse Rempe
    Commented Apr 28, 2022 at 8:38
  • $\begingroup$ PS I am interested to know which proof you used in your prior formalisation of Picard? $\endgroup$
    – Lasse Rempe
    Commented Apr 28, 2022 at 8:40
  • 1
    $\begingroup$ It wasn't formalised by me; it was first formalised by John Harrison in HOL Light and then ported over to Isabelle/HOL by Larry Paulson. $\endgroup$
    – Manuel Eberl
    Commented May 10, 2022 at 14:39

1 Answer 1

Reset to default
2
$\begingroup$

The usual proof of Picard's theorem along these lines used another modular function which is called $\lambda$ and which is related to $J$ by $$J=\frac{4}{27}\frac{(1-\lambda+\lambda^2)^3}{\lambda^2(1-\lambda)^2}.$$ This function $\lambda$ is simpler because it performs a $universal$ covering of $C\backslash\{0,1\}$ by the upper half-plane. See, for example, Ahlfors, Complex Analysis, pp. 306-308.

The interesting question whether one can prove Picard's theorem without the use of modular functions and coverings arose immediately after publication of Picard's proof, since mathematicians were puzzled by this proof, and found it unnatural and mysterious. Nowadays very many different proofs are available, for a brief survey of them see:

Theorems with many distinct proofs

Most of them use no coverings at all, and no monodromy; others use a much simpler universal covering $\exp: C\to C\backslash\{0,1\}$.

Improve this answer
$\endgroup$
4
  • $\begingroup$ I don't understand the last comment about $\exp$ at all. Surely $\exp$ does not omit 1? $\endgroup$
    – Manuel Eberl
    Commented Apr 21, 2022 at 8:53
  • $\begingroup$ Also thanks for bringing $\lambda$ to my attention, but does all of this mean that if you want to do the proof with $J$ then you need to prove that $J$ is a covering map first? And if so, is the only way to do it the hard way, i.e. by showing explicitly that for each value in the range a corresponding disjoint union of neighbourhoods in the preimage exists? $\endgroup$
    – Manuel Eberl
    Commented Apr 21, 2022 at 8:54
  • 1
    $\begingroup$ @Manuel Eberl: Look at the "Zalcman's Elementary proof" in my reference. If $f$ omits $0,1,\infty$, then $f=\exp(g)$ where $g$ omits the sequence $2\pi in$. This is the beginning of Zalcman's proof. $\endgroup$
    – Alexandre Eremenko
    Commented Apr 21, 2022 at 14:17
  • $\begingroup$ @Manuel Eberl: I only wanted to say that $\lambda$ is a simpler function than $J$ since $\lambda$ is a universal covering, and $J$ is a ramified covering. $\endgroup$
    – Alexandre Eremenko
    Commented Apr 21, 2022 at 14:20

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .