*For thin categories, the properties codistributive and distributive are equivalent.' +), +( + 'FS', + 'multi-initial object', + FALSE, + 'This is trivial.' +), +( + 'FS', + 'countable', + FALSE, + 'This is trivial.' ); diff --git a/database/data/004_property-assignments/FinAb.sql b/database/data/004_property-assignments/FinAb.sql index ff7575ef..0969814b 100644 --- a/database/data/004_property-assignments/FinAb.sql +++ b/database/data/004_property-assignments/FinAb.sql @@ -13,7 +13,7 @@ VALUES ), ( 'FinAb', - 'essentially small', + 'essentially countable', TRUE, 'The underlying set of a finite structure can be chosen to be a subset of $\mathbb{N}$.' ), @@ -29,6 +29,12 @@ VALUES TRUE, 'This is a simple special case of Pontryagin duality: The functor $\hom(-,\mathbb{Q}/\mathbb{Z})$ provides the equivalence.' ), +( + 'FinAb', + 'ℵ₁-accessible', + TRUE, + 'The inclusion $\mathbf{FinAb} \hookrightarrow \mathbf{Ab}$ is closed under ℵ₁-filtered colimits, because ℵ₁-filtered colimits are computed in the same way as in $\mathbf{Set}$ and any ℵ₁-filtered colimit of finite sets is again finite. Since every finite abelian group is ℵ₁-presentable in $\mathbf{Ab}$, it is still ℵ₁-presentable in $\mathbf{FinAb}$, hence $\mathbf{FinAb}$ is ℵ₁-accessible, where every object is ℵ₁-presentable.' +), ( 'FinAb', 'small', @@ -58,4 +64,10 @@ VALUES 'skeletal', FALSE, 'There are many trivial and hence isomorphic groups which are not equal.' +), +( + 'FinAb', + 'countable', + FALSE, + 'This is trivial.' ); diff --git a/database/data/004_property-assignments/FinGrp.sql b/database/data/004_property-assignments/FinGrp.sql index 096cc4aa..2f70092a 100644 --- a/database/data/004_property-assignments/FinGrp.sql +++ b/database/data/004_property-assignments/FinGrp.sql @@ -19,7 +19,7 @@ VALUES ), ( 'FinGrp', - 'essentially small', + 'essentially countable', TRUE, 'The underlying set of a finite structure can be chosen to be a subset of $\mathbb{N}$.' ), @@ -59,6 +59,12 @@ VALUES TRUE, 'Since epimorphisms are surjective (see below), this is the first isomorphism theorem for finite groups.' ), +( + 'FinGrp', + 'ℵ₁-accessible', + TRUE, + 'The inclusion $\mathbf{FinGrp} \hookrightarrow \mathbf{Grp}$ is closed under ℵ₁-filtered colimits, because ℵ₁-filtered colimits are computed in the same way as in $\mathbf{Set}$ and any ℵ₁-filtered colimit of finite sets is again finite. Since every finite group is ℵ₁-presentable in $\mathbf{Grp}$, it is still ℵ₁-presentable in $\mathbf{FinGrp}$, hence $\mathbf{FinGrp}$ is ℵ₁-accessible, where every object is ℵ₁-presentable.' +), ( 'FinGrp', 'normal', @@ -106,4 +112,10 @@ VALUES 'sequential colimits', FALSE, 'This follows from this lemma.' +), +( + 'FinGrp', + 'countable', + FALSE, + 'This is trivial.' ); \ No newline at end of file diff --git a/database/data/004_property-assignments/FinOrd.sql b/database/data/004_property-assignments/FinOrd.sql index 6c952719..94fe6031 100644 --- a/database/data/004_property-assignments/FinOrd.sql +++ b/database/data/004_property-assignments/FinOrd.sql @@ -61,7 +61,7 @@ VALUES ), ( 'FinOrd', - 'essentially small', + 'essentially countable', TRUE, 'Every finite ordered set is isomorphic to $\{0 < \cdots < n-1 \}$ for some $n \in \mathbb{N}$.' ), @@ -124,4 +124,10 @@ VALUES 'one-way', FALSE, 'There are three different order-preserving maps $\{0 < 1\} \to \{0 < 1\}$.' +), +( + 'FinOrd', + 'countable', + FALSE, + 'This is trivial.' ); diff --git a/database/data/004_property-assignments/FinSet.sql b/database/data/004_property-assignments/FinSet.sql index d85eedd2..d24df1d2 100644 --- a/database/data/004_property-assignments/FinSet.sql +++ b/database/data/004_property-assignments/FinSet.sql @@ -13,7 +13,7 @@ VALUES ), ( 'FinSet', - 'essentially small', + 'essentially countable', TRUE, 'Every finite set is isomorphic to some $[n] = \{1,\dotsc,n\}$ for some $n \in \mathbb{N}$.' ), @@ -41,6 +41,12 @@ VALUES TRUE, 'The two-element set is a cogenerator.' ), +( + 'FinSet', + 'ℵ₁-accessible', + TRUE, + 'The inclusion $\mathbf{FinSet} \hookrightarrow \mathbf{Set}$ is closed under ℵ₁-filtered colimits, that is, any ℵ₁-filtered colimit of finite sets is again finite. Since every finite set is ℵ₁-presentable in $\mathbf{Set}$, it is still ℵ₁-presentable in $\mathbf{FinSet}$. Therefore, $\mathbf{FinSet}$ is ℵ₁-accessible, where every object is ℵ₁-presentable.' +), ( 'FinSet', 'small', @@ -70,4 +76,10 @@ VALUES 'Malcev', FALSE, 'There are lots of non-symmetric reflexive relations.' +), +( + 'FinSet', + 'countable', + FALSE, + 'This is trivial.' ); diff --git a/database/data/004_property-assignments/Fld.sql b/database/data/004_property-assignments/Fld.sql index 51a01ab8..4337fce6 100644 --- a/database/data/004_property-assignments/Fld.sql +++ b/database/data/004_property-assignments/Fld.sql @@ -11,18 +11,6 @@ VALUES TRUE, 'There is a forgetful functor $\mathbf{Fld} \to \mathbf{Set}$ and $\mathbf{Set}$ is locally small.' ), -( - 'Fld', - 'directed colimits', - TRUE, - 'Consider a directed diagram $(F_i)$ of fields and take the colimit $F$ in the category of commutative rings. Now one checks that $F$ is a field as well, and the universal property remains true for fields.' -), -( - 'Fld', - 'connected limits', - TRUE, - 'Consider a connected diagram $(F_i)$ of fields and take the limit $F$ in the category of commutative rings. Now one checks that $F$ is a field as well, and the universal property remains true for fields. Namely, $1 = 0$ in $F$ would imply that $1 = 0$ in each $F_i$ and hence, since the diagram is connected, in some $F_i$, which is a contradiction. And if $x \in F$ is non-zero, then all components $x_i$ are non-zero and hence invertible: Choose some $j$ such that $x_j$ is non-zero. Since there is a zig zag path of morphisms between $i$ and $j$ in the index category, which get mapped to field homomorphisms which are injective, it follows that $x_i$ is non-zero.' -), ( 'Fld', 'inhabited', @@ -35,12 +23,6 @@ VALUES TRUE, 'It is well-known that every field homomorphism is injective and hence a monomorphism.' ), -( - 'Fld', - 'well-powered', - TRUE, - 'The subfields of a given field form a set.' -), ( 'Fld', 'well-copowered', @@ -49,9 +31,9 @@ VALUES ), ( 'Fld', - 'generating set', + 'multi-algebraic', TRUE, - 'The fields $Q(\mathbb{Z}[X]/\mathfrak{p})$, where $\mathfrak{p}$ runs through all prime ideals of the polynomial ring, provide a generating set. This is because for every element $a \in K$ of a field $K$ there is a prime ideal $\mathfrak{p}$ with a homomorphism $Q(\mathbb{Z}[X]/\mathfrak{p}) \to K$ mapping $[X]$ to $a$: There is a homomorphism $\mathbb{Z}[X] \to K$ mapping $X \mapsto a$. Let $\mathfrak{p}$ be its kernel. Then it extends to a field homomorphism as desired.' + 'See Eg. 4.3(1) in [AR01].' ), ( 'Fld', @@ -83,12 +65,6 @@ VALUES FALSE, 'We apply this lemma to the collection of fields: Any homomorphism of fields is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).' ), -( - 'Fld', - 'essentially small', - FALSE, - 'Consider function fields in any number of variables.' -), ( 'Fld', 'skeletal', @@ -112,4 +88,10 @@ VALUES 'binary powers', FALSE, 'Assume that the product $P := \mathbb{Q}(\sqrt{2}) \times \mathbb{Q}(\sqrt{2})$ exists. This field is isomorphic to a subfield of $\mathbb{Q}(\sqrt{2})$, hence $P \cong \mathbb{Q}$ or $P \cong \mathbb{Q}(\sqrt{2})$. In the first case, the two projections $P \rightrightarrows \mathbb{Q}(\sqrt{2})$ must be equal, which means that every two homomorphisms $K \rightrightarrows \mathbb{Q}(\sqrt{2})$ are equal, which is absurd (take $K = \mathbb{Q}(\sqrt{2})$ and its two automorphisms). In the second case, the projections induce for every field $K$ a bijection $\mathrm{Hom}(K,\mathbb{Q}(\sqrt{2})) \cong \mathrm{Hom}(K,\mathbb{Q}(\sqrt{2}))^2$, which however fails for $K = \mathbb{Q}(\sqrt{2})$: the left hand side has $2$ elements, the right hand side has $4$ elements. A more general result about products in $\mathbf{Fld}$ can be found at MSE/359352.' +), +( + 'Fld', + 'multi-terminal object', + FALSE, + 'Every field has a non-trivial extension, for instance, the rational function field over itself in one variable. Hence, a multi-terminal object never exists.' ); diff --git a/database/data/004_property-assignments/Man.sql b/database/data/004_property-assignments/Man.sql index b3fc32c9..304c9f6c 100644 --- a/database/data/004_property-assignments/Man.sql +++ b/database/data/004_property-assignments/Man.sql @@ -119,4 +119,10 @@ VALUES 'sequential colimits', FALSE, 'If $\mathbf{Man}$ had sequential colimits, then by this lemma there would be a manifold $M$ that admits a split epimorphism $M \to \mathbb{R}^n$ for every $n$. But then $M$ will have an infinite-dimensional tangent space, which is a contradiction.' +), +( + 'Man', + 'countable', + FALSE, + 'This is trivial.' ); diff --git a/database/data/004_property-assignments/N.sql b/database/data/004_property-assignments/N.sql index 79a47446..7d367ccb 100644 --- a/database/data/004_property-assignments/N.sql +++ b/database/data/004_property-assignments/N.sql @@ -53,6 +53,12 @@ VALUES TRUE, 'This is because the natural numbers with respect to $<$ are well-founded.' ), +( + 'N', + 'countable', + TRUE, + 'This is trivial.' +), ( 'N', 'countable coproducts', diff --git a/database/data/004_property-assignments/N_oo.sql b/database/data/004_property-assignments/N_oo.sql index c301d62a..beba103d 100644 --- a/database/data/004_property-assignments/N_oo.sql +++ b/database/data/004_property-assignments/N_oo.sql @@ -11,6 +11,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'N_oo', + 'countable', + TRUE, + 'This is trivial.' +), ( 'N_oo', 'coproducts', diff --git a/database/data/004_property-assignments/Set_op.sql b/database/data/004_property-assignments/Set_op.sql deleted file mode 100644 index 0e6c6982..00000000 --- a/database/data/004_property-assignments/Set_op.sql +++ /dev/null @@ -1,13 +0,0 @@ -INSERT INTO category_property_assignments ( - category_id, - property_id, - is_satisfied, - reason -) -VALUES -( - 'Set_op', - 'locally presentable', - FALSE, - 'This follows from the fact that the opposite category of a complete accessible large category is never accessible. See Makkai-Pare, Thm. 3.4.3.' -); diff --git a/database/data/004_property-assignments/Setne.sql b/database/data/004_property-assignments/Setne.sql index 90f13269..8fb760e1 100644 --- a/database/data/004_property-assignments/Setne.sql +++ b/database/data/004_property-assignments/Setne.sql @@ -83,6 +83,24 @@ VALUES TRUE, 'Use constant maps.' ), +( + 'Setne', + 'generalized variety', + TRUE, + '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 small sifted colimit of them.' +), +( + 'Setne', + 'finitely accessible', + TRUE, + '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 small filtered colimit of them.' +), +( + 'Setne', + 'multi-complete', + TRUE, + '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 cone gives a multi-limit of $D$ in $\mathbf{Set}_{\neq \varnothing}$.' +), ( 'Setne', 'sequential limits', diff --git a/database/data/004_property-assignments/Sp.sql b/database/data/004_property-assignments/Sp.sql index 58181ab1..b75420d1 100644 --- a/database/data/004_property-assignments/Sp.sql +++ b/database/data/004_property-assignments/Sp.sql @@ -64,4 +64,10 @@ VALUES 'generator', FALSE, 'Assume that a generator $G$ exists. For $n \geq 0$ let $F_n$ be the combinatorial species of sets of cardinality $\neq n$: $F_n(A) = \varnothing$ when $A$ has cardinality $n$, otherwise $F_n(A) = \{A\}$. There are two different morphisms $F_n \rightrightarrows F_n \sqcup F_n$. Hence, there must be at least one morphism $G \to F_n$. If $A$ has cardinality $n$, this implies $G(A) = \varnothing$. Since this holds for all $n$, $G$ is the initial object. But this is clearly no generator (it would mean that the category is thin).' +), +( + 'Sp', + 'essentially countable', + FALSE, + 'Any function $f\colon\mathbb{N} \to \mathbb{N}$ can be regarded as a combinatorial species with trivial actions, and distinct functions yield non-isomorphic species.' ); \ No newline at end of file diff --git a/database/data/004_property-assignments/Top.sql b/database/data/004_property-assignments/Top.sql index 7814a7c4..351e447f 100644 --- a/database/data/004_property-assignments/Top.sql +++ b/database/data/004_property-assignments/Top.sql @@ -118,4 +118,10 @@ VALUES 'co-Malcev', FALSE, 'See MO/509548. We can also phrase the proof as follows: Consider the forgetful functor $U : \mathbf{Top} \to \mathbf{Set}$ and the relation $R \subseteq U^2$ defined by $R(X) := \{(x,y) \in U(X)^2 : x \in \overline{\{y\}} \}$. Both are representable: $U$ by the singleton and $R$ by the Sierpinski space. It is clear that $R$ is reflexive, but not symmetric.' +), +( + 'Top', + 'coaccessible', + FALSE, + 'Assume $\mathbf{Top}$ is coaccessible. Let $p\colon S \to I$ be the identity map from the Sierpinski space to the two-element indiscrete space. Then, a topological space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete spaces, which is equivalent to $\mathbf{Set}$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\mathbf{Set}$ is not coaccessible, this is a contradiction.' ); diff --git a/database/data/004_property-assignments/Top_pointed.sql b/database/data/004_property-assignments/Top_pointed.sql index 9709b606..f236cda3 100644 --- a/database/data/004_property-assignments/Top_pointed.sql +++ b/database/data/004_property-assignments/Top_pointed.sql @@ -130,6 +130,12 @@ VALUES 'regular quotient object classifier', FALSE, 'We can recycle the proof for the category of pointed sets using discrete topological spaces.' +), +( + 'Top*', + 'coaccessible', + FALSE, + 'We can adjust the proof for $\mathbf{Top}$ as follows: Assume $\mathbf{Top}_*$ is coaccessible. Let $S_0=\{x,*\}$ be the pointed topological space such that $\{*\}$ is the only non-trivial open set, and let $S_1=\{x,*\}$ be the pointed space such that $\{x\}$ is the only non-trivial open set. Let $p_i\colon S_i \to \{x,*\}$ be the identity function to the two-element indiscrete pointed space. Then, a pointed topological space is discrete if and only if it is projective to the morphisms $p_0$ and $p_1$. This implies that the full subcategory spanned by all discrete pointed spaces, which is equivalent to $\mathbf{Set}_*$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\mathbf{Set}_*$ is not coaccessible, this is a contradiction.' ); diff --git a/database/data/004_property-assignments/Z_div.sql b/database/data/004_property-assignments/Z_div.sql index d18ec05b..4f38b97f 100644 --- a/database/data/004_property-assignments/Z_div.sql +++ b/database/data/004_property-assignments/Z_div.sql @@ -11,6 +11,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'Z_div', + 'countable', + TRUE, + 'This is trivial.' +), ( 'Z_div', 'products', diff --git a/database/data/004_property-assignments/real_interval.sql b/database/data/004_property-assignments/real_interval.sql index 9f66736c..85cd3ccb 100644 --- a/database/data/004_property-assignments/real_interval.sql +++ b/database/data/004_property-assignments/real_interval.sql @@ -37,7 +37,7 @@ VALUES ), ( 'real_interval', - 'essentially finite', + 'essentially countable', FALSE, 'This is trivial.' ), diff --git a/database/data/004_property-assignments/walking_commutative_square.sql b/database/data/004_property-assignments/walking_commutative_square.sql index 86551e68..6f3f356a 100644 --- a/database/data/004_property-assignments/walking_commutative_square.sql +++ b/database/data/004_property-assignments/walking_commutative_square.sql @@ -17,6 +17,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_commutative_square', + 'small', + TRUE, + 'This is trivial.' +), ( 'walking_commutative_square', 'infinitary distributive', diff --git a/database/data/004_property-assignments/walking_composable_pair.sql b/database/data/004_property-assignments/walking_composable_pair.sql index bbc83274..d0476dba 100644 --- a/database/data/004_property-assignments/walking_composable_pair.sql +++ b/database/data/004_property-assignments/walking_composable_pair.sql @@ -11,6 +11,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_composable_pair', + 'small', + TRUE, + 'This is trivial.' +), ( 'walking_composable_pair', 'semi-strongly connected', diff --git a/database/data/004_property-assignments/walking_fork.sql b/database/data/004_property-assignments/walking_fork.sql index 970f6844..9cb538b1 100644 --- a/database/data/004_property-assignments/walking_fork.sql +++ b/database/data/004_property-assignments/walking_fork.sql @@ -11,6 +11,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_fork', + 'small', + TRUE, + 'This is trivial.' +), ( 'walking_fork', 'semi-strongly connected', diff --git a/database/data/004_property-assignments/walking_idempotent.sql b/database/data/004_property-assignments/walking_idempotent.sql index 9b13b5cf..37dcde65 100644 --- a/database/data/004_property-assignments/walking_idempotent.sql +++ b/database/data/004_property-assignments/walking_idempotent.sql @@ -11,6 +11,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_idempotent', + 'small', + TRUE, + 'This is trivial.' +), ( 'walking_idempotent', 'generator', diff --git a/database/data/004_property-assignments/walking_isomorphism.sql b/database/data/004_property-assignments/walking_isomorphism.sql index 8bfc2e45..e11c8406 100644 --- a/database/data/004_property-assignments/walking_isomorphism.sql +++ b/database/data/004_property-assignments/walking_isomorphism.sql @@ -17,6 +17,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_isomorphism', + 'small', + TRUE, + 'This is trivial.' +), ( 'walking_isomorphism', 'skeletal', diff --git a/database/data/004_property-assignments/walking_morphism.sql b/database/data/004_property-assignments/walking_morphism.sql index 73c9607b..89328cd8 100644 --- a/database/data/004_property-assignments/walking_morphism.sql +++ b/database/data/004_property-assignments/walking_morphism.sql @@ -23,6 +23,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_morphism', + 'small', + TRUE, + 'This is trivial.' +), ( 'walking_morphism', 'infinitary distributive', diff --git a/database/data/004_property-assignments/walking_pair.sql b/database/data/004_property-assignments/walking_pair.sql index e1c0a20b..08e119aa 100644 --- a/database/data/004_property-assignments/walking_pair.sql +++ b/database/data/004_property-assignments/walking_pair.sql @@ -11,6 +11,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_pair', + 'small', + TRUE, + 'This is trivial.' +), ( 'walking_pair', 'self-dual', diff --git a/database/data/004_property-assignments/walking_span.sql b/database/data/004_property-assignments/walking_span.sql index 7583e21c..90a18a94 100644 --- a/database/data/004_property-assignments/walking_span.sql +++ b/database/data/004_property-assignments/walking_span.sql @@ -11,6 +11,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_span', + 'small', + TRUE, + 'This is trivial.' +), ( 'walking_span', 'skeletal', @@ -41,6 +47,12 @@ VALUES TRUE, 'The slice category over $0$ is the trivial category, and the slice category over $1$ is the interval category, which is cartesian closed (see there). The same holds for $2$ by symmetry.' ), +( + 'walking_span', + 'multi-algebraic', + TRUE, + 'We first remark that for a set $X$, the identity span $(\mathrm{id},\mathrm{id})\colon X \leftarrow X \rightarrow X$ exhibits a product if and only if $X$ is either a singleton or the empty set. Therefore, there is a (finite product, coproduct)-sketch whose $\mathbf{Set}$-model is precisely a pair $(X,Y)$ of sets such that each of $X$ and $Y$ is either a singleton or the empty set and the product $X \times Y$ is the empty set. Any $\mathbf{Set}$-model of such a sketch is isomorphic to either $(\varnothing, \varnothing)$, $(\varnothing, 1)$, or $(1, \varnothing)$; hence the category of models is equivalent to the walking span.' +), ( 'walking_span', 'sifted', diff --git a/database/data/005_implications/001_limits-colimits-existence-implications.sql b/database/data/005_implications/001_limits-colimits-existence-implications.sql index 15eaa5a3..8ef2e6c2 100644 --- a/database/data/005_implications/001_limits-colimits-existence-implications.sql +++ b/database/data/005_implications/001_limits-colimits-existence-implications.sql @@ -169,9 +169,9 @@ VALUES ), ( 'finite_filtered_colimits', - '["finite", "Cauchy complete"]', - '["filtered colimits"]', - 'See MO/509853.', + '["essentially finite", "Cauchy complete"]', + '["finitely accessible"]', + 'See MO/509853, where it is in fact shown that the ind-completion of any finite Cauchy-complete category becomes itself.', FALSE ), ( @@ -292,4 +292,32 @@ VALUES '["powers"]', 'The product $X^I$ is the cofiltered limit of the finite powers $X^E$, where $E$ ranges over the finite subsets of $I$.', FALSE +), +( + 'multi-complete_generalize_limits', + '["complete"]', + '["multi-complete"]', + 'Limits are precisely multi-limits such that the set of cones is singleton.', + FALSE +), +( + 'multi-terminal_special_case', + '["multi-complete"]', + '["multi-terminal object"]', + 'This is trivial.', + FALSE +), +( + 'multi-terminal_with_connected', + '["connected","multi-terminal object"]', + '["terminal object"]', + 'Let $(T_i)_{i\in I}$ be a multi-terminal object in a connected category $\mathcal{C}$. By definition of multi-terminal objects, for each object $C$, there are a unique index $i_C\in I$ and a unique morphism $C \to T_{i_C}$. Since the index $i_C$ is invariant under connected components, $I$ must be a singleton. The converse is trivial.', + TRUE +), +( + 'multi-complete_with_finite_coproducts', + '["multi-complete", "finite coproducts"]', + '["complete"]', + 'Let $D\colon \mathcal{S} \to \mathcal{C}$ be a small diagram in a category $\mathcal{C}$. Since $\mathcal{C}$ has finite coproducts, the category $\mathbf{Cone}(D)$ of cones over $D$ has finite coproducts. In particular, $\mathbf{Cone}(D)$ is connected, hence a multi-terminal object in it automatically becomes a terminal object.', + FALSE ); \ No newline at end of file diff --git a/database/data/005_implications/003_size-constraints-implications.sql b/database/data/005_implications/003_size-constraints-implications.sql index 5b4ee2cf..2e209325 100644 --- a/database/data/005_implications/003_size-constraints-implications.sql +++ b/database/data/005_implications/003_size-constraints-implications.sql @@ -23,13 +23,27 @@ VALUES ( 'finite_consequence', '["finite"]', - '["small", "essentially finite"]', + '["countable", "essentially finite"]', 'This is trivial.', FALSE ), ( - 'essentially_finite_consequence', + 'essentially_finite_raise', '["essentially finite"]', + '["essentially countable"]', + 'This is trivial.', + FALSE +), +( + 'countable_consequence', + '["countable"]', + '["essentially countable"]', + 'This is trivial.', + FALSE +), +( + 'essentially_countable_consequence', + '["essentially countable"]', '["essentially small"]', 'This is trivial.', FALSE diff --git a/database/data/005_implications/006_trivial-categories-implications.sql b/database/data/005_implications/006_trivial-categories-implications.sql index fe81e4d6..89749548 100644 --- a/database/data/005_implications/006_trivial-categories-implications.sql +++ b/database/data/005_implications/006_trivial-categories-implications.sql @@ -62,6 +62,13 @@ VALUES 'See Mac Lane, V.2, Prop. 3. The proof works for any category with products.', FALSE ), +( + 'freyd_countable', + '["essentially countable", "countable products"]', + '["thin", "products"]', + 'To see that the category is thin, use Mac Lane, V.2, Prop. 3. The proof can easily be adapted to this case. So the category is equivalent to a countable preordered set. But then products are just infima, so that repetitions of objects do not matter, and every product can be reduced to a countable one.', + FALSE +), ( 'freyd_finite', '["essentially finite", "finite products"]', diff --git a/database/data/005_implications/007_locally-presentable-implications.sql b/database/data/005_implications/007_locally-presentable-implications.sql index 059756e1..c375ab86 100644 --- a/database/data/005_implications/007_locally-presentable-implications.sql +++ b/database/data/005_implications/007_locally-presentable-implications.sql @@ -6,13 +6,6 @@ INSERT INTO implication_input ( is_equivalence ) VALUES -( - 'locally_finitely_presentable_condition', - '["locally finitely presentable"]', - '["locally presentable"]', - 'Locally finitely presentable categories are by definition the locally $\aleph_0$-presentable categories.', - FALSE -), ( 'locally_finitely_presentable_raise', '["locally finitely presentable"]', @@ -28,10 +21,24 @@ VALUES FALSE ), ( - 'locally_presentable_consequence', - '["locally presentable"]', - '["locally essentially small", "well-powered", "well-copowered", "complete", "cocomplete", "generating set"]', - 'For locally essential smallness, see the proof of Prop. 2.1.5 in Makkai-Pare. For the other non-trivial conclusions see Adamek-Rosicky, Thm. 1.20, Cor. 1.28, Rem. 1.56, Thm. 1.58.', + 'accessible_trivial_consequence', + '["accessible"]', + '["well-powered", "generating set"]', + 'For well-poweredness, see nLab. For a $\kappa$-accessible category, a skeleton of the full subcategory spanned by $\kappa$-presentable objects is small and dense, hence is a generating set.', + FALSE +), +( + 'accessible_locally_small', + '["accessible"]', + '["locally essentially small"]', + 'See the proof of Prop. 2.1.5 in Makkai-Pare.', + FALSE +), +( + 'accessible_wellcopowered', + '["accessible", "pushouts"]', + '["well-copowered"]', + 'See Thm. 2.49 in Adamek-Rosicky or Prop. 6.1.3 in Makkai-Pare.', FALSE ), ( @@ -42,9 +49,9 @@ VALUES FALSE ), ( - 'locally_presentable_thin', - '["locally presentable", "self-dual"]', - '["thin"]', + 'locally_presentable_essentially_small', + '["locally presentable", "locally copresentable"]', + '["essentially small"]', 'This follows from Adamek-Rosicky, Thm. 1.64.', FALSE ), @@ -61,4 +68,151 @@ VALUES '["locally finitely presentable"]', 'See Adamek-Rosicky, Cor. 3.7.', FALSE +), +( + 'locally_presentable_definition_finite', + '["locally finitely presentable"]', + '["finitely accessible", "cocomplete"]', + 'This is trivial.', + TRUE +), +( + 'locally_presentable_definition_countable', + '["locally ℵ₁-presentable"]', + '["ℵ₁-accessible", "cocomplete"]', + 'This is trivial.', + TRUE +), +( + 'locally_presentable_definition', + '["locally presentable"]', + '["accessible", "cocomplete"]', + 'This is trivial.', + TRUE +), +( + 'finitely_accessible_raise', + '["finitely accessible"]', + '["ℵ₁-accessible"]', + 'This is because any regular cardinal is strictly smaller than its successor cardinal. See nLab.', + FALSE +), +( + 'countably_accessible_special_case', + '["ℵ₁-accessible"]', + '["accessible"]', + 'This is trivial.', + FALSE +), +( + 'accessible_require_filtered_colimit', + '["finitely accessible"]', + '["filtered colimits"]', + 'This is trivial.', + FALSE +), +( + 'accessible_require_Cauchy_complete', + '["accessible"]', + '["Cauchy complete"]', + 'This is because the walking idempotent is $\kappa$-filtered for any regular cardinal $\kappa$.', + FALSE +), +( + 'small_accessible_characterization', + '["essentially small", "accessible"]', + '["essentially small", "Cauchy complete"]', + 'See Makkai-Pare, Thm. 2.2.2.', + TRUE +), +( + 'countably_accessible_thin', + '["essentially countable", "thin"]', + '["ℵ₁-accessible"]', + '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.', + FALSE +), +( + 'locally_presentable_another_definition', + '["locally presentable"]', + '["accessible", "complete"]', + 'See Makkai-Pare, Thm. 6.1.4.', + TRUE +), +( + 'locally_strongly_finitely_presentable_definition', + '["locally strongly finitely presentable"]', + '["generalized variety", "cocomplete"]', + 'This is trivial.', + TRUE +), +( + 'generalized_variety_require_sifted_colimit', + '["generalized variety"]', + '["sifted colimits"]', + 'This is trivial.', + FALSE +), +( + 'generalized_variety_implies_accessible', + '["generalized variety"]', + '["ℵ₁-accessible"]', + 'See [AR01, Remark 4.8(2)].', + FALSE +), +( + 'locally_multi-presentable_definition', + '["locally multi-presentable"]', + '["accessible", "connected limits"]', + 'This is trivial.', + TRUE +), +( + 'locally_multi-presentable_another_definition', + '["locally multi-presentable"]', + '["accessible", "multi-cocomplete"]', + 'See Adamek-Rosicky, 4.30.', + TRUE +), +( + 'locally_finitely_multi-presentable_definition', + '["locally finitely multi-presentable"]', + '["finitely accessible", "connected limits"]', + 'This is trivial.', + TRUE +), +( + 'locally_finitely_multi-presentable_another_definition', + '["locally finitely multi-presentable"]', + '["finitely accessible", "multi-cocomplete"]', + 'See Adamek-Rosicky, 4.30.', + TRUE +), +( + 'locally_poly-presentable_definition', + '["locally poly-presentable"]', + '["accessible", "wide pullbacks"]', + 'This is trivial.', + TRUE +), +( + 'multi-algebraic_implies_locally_finitely_multi-presentable', + '["multi-algebraic"]', + '["locally finitely multi-presentable"]', + 'This follows from the fact that a category is locally finitely multi-presentable if and only if it is equivalent to the category of models of an FLC-sketch, where FLC represents finite limits and small coproducts.', + FALSE +), +( + 'varieties_are_multi-algebraic', + '["locally strongly finitely presentable"]', + '["multi-algebraic"]', + 'This is because that every FP-sketch is an FPC-sketch.', + FALSE +), +( + 'multi-algebraic_another_definition', + '["multi-algebraic"]', + '["generalized variety", "multi-cocomplete"]', + 'See [AR01, Thm. 4.4].', + TRUE ); \ 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..8d26b09e 100644 --- a/database/data/007_special-morphisms/002_isomorphisms.sql +++ b/database/data/007_special-morphisms/002_isomorphisms.sql @@ -51,7 +51,7 @@ VALUES 'This is easy.' ), ( - 'BG', + 'BG_c', 'every morphism', 'It is a groupoid.' ), diff --git a/database/data/007_special-morphisms/003_monomorphisms.sql b/database/data/007_special-morphisms/003_monomorphisms.sql index d4ff8f88..4691ed66 100644 --- a/database/data/007_special-morphisms/003_monomorphisms.sql +++ b/database/data/007_special-morphisms/003_monomorphisms.sql @@ -51,7 +51,7 @@ VALUES 'The unit ball functor $U : \mathbf{Ban} \to \mathbf{Set}$ is faithful and representable (by $\mathbb{C}$), hence reflects and preserves monomorphisms.' ), ( - 'BG', + 'BG_c', 'every morphism', 'This is trivial.' ), diff --git a/database/data/007_special-morphisms/004_epimorphisms.sql b/database/data/007_special-morphisms/004_epimorphisms.sql index f594003e..e3c23503 100644 --- a/database/data/007_special-morphisms/004_epimorphisms.sql +++ b/database/data/007_special-morphisms/004_epimorphisms.sql @@ -46,7 +46,7 @@ VALUES 'Let $f : X \to Y$ be an epimorphism of Banach spaces. The subspace $U := \overline{f(X)} \subseteq Y$ is closed. It is well-known that the quotient $Y/U$ is also a Banach space with a projection $p : Y \to Y/U$. Since $p \circ f = 0 = 0 \circ f$, we infer $p = 0$, so that $U = Y$.' ), ( - 'BG', + 'BG_c', 'every morphism', 'This holds because it is a groupoid.' ), diff --git a/database/data/007_special-morphisms/005_regular-monomorphisms.sql b/database/data/007_special-morphisms/005_regular-monomorphisms.sql index 2939dc7e..6934da0f 100644 --- a/database/data/007_special-morphisms/005_regular-monomorphisms.sql +++ b/database/data/007_special-morphisms/005_regular-monomorphisms.sql @@ -41,7 +41,7 @@ VALUES 'This is because the category is mono-regular.' ), ( - 'BG', + 'BG_c', 'same as monomorphisms', 'This is because the category is mono-regular.' ), diff --git a/database/data/007_special-morphisms/006_regular-epimorphisms.sql b/database/data/007_special-morphisms/006_regular-epimorphisms.sql index db8de608..6ba4c5a9 100644 --- a/database/data/007_special-morphisms/006_regular-epimorphisms.sql +++ b/database/data/007_special-morphisms/006_regular-epimorphisms.sql @@ -46,7 +46,7 @@ VALUES 'This is because the category is epi-regular.' ), ( - 'BG', + 'BG_c', 'same as isomorphisms', 'This is because the category is left cancellative.' ), diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json index b387f2e5..629564fb 100644 --- a/scripts/expected-data/Ab.json +++ b/scripts/expected-data/Ab.json @@ -86,6 +86,18 @@ "cokernels": true, "normal": true, "conormal": true, + "accessible": true, + "finitely accessible": true, + "ℵ₁-accessible": true, + "generalized variety": true, + "locally finitely multi-presentable": true, + "locally multi-presentable": true, + "locally poly-presentable": true, + "multi-algebraic": true, + "multi-complete": true, + "multi-cocomplete": true, + "multi-terminal object": true, + "multi-initial object": true, "cartesian closed": false, "locally cartesian closed": false, @@ -124,5 +136,9 @@ "cocartesian coclosed": false, "locally cocartesian coclosed": false, "quotient object classifier": false, - "regular quotient object classifier": false + "regular quotient object classifier": false, + "locally copresentable": false, + "coaccessible": false, + "countable": false, + "essentially countable": false } diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json index e714c158..f750b77e 100644 --- a/scripts/expected-data/Set.json +++ b/scripts/expected-data/Set.json @@ -81,6 +81,18 @@ "cofiltered": true, "sifted": true, "cosifted": true, + "accessible": true, + "finitely accessible": true, + "ℵ₁-accessible": true, + "generalized variety": true, + "locally finitely multi-presentable": true, + "locally multi-presentable": true, + "locally poly-presentable": true, + "multi-algebraic": true, + "multi-complete": true, + "multi-cocomplete": true, + "multi-terminal object": true, + "multi-initial object": true, "Grothendieck abelian": false, "Malcev": false, @@ -124,5 +136,9 @@ "kernels": false, "cokernels": false, "normal": false, - "conormal": false + "conormal": false, + "locally copresentable": false, + "coaccessible": false, + "countable": false, + "essentially countable": false } diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json index 0458704a..5e644c97 100644 --- a/scripts/expected-data/Top.json +++ b/scripts/expected-data/Top.json @@ -65,6 +65,10 @@ "cofiltered": true, "sifted": true, "cosifted": true, + "multi-complete": true, + "multi-cocomplete": true, + "multi-terminal object": true, + "multi-initial object": true, "abelian": false, "additive": false, @@ -124,5 +128,17 @@ "kernels": false, "cokernels": false, "normal": false, - "conormal": false + "conormal": false, + "accessible": false, + "finitely accessible": false, + "ℵ₁-accessible": false, + "generalized variety": false, + "locally finitely multi-presentable": false, + "locally multi-presentable": false, + "locally poly-presentable": false, + "multi-algebraic": false, + "locally copresentable": false, + "coaccessible": false, + "countable": false, + "essentially countable": false } diff --git a/static/pdf/walking_parallel_pair_sifted_colimit.tex b/static/pdf/walking_parallel_pair_sifted_colimit.tex index 9bfb0fbc..1dd1896e 100644 --- a/static/pdf/walking_parallel_pair_sifted_colimit.tex +++ b/static/pdf/walking_parallel_pair_sifted_colimit.tex @@ -101,7 +101,7 @@ $D(c)=0$ and there is a morphism from itself sent to $v$ by $D$. \end{enumerate} Now, we have a cocone $(\alpha_c\colon D(c) \to 1)_{c\in\mathcal{C}}$ over $D$ by letting $\alpha_c\coloneqq \mathrm{id}_1$ if $c$ is classified into the first case, $\alpha_c\coloneqq u$ for the second case, and $\alpha_c\coloneqq v$ for the third case. -Moreover, this is a unique cocone over $D$: +Moreover, this is a unique cocone under $D$: If $\beta$ is another cocone, its vertex should be $1$ by the existence of $c_0$. If $c\in\mathcal{C}$ is classified into the first case, $\beta_c$ should be the identity. For the second case, taking a morphism $f\colon c\to x$ such that $D(f)=u$, we can obtain $\beta_c = \beta_x \circ D(f) = D(f) = u$.