Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passaudited 2026-08-28
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Every biholomorphic self-map of the punctured plane is of the form az or a/z

Statement

Every biholomorphic self-map of the punctured plane C× has the form zaz or za/z with aC×.

Facts & Assumptions

Given: A biholomorphic map f:C×C×.

[L1]

Meromorphic self-maps of the sphere are rational, and a bijective rational sphere map has degree 1 (Meromorphic functions on the Riemann sphere are exactly the rational functions, A nonconstant rational map has total fibre multiplicity equal to its degree).

[L2]

A bounded holomorphic function on a punctured disc has a removable singularity (Characterizations of removable singularities).

Proof

technique · direct
1.1

If zn0 in C× and f(zn)aC×, continuity of f1 on C× forces zn=f1(f(zn))f1(a)C×, a contradiction. Hence every cluster value of f(z) as z0 lies in {0,}. If both 0 and were cluster values, then every sufficiently small punctured disc would have image meeting both {w<1} and {w>1}; connectedness of that image would then produce points with f(z)=1 approaching 0, giving a finite nonzero cluster value after all. Therefore f(z) tends to a single limit 0{0,} as z0. The same argument applied to zf(1/z) shows that f(z) tends to a single limit {0,} as z.

givenassume-contrachoosealgebradischarge-contradiction
2.1

Let F be the extension of f to C^ with F(0)=0 and F()=, and let G be the analogous extension of f1. Step 1.1 gives continuity of both extensions at the added points, and on the dense subset C× one has GF=id=FG. By continuity the same identities hold on all of C^, so F is a sphere homeomorphism and F({0,})={0,}.

step 1.1given
3.1

Near each of 0 and , the homeomorphism F lands either in a bounded finite chart or in a neighbourhood of . In the first case the corresponding chart expression is bounded near the puncture and extends holomorphically by [L2]; in the second case its reciprocal is bounded and again extends holomorphically by [L2]. Thus F is meromorphic at both added points, and therefore on the whole sphere.

L2step 2.1given
4.1

Fact [L1] makes F a rational sphere map of degree 1, hence Möbius. A Möbius map preserving the set {0,} is either zaz or za/z with a0, and restricting back to C× gives exactly the claimed automorphisms.

L1step 2.1givenalgebra

Depends on

Used by

Dependency tree · two levels

35 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources