Initial PR for Direct limit of finite-dimensional Euclidean spaces

spaces/S000106/README.md

@@ -0,0 +1,42 @@
+---
+uid: S000106
+name: Direct limit $\mathbb R^\infty$ of Euclidean spaces $\mathbb R^n$
+refs:
+  - wikipedia: Direct_limit
+    name: Direct limit on Wikipedia
+  - mathse: 3961052
+    name: Answer to "Is the weak topology on $\mathbb{R}^{\infty}$ the same as the box topology?"
+  - mathse: 5012784
+    name: Answer to "Is $\ell^\infty$ with box topology connected?"
+  - zb: "0298.57008"
+    name: Characteristic classes (Milnor-Stasheff)
+  - zb: "0307.55015"
+    name: Fibre bundles. 2nd ed. (Husemoller)
+  - zb: "1280.54001"
+    name: Geometric aspects of general topology. (Sakai)
+  - wikipedia: Fréchet–Urysohn_space
+    name: Fréchet–Urysohn space on Wikipedia
+---
+$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. 
+
+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$. 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.
+
+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

@@ -0,0 +1,16 @@
+---
+space: S000106
+property: P000238
+value: true
+refs:
+  - zb: "1280.54001"
+    name: Geometric aspects of general topology. (Sakai)
+---
+
+$\mathbb{R}^\infty$ with the natural scalar multiplication and addition operations is a vector space
+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$. 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. 

spaces/S000106/properties/P000240.md

@@ -0,0 +1,11 @@
+---
+space: S000106
+property: P000240
+value: true
+refs:
+  - zb: "1280.54001"
+    name: Geometric aspects of general topology. (Sakai)
+---
+
+The chain of subspaces $\empty \subset \mathbb{R}^0 \subset \mathbb{R}^1 \cdots$ is a CW structure.
+