The standard product torus as a compact Lie group

By [A1], for any sequence $(A_n)$ of nonempty sets the family $\mathcal{F}=\{A_n:n\in \mathbb{N}\}$ has a choice function $g$. The composite $n\mapsto g(A_n)$ is an indexed selector, even if some sets $A_n$ repeat. Thus [F1] holds and supplies the countable-choice premise in the quotient circle definition [F2].

For one factor, [F2] makes each quotient interval $q(I)$ open because $q$ is open, and $q{\mathrm{\mid }}_I$ is injective because $I$ has length less than $1$. Its inverse chart is continuous: $q{\mathrm{\mid }}_I$ is a continuous open bijection onto $q(I)$. These charts cover the circle. If two charts overlap, local lifts differ by an integer; this integer is locally constant, so each transition map is locally a translation and hence smooth. The charts therefore define a smooth one-manifold without boundary compatible with the quotient topology.

Addition and inversion on one factor are smooth in these charts. Near any pair of points, choose local real lifts $x,y$ and an output chart around their sum; after shrinking the input intervals, the coordinate expression for addition is $x+y$ plus one fixed integer. Near any point, choose local lifts for it and its inverse; the coordinate expression for inversion is $-x$ plus one fixed integer. Both expressions are smooth. With the group law already given by [F2], this is a Lie group by [F6]. Its underlying circle is compact, Hausdorff and connected by [F2] and [F3], and it is abelian by the quotient addition law.

Iterate the binary product smooth-structure construction in [F5] over the finite number $r$ of factors. Multiplication and inversion are componentwise products of the smooth one-factor maps in step 2.1; iterating the binary component criterion in [F5] makes both operations smooth. The finite product is compact by [F3], connected by [F3], and abelian coordinatewise. It is therefore a compact connected abelian Lie group, hence a torus by [F4], of dimension $r$. The coordinate curves ${\gamma }_i(s)=(0,\dots ,[s],\dots ,0)$ are smooth group homomorphisms by the quotient charts and coordinate group law, so [F9] applies. Their derivatives at zero form the coordinate basis of $T_{0}T$, and ${\gamma }_i(s+1)={\gamma }_i(s)$, so each has period one. For any $t\in \mathbb{R}$, $s\mapsto {\gamma }_i(ts)$ is a smooth group homomorphism with initial derivative $t{e}_i$; uniqueness in [F9] makes it ${\gamma }_{t{e}_i}$. Therefore ${\exp }_T(t{e}_i)={\gamma }_{t{e}_i}(1)={\gamma }_i(t)$, as needed for the stated normalization. For $r=0$, the empty product is the one-point Lie group and these assertions hold with empty basis.

The circle has a finite CW structure with one vertex $[0]$ and one open $1$-cell, the image of $(0,1)$; its characteristic interval has both endpoints attached to that vertex. For $T$, index product cells by subsets $J\subseteq \{1,\dots ,r\}$: coordinates in $J$ lie in the open $1$-cell and all other coordinates equal $[0]$. Each cell is an open cube of dimension $\mathrm{\mid }J\mathrm{\mid }$, its closure meets only cells indexed by subsets of $J$, and its characteristic cube is the product of the factor characteristic intervals; identify each closed cube with a closed disk of the same dimension. The map $q^r:[0,1{]}^r\to T$ is a continuous surjection because every coordinate class has a representative in $[0,1]$ by [F2]. If $x\mathrm{\ne }y$ in $T$, some coordinate $k$ has $x_k\mathrm{\ne }{y}_k$; choose disjoint open neighborhoods of $x_k$ and $y_k$ in the Hausdorff circle from [F2]. Their inverse images under the $k$th coordinate projection are disjoint open neighborhoods of $x$ and $y$ in the product topology, so $T$ is Hausdorff. The cube $[0,1{]}^r$ is compact by [F10] and the finite-product theorem in [F3], including the one-point empty product when $r=0$. If $K$ is closed in that cube, [F11] makes $K$ compact; continuity of $q^r$ and [F12] make $q^r(K)$ compact; and the just-proved Hausdorff property of $T$ and [F13] make $q^r(K)$ closed in $T$. Thus $q^r$ is closed as well as continuous and surjective, so [F14] makes it a quotient map. It is the characteristic map for the top cell. Every lower-cell characteristic cube is obtained by precomposing $q^r$ with the continuous coordinate insertion that fixes omitted coordinates at $0$, so the quotient topology of $q^r$ already makes every characteristic map continuous; conversely $q^r$ is itself one of those maps. Hence this quotient topology is exactly the weak topology determined by the finitely many characteristic cubes. This gives a finite CW structure with the identity as a $0$-cell. The singleton identity is a subcomplex, so [F7] gives the homotopy extension property for its inclusion.

The compact Hausdorff space $T$ is compactly generated: its identity map from the compact Hausdorff space $T$ tests every open subset in the compactly-generated topology. For every compact Hausdorff space $C$ and continuous map $f:C\to T$, [F12] makes $f(C)$ compact, and [F13] makes $f(C)$ closed in the Hausdorff space $T$ established in step 4.1. This is precisely weak Hausdorffness. Together with the cofibration from step 4.1, [F8] shows that the based group is well-pointed.