TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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.

Equivalent characterisations of a homologically simply connected domain

Statement

Let $U$ be a complex domain. The following are equivalent.

$U$ is homologically simply connected: every complex chain which is a cycle with trace in $U$ is null-homologous in $U$ .
Every holomorphic function on $U$ has a primitive on $U$ .
Every holomorphic nowhere-zero function on $U$ has a holomorphic logarithm on $U$ .
For every $p \in C ∖ U$ , the function $z \mapsto 1 / (z - p)$ has a primitive on $U$ .
$\int_{Γ} f (z) d z = 0$ for every holomorphic $f$ on $U$ and every cycle $Γ$ with trace in $U$ .
$\int_{Γ} \frac{d z}{z - p} = 0$ for every cycle $Γ$ with trace in $U$ and every $p \in C ∖ U$ .

Facts & Assumptions

Given: A complex domain $U$ .

[L1]

A complex domain is homologically simply connected when every cycle with trace in it is null-homologous in it (Homologically simply connected complex domains), and a cycle $Γ$ with trace in $Ω$ is null-homologous in $Ω$ when $n (Γ, p) = 0$ for every $p \in C ∖ Ω$ (Null-homologous cycles and homologous cycles in an open set).

[L2]

Every holomorphic function on a homologically simply connected complex domain has a primitive there (Every holomorphic function on a homologically simply connected domain has a primitive).

[L3]

