diff --git a/databases/catdat/data/categories/Delta.yaml b/databases/catdat/data/categories/Delta.yaml index 4e8df641..966d12cb 100644 --- a/databases/catdat/data/categories/Delta.yaml +++ b/databases/catdat/data/categories/Delta.yaml @@ -54,6 +54,9 @@ satisfied_properties: - property: epi-regular reason: The proof for $\FinOrd$ also works for $\FinSet \setminus \{\varnothing\}$. + - property: ℵ₁-filtered colimits + reason: This can be deduced from the property for $\FinOrd$. + - property: cosifted reason: >- Let $X,Y \in \Delta$. We may pick $x \in X$, $y \in Y$. Then there is a "point span" $X \xleftarrow{x} [0] \xrightarrow{y} Y$. Every span $X \xleftarrow{f} Z \xrightarrow{g} Y$ is connected to such a point span: Pick $z \in Z$. This defines a morphism of spans: diff --git a/databases/catdat/data/categories/FinOrd.yaml b/databases/catdat/data/categories/FinOrd.yaml index f8ef77b0..8a6a7a7c 100644 --- a/databases/catdat/data/categories/FinOrd.yaml +++ b/databases/catdat/data/categories/FinOrd.yaml @@ -55,6 +55,9 @@ satisfied_properties: - property: core-thin reason: 'Let $f : \{1 < \cdots < n \} \to \{1 < \cdots < n \}$ be an automorphism. Then $f(i)$ is the smallest element not contained in $\{f(j) : j < i\}$. From this one can deduce $f(i)=i$ by induction.' + - property: ℵ₁-filtered colimits + reason: The proof is similar to $\FinSet$. + unsatisfied_properties: - property: small reason: Even the collection of all singleton orders is not small. diff --git a/databases/catdat/data/categories/FinSet.yaml b/databases/catdat/data/categories/FinSet.yaml index 820d795a..224d7a29 100644 --- a/databases/catdat/data/categories/FinSet.yaml +++ b/databases/catdat/data/categories/FinSet.yaml @@ -42,7 +42,7 @@ satisfied_properties: reason: This follows easily from the fact that sets form an elementary topos. - property: ℵ₁-accessible - reason: The inclusion $\FinSet \hookrightarrow \Set$ is closed under ℵ₁-filtered colimits, that is, any ℵ₁-filtered colimit of finite sets is again finite. Since every finite set is ℵ₁-presentable in $\Set$, it is still ℵ₁-presentable in $\FinSet$. Therefore, $\FinSet$ is ℵ₁-accessible, where every object is ℵ₁-presentable. + reason: The inclusion $\FinSet \hookrightarrow \Set$ is closed under ℵ₁-filtered colimits, that is, any ℵ₁-filtered colimit of finite sets is again finite (MO/400763). Since every finite set is ℵ₁-presentable in $\Set$, it is still ℵ₁-presentable in $\FinSet$. Therefore, $\FinSet$ is ℵ₁-accessible, where every object is ℵ₁-presentable. unsatisfied_properties: - property: small diff --git a/databases/catdat/data/categories/Grp_c.yaml b/databases/catdat/data/categories/Grp_c.yaml index 7c8fac0a..ce9a5114 100644 --- a/databases/catdat/data/categories/Grp_c.yaml +++ b/databases/catdat/data/categories/Grp_c.yaml @@ -85,7 +85,7 @@ unsatisfied_properties: - property: cogenerator reason: 'Assume that a cogenerator $Q$ exists in $\Grp_\c$. There are only countably many finitely generated subgroups of $Q$. But there are continuum many finitely generated simple groups; this follows from Corollary 1.5 in Finitely generated infinite simple groups of homeomorphisms of the real line by J. Hyde and Y. Lodha. Hence, there is a finitely generated (and hence countable) simple group $H$ which does not embed into $Q$. Since $H$ is simple, any homomorphism $H \to Q$ must be trivial then. But then $\id_H, 1 : H \rightrightarrows H$ are not separated by a homomorphism $H \to Q$.' - - property: ℵ₁-accessible + - property: ℵ₁-filtered colimits reason: 'We can almost copy the proof from $\Set_\c$ to show that $\Grp_\c$ does not have $\aleph_1$-filtered colimits: Fix an uncountable set $X$, let $P_\c(X)$ be the poset of countable subsets of $X$, which is $\aleph_1$-filtered, and consider the functor $P_\c(X) \to \Grp_\c$ taking a subset $Y \subseteq X$ to the free group $F(Y)$. The colimit of this diagram in $\Grp$ is given by $F(X)$ itself, so if $G$ were a colimit in $\Grp_\c$, then $\Hom(G, C_2) \cong \Hom(F(X),C_2) \cong \{0,1\}^X$. But the former has cardinality at most $2^{\aleph_0}$ and the latter has cardinality $2^{\card(X)}$, so we have obtained a contradiction if we pick $X$ large enough (e.g. $\card(X)=2^{\aleph_0}$).' special_objects: diff --git a/databases/catdat/data/categories/Man.yaml b/databases/catdat/data/categories/Man.yaml index 088103b0..62ecd002 100644 --- a/databases/catdat/data/categories/Man.yaml +++ b/databases/catdat/data/categories/Man.yaml @@ -71,7 +71,7 @@ unsatisfied_properties: - property: sequential colimits reason: If $\Man$ had sequential colimits, then by this lemma there would be a manifold $M$ that admits a split epimorphism $M \to \IR^n$ for every $n$. But then $M$ will have an infinite-dimensional tangent space, which is a contradiction. - - property: ℵ₁-accessible + - property: ℵ₁-filtered colimits reason: 'We already know that $\Set_\c$ does not have $\aleph_1$-filtered colimits. The functor $\pi_0: \Man \to \Set_\c$ is well-defined (because manifolds are second-countable), and it admits a fully faithful right adjoint (regarding a countable set as a discrete manifold). Therefore, $\Man$ does not have $\aleph_1$-filtered colimits.' - property: quotients of congruences diff --git a/databases/catdat/data/categories/Set_c.yaml b/databases/catdat/data/categories/Set_c.yaml index 20fa28b6..dec49f86 100644 --- a/databases/catdat/data/categories/Set_c.yaml +++ b/databases/catdat/data/categories/Set_c.yaml @@ -69,8 +69,8 @@ unsatisfied_properties: - property: countable powers reason: Since the forgetful functor $\Set_\c \to \Set$ is representable, it preserves (countable) products. Therefore, if the power $\{0,1\}^{\IN}$ exists in $\Set_\c$, it must be the ordinary cartesian product, which however is uncountable. - - property: ℵ₁-accessible - reason: 'In fact, $\Set_\c$ does not have $\aleph_1$-filtered colimits: Fix an uncountable set $X$, let $P_\c(X)$ be the poset of countable subsets of $X$, which is $\aleph_1$-filtered, and consider the functor $P_\c(X) \to \Set_\c$ taking a subset $Y \subseteq X$ to $Y$. The colimit of this diagram in $\Set$ is given by $X$ itself, so if $X_c$ were a colimit in $\Set_\c$, then $\Hom(X_c, \{0,1\}) \cong \Hom(X, \{0,1\})$. But the former has cardinality at most $2^{\aleph_0}$ and the latter has cardinality $2^{\card(X)}$, so we have obtained a contradiction if we pick $X$ large enough (e.g. $\card(X)=2^{\aleph_0}$).' + - property: ℵ₁-filtered colimits + reason: 'Fix an uncountable set $X$, let $P_\c(X)$ be the poset of countable subsets of $X$, which is $\aleph_1$-filtered, and consider the functor $P_\c(X) \to \Set_\c$ taking a subset $Y \subseteq X$ to $Y$. The colimit of this diagram in $\Set$ is given by $X$ itself, so if $X_c$ were a colimit in $\Set_\c$, then $\Hom(X_c, \{0,1\}) \cong \Hom(X, \{0,1\})$. But the former has cardinality at most $2^{\aleph_0}$ and the latter has cardinality $2^{\card(X)}$, so we have obtained a contradiction if we pick $X$ large enough (e.g. $\card(X)=2^{\aleph_0}$).' special_objects: initial object: diff --git a/databases/catdat/data/categories/Sp.yaml b/databases/catdat/data/categories/Sp.yaml index 317929af..ced79bef 100644 --- a/databases/catdat/data/categories/Sp.yaml +++ b/databases/catdat/data/categories/Sp.yaml @@ -23,6 +23,9 @@ satisfied_properties: - property: cogenerator reason: 'This follows from $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$, this lemma, and the fact that if $G$ is a (finite) group, the power set $P(G)$ with the evident $G$-action is a weakly terminal cogenerator in $G{-}\Set$ (resp. $G{-}\FinSet$). For the proof, notice that $\varnothing,G \in P(G)$ are fixed points, yielding two $G$-maps $1 \rightrightarrows P(G)$. In particular, $P(G)$ is weakly terminal. If $X$ is a $G$-set with distinct points $x,y$, we construct a $G$-map $f : X \to P(G)$ that separates $x,y$: First, $X$ is a coproduct of orbits. If $x,y$ lie in different orbits, let $f|_{Gx}$ be constant $\varnothing$, $f|_{Gy}$ be constant $G$, and, say, $f$ be constant $\varnothing$ on all other orbits. If $x,y$ lie in the same orbit, say $y = g_0 x$, define $f|_{Gx} : Gx \to P(G)$ by $f(x) = G_x$ (stabilizer), which is well-defined, and choose $f$ to be $\varnothing$ on all other orbits. Then $f(y) = g_0 G_x \neq G_x = f(x)$.' + - property: ℵ₁-filtered colimits + reason: This is because $\FinSet$ has this property. + unsatisfied_properties: - property: skeletal reason: This is trivial. diff --git a/databases/catdat/data/categories/walking_idempotent.yaml b/databases/catdat/data/categories/walking_idempotent.yaml index 68b3a491..ba0e99ce 100644 --- a/databases/catdat/data/categories/walking_idempotent.yaml +++ b/databases/catdat/data/categories/walking_idempotent.yaml @@ -39,8 +39,8 @@ satisfied_properties: - property: preadditive reason: The monoid $\{1,e\}$ with $e^2=e$ is the underlying multiplicative monoid of the ring $\IZ/2$, where $e=0$. Thus, the (unique) preadditive structure is given by $1 + e = e + 1 = 1$, $e + e = e$ and $1 + 1 = e$. - - property: filtered - reason: The pair $\id,e$ is coequalized by $e$ (non-universally). + - property: ℵ₁-filtered + reason: 'In fact, the walking idempotent is $\kappa$-filtered for every regular infinite cardinal $\kappa$: Every diagram $D : \I \to \Idem$ has the cocone $(e : D(i) \to 0)_{i \in \I}$.' unsatisfied_properties: - property: terminal object diff --git a/databases/catdat/data/category-implications/accessible.yaml b/databases/catdat/data/category-implications/accessible.yaml index c0018f04..92d6d51a 100644 --- a/databases/catdat/data/category-implications/accessible.yaml +++ b/databases/catdat/data/category-implications/accessible.yaml @@ -132,6 +132,7 @@ - ℵ₁-accessible conclusions: - accessible + - ℵ₁-filtered colimits reason: This is trivial. is_equivalence: false @@ -148,7 +149,7 @@ - accessible conclusions: - Cauchy complete - reason: This is because the walking idempotent is $\kappa$-filtered for any regular cardinal $\kappa$. + reason: This is because the walking idempotent is $\kappa$-filtered for any regular cardinal $\kappa$. See also Makkai-Pare, Prop. 2.2.1. is_equivalence: false - id: small_accessible_characterization @@ -160,13 +161,35 @@ reason: See Makkai-Pare, Thm. 2.2.2. is_equivalence: false -- id: countably_accessible_thin +- id: countably_accessible_criterion + # TODO: based on this, remove some of the assignments assumptions: - essentially countable - - thin + - locally finite + - Cauchy complete # TODO: clarify where this is used. it must be used (Idem...) conclusions: - ℵ₁-accessible - reason: In general, every $\kappa$-filtered diagram in a poset whose elements are less than $\kappa$ admits the greatest element. Therefore, all the elements are $\kappa$-presentable, and the poset is $\kappa$-accessible. + reason: >- + Under the given assumptions, we will prove that every $\aleph_1$-filtered diagram $D : \I \to \C$ indexed by a $\aleph_1$-filtered poset is eventually constant, i.e. there is some $i \in \I$ such that for every morphism $j \geq i$ the morphism $D(i) \to D(j)$ is an isomorphism. This will prove right away that $\aleph_1$-filtered colimits exist and that every object is $\aleph_1$-presentable. The proof will be similar to Thm. 2.2.2 in Makkai-Pare (which only gives $\aleph_2$-accessibility) and to MO/509853 (which concerns $\aleph_0$-accessibility under stronger assumptions). + + It suffices to prove this for the special case $\C = \FinSet$: For every $X \in \C$ we have a diagram of finite sets $\Hom(X,D(-)) : \I \to \FinSet$ (a priori these are only finite collections, but we may assume that they are finite sets by replacing $\C$ with an equivalent category). Assume that we have found $i_X \in \I$ such that the map of finite sets $\Hom(X,D(i_X)) \to \Hom(X,D(j))$ is an isomorphism for all $j \geq i_X$. Equivalently, $\Hom(X,D(j)) \to \Hom(X,D(j'))$ is an isomorphism for all $i_X \leq j \leq j'$. Since $\C$ is w.l.o.g. countable, we find $i_\infty \in \I$ such that $i_\infty \geq i_X$ for all $X \in \C$. Then for all $i_\infty \leq j \leq j'$ and every $X \in \C$ the map $\Hom(X,D(j)) \to \Hom(X,D(j'))$ is an isomorphism. By the Yoneda Lemma, this means that $D(j) \to D(j')$ is an isomorphism. This finishes the proof of the reduction. + + So now let $D : \I \to \FinSet$ be a diagram indexed by a $\aleph_1$-filtered poset. The transition maps will be denoted by $u_{ij} : D(i) \to D(j)$ for $i \leq j$. Let $L \in \Set$ be the colimit of $D$ considered as a diagram of sets. Thus, we have maps $u_i : D(i) \to L$ satisfying $u_j \circ u_{ij} = u_i$. These maps are jointly surjective, and we have $u_i(x)=u_i(x)$ if and only if $u_{ij}(x) = u_{ij}(y)$ for some $j \geq i$. + + We first show that $L$ is finite. If not, choose distinct elements $a_1,a_2,\dotsc$ in $L$. Each $a_n$ has a preimage $b_{i_n} \in D(i_n)$ for some $i_n \in \I$. Choose some $j \in \I$ with $i_n \leq j$ for all $n$. Then all $a_1,a_2,\dotsc$ have a preimage in $D(j)$. But this is a finite set by assumption; so we have a contradiction. + + Next, we claim that there is some $i_0 \in \I$ such that $u_{i_0} : D(i_0) \to L$ is surjective. Each of the finitely many elements in $L$ has a preimage in some $D(i)$. Since $\I$ is filtered, there is some index which works for all elements. + + Then for every $j \geq i_0$, also the map $u_j : D(j) \to L$ is surjective. However, it does not have to be injective. + + Assume we have found $i_\infty \geq i_0$ such that $u_j$ is injective (and hence bijective) for all $j \geq i_\infty$. Then for all $i_\infty \leq j \leq j'$ the equation $u_{j'} \circ u_{jj'} = u_j$ shows that $u_{jj'}$ is an isomorphism, and we are done. + + So assume the contrary: for all $i \geq i_0$ there is $j \geq i$ such that $u_j$ is not injective. By the description of the elements in $L$, this means that there is some $k \geq j$ such that $u_{jk}$ is not injective. + + For $j \geq i_0$, consider the set $R_j$ of all pairs $a,b \in D(j)$ with $u_j(a)=u_j(b)$ in $L$. For each of these, there is some $k_j \geq j$ with $u_{jk}(a) = u_{jk}(b)$. Since $R_j$ is finite and $\I$ is filtered, we may choose $k_j$ independently from the pair. Thus, $u_{jk}$ induces an injective map $D(j) / R_j \hookrightarrow D(k_j)$. + + # TODO: complete this proof + is_equivalence: false - id: locally_presentable_another_definition diff --git a/databases/catdat/data/category-implications/filtered + sifted.yaml b/databases/catdat/data/category-implications/filtered + sifted.yaml index 1b1f2b3c..ce37ad89 100644 --- a/databases/catdat/data/category-implications/filtered + sifted.yaml +++ b/databases/catdat/data/category-implications/filtered + sifted.yaml @@ -39,27 +39,64 @@ where $f=g$; hence when the category is also sifted, all cospans must be of this form, and so any two parallel morphisms are equal. is_equivalence: false -- id: terminal_object_yields_filtered +- id: filtered_criterion assumptions: - - terminal object + - finitely cocomplete + conclusions: + - filtered + reason: Every finite diagram even admits a universal cocone. + is_equivalence: false + +- id: filtered_via_coequalizers + assumptions: + - coequalizers + - semi-strongly connected conclusions: - filtered reason: This is obvious. is_equivalence: false -- id: filtered_criterion +- id: aleph1-filtered-consequence assumptions: - - finitely cocomplete + - ℵ₁-filtered conclusions: - filtered - reason: Every finite diagram even admits a universal cocone. + reason: This is trivial. is_equivalence: false -- id: filtered_via_equalizers +- id: aleph1-filtered_criterion assumptions: - coequalizers - - semi-strongly connected + - countable coproducts conclusions: - - filtered + - ℵ₁-filtered + reason: Every countable diagram even admits a universal cocone. + is_equivalence: false + +- id: terminal_object_yields_kappa_filtered + assumptions: + - terminal object + conclusions: + - ℵ₁-filtered reason: This is obvious. is_equivalence: false + +- id: filtered-finite-thin + assumptions: + - thin + - filtered + - essentially finite + conclusions: + - terminal object + reason: Let $\C$ be a thin, filtered, and w.l.o.g. finite category. The identity diagram $\C \to \C$ admits a cocone. That is, there is an object $T$ with a morphism $A \to T$ for all $A \in \C$. Then $T$ is terminal. + is_equivalence: false + +- id: aleph1-filtered-countable-thin + assumptions: + - thin + - ℵ₁-filtered + - essentially countable + conclusions: + - terminal object + reason: Let $\C$ be a thin, $\aleph_1$-filtered, and w.l.o.g. countable category. The identity diagram $\C \to \C$ admits a cocone. That is, there is an object $T$ with a morphism $A \to T$ for all $A \in \C$. Then $T$ is terminal. + is_equivalence: false diff --git a/databases/catdat/data/category-implications/filtered colimits.yaml b/databases/catdat/data/category-implications/filtered colimits.yaml index 54184796..02239e20 100644 --- a/databases/catdat/data/category-implications/filtered colimits.yaml +++ b/databases/catdat/data/category-implications/filtered colimits.yaml @@ -61,6 +61,22 @@ reason: We may assume that the category $\C$ is finite and Cauchy complete. The answer at MO/509853 shows that every filtered colimit in $\C$ exists, in fact it is a retract of one of the objects in the diagram. Now apply this to the morphism category of $\C$. It follows that for every filtered diagram of morphisms $X_i \to Y_i$ their colimit $X_\infty \to Y_\infty$ exists, which is a retract of one of the $X_i \to Y_i$. Therefore, if every $X_i \to Y_i$ is a monomorphism, also $X_\infty \to Y_\infty$ is a monomorphism. is_equivalence: false +- id: aleph1-filtered-colimits-include-filtered-colimits + assumptions: + - filtered colimits + conclusions: + - ℵ₁-filtered colimits + reason: Every $\aleph_1$-filtered category is also $\aleph_0$-filtered, i.e. filtered. Therefore, every $\aleph_1$-filtered diagram is also a filtered diagram, hence has a colimit by assumption. + is_equivalence: false + +- id: kappa-filtered-colimits_require_Cauchy_complete + assumptions: + - ℵ₁-filtered colimits + conclusions: + - Cauchy complete + reason: More generally, if $\kappa$ is any infinite regular cardinal, a category with $\kappa$-filtered colimits must be Cauchy cocomplete. This is because the walking idempotent is $\kappa$-filtered. See also Makkai-Pare, Prop. 2.2.1. + is_equivalence: false + - id: sifted_categories_are_connected assumptions: - connected colimits diff --git a/databases/catdat/data/category-properties/aleph1-accessible.yaml b/databases/catdat/data/category-properties/aleph1-accessible.yaml index 23532d7a..6b3d96c2 100644 --- a/databases/catdat/data/category-properties/aleph1-accessible.yaml +++ b/databases/catdat/data/category-properties/aleph1-accessible.yaml @@ -1,6 +1,6 @@ id: ℵ₁-accessible relation: is -description: This is the special case of the notion of $\kappa$-accessible categories, where $\kappa = \aleph_1$ is the first uncountable cardinal. +description: This is the special case of the notion of a $\kappa$-accessible category, where $\kappa = \aleph_1$ is the first uncountable cardinal. Concretely, a category is $\aleph_1$-accessible when it has $\aleph_1$-filtered colimits and there is a small set $G$ of $\aleph_1$-presentable objects such that every object is a $\aleph_1$-filtered colimit of objects in $G$. nlab_link: https://ncatlab.org/nlab/show/accessible+category invariant_under_equivalences: true @@ -8,3 +8,4 @@ related_properties: - accessible - finitely accessible - locally ℵ₁-presentable + - ℵ₁-filtered colimits diff --git a/databases/catdat/data/category-properties/aleph1-filtered colimits.yaml b/databases/catdat/data/category-properties/aleph1-filtered colimits.yaml new file mode 100644 index 00000000..1a583f6a --- /dev/null +++ b/databases/catdat/data/category-properties/aleph1-filtered colimits.yaml @@ -0,0 +1,12 @@ +id: ℵ₁-filtered colimits +relation: has +description: A category has $\aleph_1$-filtered colimits if it has colimits of diagrams indexed by small $\aleph_1$-filtered categories. This is the special case of having small $\kappa$-filtered colimits for $\kappa=\aleph_1$, the first uncountable cardinal. +nlab_link: https://ncatlab.org/nlab/show/filtered+colimit +dual_property: null +invariant_under_equivalences: true + +related_properties: + - cocomplete + - filtered colimits + - ℵ₁-accessible + - ℵ₁-filtered diff --git a/databases/catdat/data/category-properties/aleph1-filtered.yaml b/databases/catdat/data/category-properties/aleph1-filtered.yaml new file mode 100644 index 00000000..52183594 --- /dev/null +++ b/databases/catdat/data/category-properties/aleph1-filtered.yaml @@ -0,0 +1,11 @@ +id: ℵ₁-filtered +relation: is +description: A category is $\aleph_1$-filtered if every countable diagram admits a cocone. This is the special case of the notion of a $\kappa$-filtered category for $\kappa = \aleph_1$, the first uncountable cardinal. An equivalent characterization is given as Theorem 2.2 at the nLab. +nlab_link: https://ncatlab.org/nlab/show/filtered+category +dual_property: null +invariant_under_equivalences: true + +related_properties: + - filtered + - ℵ₁-filtered colimits + - cocomplete diff --git a/databases/catdat/data/category-properties/filtered colimits.yaml b/databases/catdat/data/category-properties/filtered colimits.yaml index ebab748e..9cc8bc4f 100644 --- a/databases/catdat/data/category-properties/filtered colimits.yaml +++ b/databases/catdat/data/category-properties/filtered colimits.yaml @@ -10,3 +10,4 @@ related_properties: - directed colimits - filtered - sifted colimits + - ℵ₁-filtered colimits diff --git a/databases/catdat/data/category-properties/filtered.yaml b/databases/catdat/data/category-properties/filtered.yaml index 938bdf4a..7ce6254b 100644 --- a/databases/catdat/data/category-properties/filtered.yaml +++ b/databases/catdat/data/category-properties/filtered.yaml @@ -1,10 +1,12 @@ id: filtered relation: is -description: A category is filtered if every finite diagram admits a cocone. Equivalently, it is inhabited, for every two objects $x,y$ there is a cospan $x \rightarrow s \leftarrow y$ (not necessarily universal), and every parallel pair $x \rightrightarrows y$ is coequalized by some morphism $y \to c$ (not necessarily universal). +description: A category is filtered if every finite diagram admits a cocone. Equivalently, it is inhabited, for every two objects $x,y$ there is a cospan $x \rightarrow s \leftarrow y$ (not necessarily universal), and every parallel pair $x \rightrightarrows y$ is coequalized by some morphism $y \to c$ (not necessarily universal). This is the special case of the notion of a $\kappa$-filtered category for $\kappa = \aleph_0$. nlab_link: https://ncatlab.org/nlab/show/filtered+category dual_property: cofiltered invariant_under_equivalences: true related_properties: + - ℵ₁-filtered - filtered colimits - - finitely cocomplete + - cocomplete + - sifted diff --git a/databases/catdat/scripts/expected-data/Ab.json b/databases/catdat/scripts/expected-data/Ab.json index 5727343b..80ed4b99 100644 --- a/databases/catdat/scripts/expected-data/Ab.json +++ b/databases/catdat/scripts/expected-data/Ab.json @@ -79,6 +79,7 @@ "finite copowers": true, "binary copowers": true, "filtered": true, + "ℵ₁-filtered": true, "cofiltered": true, "sifted": true, "cosifted": true, @@ -89,6 +90,7 @@ "accessible": true, "finitely accessible": true, "ℵ₁-accessible": true, + "ℵ₁-filtered colimits": true, "generalized variety": true, "locally finitely multi-presentable": true, "locally multi-presentable": true, diff --git a/databases/catdat/scripts/expected-data/Set.json b/databases/catdat/scripts/expected-data/Set.json index 5e68abb2..746b5232 100644 --- a/databases/catdat/scripts/expected-data/Set.json +++ b/databases/catdat/scripts/expected-data/Set.json @@ -77,12 +77,14 @@ "finite copowers": true, "binary copowers": true, "filtered": true, + "ℵ₁-filtered": true, "cofiltered": true, "sifted": true, "cosifted": true, "accessible": true, "finitely accessible": true, "ℵ₁-accessible": true, + "ℵ₁-filtered colimits": true, "generalized variety": true, "locally finitely multi-presentable": true, "locally multi-presentable": true, diff --git a/databases/catdat/scripts/expected-data/Top.json b/databases/catdat/scripts/expected-data/Top.json index 1f714393..e245220a 100644 --- a/databases/catdat/scripts/expected-data/Top.json +++ b/databases/catdat/scripts/expected-data/Top.json @@ -61,6 +61,7 @@ "finite copowers": true, "binary copowers": true, "filtered": true, + "ℵ₁-filtered": true, "cofiltered": true, "sifted": true, "cosifted": true, @@ -137,6 +138,7 @@ "accessible": false, "finitely accessible": false, "ℵ₁-accessible": false, + "ℵ₁-filtered colimits": true, "generalized variety": false, "locally finitely multi-presentable": false, "locally multi-presentable": false,