Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)audited 2026-10-08
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.

A degree-one holomorphic map of compact Riemann surfaces is an isomorphism

Statement

Let f:X→Y be a nonconstant holomorphic map between compact connected Riemann surfaces (Holomorphic maps and meromorphic functions on Riemann surfaces, Riemann surfaces and holomorphic atlases). Then f is proper and has a degree d as in Degree of a proper holomorphic map of Riemann surfaces. If d=1, then f is bijective and its set-theoretic inverse g:Y→X is holomorphic. Thus g∘f=idX and f∘g=idY, so f is an isomorphism of Riemann surfaces.

Facts & Assumptions

Given: A nonconstant holomorphic map f:X→Y between compact connected Riemann surfaces.

[F1]

The source X is compact, and the target Y is Hausdorff because it is a Riemann surface (Riemann surfaces and holomorphic atlases).

[F2]

A holomorphic map of Riemann surfaces is continuous (Holomorphic maps and meromorphic functions on Riemann surfaces).

[F4]

For a proper nonconstant holomorphic map between connected Riemann surfaces, every fibre is nonempty and finite, and the degree is the constant weighted count ∑x∈f−1(y)ex(f) (Degree of a proper holomorphic map of Riemann surfaces).

[F5]

Each ramification index ex(f) is a positive integer, and ex(f)=1 exactly when f is a local biholomorphism at x (Ramification index, ramification order and branch value).

[F6]

In suitable centred charts, f is locally z↦zex(f); in particular, if ex(f)=1, the local inverse is holomorphic (Local power-map normal form on Riemann surfaces, Biholomorphic maps between complex domains).

Proof

technique · direct
1.1F1F2F3F4

Let K⊆Y be compact. By [F3], K is closed in Y, and by [F2] its preimage f−1(K) is closed in X. Since X is compact by [F1], f−1(K) is compact. This holds for every compact K, so f is proper and the degree in [F4] is defined.

1.2F4F5

Suppose d=1. For every y∈Y, [F4] gives a nonempty finite fibre with ∑x∈f−1(y)ex(f)=1. Each summand is a positive integer by [F5], so the fibre has exactly one point, with ramification index 1. Thus f is bijective and is unramified at every point.

2.1F6step 1.2∎

For each x∈X, [F6] gives charts in which f is z↦z near x, so it has a holomorphic local inverse near f(x). The set-theoretic inverse g from step 1.2 agrees with each such local inverse on its domain, hence is holomorphic on all of Y. Its defining identities g∘f=idX and f∘g=idY show that f is an isomorphism.

Depends on

Used by

Dependency tree · two levels

31 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