If $Γ$ is a cycle whose trace lies in an open $V$ and $F$ is a primitive on $V$ of a continuous $f$ with $F^{'} = f$ continuous, then $\int_{Γ} f d z = 0$ (The integral of a continuous derivative over a cycle is zero).

[L4]

If $L$ and $h$ are holomorphic on an open set with $\exp \circ L = h$ , then $h$ is nowhere zero and $L^{'} = h^{'} / h$ ; for $h (z) = z - p$ on a set missing $p$ this gives $L^{'} (z) = 1 / (z - p)$ (A holomorphic logarithm is a primitive of the logarithmic derivative).

[L5]

$n (Γ, p) = (2 π i)^{- 1} \int_{Γ} d z / (z - p)$ for a chain $Γ$ and $p \notin Γ^{*}$ (Integration over a complex chain and the index of a chain), a chain being a finite list of integer-weighted complex contours (Complex chains, their traces, and cycles).

[L6]

A primitive of $f$ on $V$ is a holomorphic $F$ with $F^{'} = f$ on $V$ (A primitive of a complex function on an open set).

[L7]

Linear combinations, products and nonvanishing quotients of functions complex differentiable at a point are complex differentiable there; constants have derivative $0$ and the identity has derivative $1$ (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[L8]

A complex domain is a nonempty, connected, open subset of $C$ (A complex domain is a nonempty connected open subset of $C$ ).

[L9]

The complex exponential is entire with $\exp^{'} = \exp$ (The complex exponential is entire and its complex derivative is itself), and if $f : V \to W$ and $g : W \to C$ are complex differentiable at the relevant points, then $(g \circ f)^{'} (a) = g^{'} (f (a)) f^{'} (a)$ (The chain rule for complex derivatives).

[L10]

The complex exponential maps $C$ onto $C ∖ {0}$ (The complex exponential maps $C$ onto $C ∖ {0}$ ).

[L11]

A holomorphic function with vanishing derivative on a complex domain is constant there (A holomorphic function with zero derivative on a domain is constant).

[L12]

For real $x, y$ , $∣ \exp (x + i y) ∣ = e^{x}$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[L13]

A complex differentiable function is continuous (Complex differentiability at a point implies continuity there), and every holomorphic function has complex derivatives of all natural orders locally (All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle).

[L14]

$\exp (z + w) = \exp z \exp w$ , so $\exp (w) \exp (- w) = 1$ for every complex $w$ ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential).

Proof

technique · direct

1.1

Condition 1 implies condition 2: this is [L2] applied to the domain $U$ , which condition 1 makes homologically simply connected by [L1].

givenL1L2

1.2

Condition 2 implies condition 3, argued from condition 2 alone and not from the theorem about homologically simply connected domains. Let $f$ be holomorphic and nowhere zero on $U$ ; by [L13] the derivative $f^{'}$ is holomorphic, so $f^{'} / f$ is holomorphic on $U$ by [L7], and condition 2 supplies a primitive $G$ with $G^{'} = f^{'} / f$ ([L6]). Fix $z_{0} \in U$ , nonempty by [L8], and use [L10] to pick $w_{0}$ with $\exp (w_{0}) = f (z_{0})$ ; put $F = G - G (z_{0}) + w_{0}$ . Since [L12] shows the exponential never vanishes, $\exp (- F)$ is holomorphic and nowhere zero, so $f \exp (- F)$ is holomorphic with derivative $(f^{'} - f (f^{'} / f)) \exp (- F) = 0$ on $U$ by [L7] and [L9], hence constant by [L11] and [L8]; its value at $z_{0}$ is $\exp (w_{0}) \exp (- w_{0}) = 1$ by [L14], so $\exp \circ F = f$ .

givenL6L7L8L9L10L11L12L13L14

1.3

Condition 3 implies condition 4. Let $p \in C ∖ U$ ; then $h (z) = z - p$ is holomorphic and nowhere zero on $U$ by [L7], so condition 3 gives a holomorphic $g$ on $U$ with $\exp \circ g = h$ , and [L4] gives $g^{'} (z) = 1 / (z - p)$ ; thus $g$ is a primitive of $z \mapsto 1 / (z - p)$ on $U$ in the sense of [L6].

givenL4L6L7

1.4

Condition 4 implies condition 6. Let $Γ$ be a cycle with trace in $U$ and $p \in C ∖ U$ . Condition 4 supplies a primitive of $z \mapsto 1 / (z - p)$ on the open set $U$ , whose derivative is that function and is continuous by [L7] and [L13]; so [L3] gives $\int_{Γ} d z / (z - p) = 0$ .

givenL3L6L7L13

1.5

Condition 6 implies condition 1. For a cycle $Γ$ with trace in $U$ and $p \in C ∖ U$ , condition 6 and [L5] give $n (Γ, p) = 0$ ; by [L1] that is exactly null-homology of $Γ$ in $U$ , for every such $Γ$ , which is condition 1.

givenL1L5

1.6

Condition 2 implies condition 5. Given a holomorphic $f$ on $U$ and a cycle $Γ$ with trace in $U$ , condition 2 supplies a primitive $F$ with $F^{'} = f$ , continuous by [L13]; so [L3] gives $\int_{Γ} f d z = 0$ .

givenL3L6L13

1.7

Condition 5 implies condition 6. For $p \in C ∖ U$ the function $z \mapsto 1 / (z - p)$ is holomorphic on $U$ by [L7], so condition 5 applied to it gives $\int_{Γ} d z / (z - p) = 0$ for every cycle $Γ$ with trace in $U$ .

givenL5L7

2.1

Steps 1.1, 1.2, 1.3, 1.4 and 1.5 close the cycle of implications $1 \Rightarrow 2 \Rightarrow 3 \Rightarrow 4 \Rightarrow 6 \Rightarrow 1$ , so conditions 1, 2, 3, 4 and 6 are equivalent; steps 1.6 and 1.7 insert condition 5 between conditions 2 and 6, which are already known equivalent, so all six conditions are equivalent.

step 1.1step 1.2step 1.3step 1.4step 1.5step 1.6step 1.7∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

71 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

L. V. Ahlfors, Complex Analysis, 3rd ed., Ch. 4 §4.4, Theorem 14 (standard reference, not scraped)
M. Weber, Complex Analysis (Indiana University), Ch. 4 §4.1 (standard reference, not scraped)