diff --git a/database/data/001_categories/003_topology.sql b/database/data/001_categories/003_topology.sql index eef19e7f..1af4752e 100644 --- a/database/data/001_categories/003_topology.sql +++ b/database/data/001_categories/003_topology.sql @@ -43,7 +43,7 @@ VALUES 'sSet', 'category of simplicial sets', '$\mathbf{sSet}$', - 'simplicial sets, i.e. functors $\Delta^{\mathrm{op}} \to \mathbf{Set}$', + 'simplicial sets, i.e. functors $\Delta^{\mathrm{op}} \to \mathbf{Set}$ where $\Delta$ is the simplex category', 'natural transformations', NULL, 'https://ncatlab.org/nlab/show/SimpSet', @@ -58,4 +58,14 @@ VALUES 'Here, a smooth manifold is defined as a second-countable Hausdorff space with a smooth atlas. The dimension is locally constant, not necessarily constant.', 'https://ncatlab.org/nlab/show/Diff', NULL +), +( + 'Delta', + 'simplex category', + '$\Delta$', + 'the non-empty ordered sets $[n] := \{0 < \cdots < n\}$ for $n \in \mathbb{N}$', + 'order-preserving maps', + 'The simplex category is a skeleton of $\mathbf{FinOrd} \setminus \{\varnothing\}$. It plays an important role in topology and is used to to define the category of simplicial sets.', + 'https://ncatlab.org/nlab/show/simplex+category', + NULL ); \ No newline at end of file diff --git a/database/data/001_categories/100_related-categories.sql b/database/data/001_categories/100_related-categories.sql index 19d5395e..606840f8 100644 --- a/database/data/001_categories/100_related-categories.sql +++ b/database/data/001_categories/100_related-categories.sql @@ -31,6 +31,9 @@ VALUES ('CRing', 'CAlg(R)'), ('CRing', 'Ring'), ('CRing', 'Rng'), +('Delta', 'sSet'), +('Delta', 'FinOrd'), +('Delta', 'Setne'), ('FI', 'B'), ('FI', 'FS'), ('FS', 'B'), @@ -40,6 +43,7 @@ VALUES ('FinAb', 'FinGrp'), ('FinOrd', 'FinSet'), ('FinOrd', 'Pos'), +('FinOrd', 'Delta'), ('FinSet', 'Set'), ('Fld', 'CRing'), ('FreeAb', 'Ab'), @@ -104,6 +108,8 @@ VALUES ('Sh(X,Ab)', 'Sh(X)'), ('Sp', 'B'), ('Sp', 'FinSet'), +('sSet', 'Delta'), +('sSet', 'Top'), ('Top', 'Met_c'), ('Top', 'Haus'), ('Top', 'Top*'), diff --git a/database/data/002_tags/002_category-tags.sql b/database/data/002_tags/002_category-tags.sql index c501eacd..52c3011b 100644 --- a/database/data/002_tags/002_category-tags.sql +++ b/database/data/002_tags/002_category-tags.sql @@ -30,6 +30,9 @@ VALUES ('Cat', 'category theory'), ('CMon', 'algebra'), ('CRing', 'algebra'), +('Delta', 'order theory'), +('Delta', 'topology'), +('Delta', 'combinatorics'), ('FI', 'combinatorics'), ('FI', 'set theory'), ('FinAb', 'algebra'), diff --git a/database/data/004_property-assignments/Delta.sql b/database/data/004_property-assignments/Delta.sql new file mode 100644 index 00000000..62c0ff58 --- /dev/null +++ b/database/data/004_property-assignments/Delta.sql @@ -0,0 +1,85 @@ +INSERT INTO category_property_assignments ( + category_id, + property_id, + is_satisfied, + reason +) +VALUES +( + 'Delta', + 'skeletal', + TRUE, + 'If $[n] \to [m]$ is a bijection, then $n+1 = m+1$ by comparing the sizes, hence $n=m$.' +), +( + 'Delta', + 'small', + TRUE, + 'This is trivial.' +), +( + 'Delta', + 'terminal object', + TRUE, + 'The ordered set $[0] = \{0\}$ is terminal.' +), +( + 'Delta', + 'strongly connected', + TRUE, + 'For all $n,m$ there is a morphism $[n] \to [0] \to [m]$.' +), +( + 'Delta', + 'cogenerator', + TRUE, + 'The ordered set $[1] = \{0 < 1\}$ is a cogenerator, even for the category of posets, see there for a proof.' +), +( + 'Delta', + 'coequalizers', + TRUE, + 'Assume that $X \rightrightarrows Y$ are morphisms in $\mathbf{FinOrd} \setminus \{\varnothing\}$. Since $\mathbf{FinOrd}$ has coequalizers (see there), we have a coequalizer $Y \to Q$. Since $Y$ is non-empty, also $Q$ is non-empty, and clearly $Y \to Q$ is now also the coequalizer in $\mathbf{FinOrd} \setminus \{\varnothing\}$.' +), +( + 'Delta', + 'generator', + TRUE, + 'The ordered set $[0] = \{0\}$ is a generator.' +), +( + 'Delta', + 'cofiltered', + FALSE, + 'The two maps $d^0,d^1 : [0] \rightrightarrows [1]$ are not equalized by any morphism.' +), +( + 'Delta', + 'binary powers', + FALSE, + 'Let us work with $\mathbf{FinOrd} \setminus \{\varnothing\}$. We can repeat the proof for $\mathbf{FinOrd}$ then: The forgetful functor to $\mathbf{Set}$ is representable, hence preserves all limits. Thus, if the power $\{0 < 1\} \times \{0 < 1\}$ exists in $\mathbf{FinOrd} \setminus \{\varnothing\}$, we may assume its underlying set is the cartesian product and the projection morphisms are the usual projection maps. Moreover, these maps are order-preserving. Since the result must be a total order, we have $(0,1) \leq (1,0)$ or $(1,0) \leq (0,1)$. In the first case, apply $p_2$ to get $1 \leq 0$, a contradiction. In the second case, use $p_1$ to get a contradiction.' +), +( + 'Delta', + 'binary copowers', + FALSE, + 'Let us work with $\mathbf{FinOrd} \setminus \{\varnothing\}$. We can repeat the proof for $\mathbf{FinOrd}$ then: Assume that the copower $1+1$, i.e. the coproduct of two terminal objects exists, denoted $\{x\}$ and $\{y\}$. If $x \leq y$ holds in the coproduct, then the universal property would imply this relation for all pairs of elements in any non-empty finite order, which is absurd. Otherwise, $y \leq x$ holds in the coproduct, which yields the same contradiction.' +), +( + 'Delta', + 'essentially finite', + FALSE, + 'The set $\mathbb{N}$ is not finite.' +), +( + 'Delta', + 'one-way', + FALSE, + 'There are three morphisms $[1] \to [1]$.' +), +( + 'Delta', + 'right cancellative', + FALSE, + 'The map $d^0 : [0] \to [1]$ is not an epimorphism.' +); \ No newline at end of file diff --git a/database/data/007_special-morphisms/002_isomorphisms.sql b/database/data/007_special-morphisms/002_isomorphisms.sql index ad35047e..0e5baf81 100644 --- a/database/data/007_special-morphisms/002_isomorphisms.sql +++ b/database/data/007_special-morphisms/002_isomorphisms.sql @@ -90,6 +90,11 @@ VALUES 'bijective ring homomorphisms', 'This characterization holds in every algebraic category.' ), +( + 'Delta', + 'bijective order-preserving maps', + 'This is easy. Notice that bijective order-preserving maps automatically also reflect the order (because we work with totally ordered sets).' +), ( 'FI', 'bijective maps', diff --git a/database/data/007_special-morphisms/003_monomorphisms.sql b/database/data/007_special-morphisms/003_monomorphisms.sql index d4ff8f88..465596e7 100644 --- a/database/data/007_special-morphisms/003_monomorphisms.sql +++ b/database/data/007_special-morphisms/003_monomorphisms.sql @@ -85,6 +85,11 @@ VALUES 'injective ring homomorphisms', 'This holds in every finitary algebraic category: the forgetful functor to $\mathbf{Set}$ is faithful, hence reflects monomorphisms, and it is continuous (even representable), hence preserves monomorphisms.' ), +( + 'Delta', + 'injective order-preserving maps', + 'The non-trivial direction follows since the forgetful functor $\Delta \to \mathbf{Set}$ is representable (by $[0]$), hence preserves monomorphisms.' +), ( 'FI', 'every morphism',