Skip to content

Commit d93fe03

Browse files
ykawase5048ScriptRaccoon
authored andcommitted
assign multi-completeness
1 parent cf9fd08 commit d93fe03

2 files changed

Lines changed: 25 additions & 0 deletions

File tree

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,12 @@ VALUES
5353
TRUE,
5454
'If $f : X \to Y$ is a surjective map of finite sets, it is the coequalizer of the two projections $p_1, p_2 : X \times_Y X \rightrightarrows X$ in $\mathbf{FinSet}$, but also in $\mathbf{FS}$. Notice that $p_1,p_2$ are surjective. Even though $X \times_Y X$ is not a pullback in $\mathbf{FS}$, we can use this finite set here.'
5555
),
56+
(
57+
'FS',
58+
'multi-terminal object',
59+
TRUE,
60+
'The empty set and a singleton give a multi-terminal object.'
61+
),
5662
(
5763
'FS',
5864
'small',
@@ -117,6 +123,12 @@ VALUES
117123
$(E_1 \vee E_2) \wedge (E_1 \vee E_3) = \top \wedge \top = \top$.
118124
<p>*For thin categories, the properties codistributive and distributive <a href="/category-implication/distributive_duality">are equivalent</a>.'
119125
),
126+
(
127+
'FS',
128+
'multi-initial object',
129+
FALSE,
130+
'If a multi-initial object exists, then the connected component consisting of non-empty finite sets has an initial object $X$. Then, any non-empty finite set cannot have a cardinality strictly greater than $X$, which is a contradiction.'
131+
),
120132
(
121133
'FS',
122134
'countable',

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

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -89,6 +89,19 @@ VALUES
8989
TRUE,
9090
'Since the inclusion $\mathbf{Set}_{\neq \varnothing} \hookrightarrow \mathbf{Set}$ is closed under non-empty colimits, it is also closed under filtered colimits. Therefore, non-empty finite sets are still finitely presentable in $\mathbf{Set}_{\neq \varnothing}$, and every non-empty set is written as a filtered colimit of them.'
9191
),
92+
(
93+
'Setne',
94+
'generalized variety',
95+
TRUE,
96+
'Since the inclusion $\mathbf{Set}_{\neq \varnothing} \hookrightarrow \mathbf{Set}$ is closed under non-empty colimits, it is also closed under sifted colimits. Therefore, non-empty finite sets are still strongly finitely presentable in $\mathbf{Set}_{\neq \varnothing}$, and every non-empty set is written as a sifted colimit of them.'
97+
),
98+
99+
(
100+
'Setne',
101+
'multi-complete',
102+
TRUE,
103+
'Let $D$ be a diagram in $\mathbf{Set}_{\neq \varnothing}$, and let $L$ be a limit of $D$ in $\mathbf{Set}$. If $L$ is non-empty, it gives a limit in $\mathbf{Set}_{\neq \varnothing}$ as well. If $L$ is the empty set, there is no cone over $D$ in $\mathbf{Set}_{\neq \varnothing}$; hence the empty set of cones gives a multi-limit of $D$ in $\mathbf{Set}_{\neq \varnothing}$.'
104+
),
92105
(
93106
'Setne',
94107
'sequential limits',

0 commit comments

Comments
 (0)