Adjustments

Author: GeoffreySangston

spaces/S000106/README.md

@@ -17,28 +17,26 @@ refs:
   - wikipedia: Fréchet–Urysohn_space
     name: Fréchet–Urysohn space on Wikipedia
 ---
-The subset $\mathbb{R}^\infty$ of eventually $0$ sequences in $\mathbb{R}^\omega$, with the finest 
-topology such that the standard inclusion maps $\mathbb{R}^n \hookrightarrow \mathbb{R}^\infty$, 
-$x \mapsto (x^1, \ldots, x^n, 0, \ldots)$, are continuous for each $n$, where $\mathbb{R}^n$ has 
-the Euclidean topology.
+$X$ is the subset $\mathbb{R}^\infty$ of eventually $0$ sequences in $\mathbb{R}^\omega$, with the final 
+topology with respect to the standard inclusion maps $\mathbb{R}^n \hookrightarrow \mathbb{R}^\infty$, 
+$x \mapsto (x^1, \ldots, x^n, 0, \ldots)$. By definition of final topology, this means that $\mathbb{R}^\infty$ has the finest topology such that each such inclusion map is continuous.
 
 Equivalently, the set $U \subset \mathbb{R}^\infty$ is open if and only if $U \cap \mathbb{R}^n$ 
 is open in $\mathbb{R}^n$ for each $n$, where we identify each Euclidean space $\mathbb{R}^n$ with 
-its image.
+its image. 
 
-Equivalently, $\mathbb{R}^\infty$ is the direct limit $\varinjlim \mathbb{R}^n$ of the directed 
+Equivalently, $\mathbb{R}^\infty$ is the direct limit $\varinjlim \mathbb{R}^n := (\bigsqcup_{i = 1}^\infty \mathbb{R}^i)/\sim$ of the directed 
 system consisting of Euclidean spaces and standard inclusion maps 
 $\mathbb{R}^i \hookrightarrow \mathbb{R}^j$, $x \mapsto (x^1, \ldots, x^i, 0, \ldots)$, 
-for each $i < j$.
+for each $i < j$. The equivalence relation $\sim$ identifies points which correspond under these inclusions.
+For general discussion on direct limits, see {{wikipedia:Direct_limit}}.
 
 Equivalently, $\mathbb{R}^\infty \subset \mathbb{R}^\omega$ has the subspace topology, where
 $\mathbb{R}^\omega$ is given the box topology; this is shown in {{mathse:3961052}}. Moreover,
 it is shown in {{mathse:5012784}} that $\mathbb{R}^\infty$ is a quasi-component of the origin in
 $\mathbb{R}^\omega$. Hence $\mathbb{R}^\infty$ embeds into {{S107}}
 as a path component.
 
-For general discussion on direct limits, see {{wikipedia:Direct_limit}}.
-
 Defined on page 62 of {{zb:"0298.57008"}}, on page 2 of {{zb:"0307.55015"}}, 
 on page 56 of {{zb:"1280.54001}}, and on {{wikipedia:Fréchet–Urysohn_space}} 
 under Direct limit of finite-dimensional Euclidean spaces.

spaces/S000106/properties/P000238.md

@@ -11,6 +11,6 @@ $\mathbb{R}^\infty$ with the natural scalar multiplication and addition operatio
 over $\mathbb{R}$. It remains to argue each operation is continuous.
 
 For each $n$, the scalar multiplication function $\mathbb{R} \times \mathbb{R}^\infty \to \mathbb{R}^\infty$ restricted to $\mathbb{R} \times \mathbb{R}^n \to \mathbb{R}^n \hookrightarrow \mathbb{R}^\infty$ is continuous, since the first map identifies with the usual scalar multiplication of $n$-dimensional Euclidean space. Since [S25|P130], Proposition 2.8.3 of {{zb:"1280.54001"}} implies $\mathbb{R} \times \mathbb{R}^\infty \cong \varinjlim (\mathbb{R} \times \mathbb{R}^n)$. This means that $\mathbb{R} \times \mathbb{R}^\infty$ has the final topology with respect to the inclusions 
-$\mathbb{R} \times \mathbb{R}^n \hookrightarrow \mathbb{R} \times \mathbb{R}^\infty$. Thus $\mathbb{R} \times \mathbb{R}^\infty \to \mathbb{R}^\infty$ is continuous.
+$\mathbb{R} \times \mathbb{R}^n \hookrightarrow \mathbb{R} \times \mathbb{R}^\infty$. By the universal property of the final topology, it follows that $\mathbb{R} \times \mathbb{R}^\infty \to \mathbb{R}^\infty$ is continuous.
 
 Since each $\mathbb{R}^n$ is locally compact, Proposition 2.8.4 of {{zb:"1280.54001"}} implies $\mathbb{R}^\infty \times \mathbb{R}^\infty \cong \varinjlim (\mathbb{R}^n \times \mathbb{R}^n)$. Making a similar argument as above shows that the natural addition operation on $\mathbb{R}^\infty$ is continuous.