add lemma about Hilbert's Hotel

Author: ScriptRaccoon

.vscode/settings.json

@@ -15,7 +15,8 @@
 		"infty",
 		"chartjs",
 		"Prost",
-		"SetxSet"
+		"SetxSet",
+		"hilberts"
 	],
 	"cSpell.words": [
 		"abelian",

database/data/004_property-assignments/Ab_fg.sql

@@ -51,13 +51,13 @@ VALUES
 	'Ab_fg',
 	'countable powers',
 	FALSE,
-	'Assume that the power $P := \mathbb{Z}^{\mathbb{N}} = \prod_{n \geq 0} \mathbb{Z}$ exists in this category. Since products are associative and finite products exist, we have $P \cong \mathbb{Z} \times P$. Tensoring with $\mathbb{Q}$ yields an isomorphism of finite-dimensional vector spaces $P_{\mathbb{Q}} \cong \mathbb{Q} \times P_{\mathbb{Q}}$, which is impossible: the dimension $d$ of $P_{\mathbb{Q}}$ (i.e. the rank of $P$) would satisfy $d = 1+d$.'
+	'If countable powers exist, then by <a href="/lemma/hilberts_hotel">Hilbert''s Hotel</a> there is some object $P$ with $P \cong \mathbb{Z} \times P$. Tensoring with $\mathbb{Q}$ yields an isomorphism of finite-dimensional vector spaces $P_{\mathbb{Q}} \cong \mathbb{Q} \times P_{\mathbb{Q}}$, which is impossible: the dimension $d$ of $P_{\mathbb{Q}}$ (i.e. the rank of $P$) would satisfy $d = 1+d$.'
 ),
 (
 	'Ab_fg',
 	'countable copowers',
 	FALSE,
-	'Assume that the copower $C := \mathbb{N} \otimes \mathbb{Z} = \coprod_{n \geq 0} \mathbb{Z}$ exists in this category. Since coproducts are associative and finite coproducts exist, we have $C \cong \mathbb{Z} \oplus C$. Tensoring with $\mathbb{Q}$ yields an isomorphism of finite-dimensional vector spaces $C_{\mathbb{Q}} \cong \mathbb{Q} \oplus C_{\mathbb{Q}}$, which is impossible: the dimension $d$ of $C_{\mathbb{Q}}$ (i.e. the rank of $C$) would satisfy $d = 1+d$.'
+	'If countable powers exist, then by <a href="/lemma/hilberts_hotel">Hilbert''s Hotel</a> there is some object $P$ with $P \cong \mathbb{Z} \oplus P$. Tensoring with $\mathbb{Q}$ yields an isomorphism of finite-dimensional vector spaces $C_{\mathbb{Q}} \cong \mathbb{Q} \oplus C_{\mathbb{Q}}$, which is impossible: the dimension $d$ of $C_{\mathbb{Q}}$ (i.e. the rank of $C$) would satisfy $d = 1+d$.'
 ),
 (
 	'Ab_fg',

database/data/004_property-assignments/FinAb.sql

@@ -51,7 +51,7 @@ VALUES
 	'FinAb',
 	'countable powers',
 	FALSE,
-	'Assume that the power $P := (\mathbb{Z}/2)^{\mathbb{N}}$ exists. Since products are associative and finite products exist, we conclude $P \cong \mathbb{Z}/2 \times P$. If $P$ has $n$ elements, this means $n = 2n$, i.e. $n = 0$, a contradiction.'
+	'If countable powers exist, then by <a href="/lemma/hilberts_hotel">Hilbert''s Hotel</a> there is some object $P$ with $P \cong \mathbb{Z}/2 \times P$. If $P$ has $n$ elements, this means $n = 2n$, i.e. $n = 0$, a contradiction.'
 ),
 (
 	'FinAb',

database/data/004_property-assignments/FinSet.sql

@@ -51,13 +51,13 @@ VALUES
 	'FinSet',
 	'countable copowers',
 	FALSE,
-	'Assume that the copower $C := \mathbb{N} \otimes 1$ exists. Since coproducts are associative and finite coproducts exist, we get $C \cong 1 \sqcup C$. It $C$ has $m \in \mathbb{N}$ elements, this implies $m = 1 + m$, which is a contradiction.'
+	'If countable copowers exist, then by <a href="/lemma/hilberts_hotel">Hilbert''s Hotel</a> there is some object $C$ with $C \cong 1 \sqcup C$. If $C$ has $m \in \mathbb{N}$ elements, this implies the contradiction $m = 1 + m$.'
 ),
 (
 	'FinSet',
 	'countable powers',
 	FALSE,
-	'Assume that the power $P := \{0,1\}^{\mathbb{N}}$ exists. Since products are associative and finite products exists, we get $P \cong \{0,1\} \times P$. If $P$ has $m \in \mathbb{N}$ elements, this implies $m = 2m$ and hence $m = 0$, i.e. $P = \varnothing$. But there is a diagonal morphism $\{0,1\} \to P$, making $P = \varnothing$ impossible.'
+	'If countable powers exist, then by <a href="/lemma/hilberts_hotel">Hilbert''s Hotel</a> there is an object $P$ with $P \cong \{0,1\} \times P$ and a morphism $\{0,1\} \to P$. If $P$ has $m \in \mathbb{N}$ elements, this implies $m = 2m$ and hence $m = 0$, i.e. $P = \varnothing$. But then there cannot be a map $\{0,1\} \to P$.'
 ),
 (
 	'FinSet',

database/data/010_lemmas/000_lemmas.sql

@@ -9,4 +9,10 @@ INSERT INTO lemmas (
     'Algebraic categories are "never" thin',
     'Let $\mathcal{C}$ be a <a href="/category-property/thin">thin</a> and <a href="/category-property/finitary_algebraic">finitary algebraic</a> category. Then $\mathcal{C} \simeq 1$ or $\mathcal{C} \simeq \{0 < 1\}$.',
     'Let $F : \mathbf{Set} \to \mathcal{C}$ denote the free algebra functor. Every object $A \in \mathcal{C}$ admits a regular epimorphism $F(X) \twoheadrightarrow A$ for some set $X$. But since $\mathcal{C}$ is thin, every regular epimorphism must be an isomorphism. Also, $F(X)$ is a coproduct of copies of $F(1)$, which means it is either the initial object $0$ or $F(1)$ itself (since $\mathcal{C}$ is thin). If $F(1) \cong 0$, then every object is isomorphic to the initial object $0$, and hence $\mathcal{C}$ is trivial. If not, then $\mathcal{C}$ has exactly two objects up to isomorphism, $0$ and $F(1)$, there is a morphism $0 \to F(1)$, but no morphism $F(1) \to 0$. Since $\mathcal{C}$ is thin, we conclude $\mathcal{C} \simeq \{0 \to 1\}$.'
+),
+(
+    'hilberts_hotel',
+    'Hilbert''s Hotel',
+    'Let $\mathcal{C}$ be a category with countable powers. Then for every object $X \in \mathcal{C}$ there is an object $P \in \mathcal{C}$ with $P \cong X \times P$ and which has a morphism $X \to P$.',
+    'Take $P := X^{\mathbb{N}}$. Since $\mathbb{N} \cong 1 + \mathbb{N}$ as sets, we have $P \cong X \times P$. The diagonal provides a morphism $X \to P$.'
 );