ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-21

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.

Maps between connected circle coverings are governed by divisibility

Example

For positive integers $m, n$ , let $E_{m}$ and $E_{n}$ be the based connected circle coverings classified by $m Z$ and $n Z$ . There is a based covering morphism

$E_{m} ⟶ E_{n}$

exactly when $n ∣ m$ . It is unique when it exists. If $m = n q$ , then this morphism has $q$ sheets; in particular, $q = 1$ gives a based covering isomorphism.

Facts & Assumptions

Given: Positive integers $m, n$ and the classified based covers $E_{m}, E_{n}$ .

[L1]

Over a path-connected locally path-connected base, a unique based morphism between coverings with connected total spaces exists exactly when the source induced subgroup is contained in the target induced subgroup, and such a morphism is a surjective covering map (A based morphism between connected coverings exists exactly when the induced subgroups are included).

[F1]

The relation $n ∣ m$ means that $m = n q$ for some integer $q$ (Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

[F2]

For a covering with nonempty path-connected total space, the sheet number equals the index of its induced fundamental-group subgroup (For a nonempty path-connected total space, a covering fibre is in bijection with the right cosets of the induced fundamental-group subgroup).

[F3]

For a positive integer $q$ , every integer has a unique remainder $r$ with $0 \leq r < q$ modulo $q$ (Division with remainder in $Z$ : for $a \in Z$ and $b > 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < b$ ).

[F4]

A covering map induces an injective homomorphism on fundamental groups (A covering map induces an injective homomorphism on fundamental groups).

[F5]

Induced fundamental-group homomorphisms respect composition (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).

[F6]

Open quotient arcs of length below one are homeomorphic to real intervals (The quotient map is open, and every interval shorter than one embeds in $R / Z$ ).

[F7]

Every nonempty convex real interval is path-connected (Every nonempty convex subset of $R^{n}$ is simply connected).

[F8]

Local path-connectedness means that every neighbourhood contains an open path-connected neighbourhood (Locally connected and locally path-connected spaces: a neighbourhood base of open connected, respectively open path-connected, sets at every point).

[F9]

Local path-connectedness lifts from the base of a covering to its total space (Local path-connectedness lifts and descends along covering maps).

[F10]

A connected locally path-connected space is path-connected (A connected, locally path-connected space is path-connected, because its path components are open).

[F11]

The quotient circle $R / Z$ is path-connected ( $R / Z$ is compact and path-connected).

Verification

technique · direct

1.1

For the forward direction, $m Z \subseteq n Z$ puts $m \in n Z$ , so $m = n q$ for an integer $q$ and $n ∣ m$ . For the reverse direction, if $m = n q$ , then every $m k = n (q k)$ is in $n Z$ , so $m Z \subseteq n Z$ . Since $m, n > 0$ , the quotient $q = m / n$ is positive.

F1algebra

2.1

The quotient circle is path-connected by [F11] and locally path-connected because [F6] gives arbitrarily small open neighbourhoods homeomorphic to convex intervals, which are path-connected by [F7], so [F8] applies. Hence [L1] and step 1.1 give a unique based morphism $E_{m} \to E_{n}$ exactly when $n ∣ m$ .

step 1.1L1F6F7F8F11

3.1

Suppose $m = n q$ . The local path-connectedness established in step 2.1 lifts to $E_{m}$ by [F9], and connectedness then makes $E_{m}$ path-connected by [F10]. Functoriality for the morphism $f : E_{m} \to E_{n}$ gives $(p_{n})_{*} f_{*} = (p_{m})_{*}$ , and [F4] identifies $π_{1} (E_{n})$ with $n Z$ and $f_{*} π_{1} (E_{m})$ with $m Z$ inside it. Under the isomorphism $n Z \to Z$ , $n k \mapsto k$ , the subgroup $m Z = n q Z$ corresponds to $q Z$ . By [F3], the latter has the $q$ cosets represented by $0, 1, \dots, q - 1$ . Thus $[n Z : m Z] = q$ , and the path-connected total space licenses [F2], which gives $q$ sheets. At $q = 1$ the two subgroups are equal, so the morphism is an isomorphism.

step 2.1F2F3F4F5F9F10∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

77 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

J. Peter May, A Concise Course in Algebraic Topology, Chapter 3, Section 7 (standard reference, not scraped)