LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

The multiplicative unit circle is a compact metrizable topological abelian group

Statement

Let $T : = {z \in C : ∣ z ∣ = 1}$ carry the subspace topology of $C$ (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace, The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane) and the multiplication of $C$ , and let $ε : R / Z \to T$ , $ε ([t]) : = \exp (2 π i t)$ , for the published one-dimensional torus $R / Z$ (The one-dimensional torus and its normalized Haar integral). Then $T$ is a compact metrizable topological abelian group (Topological group: multiplication and inversion are continuous), $ε$ is an isomorphism of topological groups, and $∣ z w - z ∣ = ∣ w - 1 ∣, ∣ z^{- 1} - w^{- 1} ∣ = ∣ z - w ∣$ for all $z, w \in T$ .

Facts & Assumptions

[F1]

For all complex $z, w$ , $\exp (z + w) = \exp z \exp w$ , and for real $x, y$ , $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ with $∣ \exp (x + i y) ∣ = e^{x}$ . The real exponential satisfies $e^{0} = 1$ (its defining series has constant term $1$ and all other terms $0$ ). ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , The real exponential function and the number $e$ by a power series)

[F2]

$\sin$ and $\cos$ are differentiable on $R$ , hence continuous, and $\sin 0 = 0$ , $\cos 0 = 1$ . (The derivatives of sine and cosine are cosine and minus sine, A function differentiable at $c$ is continuous at $c$ )

[F3]

$\sin$ and $\cos$ have period $2 π$ : $\sin (x + 2 π) = \sin x$ and $\cos (x + 2 π) = \cos x$ for every real $x$ . (The zero sets of sine and cosine and the least positive common period 2 pi)

[F4]

$t \mapsto (\cos t, \sin t)$ is a bijection from $[0, 2 π)$ onto the Euclidean unit circle $S^{1} = {(a, b) : a^{2} + b^{2} = 1}$ . ( $t \mapsto (\cos t, \sin t)$ is a bijection from $[0, 2 π)$ onto the real unit circle)

[F5]

$Φ : C \to R^{2}$ , $Φ (a + b i) = (a, b)$ , is a bijection compatible with addition and multiplication; $d_{C} (z, w) = ∣ z - w ∣ = ∥ Φ (z) - Φ (w) ∥_{2}$ . For all $z, w \in C$ , $z \overline{z} = ∣ z ∣^{2}$ , $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ and $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ . Continuity of maps between subsets of $C$ is continuity for the metric $d_{C}$ . ( $C$ is the real coordinate plane, with coordinate arithmetic, The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane, Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form, Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive)

[F6]

The canonical projection $q : R \to R / Z$ is continuous and open, $[s] = [t]$ exactly when $s - t \in Z$ , every class has exactly one representative in $[0, 1)$ , and $R / Z$ is the quotient group of the additive group $R$ by its subgroup $Z$ , with $[s] + [t] = [s + t]$ . Moreover $R / Z$ is compact. (The one-dimensional torus and its normalized Haar integral, The quotient group $G / N$ and coset product $(g N) (h N) = g h N$ , $R / Z$ is compact and path-connected)

[F7]

Quotient universal property: a continuous map $g : R \to W$ constant on the fibres of $q$ factors uniquely as $g = \overset{ˉ}{g} \circ q$ with $\overset{ˉ}{g}$ continuous. (For a quotient map $q : X \to Y$ , a map out of $Y$ is continuous iff its composite with $q$ is; a continuous map on $X$ constant on the fibres of $q$ factors uniquely through $q$ ; and a composite of quotient maps is a quotient map)

[F8]

The product topology on $R^{2}$ is the Euclidean metric topology. A map into a product is continuous exactly when all its components are; a composite of continuous maps is continuous; the identity and scalar multiples $α i d$ of real functions are continuous. (A subset of $R^{n}$ with the product topology is compact exactly when it is closed and bounded, the product topology being the Euclidean metric topology, A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice, Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous, Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function)

[F9]

Continuous images of compact spaces are compact; a continuous bijection from a compact space onto a Hausdorff space is a homeomorphism. A metric space is Hausdorff, and the metric topology of a metric subspace is its subspace topology. (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism, Distinct points of a metric space have disjoint balls around them, Isometry, isometric embedding, and the subspace metric on a subset)

[F10]

A topological group is a group whose multiplication and inversion are continuous for the product topology. (Topological group: multiplication and inversion are continuous)

Proof

Given: The multiplicative unit circle $T \subseteq C$ with the subspace topology, and $ε ([t]) = \exp (2 π i t)$ on the published torus $R / Z$ .

1.1F1F2F3

For every integer $k$ , $\exp (2 π i k) = 1$ : by [F1] and [F3] with [F2], $\exp (2 π i k) = e^{0} (\cos (2 π k) + i \sin (2 π k)) = \cos 0 + i \sin 0 = 1$ , because $2 π k$ is an integer multiple of the period $2 π$ of sine and cosine.

1.2F1

The image of $ε$ lies in $T$ : for real $t$ , $∣ \exp (2 π i t) ∣ = e^{0} = 1$ by [F1].

1.3F1F4F5

