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.
Holomorphic inverse function theorem and local-degree criterion
Statement
For a nonconstant holomorphic map, nonzero derivative, local degree one, local injectivity, and local biholomorphy are equivalent.
Precisely, let be nonconstant and holomorphic on a complex domain , and let . The following are equivalent:
- ;
- (Local degree of a nonconstant holomorphic map);
- is locally injective at (Locally injective holomorphic maps);
- is biholomorphic between neighbourhoods of and (Biholomorphic maps between complex domains).
For a local inverse , one has throughout its domain.
Facts & Assumptions
Given: A nonconstant holomorphic function on a complex domain and a point . The complex chain rule applies to inverse identities (The chain rule for complex derivatives).
If is holomorphic near and , then is biholomorphic between neighbourhoods of and (A nonzero complex derivative gives a local biholomorphism).
For every neighbourhood of , there are a smaller open neighbourhood and a real such that every with , where , has exactly distinct preimages in (A local degree-m holomorphic map has m nearby sheets).
A holomorphic function has finite order at exactly when, on some neighbourhood of , it is with holomorphic and (The order of a zero is the exponent in its local holomorphic factorization).
Proof
For the equivalence between claims 1 and 2, [L3] gives with and . If , differentiation at gives ; if , it gives . Thus exactly when .
For the implication from claim 1 to claim 4, [L1] directly makes biholomorphic between neighbourhoods of and .
For the implication from claim 4 to claim 3, a biholomorphic restriction is bijective and hence injective on its source neighbourhood.
For the converse implication from claim 3 back to claim 2, suppose is injective on a neighbourhood of . If , take and from [L2] and put . Then has distinct preimages in , contradicting injectivity on . Since is positive, , and step 1.1 then gives .
For the derivative formula, let be the inverse supplied in step 1.2. Differentiating gives , so, writing , one obtains .
Depends on
- Locally injective holomorphic maps
- Biholomorphic maps between complex domains
- Local degree of a nonconstant holomorphic map
- The order of a zero is the exponent in its local holomorphic factorization
- A nonzero complex derivative gives a local biholomorphism
- A local degree-m holomorphic map has m nearby sheets
- The chain rule for complex derivatives
Used by
Dependency tree · two levels
28 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
- B. V. Shabat, Introduction to Complex Analysis, Theorem 1.10 (standard reference, not scraped)
- J. Lebl, Guide to Cultivating Complex Analysis, §5.6 (standard reference, not scraped)