$ε$ is surjective onto $T$ : if $z = a + b i \in T$ then $a^{2} + b^{2} = ∣ z ∣^{2} = 1$ by [F5], so $(a, b) \in S^{1}$ and [F4] gives $θ \in [0, 2 π)$ with $(a, b) = (\cos θ, \sin θ)$ ; putting $t : = θ / (2 π) \in [0, 1)$ and using [F1] and [F5] gives $ε ([t]) = \exp (2 π i t) = \cos θ + i \sin θ = a + b i = z$ .

1.4F5

$T$ is closed under multiplication and inversion, and the two displayed identities hold: for $z, w \in T$ , $∣ z w ∣ = ∣ z ∣ ∣ w ∣ = 1$ and $∣ z^{- 1} ∣ = ∣ z ∣^{- 1} = 1$ by [F5], so $z w, z^{- 1} \in T$ ; also $∣ z w - z ∣ = ∣ z ∣ ∣ w - 1 ∣ = ∣ w - 1 ∣$ and $∣ z^{- 1} - w^{- 1} ∣ = ∣ w - z ∣ / (∣ z ∣ ∣ w ∣) = ∣ z - w ∣$ by [F5].

2.1step 1.1F1F6

$ε$ is well defined on classes and is a group homomorphism: if $[s] = [t]$ then $s - t = k \in Z$ by [F6], so $\exp (2 π i s) = \exp (2 π i t) \exp (2 π i k) = \exp (2 π i t)$ by [F1] and step 1.1; and $ε ([s] + [t]) = \exp (2 π i (s + t)) = \exp (2 π i s) \exp (2 π i t) = ε ([s]) ε ([t])$ by [F1] and [F6].

3.1step 2.1F1F4F5F6

$ε$ is injective: if $ε ([s]) = ε ([t])$ , replace the classes by their unique representatives $s, t \in [0, 1)$ by [F6]; then $\cos (2 π s) = \cos (2 π t)$ and $\sin (2 π s) = \sin (2 π t)$ by [F1] and [F5], so the bijectivity in [F4] applied to $2 π s, 2 π t \in [0, 2 π)$ gives $2 π s = 2 π t$ , hence $s = t$ , hence $[s] = [t]$ .

3.2step 2.1step 1.2F2F5F7F8

$ε$ is continuous as a map $R / Z \to C$ : the map $g (t) : = \exp (2 π i t)$ is continuous on $R$ because $t \mapsto 2 π t$ , $\sin$ and $\cos$ are continuous by [F2] and [F8], hence $t \mapsto (\cos 2 π t, \sin 2 π t)$ is continuous into $R^{2}$ by [F8], and $g = Φ^{- 1} (\cos 2 π \cdot, \sin 2 π \cdot)$ is continuous by [F5], [F8] and the distance identity $d_{C} (z, w) = ∥ Φ (z) - Φ (w) ∥_{2}$ read as $ε$ - $δ$ continuity of $Φ^{- 1}$ ; by step 2.1 $g$ is constant on the fibres of $q$ , so the quotient universal property [F7] makes $ε$ continuous into $C$ , and its corestriction to the subspace $T$ is continuous by the subspace topology.

4.1step 1.3step 3.2F6F9

$T$ is compact: it is the image $ε (R / Z)$ by step 1.3 of the compact space $R / Z$ under the continuous map of step 3.2, and continuous images of compact spaces are compact by [F9].

4.2step 1.2step 3.1step 1.3step 3.2F5F6F9

$ε$ is a homeomorphism onto $T$ : it is a continuous bijection by steps 2.1, 3.1, 1.3 and 3.2 whose domain is compact by [F6] and whose image lies in $T$ by step 1.2, and $T$ is Hausdorff as a subspace of the metric space $C$ by [F5] and [F9]; the compact-to-Hausdorff clause of [F9] applies to the corestriction.

5.1step 4.2step 1.4F5F9F10∎

Multiplication and inversion on $T$ are continuous, so $T$ is a topological abelian group: for $z, z_{0}, w, w_{0} \in T$ , $∣ z w - z_{0} w_{0} ∣ \leq ∣ z - z_{0} ∣ ∣ w ∣ + ∣ z_{0} ∣ ∣ w - w_{0} ∣ = ∣ z - z_{0} ∣ + ∣ w - w_{0} ∣$ by [F5], so the open rectangle $(B (z_{0}, δ) \cap T) \times (B (w_{0}, δ) \cap T)$ with $δ = ε / 2$ is mapped into $B (z_{0} w_{0}, ε) \cap T$ , which is continuity of multiplication at $(z_{0}, w_{0})$ ; and $∣ z^{- 1} - w^{- 1} ∣ = ∣ z - w ∣$ by step 1.4 makes inversion distance preserving, hence continuous. Group axioms and commutativity are inherited from $C$ by steps 2.1, 3.1 and 1.3, and metrizability of $T$ is [F9] applied to the metric subspace $T \subseteq C$ .

Depends on

Used by

Dependency tree · two levels

159 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

Dikran D. Dikranjan, Introduction to Topological Groups (author lecture notes, Universita di Udine / Universidad Complutense de Madrid, 2007) (standard reference, not scraped)
Manfred Einsiedler and Thomas Ward, Ergodic Theory with a View Towards Number Theory, Appendix C (course-hosted full text) (standard reference, not scraped)
Lynn H. Loomis, Introduction to Abstract Harmonic Analysis, D. Van Nostrand 1953, Chapter VII, Sections 34-35 (printed pp. 134-140) (standard reference, not scraped)