diff --git a/database/data/categories/Ab.yaml b/database/data/categories/Ab.yaml index 6564f3d1..df52e7bb 100644 --- a/database/data/categories/Ab.yaml +++ b/database/data/categories/Ab.yaml @@ -22,6 +22,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Ab \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: abelian proof: This is standard, see Mac Lane, Ch. VIII. diff --git a/database/data/categories/Ab_fg.yaml b/database/data/categories/Ab_fg.yaml index 7ab864bd..8d2a11be 100644 --- a/database/data/categories/Ab_fg.yaml +++ b/database/data/categories/Ab_fg.yaml @@ -17,9 +17,19 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\FinAb \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: abelian proof: This follows from the fact for abelian groups and the fact that subgroups of finitely generated abelian groups are also finitely generated. + dependencies: + - id: Ab + type: category + property: abelian + satisfied: true - property: generator proof: The group $\IZ$ is a generator since it represents the forgetful functor to $\Set$. @@ -29,6 +39,11 @@ satisfied_properties: - property: ℵ₁-accessible proof: The inclusion $\Ab_{\fg} \hookrightarrow \Ab$ is closed under $\aleph_1$-filtered colimits by MO/400763. In particular, $\Ab_{\fg}$ has $\aleph_1$-filtered colimits. Since $\Ab_{\fg}$ is essentially small, there is a set $G$ such that every f.g. abelian group is isomorphic to one in $G$. So trivially it is also a $\aleph_1$-filtered colimit of such objects (take the constant diagram). Finally, every object is $\Ab_{\fg} = \Ab_{\fp}$ is finitely presentable in $\Ab$ and hence also in $\Ab_{\fg}$, a fortiori $\aleph_1$-presentable. + dependencies: + - id: Ab + type: category + property: ℵ₁-filtered colimits + satisfied: true - property: ℵ₁-cofiltered limits proof: A proof can be found here. diff --git a/database/data/categories/Alg(R).yaml b/database/data/categories/Alg(R).yaml index e8d409bc..bdcf4e04 100644 --- a/database/data/categories/Alg(R).yaml +++ b/database/data/categories/Alg(R).yaml @@ -17,6 +17,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Alg(R) \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: finitary algebraic proof: Take the algebraic theory of an $R$-algebra. @@ -26,9 +31,21 @@ satisfied_properties: - property: disjoint finite products proof: One can take the same proof as for $\Ring$. + dependencies: + - id: Ring + type: category + property: disjoint finite products + satisfied: true + with_proof: true - property: Malcev proof: This follows in the same way as for $\Grp$, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. + dependencies: + - id: Grp + type: category + property: Malcev + satisfied: true + with_proof: true unsatisfied_properties: - property: skeletal @@ -39,6 +56,11 @@ unsatisfied_properties: - property: semi-strongly connected proof: This is because already the full subcategory $\CAlg(R)$ of commutative algebras is not semi-strongly connected. + dependencies: + - id: CAlg(R) + type: category + property: semi-strongly connected + satisfied: false - property: cogenerating set proof: 'We apply this lemma to the collection of $R$-algebras which are fields: If $F$ is an $R$-algebra that is also a field and $A$ is a non-trivial $R$-algebra, any algebra homomorphism $F \to A$ is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables over some residue field of $R$ has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).' @@ -51,9 +73,21 @@ unsatisfied_properties: - property: coregular proof: 'We just need to tweak the proof for $\Ring$. Since $R \neq 0$, there is an infinite field $K$ with a homomorphism $R \to K$. Since $K$ is infinite, we may choose some $\lambda \in K \setminus \{0,1\}$. Let $B \coloneqq M_2(K)$ and $A \coloneqq K \times K$. Then $A \to B$, $(x,y) \mapsto \diag(x,y)$ is a regular monomorphism: A direct calculation shows that a matrix is diagonal iff it commutes with $M \coloneqq \bigl(\begin{smallmatrix} 1 & 0 \\ 0 & \lambda \end{smallmatrix}\bigr)$, so that $A \to B$ is the equalizer of the identity $B \to B$ and the conjugation $B \to B$, $X \mapsto M X M^{-1}$. Consider the homomorphism $A \to K$, $(a,b) \mapsto a$. We claim that $K \to K \sqcup_A B$ is not a monomorphism, because in fact, the pushout $K \sqcup_A B$ is zero: Since $A \to K$ is surjective with kernel $0 \times K$, the pushout is $B/\langle 0 \times K \rangle$, which is $0$ because $B$ is simple (proof) or via a direct calculation with elementary matrices.' + dependencies: + - id: Ring + type: category + property: coregular + satisfied: false + with_proof: true - property: regular quotient object classifier - proof: We may copy the proof for $\CRing$ (since the proof there did not use that $P$ is commutative). Alternatively, any regular quotient object classifier in $\Alg(R)$ would produce one in the reflective subcategory $\CAlg(R)$ by Lemma 1 here (dualized). + proof: We may copy the proof for $\CAlg(R)$ (since the proof there did not use that $P$ is commutative). Alternatively, any regular quotient object classifier in $\Alg(R)$ would produce one in the reflective subcategory $\CAlg(R)$ by Lemma 1 here (dualized). + dependencies: + - id: CAlg(R) + type: category + property: regular quotient object classifier + satisfied: false + with_proof: true - property: cocartesian cofiltered limits proof: >- @@ -62,10 +96,21 @@ unsatisfied_properties: Because of $w_n \equiv w_{n-1} \bmod Y^n$ these form an element $w \in \lim_n (A \sqcup B_n)$. Expanding $w_n$, the longest term is $XY XY^2 \cdots X Y^n$ of "free product" length $2n$, which is unbounded. - property: cofiltered-limit-stable epimorphisms - proof: We already know that $\CAlg(R)$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the forgetful functor $\CAlg(R) \to \Alg(R)$. It preserves epimorphisms by MSE/5133488. + proof: We already know that $\CAlg(R)$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the forgetful functor $\CAlg(R) \to \Alg(R)$. It preserves epimorphisms by MSE/5133488. + dependencies: + - id: CAlg(R) + type: category + property: cofiltered-limit-stable epimorphisms + satisfied: false - property: effective cocongruences proof: 'The counterexample is similar to the one for $\Ring$: Let $X \coloneqq R[p] / (p^2-p)$ with cocongruence $E \coloneqq R \langle p, q \rangle / (p^2-p, q^2-q, pq-q, qp-p)$.' + dependencies: + - id: Ring + type: category + property: effective cocongruences + satisfied: false + with_proof: true special_objects: initial object: diff --git a/database/data/categories/B.yaml b/database/data/categories/B.yaml index d4c142df..fe051316 100644 --- a/database/data/categories/B.yaml +++ b/database/data/categories/B.yaml @@ -17,9 +17,19 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\IB \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: locally finite proof: There is a faithful functor $\IB \to \FinSet$ and $\FinSet$ is locally finite. + dependencies: + - id: FinSet + type: category + property: locally finite + satisfied: true - property: inhabited proof: This is trivial. diff --git a/database/data/categories/BN.yaml b/database/data/categories/BN.yaml index 6de618cb..725788e0 100644 --- a/database/data/categories/BN.yaml +++ b/database/data/categories/BN.yaml @@ -35,6 +35,15 @@ satisfied_properties: - property: locally cartesian closed proof: The slice category $B\IN / *$ is isomorphic to the poset $(\IN,\geq)$ (not to $(\IN,\leq)$). This category is thin and and semi-strongly connected, hence cartesian closed. + dependencies: + - id: N + type: category + property: thin + satisfied: true + - id: N + type: category + property: semi-strongly connected + satisfied: true - property: ℵ₁-accessible proof: A proof can be found here as Proposition 2. diff --git a/database/data/categories/BOn.yaml b/database/data/categories/BOn.yaml index 4c681c40..612d6058 100644 --- a/database/data/categories/BOn.yaml +++ b/database/data/categories/BOn.yaml @@ -33,6 +33,15 @@ satisfied_properties: - property: locally cartesian closed proof: The slice category $B\On / *$ is isomorphic to the poset $(\On,\geq)$ (not to $(\On,\leq)$). This category is thin and and semi-strongly connected, hence cartesian closed. + dependencies: + - id: On + type: category + property: thin + satisfied: true + - id: On + type: category + property: semi-strongly connected + satisfied: true - property: ℵ₁-cofiltered proof: In fact, it is $\kappa$-cofiltered for every cardinal $\kappa$. By the dual of Theorem 2.2 at the nLab it suffices to prove any set of objects has a cone (which is trivial in a one-object category) and that any set of parallel morphisms is equalized by some morphism. Here, this means that for every set of ordinals $A$ there is some ordinal $\beta$ such that $\alpha + \beta$ for $\alpha \in A$ does not depend on $\alpha$. Take $\beta$ to be any ordinal larger than $\sup(A)$ of the form $\omega^\gamma$. It is well-known that $\omega^\gamma$ has the property that $\alpha + \omega^\gamma = \omega^\gamma$ for all $\alpha < \omega^\gamma$ (Kunen's Set Theory, Exercise I.9.53), from which the claim follows. diff --git a/database/data/categories/Ban.yaml b/database/data/categories/Ban.yaml index f42a8899..bb838715 100644 --- a/database/data/categories/Ban.yaml +++ b/database/data/categories/Ban.yaml @@ -15,6 +15,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Ban \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: pointed proof: The trivial Banach space $\{0\}$ is a zero object. @@ -31,9 +36,19 @@ satisfied_properties: - property: cartesian filtered colimits proof: If $X$ is a Banach space and $(Y_i)$ is a filtered diagram of Banach spaces, the canonical map $\colim_i (X \times Y_i) \to X \times \colim_i Y_i$ is the completion of the canonical map in the category of normed vector spaces with non-expansive linear maps. Now the claim follows directly from $\Met$. + dependencies: + - id: Met + type: category + property: cartesian filtered colimits + satisfied: true - property: cocartesian cofiltered limits proof: 'If $X$ is a Banach space and $(Y_i)$ is a cofiltered diagram of Banach spaces, the canonical map $X \oplus \lim_i Y_i \to \lim_i (X \oplus Y_i)$ is an isomorphism: Since the forgetful functor $\Ban \to \Vect$ preserves finite coproducts and all limits, and $\Vect$ has the claimed property (see here), the canonical map is bijective. It remains to show that it is isometric. For $(x,y) \in X \oplus \lim_i Y_i$ the norm in the domain is $|x| + \sup_i |y_i|$, and the norm in the codomain is $\sup_i (|x| + |y_i|)$, and these clearly agree.' + dependencies: + - id: Vect + type: category + property: cocartesian cofiltered limits + satisfied: true - property: regular proof: >- @@ -91,6 +106,11 @@ satisfied_properties: Since $R \hookrightarrow X \times X$ is an isometry, $R$ is a closed subspace of $X \times X$. It follows that also $U$ is a closed subspace of $X$. Finally, $R$ is the kernel pair of the projection $X \to X/U$ since this is true by construction on the level of vector spaces and the kernel pair carries the $\max$-norm, just like $R$. + dependencies: + - id: Vect + type: category + property: effective congruences + satisfied: true unsatisfied_properties: - property: skeletal @@ -111,6 +131,11 @@ unsatisfied_properties: $$\Hom(\Psi,X) \to S(X), \quad f \mapsto \overline{\im(f)}$$ is bijective. In particular, there is a morphism $f : \Psi \to X$ with dense image, i.e. an epimorphism. But this contradicts the already established fact that $\Ban$ is well-copowered (since it is locally presentable). Alternatively, we may use that for every cardinal $\kappa$ the Banach space $\ell^2(\kappa^+)$ has no dense subset of size $\kappa$. + dependencies: + - id: Ban + type: category + property: well-copowered + satisfied: true - property: unital proof: The canonical morphism $X \sqcup Y \to X \times Y$ is injective, and therefore a monomorphism. Hence, if it were also a strong epimorphism, it would be an isomorphism. However, for example, when $X = Y = \IC$, the norms do not agree. @@ -120,6 +145,12 @@ unsatisfied_properties: - property: filtered-colimit-stable monomorphisms proof: 'The proof is similar to $\Met$. For $n \geq 1$ let $X_n$ be the Banach space with underlying vector space $\IC$ and the norm $|x|_n \coloneqq \frac{1}{n} |x|$. For $n \leq m$ the identity map provides a morphism $X_n \to X_m$, which is clearly a monomorphism (also an epimorphism by the way, but an isomorphism iff $n=m$). Let $X$ be the colimit of all $X_n$ in the category of semi-normed vector spaces. It is constructed as the colimit in the category of vector spaces with the semi-norm $|x| \coloneqq \inf \{|x|_m : n \leq m \}$ for $x \in X_n$. So clearly, the semi-norm is zero. Hence, the colimit in the category of normed vector spaces is $0$. The colimit in the category of Banach spaces is its completion, which is also $0$. Thus, the monomorphisms $X_1 \hookrightarrow X_n$ become the zero map $X_1 \to 0$ in the colimit, which is not a monomorphism.' + dependencies: + - id: Met + type: category + property: filtered-colimit-stable monomorphisms + satisfied: false + with_proof: true - property: cofiltered-limit-stable epimorphisms proof: 'We show that epimorphisms are not stable under sequential limits. Let $X_n = Y_n = \IC$ for all $n \geq 0$, equipped with the usual norm. The transition morphism $Y_{n+1} \to Y_n$ is the identity, and the transition morphism $X_{n+1} \to X_n$ is $x \mapsto x/2$. The morphisms $X_n \to Y_n$, $x \mapsto x/2^n$ are compatible with the transitions, and they are surjective, hence epimorphisms. Now we check $\lim_n X_n = 0$: An element $(x_n) \in \lim_n X_n$ is a family of complex numbers satisfying $x_n = x_{n+1}/2$ and $\sup_n |x_n| < \infty$. But then $x_n = 2^n x_0$ and this can only be bounded when $x_0=0$. Hence, $0 = \lim_n X_n \to \lim_n Y_n = \IC$ is no epimorphism.' diff --git a/database/data/categories/CAlg(R).yaml b/database/data/categories/CAlg(R).yaml index 04313c46..023aefc1 100644 --- a/database/data/categories/CAlg(R).yaml +++ b/database/data/categories/CAlg(R).yaml @@ -17,6 +17,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\CAlg(R) \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: finitary algebraic proof: Take the algebraic theory of a commutative ring. @@ -27,9 +32,21 @@ satisfied_properties: - property: Malcev proof: This follows in the same way as for $\Grp$, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. + dependencies: + - id: Grp + type: category + property: Malcev + satisfied: true + with_proof: true - property: coextensive proof: One can use the same proof as for $\CRing$. + dependencies: + - id: CRing + type: category + property: coextensive + satisfied: true + with_proof: true unsatisfied_properties: - property: skeletal @@ -55,6 +72,12 @@ unsatisfied_properties: - property: regular quotient object classifier proof: 'The strategy is similar to the one for $\CRing$: Assume that $P \to R$ is a regular quotient object classifier. If $J$ denotes the kernel of $P \to R$, every ideal $I \subseteq A$ of any commutative $R$-algebra has the form $I = \langle \varphi(J) \rangle$ for a unique homomorphism $\varphi : P \to A$. If $\sigma : A \to A$ is an automorphism with $\sigma(I)=I$, then uniqueness gives us $\sigma \circ \varphi = \varphi$, which means that $\varphi(J)$ lies in $A^{\sigma}$, the fixed algebra of $\sigma$. But then $I$ is generated by elements in $A^{\sigma} \cap I$. If $K$ is a residue field of $R$, this fails for $A = K[X,Y]$, $I = \langle X,Y \rangle$, $\sigma(X)=Y$, $\sigma(Y)=X$. The fixed algebra is the subalgebra of symmetric polynomials, which is $K[X+Y,XY]$. So $\langle X,Y \rangle$ is generated by symmetric polynomials without constant term, which implies $\langle X,Y \rangle \subseteq \langle X+Y,XY \rangle$ in $K[X,Y]$. But reducing an equation like $X = a(X,Y) \cdot (X+Y) + b(X,Y) \cdot (XY)$ modulo $\langle X^2,Y^2,XY \rangle$ yields a contradiction.' + dependencies: + - id: CRing + type: category + property: regular quotient object classifier + satisfied: false + with_proof: true - property: cofiltered-limit-stable epimorphisms proof: Let $K$ be a field over $R$. Consider the sequence of projections $\cdots \to K[X]/\langle X^2 \rangle \to K[X]/\langle X \rangle$ and the constant sequence $\cdots \to K[X] \to K[X]$. The surjective homomorphisms $K[X] \to K[X]/\langle X^n \rangle$ induce the inclusion $K[X] \hookrightarrow K[[X]]$ in the limit, where $K[[X]]$ is the algebra of formal power series. It is clearly not surjective, but this is not sufficient, we need to argue that it is not an epimorphism in $\CAlg(R)$, or equivalently, in $\CRing$. For a proof, see MSE/2391187. diff --git a/database/data/categories/CMon.yaml b/database/data/categories/CMon.yaml index 1951443b..45c9f123 100644 --- a/database/data/categories/CMon.yaml +++ b/database/data/categories/CMon.yaml @@ -17,6 +17,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\CMon \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: pointed proof: The trivial monoid is a zero object. @@ -45,10 +50,15 @@ unsatisfied_properties: proof: See MO/509232. - property: coregular - proof: 'We can show this analogously to the case of commutative rings MSE/3746890. Consider the commutative monoid $\IN^2$ and its submonoid $U \coloneqq \{(m,n)\mid m\ge n\}$ with the inclusion $i : U\hookrightarrow\IN^2$. Then, the pushout of $i$ along itself is $\langle x,y,z : x+y=x+z \rangle$, and the equalizer of the cokernel pair of $i$ is $D \coloneqq \{(m,n)\mid m=0 \implies n=0 \}$. If the category $\CMon$ were coregular, the canonical inclusion $j : U \hookrightarrow D$ would have to be an epimorphism. However, it is not: let $I \coloneqq \{0,1\}$ be the two-element commutative monoid with $1+1=1$, and let $u,v : D \rightrightarrows I$ be the morphisms defined by $u^{-1}(0)=\{(0,0)\}$ and $v^{-1}(0)=\{(0,0),(1,2)\}$; then we have $u\circ j = v\circ j$.' + proof: 'We can show this analogously to the case of commutative rings, cf. MSE/3746890. Consider the commutative monoid $\IN^2$ and its submonoid $U \coloneqq \{(m,n)\mid m\ge n\}$ with the inclusion $i : U\hookrightarrow\IN^2$. Then, the pushout of $i$ along itself is $\langle x,y,z : x+y=x+z \rangle$, and the equalizer of the cokernel pair of $i$ is $D \coloneqq \{(m,n)\mid m=0 \implies n=0 \}$. If the category $\CMon$ were coregular, the canonical inclusion $j : U \hookrightarrow D$ would have to be an epimorphism. However, it is not: let $I \coloneqq \{0,1\}$ be the two-element commutative monoid with $1+1=1$, and let $u,v : D \rightrightarrows I$ be the morphisms defined by $u^{-1}(0)=\{(0,0)\}$ and $v^{-1}(0)=\{(0,0),(1,2)\}$; then we have $u\circ j = v\circ j$.' - property: regular subobject classifier proof: We can use exactly the same proof as for $\Mon$. + dependencies: + - id: Mon + type: category + property: regular subobject classifier + satisfied: false - property: regular quotient object classifier proof: 'If $P \in \CMon$ is a regular quotient object classifier, this means that every surjective homomorphism of commutative monoids $A \to B$ is the cokernel of a unique homomorphism $P \to A$. But there are many surjective homomorphisms which are no cokernels at all: Consider the Boolean monoid $(\{0,1\},\vee)$ with $1 \vee 1 = 1$ and the surjective homomorphism $f : (\IN,+) \to (\{0,1\},\vee)$ defined by $f(0)=0$ and $f(n)=1$ for $n \geq 1$. It has trivial kernel, but is no isomorphism, so it cannot be a cokernel.' diff --git a/database/data/categories/CRing.yaml b/database/data/categories/CRing.yaml index cd2d74ed..b46641cd 100644 --- a/database/data/categories/CRing.yaml +++ b/database/data/categories/CRing.yaml @@ -20,6 +20,11 @@ comments: satisfied_properties: - property: locally small proof: There is a forgetful functor $\CRing \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: finitary algebraic proof: Take the algebraic theory of a commutative ring. @@ -30,6 +35,11 @@ satisfied_properties: - property: Malcev proof: This follows in the same way as for $\Grp$, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. + dependencies: + - id: Grp + type: category + property: Malcev + satisfied: true - property: coextensive proof: '[Sketch] A ring homomorphism $f : A \times B \to R$ yields the idempotent element $e \coloneqq f(1,0) \in R$, so that $R \cong eR \times (1-e)R$. Then $f$ decomposes into the ring homomorphisms $f_A : A \to eR$, $f_A(a) \coloneqq f(a,0)$ and $f_B : B \to (1-e)R$, $f_B(b) \coloneqq f(0,b)$.' diff --git a/database/data/categories/Cat.yaml b/database/data/categories/Cat.yaml index 58c86d4f..872275ff 100644 --- a/database/data/categories/Cat.yaml +++ b/database/data/categories/Cat.yaml @@ -17,6 +17,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Cat \to \Set \times \Set$, $\C \mapsto (\Ob(\C),\Mor(\C))$, and $\Set \times \Set$ is locally small. + dependencies: + - id: SetxSet + type: category + property: locally small + satisfied: true - property: cartesian closed proof: See p. 98 in Mac Lane. @@ -32,6 +37,11 @@ satisfied_properties: - property: infinitary extensive proof: '[Sketch] This is straight forward from the fact that $\Set$ is infinitary extensive: A functor $\C \to \coprod_i \D_i$ yields full subcategories $\C_i \subseteq \C$ (the preimages of $\D_i)$ with $\C = \coprod_i \C_i$.' + dependencies: + - id: Set + type: category + property: infinitary extensive + satisfied: true unsatisfied_properties: - property: skeletal @@ -39,30 +49,65 @@ unsatisfied_properties: - property: balanced proof: Since we know that $\Mon$ is not balanced, there is a monoid map $M \to N$ which is a monomorphism and an epimorphism which is not an isomorphism. Then $B(M) \to B(N)$ has the corresponding properties. + dependencies: + - id: Mon + type: category + property: balanced + satisfied: false - property: cogenerating set proof: 'Assume that $S$ is a cogenerating set in $\Cat$. Then one checks that the set of monoids $\{\End(X) : X \in \C \in S\}$ is a cogenerating set in $\Mon$, which we know does not exist.' + dependencies: + - id: Mon + type: category + property: cogenerating set + satisfied: false - property: regular proof: See Example 3.14 at the nLab. - property: coregular proof: 'We already know that $\Mon$ is not coregular, in fact there is a regular monomorphism $M \to N$ of monoids and a morphism $M \to K$ such that $K \to K \sqcup_M N$ is not a monomorphism. The delooping functor $B : \Mon \to \Cat$ has a left adjoint (MSE/574745), hence it preserves regular monomorphisms. It also preserves pushouts (MSE/5130854), and it reflects monomorphisms since it is faithful. Therefore, $B(M) \to B(N)$ provides the desired counterexample of a non-stable regular monomorphism of categories.' + dependencies: + - id: Mon + type: category + property: coregular + satisfied: false - property: Malcev proof: Use that $\Set$ is not Malcev and consider sets as discrete categories. + dependencies: + - id: Set + type: category + property: Malcev + satisfied: false - property: co-Malcev proof: 'We can adapt the proof from $\Mon$ as follows: Consider the functor $U : \Cat \to \Set^+$ sending a category $\C$ to the (large) set $\{(x,u) : x \in \Ob(\C) ,\, u \in \End(x) \}$. It is represented by $B \IN$, the one-object category associated to the free monoid in one generator. Consider the relation $R \subseteq U^2$ consisting of those pairs $((x,u),(y,v))$ where $x = y$ and $uv = u^2$. This also representable, namely be the one-object category associated to the monoid with the presentation $\langle u,v : uv = u^2 \rangle$. Clearly, $R$ is reflexive, but not symmetric.' + dependencies: + - id: Mon + type: category + property: co-Malcev + satisfied: false - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \Cat$ that maps a set to its discrete category. + dependencies: + - id: Set + type: category + property: cofiltered-limit-stable epimorphisms + satisfied: false - property: effective cocongruences proof: >- The counterexample is similar to the one for $\Mon$: Let $X$ be the walking idempotent, and let $E$ be the delooping of the monoid with presentation $$\langle p, q \mid p^2=p,\, q^2=q,\, pq=q,\, qp=p \rangle.$$ The induced relation on functors in $[X, \C]$ is that $F \sim G$ if and only if $F$ and $G$ send the object of $X$ to the same object of $\C$, and they send the idempotent of $X$ to idempotent morphisms $a, b$ in $\C$ satisfying $ab=b$, $ba=a$. From here, the proof that this gives a cocongruence on $\Cat$ which is not effective is similar to the one in $\Mon$. + dependencies: + - id: Mon + type: category + property: effective cocongruences + satisfied: false - property: regular subobject classifier proof: >- diff --git a/database/data/categories/CompHaus.yaml b/database/data/categories/CompHaus.yaml index 380993bc..d16875e8 100644 --- a/database/data/categories/CompHaus.yaml +++ b/database/data/categories/CompHaus.yaml @@ -16,21 +16,46 @@ related: satisfied_properties: - property: locally small proof: It is a full subcategory of $\Top$, which is locally small. + dependencies: + - id: Top + type: category + property: locally small + satisfied: true - property: semi-strongly connected proof: This is already true for $\Top$. + dependencies: + - id: Top + type: category + property: semi-strongly connected + satisfied: true - property: products proof: By the Tychonoff product theorem, a product in $\Top$ of compact Hausdorff spaces is compact; it is also clearly Hausdorff. Since the forgetful functor from $\CompHaus$ to $\Top$ is fully faithful, this limit is reflected in $\CompHaus$ as well. check_redundancy: false + dependencies: + - id: Top + type: category + property: products + satisfied: true - property: equalizers proof: 'The equalizer in $\Top$ of two continuous functions $f, g : X \rightrightarrows Y$ between compact Hausdorff spaces is a closed subspace of $X$, and therefore it is also compact Hausdorff. Since the forgetful functor from $\CompHaus$ to $\Top$ is fully faithful, this limit is reflected in $\CompHaus$ as well.' check_redundancy: false + dependencies: + - id: Top + type: category + property: equalizers + satisfied: true - property: cocomplete proof: $\CompHaus$ is a reflective subcategory of $\Top$, with the reflector being the Stone-Čech compactification functor. See nLab for example. Therefore, as usual, we can form colimits in $\CompHaus$ by forming colimits in $\Top$ and then applying Stone-Čech compactification. check_redundancy: false + dependencies: + - id: Top + type: category + property: cocomplete + satisfied: true - property: generator proof: The one-point space is a generator because it represents the forgetful functor to $\Set$, which is faithful. @@ -54,6 +79,11 @@ satisfied_properties: - property: extensive proof: This follows as for $\Top$ or $\Haus$ since finite coproducts in $\CompHaus$ are formed as disjoint union spaces with the disjoint union topology. + dependencies: + - id: Top + type: category + property: extensive + satisfied: true - property: cofiltered-limit-stable epimorphisms proof: 'Suppose we have a cofiltered diagram of epimorphisms $(f_i : X_i \to Y_i)$, and $y = (y_i) \in \lim_i Y_i$. Then by lemma 1 here, the limit of $f_i^{-1}(\{ y_i \})$ is non-empty. If $x$ is in this limit, that implies that $(\lim_i f_i)(x) = y$.' @@ -67,9 +97,19 @@ unsatisfied_properties: - property: Malcev proof: This is clear since $\FinSet$ is not Malcev and can be interpreted as the subcategory of finite discrete spaces. + dependencies: + - id: FinSet + type: category + property: Malcev + satisfied: false - property: regular subobject classifier proof: The proof is almost identical to the one for $\Haus$. + dependencies: + - id: Haus + type: category + property: regular subobject classifier + satisfied: false - property: natural numbers object proof: >- @@ -82,6 +122,11 @@ unsatisfied_properties: - property: filtered-colimit-stable monomorphisms proof: 'The proof is similar to $\Haus$. For $n \geq 1$ let $X_n$ be the pushout of $[1/n, 1] \hookrightarrow [0, 1]$ with itself. That is, $X_n$ is the union of two unit intervals $[0, 1] \times \{ 1 \}$ and $[0, 1] \times \{ 2 \}$ where we identify $(x,1) \equiv (x,2)$ when $x \geq 1/n$. As in the construction for $\Haus$, we see that the colimit in $\Haus$ is $[0, 1]$ where all corresponding points of both unit intervals are identified. Since this is compact Hausdorff, it also provides the colimit in $\CompHaus$. Again, the injective continuous maps $\{1,2\} \to X_n$, $i \mapsto (0,i)$ (where $\{1,2\}$ is discrete) become the constant map $0 : \{1,2\} \to [0,1]$ in the colimit, which is not a monomorphism.' + dependencies: + - id: Haus + type: category + property: filtered-colimit-stable monomorphisms + satisfied: false - property: exact cofiltered limits proof: |- diff --git a/database/data/categories/Delta.yaml b/database/data/categories/Delta.yaml index 2c8930b4..cd2b08a2 100644 --- a/database/data/categories/Delta.yaml +++ b/database/data/categories/Delta.yaml @@ -23,6 +23,11 @@ satisfied_properties: - property: locally finite proof: There is a faithful functor $\Delta \to \FinSet$ and $\FinSet$ is locally finite. + dependencies: + - id: FinSet + type: category + property: locally finite + satisfied: true - property: countable proof: This is obvious. @@ -44,15 +49,35 @@ satisfied_properties: - property: coequalizers proof: Assume that $X \rightrightarrows Y$ are morphisms in $\FinOrd \setminus \{\varnothing\}$. Since $\FinOrd$ has coequalizers, we have a coequalizer $Y \to Q$. Since $Y$ is non-empty, $Q$ is non-empty as well, and clearly $Y \to Q$ is then also the coequalizer in $\FinOrd \setminus \{\varnothing\}$. + dependencies: + - id: FinOrd + type: category + property: coequalizers + satisfied: true - property: core-thin proof: The category $\FinOrd \setminus \{\varnothing\}$ is core-thin because already $\FinOrd$ is core-thin. + dependencies: + - id: FinOrd + type: category + property: core-thin + satisfied: true - property: mono-regular proof: The proof for $\FinOrd$ also works for $\FinSet \setminus \{\varnothing\}$. + dependencies: + - id: FinOrd + type: category + property: mono-regular + satisfied: true - property: epi-regular proof: The proof for $\FinOrd$ also works for $\FinSet \setminus \{\varnothing\}$. + dependencies: + - id: FinOrd + type: category + property: epi-regular + satisfied: true - property: cosifted proof: >- @@ -64,6 +89,11 @@ satisfied_properties: - property: ℵ₁-cofiltered limits proof: We already know that $\FinOrd$ has $\aleph_1$-cofiltered limits and that the forgetful functors to $\FinSet$ and $\Set$ preserve them. Therefore, it suffices to prove that a $\aleph_1$-cofiltered limit of non-empty finite sets is also non-empty. While a direct proof is possible, we can conveniently derive this from Lemma 1 here by regarding finite sets as discrete compact Hausdorff spaces. + dependencies: + - id: FinOrd + type: category + property: ℵ₁-cofiltered limits + satisfied: true unsatisfied_properties: - property: strict terminal object @@ -77,9 +107,19 @@ unsatisfied_properties: - property: sequential colimits proof: We can just copy the proof for $\FinOrd$ to show that the sequence of inclusions $[0] \hookrightarrow [1] \hookrightarrow [2] \hookrightarrow \cdots$ has no colimit. + dependencies: + - id: FinOrd + type: category + property: sequential colimits + satisfied: false - property: sequential limits proof: We can just copy the proof for $\FinOrd$ to show that the sequence of truncations $\cdots \twoheadrightarrow [2] \twoheadrightarrow [1] \twoheadrightarrow [0]$ has no limit. + dependencies: + - id: FinOrd + type: category + property: sequential limits + satisfied: false - property: pushouts proof: Assume that the two inclusions $\{0 < 1\} \leftarrow \{0\} \rightarrow \{0 < 2\}$ have a pushout in $\FinOrd \setminus \{\varnothing\}$. This would be a universal non-empty finite ordered set $X$ with three elements $0,1,2$ satisfying $0 \leq 1$ and $0 \leq 2$. Assume w.l.o.g. $1 \leq 2$ (the case $2 \leq 1$ is similar). The universal property yields an order-preserving map $X \to \{a < b < c\}$ with $0 \mapsto a$, $1 \mapsto c$, $2 \mapsto b$. But then $c \leq b$, which is a contradiction. diff --git a/database/data/categories/FI.yaml b/database/data/categories/FI.yaml index 0db4df27..2b134f61 100644 --- a/database/data/categories/FI.yaml +++ b/database/data/categories/FI.yaml @@ -19,9 +19,19 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\FI \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: locally finite proof: There is a faithful functor $\FI \to \FinSet$ and $\FinSet$ is locally finite. + dependencies: + - id: FinSet + type: category + property: locally finite + satisfied: true - property: left cancellative proof: This is trivial. @@ -34,9 +44,19 @@ satisfied_properties: - property: equalizers proof: We construct equalizers just like in $\FinSet$ and observe that the universal property still holds. + dependencies: + - id: FinSet + type: category + property: equalizers + satisfied: true - property: wide pullbacks proof: 'We construct wide pullbacks just like in $\Set$, i.e., for a w.l.o.g. non-empty family of injective maps $f_i : X_i \to S$ we consider the subset $P \subseteq \prod_{i \in I} X_i$ of those tuples $x$ where $f_i(x_i) = f_j(x_j)$. Each projection $P \to X_i$ is injective, so in particular $P$ is finite, and $P \to X_i$ becomes a morphism in $\FI$. It is easy to check that the universal property still holds in $\FI$.' + dependencies: + - id: Set + type: category + property: wide pullbacks + satisfied: true - property: mono-regular proof: 'If $f : X \to Y$ is an injective map of finite sets, it is the equalizer of the two injective maps $i_1,i_2 : Y \rightrightarrows Y \sqcup_X Y$, and $Y \sqcup_X Y$ is finite.' @@ -56,6 +76,11 @@ unsatisfied_properties: - property: core-thin proof: Its core is $\IB$, which we know is not thin. + dependencies: + - id: B + type: category + property: thin + satisfied: false - property: strongly connected proof: There is no map from a non-empty set to the empty set. diff --git a/database/data/categories/FS.yaml b/database/data/categories/FS.yaml index c5415c43..3fbd6662 100644 --- a/database/data/categories/FS.yaml +++ b/database/data/categories/FS.yaml @@ -18,9 +18,19 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\FS \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: locally finite proof: There is a faithful functor $\FS \to \FinSet$ and $\FinSet$ is locally finite. + dependencies: + - id: FinSet + type: category + property: locally finite + satisfied: true - property: essentially countable proof: Every finite set is isomorphic to some $\{1,\dotsc,n\}$ for some $n \in \IN$. @@ -33,18 +43,38 @@ satisfied_properties: - property: coequalizers proof: We construct coequalizers as in $\FinSet$ (or $\Set$) and observe that the universal property still holds when we restrict to surjective maps. + dependencies: + - id: FinSet + type: category + property: coequalizers + satisfied: true - property: wide pushouts proof: 'We construct wide pushouts as in $\Set$ and observe that the universal property still holds when we restrict to surjective maps. If $f_i : S \to X_i$ are surjective maps and $P$ is their wide pushout, then each $X_i \to P$ is surjective, so that in particular $P$ is finite.' + dependencies: + - id: Set + type: category + property: wide pushouts + satisfied: true - property: epi-regular proof: '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 $\FinSet$, but also in $\FS$. Notice that $p_1,p_2$ are surjective. Even though $X \times_Y X$ is not a pullback in $\FS$, we can use this finite set here.' + dependencies: + - id: FinSet + type: category + property: epi-regular + satisfied: true - property: multi-complete proof: >- Let $D : \I \to \FS$ be a small diagram. Let $L \subseteq \prod_{i \in \I} D(i)$ be the limit object of the corresponding diagram in $\Set$. Consider the set of all finite subsets $R \subseteq L$ with the property that $p_i(R) = D(i)$ for every $i \in \I$. For each of these, $(R \xrightarrow{p_i|_R} D(i))_{i \in \I}$ is a cone in $\FS$. We claim that the set of these cones is universal: Let $(f_i : T \to D(i))_{i \in \I}$ be any cone in $\FS$. Let $R \subseteq L$ be the image of the induced map of sets $f : T \to \prod_{i \in \I} D(i)$ defined by $p_i f = f_i$. Then $R$ is finite, since $T$ is finite, and we have $p_i(R) = p_i(f(T)) = f_i(T) = D(i)$. Moreover, the map $f$ corestricts to a map $f' : T \to R$ with $p_i|_R \, f' = f_i$. Therefore, $f'$ is a morphism of cones. Conversely, let $h : T \to R$ be a morphism of cones, i.e. $p_i|_R \, h = f_i$, where $R$ is not known yet. Then $h$ equals the corestriction of the map into the product induced by the $f_i$, and $h$ is surjective as a morphism in $\FS$. This shows that both $R$ and the morphism of cones are unique. + dependencies: + - id: Set + type: category + property: multi-complete + satisfied: true - property: generalized variety proof: 'Let $D : \I \to \FS$ be a sifted diagram. Consider the set @@ -75,6 +105,11 @@ unsatisfied_properties: - property: core-thin proof: Its core is $\IB$, which we know is not thin. + dependencies: + - id: B + type: category + property: thin + satisfied: false - property: generator proof: Let $G$ be a finite set. There are at least two morphisms $G + 2 \rightrightarrows 2$, but there is no morphism $G \to G + 2$ at all. Hence, $G$ is not a generator. diff --git a/database/data/categories/FiltVect.yaml b/database/data/categories/FiltVect.yaml index 29d7ae93..76a30c12 100644 --- a/database/data/categories/FiltVect.yaml +++ b/database/data/categories/FiltVect.yaml @@ -21,25 +21,55 @@ comments: satisfied_properties: - property: locally small proof: There is a forgetful functor $\FiltVect \to \Vect$, and $\Vect$ is locally small. + dependencies: + - id: Vect + type: category + property: locally small + satisfied: true - property: preadditive proof: We know that $\Vect$ is preadditive with pointwise operations. It is easy to check that the sum of two filtered linear maps is again a filtered linear map. Moreover, the additive inverse of a filtered linear map is again a filtered linear map. + dependencies: + - id: Vect + type: category + property: preadditive + satisfied: true - property: kernels proof: 'Let $f : (V,F) \to (W,F)$ be a filtered linear map. Equip the kernel $U \subseteq V$ of the underlying linear map $f : V \to W$ with the induced filtration $F^n(U) \coloneqq U \cap F^n(V)$. Then $(U,F)$ is a filtered vector space together with a filtered linear map $\iota : (U,F) \to (V,F)$, which is clearly the kernel of $f$ in $\FiltVect$.' check_redundancy: false + dependencies: + - id: Vect + type: category + property: kernels + satisfied: true - property: cokernels proof: 'Let $f : (V,F) \to (W,F)$ be a filtered linear map. Let $\pi : W \to C$ be the cokernel of the underlying linear map $f : V \to W$. Equip $C$ with the induced filtration $F^n(C) \coloneqq \pi_*(F^n(W))$. Then $(C,F)$ is a filtered vector space together with a filtered linear map $\pi : (W,F) \to (C,F)$, which is clearly the cokernel of $f$ in $\FiltVect$.' check_redundancy: false + dependencies: + - id: Vect + type: category + property: cokernels + satisfied: true - property: products proof: 'Let $(V_i,F)_{i \in I}$ be a family of filtered vector spaces. Equip the product $\prod_{i \in I} V_i$ with the filtration $F^n(\prod_{i \in I} V_i) \coloneqq \prod_{i \in I} F^n(V_i)$. It is straightforward to check that this satisfies the universal property of products in $\FiltVect$.' check_redundancy: false + dependencies: + - id: Vect + type: category + property: products + satisfied: true - property: coproducts proof: 'Let $(V_i,F)_{i \in I}$ be a family of filtered vector spaces. Equip the direct sum $\bigoplus_{i \in I} V_i$ with the filtration $F^n(\bigoplus_{i \in I} V_i) \coloneqq \bigoplus_{i \in I} F^n(V_i)$. It is straightforward to check that this satisfies the universal property of coproducts in $\FiltVect$.' check_redundancy: false + dependencies: + - id: Vect + type: category + property: coproducts + satisfied: true - property: generator proof: The vector space $K$ equipped with the trivial filtration $F^n(K) \coloneqq 0$ is a generator, since it represents the forgetful functor $\FiltVect \to \Set$. @@ -62,6 +92,7 @@ satisfied_properties: Second, every filtered vector space $(V,F)$ is the filtered colimit of the spaces $(V,F_{< N})$ for $N \in \IN$, where $$F_{< N}^n(V) \coloneqq \begin{cases} F^n(V) & n < N \\ 0 & n \geq N. \end{cases}$$ Indeed, we have $F_{< N} \subseteq F_{< N+1}$, so that $\id_V : (V,F_{- It remains to prove that regular epimorphisms are stable under pullbacks. This follows immediately from their classification below, from the fact that $F^n$ preserves limits, and from the regularity of $\Vect$. @@ -70,10 +101,21 @@ satisfied_properties: In more detail, if $(V,F) \to (W,F)$ is a regular epimorphism and $(U,F) \to (W,F)$ is any morphism, then $(V,F) \times_{(W,F)} (U,F) \to (U,F)$ is a regular epimorphism, since $V \times_W U \to U$ is surjective and, for every $n \in \IZ$, the restricted map $$F^n(V \times_W U) = F^n(V) \times_{F^n(W)} F^n(U) \to F^n(U)$$ is surjective. + dependencies: + - id: Vect + type: category + property: regular + satisfied: true + - property: coregular proof: >- - It remains to prove that regular monomorphisms (as classified below) are stable under pushouts. Let $i : (U,F) \to (V,F)$ be a regular monomorphism, i.e. $i$ is injective and $F^n(U) = i^*(F^n(V))$. Let $f : (U,F) \to (W,F)$ be any morphism. We must prove that the canonical morphism $(W,F) \to (V,F) \oplus_{(U,F)} (W,F)$ is a regular monomorphism. It is certainly injective, since the forgetful functor to $\Vect$ preserves colimits and $\Vect$ is abelian, and hence coregular. Now suppose that $w \in W$ is an element whose image $[0,w] \in V \oplus_U W$ lies in $F^n(V \oplus_U W)$; we must show that $w \in F^n(W)$. + It remains to prove that regular monomorphisms (as classified below) are stable under pushouts. Let $i : (U,F) \to (V,F)$ be a regular monomorphism, i.e. $i$ is injective and $F^n(U) = i^*(F^n(V))$. Let $f : (U,F) \to (W,F)$ be any morphism. We must prove that the canonical morphism $(W,F) \to (V,F) \oplus_{(U,F)} (W,F)$ is a regular monomorphism. It is certainly injective, since the forgetful functor to $\Vect$ preserves colimits and $\Vect$ is coregular. Now suppose that $w \in W$ is an element whose image $[0,w] \in V \oplus_U W$ lies in $F^n(V \oplus_U W)$; we must show that $w \in F^n(W)$. Since, by the construction of colimits in $\FiltVect$, the subspace $F^n(V \oplus_U W)$ is the sum of the images of $F^n(V)$ and $F^n(W)$, there exist $v \in F^n(V)$ and $w' \in F^n(W)$ such that $[0,w] = [v,w']$. This means that there exists some $u \in U$ with $v = i(u)$ and $w = f(u) + w'$. Then $u \in F^n(U)$ because $i(u) \in F^n(V)$. Hence $f(u) \in F^n(W)$, and therefore $w = f(u) + w' \in F^n(W)$. + dependencies: + - id: Vect + type: category + property: coregular + satisfied: true unsatisfied_properties: - property: skeletal diff --git a/database/data/categories/FinAb.yaml b/database/data/categories/FinAb.yaml index b5237d1b..f7cce33a 100644 --- a/database/data/categories/FinAb.yaml +++ b/database/data/categories/FinAb.yaml @@ -17,16 +17,31 @@ related: satisfied_properties: - property: locally small - proof: There is a forgetful functor $\FinAb \to \Set$ and $\Set$ is locally small. + proof: It is a full subcategory of $\Ab$, which is locally small. + dependencies: + - id: Ab + type: category + property: locally small + satisfied: true - property: locally finite proof: There is a faithful functor $\FinAb \to \FinSet$ and $\FinSet$ is locally finite. + dependencies: + - id: FinSet + type: category + property: locally finite + satisfied: true - property: essentially countable proof: The underlying set of a finite structure can be chosen to be a subset of $\IN$. - property: abelian proof: This follows from the fact for $\Ab$. + dependencies: + - id: Ab + type: category + property: abelian + satisfied: true - property: self-dual proof: 'This is a simple special case of Pontryagin duality: The functor $\Hom(-,\IQ/\IZ)$ provides the equivalence.' diff --git a/database/data/categories/FinGrp.yaml b/database/data/categories/FinGrp.yaml index fb1b22a6..6d7a18f2 100644 --- a/database/data/categories/FinGrp.yaml +++ b/database/data/categories/FinGrp.yaml @@ -17,9 +17,19 @@ related: satisfied_properties: - property: locally small proof: It is a full subcategory of $\Grp$, which is locally small. + dependencies: + - id: Grp + type: category + property: locally small + satisfied: true - property: locally finite proof: There is a faithful functor $\FinGrp \to \FinSet$ and $\FinSet$ is locally finite. + dependencies: + - id: FinSet + type: category + property: locally finite + satisfied: true - property: pointed proof: The trivial group is a zero object. @@ -42,15 +52,30 @@ satisfied_properties: - property: effective congruences proof: 'Suppose we have a congruence $f, g : E \rightrightarrows X$ in $\FinGrp$. Since the embedding $\FinGrp \hookrightarrow \Grp$ preserves finite limits, it is also a congruence in $\Grp$. We already know that $\Grp$ has effective congruences since it is algebraic. Using this result, we see that $E$ is the kernel pair of $X \to (X/E)_{\Grp}$ in $\Grp$. Also, the quotient $(X/E)_{\Grp}$ is finite; and the forgetful functor $\FinGrp \to \Grp$ is fully faithful and therefore reflects limits. Thus, we conclude that $E$ is the kernel pair of $X \to (X/E)_{\Grp}$ in $\FinGrp$ as well.' + dependencies: + - id: Grp + type: category + property: effective congruences + satisfied: true - property: effective cocongruences proof: 'A proof can be found in MO/511516. It even shows that every cocongruence in $\FinGrp$ is trivial. In short, the proof goes like this: We know that $\Grp$ has effective cocongruences. Using the fact that amalgamated sums of finite groups are residually finite, one can can show that every cocongruence in $\FinGrp$ is also a cocongruence in $\Grp$.' + dependencies: + - id: Grp + type: category + property: effective cocongruences + satisfied: true - property: regular proof: The category is Malcev and hence finitely complete, and it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks. - property: ℵ₁-cofiltered limits proof: For $\FinSet$ know that the embedding $\FinSet \hookrightarrow \Set$ is closed under $\aleph_1$-cofiltered limits. From this and the fact that the forgetful functor $\Grp \to \Set$ preserves limits it follows that $\FinGrp \hookrightarrow \Grp$ is closed under $\aleph_1$-cofiltered limits. + dependencies: + - id: FinSet + type: category + property: ℵ₁-cofiltered limits + satisfied: true unsatisfied_properties: - property: small diff --git a/database/data/categories/FinOrd.yaml b/database/data/categories/FinOrd.yaml index ff171468..f26db6dc 100644 --- a/database/data/categories/FinOrd.yaml +++ b/database/data/categories/FinOrd.yaml @@ -18,9 +18,19 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\FinOrd \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: locally finite proof: There is a faithful functor $\FinOrd \to \FinSet$ and $\FinSet$ is locally finite. + dependencies: + - id: FinSet + type: category + property: locally finite + satisfied: true - property: essentially countable proof: Every finite ordered set is isomorphic to $\{0 < \cdots < n-1 \}$ for some $n \in \IN$. @@ -42,6 +52,11 @@ satisfied_properties: - property: equalizers proof: Take the equalizer in $\FinSet$ and restrict the order. + dependencies: + - id: FinSet + type: category + property: equalizers + satisfied: true - property: coequalizers proof: It suffices to construct quotients by equivalence relations. Let $\sim$ be an equivalence relation on $X$, where $(X,\leq)$ is a finite ordered set. Since $X$ is finite, by induction we may assume that $\sim$ is generated by a single relation $(a,b)$. If $a=b$, there is nothing to prove. If $a < b$ and $X = \{0,1,\dotsc,n-1\}$ with the usual order, the quotient is $\{0,1,\dotsc,a,b+1,\dotsc,n-1\}$ with the usual order. @@ -57,6 +72,11 @@ satisfied_properties: - property: ℵ₁-cofiltered limits proof: 'Let $D : \I \to \FinOrd$ be an $\aleph_1$-cofiltered diagram. Since $\FinSet$ is closed under $\aleph_1$-cofiltered limits in $\Set$, the limit of $D$ taken in $\Set$ is a finite set $L$. We define a partial order on $L$ in the obvious way: $x \leq y$ iff $p_i(x) \leq p_i(y)$ for all $i \in \I$. It remains to prove that this is indeed a total order. So assume that $x,y \in L$ satisfy neither $x \leq y$ nor $y \leq x$. Then there exist $i,j \in \I$ such that $p_i(x) \not\leq p_i(y)$ and $p_j(y) \not\leq p_j(x)$. Choose a span $i \leftarrow k \rightarrow j$. Then $p_k(x) \not\leq p_k(y)$ and $p_k(y) \not\leq p_k(x)$ in $D(k)$, which is impossible.' + dependencies: + - id: FinSet + type: category + property: ℵ₁-cofiltered limits + satisfied: true unsatisfied_properties: - property: small diff --git a/database/data/categories/FinSet.yaml b/database/data/categories/FinSet.yaml index be7aa454..303e6c29 100644 --- a/database/data/categories/FinSet.yaml +++ b/database/data/categories/FinSet.yaml @@ -19,6 +19,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\FinSet \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: locally finite proof: This is trivial. diff --git a/database/data/categories/FinVect_c.yaml b/database/data/categories/FinVect_c.yaml index 02db896f..99401170 100644 --- a/database/data/categories/FinVect_c.yaml +++ b/database/data/categories/FinVect_c.yaml @@ -19,6 +19,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\FinVect_K \to \Vect_K$, and $\Vect_K$ is locally small. + dependencies: + - id: Vect + type: category + property: locally small + satisfied: true - property: essentially countable proof: Every object is isomorphic to $K^n$ for some $n \in \IN$, and $\Hom(K^n,K^m) \cong M_{m \times n}(K)$ is a countable set. @@ -28,6 +33,11 @@ satisfied_properties: - property: split abelian proof: This follows directly from the corresponding fact for $\Vect_K$. + dependencies: + - id: Vect + type: category + property: split abelian + satisfied: true - property: self-dual proof: The functor $V \mapsto V^*$ defines an equivalence of categories $\FinVect_K^{\op} \simeq \FinVect_K$. In fact, the natural map $V \to V^{**}$, $v \mapsto (\omega \mapsto \omega(v))$ is an isomorphism by standard linear algebra. diff --git a/database/data/categories/FinVect_f.yaml b/database/data/categories/FinVect_f.yaml index 78006a99..34c2bd32 100644 --- a/database/data/categories/FinVect_f.yaml +++ b/database/data/categories/FinVect_f.yaml @@ -19,6 +19,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\FinVect_K \to \Vect_K$, and $\Vect_K$ is locally small. + dependencies: + - id: Vect + type: category + property: locally small + satisfied: true - property: essentially countable proof: Every object is isomorphic to $K^n$ for some $n \in \IN$, and $\Hom(K^n,K^m) \cong M_{m \times n}(K)$ is a finite, hence countable set. @@ -31,6 +36,11 @@ satisfied_properties: - property: split abelian proof: This follows directly from the corresponding fact for $\Vect_K$. + dependencies: + - id: Vect + type: category + property: split abelian + satisfied: true - property: self-dual proof: The functor $V \mapsto V^*$ defines an equivalence of categories $\FinVect_K^{\op} \simeq \FinVect_K$. In fact, the natural map $V \to V^{**}$, $v \mapsto (\omega \mapsto \omega(v))$ is an isomorphism by standard linear algebra. diff --git a/database/data/categories/FinVect_u.yaml b/database/data/categories/FinVect_u.yaml index c7734fc3..4992f6bc 100644 --- a/database/data/categories/FinVect_u.yaml +++ b/database/data/categories/FinVect_u.yaml @@ -19,6 +19,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\FinVect_K \to \Vect_K$, and $\Vect_K$ is locally small. + dependencies: + - id: Vect + type: category + property: locally small + satisfied: true - property: essentially small proof: Every object is isomorphic to $K^n$ for some $n \in \IN$, and $\Hom(K^n,K^m) \cong M_{m \times n}(K)$ is a set. @@ -28,6 +33,11 @@ satisfied_properties: - property: split abelian proof: This follows directly from the corresponding fact for $\Vect_K$. + dependencies: + - id: Vect + type: category + property: split abelian + satisfied: true - property: self-dual proof: The functor $V \mapsto V^*$ defines an equivalence of categories $\FinVect_K^{\op} \simeq \FinVect_K$. In fact, the natural map $V \to V^{**}$, $v \mapsto (\omega \mapsto \omega(v))$ is an isomorphism by standard linear algebra. diff --git a/database/data/categories/Fld.yaml b/database/data/categories/Fld.yaml index 4795866c..6daec378 100644 --- a/database/data/categories/Fld.yaml +++ b/database/data/categories/Fld.yaml @@ -18,6 +18,11 @@ comments: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Fld \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: inhabited proof: This is trivial. diff --git a/database/data/categories/FreeAb.yaml b/database/data/categories/FreeAb.yaml index ab65e1fd..12cb1848 100644 --- a/database/data/categories/FreeAb.yaml +++ b/database/data/categories/FreeAb.yaml @@ -16,12 +16,27 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\FreeAb \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: additive proof: The embedding $\FreeAb \hookrightarrow \Ab$ is closed under (finite) direct sums, and $\Ab$ is additive. + dependencies: + - id: Ab + type: category + property: additive + satisfied: true - property: coproducts proof: This is is because free abelian groups are closed under direct sums of abelian groups. + dependencies: + - id: Ab + type: category + property: coproducts + satisfied: true - property: generator proof: As for $\Ab$, the group $\IZ$ is a generator. @@ -40,6 +55,11 @@ satisfied_properties: This follows formally from the fact that $\Ab$ is regular and $\FreeAb$ is closed under subobjects and finite products: By Prop. 2.5 in the nLab it suffices to prove that there are pullback-stable (reg epi, mono)-factorizations. Every homomorphism $f : A \to B$ in $\FreeAb$ factors as $f = i \circ p : A \twoheadrightarrow C \hookrightarrow B$, where $C$ is a subgroup of $B$, hence free abelian, and $A \to C$ is surjective. Clearly, surjective homomorphisms are pullback-stable. It remains to show that they coincide with the regular epimorphisms. (1) If $f : A \to B$ is surjective, it is the coequalizer of $A \times_B A \rightrightarrows A$ in $\Ab$. Since $A \times_B A$ is free abelian (as a subgroup of $A \times A$), $f$ is also a coequalizer in $\FreeAb$. (2) If $f : A \to B$ is a regular epimorphism in $\FreeAb$, consider the factorization $f = i \circ p$ as above. Since $f$ is an extremal epimorphism, $i$ must be an isomorphism, so that $f$ is surjective. + dependencies: + - id: Ab + type: category + property: regular + satisfied: true unsatisfied_properties: - property: balanced diff --git a/database/data/categories/Grp.yaml b/database/data/categories/Grp.yaml index 68fe0c40..f1a985b4 100644 --- a/database/data/categories/Grp.yaml +++ b/database/data/categories/Grp.yaml @@ -19,6 +19,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Grp \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: pointed proof: The trivial group is a zero object. @@ -67,6 +72,11 @@ unsatisfied_properties: - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Ab$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the forgetful functor $\Ab \to \Grp$ which indeed preserves epimorphisms. + dependencies: + - id: Ab + type: category + property: cofiltered-limit-stable epimorphisms + satisfied: false - property: cocartesian cofiltered limits proof: >- diff --git a/database/data/categories/Grp_c.yaml b/database/data/categories/Grp_c.yaml index 7b2f8593..83e70112 100644 --- a/database/data/categories/Grp_c.yaml +++ b/database/data/categories/Grp_c.yaml @@ -17,6 +17,11 @@ related: satisfied_properties: - property: locally small proof: There is an embedding $\Grp_\c \hookrightarrow \Grp$ and $\Grp$ is locally small. + dependencies: + - id: Grp + type: category + property: locally small + satisfied: true - property: essentially small proof: Every countable group is isomorphic to a group whose underlying set is a subset of $\IN$. @@ -31,34 +36,79 @@ satisfied_properties: - property: finite products proof: This is because $\Grp$ has finite (in fact, all) products, and $\Grp_\c \hookrightarrow \Grp$ is closed under finite products. This is because a finite product of countable sets is again countable. check_redundancy: false + dependencies: + - id: Grp + type: category + property: finite products + satisfied: true - property: equalizers proof: One can use the same construction as in $\Grp$ since a subgroup of a countable group is again countable. check_redundancy: false + dependencies: + - id: Grp + type: category + property: equalizers + satisfied: true - property: coequalizers proof: One can use the same construction as in $\Grp$ since a quotient of a countable group is again countable. + dependencies: + - id: Grp + type: category + property: coequalizers + satisfied: true - property: countable coproducts proof: This is because $\Grp$ has countable (in fact, all) coproducts, and $\Grp_\c \hookrightarrow \Grp$ is closed under countable coproducts. This is because a countable union of countable sets is again countable. + dependencies: + - id: Grp + type: category + property: countable coproducts + satisfied: true - property: mono-regular proof: 'This can be deduced from the corresponding property of $\Grp$ as follows: Let $i : K \hookrightarrow G$ be a monomorphism in $\Grp_\c$, i.e. an injective homomorphism of countable groups. Since $\Grp$ is mono-regular, there is a group $H$ and two homomorphisms $f,g : G \rightrightarrows H$ with $i = \eq(f,g)$. Let $H'' \subseteq H$ be the subgroup generated by $\im(f) \cup \im(g)$. Since $G$ is countable, $H''$ is countable as well, and $f,g$ corestrict to homomorphisms $f'', g'' : G \rightrightarrows H''$. Hence, $i = \eq(f'',g'')$.' + dependencies: + - id: Grp + type: category + property: mono-regular + satisfied: true - property: conormal proof: 'If $f : G \to H$ is an epimorphism in $\Grp_\c$, i.e. a surjective homomorphism of countable groups, then $f$ is the cokernel of $K \hookrightarrow G$ in $\Grp$, where $K$ is the kernel of $f$. Since $K$ is countable, it is also the cokernel in $\Grp_\c$.' + dependencies: + - id: Grp + type: category + property: conormal + satisfied: true - property: Malcev proof: We can use the same proof as for $\Grp$. + dependencies: + - id: Grp + type: category + property: Malcev + satisfied: true - property: regular proof: We already know that the category is finitely complete, and that it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks. - property: effective congruences proof: 'A congruence on a countable group $G$ has the form $\{(g,h) \in G^2 : g^{-1} h \in N \}$ for some normal subgroup $N \subseteq G$. It is the kernel pair of the projection $p : G \twoheadrightarrow G/N$ in $\Grp$, but also in $\Grp_\c$ since $G/N$ is countable.' + dependencies: + - id: Grp + type: category + property: effective congruences + satisfied: true - property: effective cocongruences proof: 'Let $G + G \twoheadrightarrow H$ be a cocongruence in $\Grp_\c$. Since $\Grp_\c \hookrightarrow \Grp$ is closed under finite colimits, this is the same as a cocongruence in $\Grp$ where $G,H \in \Grp$ happen to be countable groups. Since we already know that $\Grp$ has effective cocongruences, the cocongruence is the cokernel pair of some homomorphism of groups $K \to H$. If $K'' \subseteq H$ denotes the image of $K$, it is then also the cokernel pair of the inclusion $K'' \hookrightarrow H$, and $K''$ is countable.' + dependencies: + - id: Grp + type: category + property: effective cocongruences + satisfied: true unsatisfied_properties: - property: skeletal @@ -81,6 +131,11 @@ unsatisfied_properties: - property: regular quotient object classifier proof: We can copy the proof from $\Grp$. + dependencies: + - id: Grp + type: category + property: regular quotient object classifier + satisfied: false - property: coregular proof: Pushouts of injective homomorphisms between countable groups do not need to be injective, see MSE/5088032. @@ -96,6 +151,11 @@ unsatisfied_properties: For $r \in R$ we define $\varepsilon(r) \in \lim(X)$ by $$\varepsilon(r)_C = \begin{cases} r & r \in C \\ 0 & r \notin C \end{cases}$$ It is easily checked that this indeed lies in the limit. Moreover, $\varepsilon(r) = \varepsilon(r')$ implies $r=r'$, since evaluating at $C \coloneqq \{r\}$ yields $r = r'$. Hence, $\lim(X)$ is uncountable. + dependencies: + - id: Set_c + type: category + property: ℵ₁-cofiltered limits + satisfied: false special_objects: initial object: diff --git a/database/data/categories/Haus.yaml b/database/data/categories/Haus.yaml index 130249be..d76f5fca 100644 --- a/database/data/categories/Haus.yaml +++ b/database/data/categories/Haus.yaml @@ -17,25 +17,55 @@ related: satisfied_properties: - property: locally small proof: It is a full subcategory of $\Top$, which is locally small. + dependencies: + - id: Top + type: category + property: locally small + satisfied: true - property: generator proof: The one-point space is a generator since it represents the forgetful functor $\Haus \to \Set$. - property: semi-strongly connected - proof: Every non-empty Hausdorff space is weakly terminal (by using constant maps). + proof: This is because even $\Top$ is semi-strongly connected. + dependencies: + - id: Top + type: category + property: semi-strongly connected + satisfied: true - property: equalizers proof: This follows from the corresponding fact for $\Top$ since subspaces of Hausdorff spaces are again Hausdorff. + dependencies: + - id: Top + type: category + property: equalizers + satisfied: true - property: products proof: This follows from the corresponding fact for $\Top$ since products of Hausdorff spaces are again Hausdorff. + dependencies: + - id: Top + type: category + property: products + satisfied: true - property: cocomplete proof: This follows since $\Haus$ is a reflective subcategory of $\Top$, which is cocomplete. For the reflector, see e.g. the nLab. Explicitly, we construct the colimit of Hausdorff spaces by applying the reflector to the colimit of the underlying topological spaces. check_redundancy: false + dependencies: + - id: Top + type: category + property: cocomplete + satisfied: true - property: infinitary extensive proof: This follows exactly as for $\Top$ since Hausdorff spaces are closed under taking subspaces and coproducts in $\Top$. + dependencies: + - id: Top + type: category + property: infinitary extensive + satisfied: true - property: well-powered proof: This is clear from the classification of monomorphisms as injective continuous maps. @@ -58,6 +88,11 @@ unsatisfied_properties: - property: Malcev proof: This is clear since $\Set$ is not Malcev and can be interpreted as the subcategory of discrete spaces (which are Hausdorff). + dependencies: + - id: Set + type: category + property: Malcev + satisfied: false - property: regular subobject classifier proof: Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\Hom(X,\Omega)$ and the set of closed subsets of $X$ for any Hausdorff space $X$. If we take $X = 1$ we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, $\Omega \cong 1 + 1$ must be discrete. But then $\Hom(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$). @@ -67,12 +102,22 @@ unsatisfied_properties: - property: cofiltered-limit-stable epimorphisms proof: 'Recall the counterexample for sets: The unique maps $\IN_{\geq n} \to 1$ are surjective, but their limit $0 = \bigcap_{n \geq 0} \IN_{\geq n} \to 1$ is not. This also works in $\Haus$ by using discrete topologies. We could also apply a variant of (the dual of) Lemma 2 here to the discrete topology functor $\Set \to \Haus$, which does not preserve all cofiltered limits, but does preserve intersections.' + dependencies: + - id: Set + type: category + property: cofiltered-limit-stable epimorphisms + satisfied: false - property: filtered-colimit-stable monomorphisms proof: |- The proof is similar to $\Met$. For $n \geq 1$ let $X_n$ be the pushout of $$(-\infty, -1/n] \cup [1/n, \infty) \hookrightarrow \IR$$ with itself. That is, $X_n$ is the union of two lines $\IR \times \{1\}$ and $\IR \times \{2\}$ where we identify $(x,1) \equiv (x,2)$ when $|x| \geq 1/n$. Then $X_n$ is Hausdorff, and there is a canonical surjective continuous map $X_n \to X_{n+1}$. The colimit in $\Top$ is the union of two lines where we identify $(x,1) \equiv (x,2)$ when $|x| \geq 1/n$ for some $n$, i.e. when $x \neq 0$. This is the line with the double origin, which is not Hausdorff. Its Hausdorff reflection is the line $\IR$ where all points of both lines are identified, and it provides the colimit in $\Haus$. Now, the injective continuous maps $\{1,2\} \to X_n$, $i \mapsto (0,i)$ (where $\{1,2\}$ is discrete) become the constant map $0 : \{1,2\} \to \IR$ in the colimit, which is not a monomorphism. + dependencies: + - id: Met + type: category + property: filtered-colimit-stable monomorphisms + satisfied: false - property: accessible proof: In fact, it does not have any small colimit-dense subcategory by MSE/4097315. diff --git a/database/data/categories/LRS_R.yaml b/database/data/categories/LRS_R.yaml index 65355a68..8d4af003 100644 --- a/database/data/categories/LRS_R.yaml +++ b/database/data/categories/LRS_R.yaml @@ -24,12 +24,26 @@ satisfied_properties: - property: cocomplete proof: See Demazure-Gabriel's "Groupes algébriques", I. §1. 1.6. Specifically, the forgetful functor from locally ringed spaces to ringed spaces preserves colimits, and colimits of ringed spaces are built from colimits of topological spaces and limits of commutative rings, see MSE/1646202. + dependencies: + - id: Top + type: category + property: cocomplete + satisfied: true + - id: CRing + type: category + property: complete + satisfied: true - property: well-copowered proof: This follows from the characterization of epimorphisms below. - property: infinitary extensive proof: '[Sketch] Since $\Top$ is infinitary extensive, a morphism $f : Y \to \coprod_i X_i \eqqcolon X$ yields a decomposition $Y = \coprod_i Y_i$ (as topological spaces) with continuous maps $f_i : Y_i \to X_i$. Endow the open subset $Y_i \subseteq Y$ with the restricted sheaf. Then each $f_i$ becomes a morphism of locally ringed spaces, and $Y = \coprod_i Y_i$ holds as locally ringed spaces.' + dependencies: + - id: Top + type: category + property: infinitary extensive + satisfied: true unsatisfied_properties: - property: skeletal @@ -40,18 +54,38 @@ unsatisfied_properties: - property: semi-strongly connected proof: This is because already the full subcategory $\Sch_R$ of $R$-schemes is not semi-strongly connected. + dependencies: + - id: Sch_R + type: category + property: semi-strongly connected + satisfied: false - property: Malcev proof: This is because already the full subcategory $\Sch_R$ of $R$-schemes is not Malcev. + dependencies: + - id: Sch_R + type: category + property: Malcev + satisfied: false - property: co-Malcev proof: 'We can adjust the proof for $\Top$ (see MO/509548) as follows: Let $K$ be a residue field of $R$, let $X$ be a singleton and $Y = \{u,v\}$ be the Sierpinski space where $\{u\}$ is open, but $\{v\}$ is not. Endow both with the sheaf of locally constant functions to $K$. Thus, $\O_X(X) = K$, $\O_Y(Y) = \O_Y(\{u\}) = K$. There is a canonical morphism $p : X + X \to Y$. It is a coreflexive corelation that is not cosymmetric.' + dependencies: + - id: Top + type: category + property: co-Malcev + satisfied: false - property: generating set proof: >- Out of any small set $S$ of locally ringed spaces, there is only a small set of residue fields at their points. Therefore, if $K$ is a field over $R$ with a strictly larger cardinality than any of these residue fields, then the only possible morphism from an element of $S$ to $\Spec K(X,Y)$ is one with an empty domain. However, that makes it impossible for $S$ to distinguish the two canonical automorphisms of $\Spec K(X,Y)$. Alternatively, using the usual adjunction between affine schemes and locally ringed spaces (EGA I (1971), Ch. 1, Prop. 1.6.3), a generating set in $\LRS_R$ would induce a generating set in the category of affine $R$-schemes, which contradicts the fact that $\CAlg(R)$ does not have a cogenerating set. + dependencies: + - id: CAlg(R) + type: category + property: cogenerating set + satisfied: false - property: cartesian closed proof: This is Corollary 4(a) here. diff --git a/database/data/categories/M-Set.yaml b/database/data/categories/M-Set.yaml index 4758ea78..151f21de 100644 --- a/database/data/categories/M-Set.yaml +++ b/database/data/categories/M-Set.yaml @@ -17,6 +17,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $M{-}\Set \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: Grothendieck topos proof: It is the category of sheaves on the opposite of the one-object category associated to $M$. diff --git a/database/data/categories/Man.yaml b/database/data/categories/Man.yaml index e3e6a664..963c9b76 100644 --- a/database/data/categories/Man.yaml +++ b/database/data/categories/Man.yaml @@ -17,10 +17,20 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Man \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: finite products proof: In short, this follows from the corresponding statement for topological spaces and $\IR^n \times \IR^m \cong \IR^{n+m}$. check_redundancy: false + dependencies: + - id: Top + type: category + property: finite products + satisfied: true - property: generator proof: The $0$-dimensional one-point manifold is a generator since it represents the forgetful functor $\Top \to \Set$. @@ -36,10 +46,20 @@ satisfied_properties: - property: extensive proof: '[Sketch] Since $\Top$ is infinitary extensive, a continuous map $f : M \to \coprod_i N_i$ corresponds to a decomposition $M = \coprod_i M_i$ (as topological spaces) with continuous maps $f_i : M_i \to N_i$. Endow the open subset $M_i \subseteq M$ with the smooth structure inherited from $M$. Now remark that $f$ is smooth iff each $f_i$ is smooth.' + dependencies: + - id: Top + type: category + property: infinitary extensive + satisfied: true - property: countably distributive # TODO: maybe add "countably extensive" to make this more conceptual proof: To construct countable coproducts, take the usual disjoint union of spaces, which is clearly locally Euclidean and Hausdorff, and it is second countable since we are using only countable many spaces. (Without that condition, all coproducts would exist.) Now we need to check that the canonical smooth map $\coprod_i X \times Y_i \to X \times \coprod_i Y_i$ is a diffeomorphism (for countable families). It is a homeomorphism since $\Top$ is infinitary distributive. The inverse $X \times \coprod_i Y_i \to \coprod_i X \times Y_i$ is smooth since the domain is covered by the open subsets $X \times Y_i$ on which the map is clearly smooth. + dependencies: + - id: Top + type: category + property: countably distributive + satisfied: true - property: Cauchy complete proof: See Theorem 2.1 at the nLab. @@ -51,6 +71,11 @@ satisfied_properties: - property: effective cocongruences proof: 'From the proof that $\Man$ has coquotients of cocongruences, we know that for any cocongruence $X \rightrightarrows E$, there is a clopen submanifold $U$ of $X$ such that the fibers of $r : E \twoheadrightarrow X$ have one point on $U$, and two points on $X \setminus U$. Therefore, $E$ is the cokernel pair of the inclusion map $U \hookrightarrow X$.' + dependencies: + - id: Man + type: category + property: coquotients of cocongruences + satisfied: true unsatisfied_properties: - property: skeletal @@ -81,9 +106,14 @@ unsatisfied_properties: Assume that there exists a limit cone $(\pi_C : M \to C \sqcup \{\ast\})$ in $\Man$. Since the forgetful functor $\Man \to \Set$ is representable, it preserves limits. In particular, the underlying set of $M$ is the limit of the underlying sets and is therefore uncountable. Since the codomain of $\pi_C$ is discrete, the map $\pi_C$ is locally constant. Thus, for every connected component $K \subseteq M$, the map $\pi_C$ is constant on $K$. Since the maps $\pi_C$ are jointly injective, it follows that every connected component of $M$ consists of a single point. Hence, $M$ is totally disconnected. Since $M$ is a smooth manifold, it follows that $M$ has dimension $0$. Since $M$ is also second-countable, it follows that the underlying set of $M$ is countable, contradicting our previous observation. + dependencies: + - id: Set_c + type: category + property: ℵ₁-cofiltered limits + satisfied: false - property: quotients of congruences - proof: If $\Man$ had quotients of congruences, then by this lemma, it would have a pushout of $\IR \leftarrow \{ 0 \} \rightarrow \IR$. This contradicts MO/19916. + proof: If $\Man$ had quotients of congruences, then by this lemma, it would have a pushout of $\IR \leftarrow \{ 0 \} \rightarrow \IR$. This contradicts MO/19916. special_objects: initial object: diff --git a/database/data/categories/Meas.yaml b/database/data/categories/Meas.yaml index d7221d06..8b934e24 100644 --- a/database/data/categories/Meas.yaml +++ b/database/data/categories/Meas.yaml @@ -18,6 +18,11 @@ comments: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Meas \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: semi-strongly connected proof: Every non-empty measurable space is weakly terminal (by using constant maps). @@ -36,15 +41,35 @@ satisfied_properties: - property: complete proof: Take the limit of the underlying sets and take the smallest $\sigma$-algebra making all projections measurable. + dependencies: + - id: Set + type: category + property: complete + satisfied: true - property: cocomplete proof: Take the colimit of the underlying sets and take the largest $\sigma$-algebra making all inclusions measurable. That is, a set is measurable iff its preimage under each inclusion is measurable. + dependencies: + - id: Set + type: category + property: cocomplete + satisfied: true - property: infinitary extensive proof: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : Y \to \coprod_i X_i \eqqcolon X$ corresponds to a decomposition $Y = \coprod_i Y_i$ (as sets) with maps $f_i : Y_i \to X_i$. Endow the measurable subset $Y_i \subseteq Y$ with the restricted $\sigma$-algebra. If $f$ is measurable, each $f_i$ is measurable, and $Y = \coprod_i Y_i$ holds as measurable spaces.' + dependencies: + - id: Set + type: category + property: infinitary extensive + satisfied: true - property: filtered-colimit-stable monomorphisms proof: This follows from Lemma 2 here applied to the forgetful functor to $\Set$. + dependencies: + - id: Set + type: category + property: filtered-colimit-stable monomorphisms + satisfied: true - property: regular subobject classifier proof: The set $\{0,1\}$ with the trivial $\sigma$-algebra is a regular subobject classifier since measurable maps $X \to \{0,1\}$ correspond to subsets of $X$. @@ -61,9 +86,19 @@ unsatisfied_properties: - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \Meas$ which equips a set with the trivial $\sigma$-algebra. + dependencies: + - id: Set + type: category + property: cofiltered-limit-stable epimorphisms + satisfied: false - property: effective cocongruences proof: 'The proof is similar to the one for $\Top$: Use the trivial $\sigma$-algebra on a two-point set.' + dependencies: + - id: Top + type: category + property: effective cocongruences + satisfied: false - property: regular proof: A proof can be found here. diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index c6d342cc..ad2f1f82 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -18,6 +18,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Met \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: strict initial object proof: The empty metric space is initial and clearly strict. @@ -33,10 +38,20 @@ satisfied_properties: - property: equalizers proof: Just restrict the metric to the equalizer built from the sets. + dependencies: + - id: Set + type: category + property: equalizers + satisfied: true - property: binary products proof: The product of two metric spaces $(X,d)$, $(Y,d)$ is $(X \times Y,d)$ with $d((x_1,y_1),(x_2,x_2)) \coloneqq \sup(d(x_1,x_2),d(y_1,y_2))$. check_redundancy: false + dependencies: + - id: Set + type: category + property: binary products + satisfied: true - property: terminal object proof: The one-point metric space is terminal. @@ -44,10 +59,20 @@ satisfied_properties: - property: coequalizers proof: This is because the category of pseudo-metric spaces $\PMet$ has coequalizers and $\Met \hookrightarrow \PMet$ has a left adjoint, mapping a pseudo-metric space $X$ to $X /{\sim}$ where $x \sim y \iff d(x,y)=0$. Concretely, we take the coequalizer in the category of pseudo-metric spaces and then identify points with distance zero. + dependencies: + - id: PMet + type: category + property: coequalizers + satisfied: true - property: filtered colimits proof: This is because the category of pseudo-metric spaces $\PMet$ has filtered colimits and $\Met \hookrightarrow \PMet$ has a left adjoint, mapping a pseudo-metric space $X$ to $X /{\sim}$ where $x \sim y \iff d(x,y)=0$. Concretely, we take the filtered colimit in the category of pseudo-metric spaces and then identify points with distance zero. check_redundancy: false + dependencies: + - id: PMet + type: category + property: filtered colimits + satisfied: true - property: cartesian filtered colimits proof: >- @@ -61,6 +86,11 @@ satisfied_properties: Suppose otherwise. Then for every $n \in \IN$ there exists an object $i_n \in \I$ such that $d(x_{i_n},y_{i_n}) \geq n$. Since $\I$ is $\aleph_1$-cofiltered, there exists a cone $(j \to i_n)_{n \in \IN}$. Since the maps $D(j) \to D(i_n)$ are non-expansive, we have $$d(x_j,y_j) \geq d(x_{i_n},y_{i_n}) \geq n$$ for every $n \in \IN$. This is impossible since the metric on $D(j)$ takes only finite values. + dependencies: + - id: Met_oo + type: category + property: ℵ₁-cofiltered limits + satisfied: true - property: well-copowered proof: 'If $f : X \to Y$ is an epimorphism, then $f(X)$ is dense in $Y$ (see below). Hence, there is an injective map $Y \to X^{\IN}$, which bounds the size of $Y$.' @@ -75,6 +105,7 @@ satisfied_properties: Then, countable metric spaces in $\Met$ are $\aleph_1$-presentable not only in $\Met_\infty$, but also in $\Met$. On the other hand, every object in $\Met_\infty$ is an $\aleph_1$-filtered colimit of its countable isometric subspaces, and the same is true in $\Met$. Hence, $\Met$ is $\aleph_1$-accessible. + unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml index 74e9dd02..3df4ba33 100644 --- a/database/data/categories/Met_c.yaml +++ b/database/data/categories/Met_c.yaml @@ -18,15 +18,30 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Met_c \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: semi-strongly connected proof: Every non-empty metric space is weakly terminal (by using constant maps). - property: equalizers proof: Just restrict the metric to the equalizer built from the sets. + dependencies: + - id: Set + type: category + property: equalizers + satisfied: true - property: countable products proof: For finite products, we take the cartesian product with, say, the sup-metric. The product of countably many metric spaces $(X_i,d_i)_{i \geq 0}$ is given by the cartesian product $\prod_{i \geq 0} X_i$ with the metric $d(x,y) \coloneqq \sum_{i \geq 0} d_i(x_i,y_i)/(1 + d_i(x_i,y_i))$. See Engelking's book General Topology. + dependencies: + - id: Set + type: category + property: countable products + satisfied: true - property: coproducts proof: See MSE/5004389. @@ -46,6 +61,11 @@ satisfied_properties: - property: infinitary extensive proof: This follows from the existence of coproducts and finite products, and from the fact that $\Top$ is infinitary extensive. + dependencies: + - id: Top + type: category + property: infinitary extensive + satisfied: true - property: effective cocongruences proof: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Met_c$. Then the image in $\Haus$ is a coreflexive corelation (since epimorphisms in both categories are continuous maps with dense image). By MO/509548, that implies that image is of the form $X +_S X$ for a closed subset $S$ of $X$. Since $S$ is metrizable, and the functor $\Met_c \to \Haus$ is fully faithful and therefore reflects colimits, we conclude that $E$ is effective in $\Met_c$.' @@ -65,6 +85,11 @@ unsatisfied_properties: - property: regular subobject classifier proof: 'We recycle the proof from $\Haus$: Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\Hom(X,\Omega)$ and the set of closed subsets of $X$ for any metric space $X$. If we take $X = 1$ we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, $\Omega \cong 1 + 1$ must be discrete. But then $\Hom(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$).' + dependencies: + - id: Haus + type: category + property: regular subobject classifier + satisfied: false - property: sequential colimits proof: See MO/510316 for a proof that the diagram $\IN \to \Met_c$, $n \mapsto \IR^n$ does not have a colimit. diff --git a/database/data/categories/Met_oo.yaml b/database/data/categories/Met_oo.yaml index f77f1e5b..a96d96d6 100644 --- a/database/data/categories/Met_oo.yaml +++ b/database/data/categories/Met_oo.yaml @@ -16,6 +16,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Met_{\infty} \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: generator proof: The singleton metric space $1$ is a generator, since morphisms $1 \to X$ correspond to the elements of $X$. @@ -31,9 +36,19 @@ satisfied_properties: - property: cartesian filtered colimits proof: We can use the same proof as for $\Met$ since the equation $\inf_i \max(r, s_i) = \max(r, \inf_i s_i)$ also holds for for $r, s_i \in \IR \cup \{\infty\}$. + dependencies: + - id: Met + type: category + property: cartesian filtered colimits + satisfied: true - property: infinitary extensive proof: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : Y \to \coprod_i X_i \eqqcolon X$ corresponds to a decomposition $Y = \coprod_i Y_i$ (as sets) with maps $f_i : Y_i \to X_i$. Endow $Y_i$ with the restricted metric. If $f$ is non-expansive, each $f_i$ is non-expansive, and for $x_i \in Y_i$ and $i \neq j$ we have $d_Y(x_i,x_j) \geq d_X(f(x_i),f(x_j)) = \infty$, so that $Y = \coprod_i Y_i$ holds as metric spaces.' + dependencies: + - id: Set + type: category + property: infinitary extensive + satisfied: true unsatisfied_properties: - property: skeletal @@ -53,15 +68,35 @@ unsatisfied_properties: - property: filtered-colimit-stable monomorphisms proof: We can copy the proof from $\Met$. + dependencies: + - id: Met + type: category + property: filtered-colimit-stable monomorphisms + satisfied: false - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \Met_{\infty}$ that equips a set with the discrete topology. + dependencies: + - id: Set + type: category + property: cofiltered-limit-stable epimorphisms + satisfied: false - property: effective cocongruences proof: The same counterexample as for $\Met$ works here. The difference in this case is that a binary copower of two copies of $(0,1)$ does exist in $\Met_\infty$. However, this would assign a distance of $\infty$ between points in $(-1,0)$ and points in $(0,1)$, which does not agree with the chosen subspace metric on $(-1,0) \cup (0,1)$. + dependencies: + - id: Top + type: category + property: effective cocongruences + satisfied: false - property: regular proof: We can take the same counterexample as for $\PMet$. + dependencies: + - id: PMet + type: category + property: regular + satisfied: false special_objects: initial object: diff --git a/database/data/categories/Mon.yaml b/database/data/categories/Mon.yaml index ccff1fea..cd8d614f 100644 --- a/database/data/categories/Mon.yaml +++ b/database/data/categories/Mon.yaml @@ -18,6 +18,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Mon \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: pointed proof: The trivial monoid is a zero object. @@ -60,12 +65,27 @@ unsatisfied_properties: - property: regular quotient object classifier proof: We can just copy the proof for $\CMon$. Alternatively, we may use Lemma 1 here (dualized) applied to the forgetful functor $\CMon \to \Mon$. + dependencies: + - id: CMon + type: category + property: regular quotient object classifier + satisfied: false - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Grp$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the forgetful functor $\Grp \to \Mon$. It preserves epimorphisms since it has a right adjoint, the unit group functor. + dependencies: + - id: Grp + type: category + property: cofiltered-limit-stable epimorphisms + satisfied: false - property: cocartesian cofiltered limits proof: 'We know that $\Grp$ fails to satisfy this property. The same counterexample works here since the inclusion $\Grp \hookrightarrow \Mon$ preserves limits and colimits (it has a left and a right adjoint) and is conservative. A similar counterexample is given by the free monoids $N_n = \langle x_1,\dotsc,x_n \rangle$ and the Boolean monoid $M = \langle e : e^2=e \rangle$ with the maps $N_{n+1} \to N_n$, $x_{n+1} \mapsto 1$. Then the element $(x_1 e \cdots x_n e) \in \lim_n (M \sqcup N_n)$ does not come from $M \sqcup \lim_n N_n$ because its components have unbounded free product length.' + dependencies: + - id: Grp + type: category + property: cocartesian cofiltered limits + satisfied: false - property: effective cocongruences proof: >- @@ -75,6 +95,11 @@ unsatisfied_properties: On the other hand, using the multiplicative map $$E \to M_{2\times 2}(\IZ), \quad p \mapsto \begin{pmatrix} 1 & 0 \\ 0 & 0 \end{pmatrix},\quad q \mapsto \begin{pmatrix} 1 & 1 \\ 0 & 0 \end{pmatrix},$$ we can see that $p \ne q$ in $E$, so the equalizer of the two maps $X \rightrightarrows E$ is the trivial submonoid $\{ 1 \}$. Therefore, if $E$ were effective, it would be isomorphic to the coproduct $X \sqcup X$, whose underlying set consists of words in $p,q$ with $p,q$ strictly alternating. In particular, in this coproduct, $pq \ne q$. + dependencies: + - id: Ring + type: category + property: effective cocongruences + satisfied: false special_objects: initial object: diff --git a/database/data/categories/Mono.yaml b/database/data/categories/Mono.yaml index b4099c13..ab37397b 100644 --- a/database/data/categories/Mono.yaml +++ b/database/data/categories/Mono.yaml @@ -21,9 +21,19 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Mono \to \Set$, $(X, X') \mapsto X$, and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: semi-strongly connected proof: This is immediate from the fact that $\Mono$ is equivalent to a full subcategory of $\Set^{\rightarrow}$, and the latter is semi-strongly connected. + dependencies: + - id: Set_arrow + type: category + property: semi-strongly connected + satisfied: true - property: generator proof: >- @@ -39,6 +49,11 @@ satisfied_properties: More concretely, suppose we have a diagram $((X_i, X_i'))_{i \in \I}$, with limit cone $p_i : \lim_{i\in\I} X_i \to X_i$ in $\Set$. Then the limit in $\Mono$ is $(\lim_{i\in\I} X_i, \bigcap_{i\in\I} p_i^{-1}(X_i'))$. (It is easy to see that in the subset component, we can also restrict $i$ to range over a weakly initial set of objects of $\I$.) check_redundancy: false + dependencies: + - id: Set + type: category + property: complete + satisfied: true - property: cocomplete proof: >- @@ -46,9 +61,19 @@ satisfied_properties: More concretely, suppose we have a diagram $((X_i, X_i'))_{i \in \I}$, with colimit cone $c_i : X_i \to \colim_{i\in\I} X_i$ in $\Set$. Then the colimit in $\Mono$ is $(\colim_{i\in\I} X_i, \bigcup_{i\in\I} c_i(X_i'))$. (It is easy to see that in the subset component, we can also restrict $i$ to range over a weakly terminal set of objects of $\I$.) check_redundancy: false + dependencies: + - id: Set_arrow + type: category + property: cocomplete + satisfied: true - property: disjoint coproducts proof: This follows from the fact that coproducts in $\Mono$ can be computed component-wise, along with the fact that $\Set$ has disjoint coproducts. + dependencies: + - id: Set + type: category + property: disjoint coproducts + satisfied: true - property: locally cartesian closed proof: >- @@ -76,13 +101,28 @@ satisfied_properties: is surjective. To see it is injective, use the fact that the unique morphism $(1, 0) \to (1, 1)$ is an epimorphism (see below), and we have already seen that the corresponding function for $(1,0)$ is injective. Therefore, any finite coproduct of $(1, 0)$ and $(1, 1)$ is finitely presentable; this means any object of the form $([n], [m])$ with $m, n \in \IN$ and $m \le n$ is finitely presentable. All such objects form a small set. Moreover, any object $(X,X')$ of $\Mono$ is a filtered colimit of the subobjects $(F, F \cap X')$ where $F$ is a finite subset of $X$, and each $(F, F \cap X')$ is isomorphic to some $([n], [m])$. + dependencies: + - id: Mono + type: category + property: cocomplete + satisfied: true - property: co-Malcev proof: >- Suppose we have a coreflexive corelation $p : (X \sqcup X, X' \sqcup X') \twoheadrightarrow (E, E')$ with coreflexivity morphism $r : (E, E') \to (X, X')$. From the assumption that $p$ is an epimorphism, we have that $p : X \sqcup X \to E$ is a surjective function. Since $\Set$ is co-Malcev, it follows that $E \cong X \sqcup_Y X$ for some subset $Y \subseteq X$. It remains to show that $E' = i_1(X') \cup i_2(X') \subseteq X \sqcup_Y X$. Certainly, since we have a morphism $(X \sqcup_Y X, i_1(X') \cup i_2(X')) \to (E, E')$ induced by $p$, we must have $i_1(X') \cup i_2(X') \subseteq E'$. On the other hand, any element of $E'$ is an element of $E$ and hence is equal to either $i_1(x)$ or $i_2(x)$ for $x \in X$. In the first case, we must have $x = r(i_1(x)) \in X'$, so $i_1(x) \in i_1(X')$; and similarly for the second case. + dependencies: + - id: Set + type: category + property: co-Malcev + satisfied: true - property: effective cocongruences proof: 'See the proof that $\Mono$ is co-Malcev: It shows that in fact any coreflexive corelation is equivalent to an effective cocongruence $X \sqcup X \twoheadrightarrow X \sqcup_Y X$.' + dependencies: + - id: Mono + type: category + property: co-Malcev + satisfied: true unsatisfied_properties: - property: skeletal @@ -94,6 +134,11 @@ unsatisfied_properties: - property: cofiltered-limit-stable epimorphisms proof: >- We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \Mono$ which sends a set $X$ to the pair $(X, X)$. + dependencies: + - id: Set + type: category + property: cofiltered-limit-stable epimorphisms + satisfied: false special_objects: initial object: diff --git a/database/data/categories/N_oo.yaml b/database/data/categories/N_oo.yaml index 7303fcb0..d2561e8c 100644 --- a/database/data/categories/N_oo.yaml +++ b/database/data/categories/N_oo.yaml @@ -32,6 +32,11 @@ satisfied_properties: - property: locally strongly finitely presentable proof: We already saw that coproducts, and therefore colimits exist. Every natural number is strongly finitely presentable, and $\infty$ is the colimit of all $n < \infty$. + dependencies: + - id: N_oo + type: category + property: coproducts + satisfied: true unsatisfied_properties: - property: essentially finite diff --git a/database/data/categories/PMet.yaml b/database/data/categories/PMet.yaml index 9ceac19e..8a0688f7 100644 --- a/database/data/categories/PMet.yaml +++ b/database/data/categories/PMet.yaml @@ -15,6 +15,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\PMet \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: generator proof: The one-point (pseudo-)metric space is a generator since it represents the forgetful functor $\PMet \to \Set$. @@ -37,10 +42,20 @@ satisfied_properties: - property: equalizers proof: Just restrict the pseudo-metric to the equalizer built from the sets. check_redundancy: false + dependencies: + - id: Set + type: category + property: equalizers + satisfied: true - property: binary products proof: The product of two pseudo-metric spaces $(X,d)$, $(Y,d)$ is $(X \times Y,d)$ with $d((x_1,y_1),(x_2,x_2)) \coloneqq \sup(d(x_1,x_2),d(y_1,y_2))$. check_redundancy: false + dependencies: + - id: Set + type: category + property: binary products + satisfied: true - property: terminal object proof: The one-point (pseudo-)metric space is terminal. @@ -52,12 +67,27 @@ satisfied_properties: - property: filtered colimits proof: 'Given a filtered diagram $(X_i)$ of pseudo-metric spaces, take the filtered colimit $X$ of the underlying sets with the following pseudo-metric: If $x,y \in X$, let $d(x,y)$ be infimum of all $d(x_i,y_i)$, where $x_i,y_i \in X_i$ are some preimages of $x,y$ in some $X_i$. The definition ensures that each $X_i \to X$ is non-expansive, and the universal property is easy to check.' check_redundancy: false + dependencies: + - id: Set + type: category + property: filtered colimits + satisfied: true - property: exact filtered colimits proof: 'We already saw that finite limits and filtered colimits exist. Now let $\I$ be a finite category and $\J$ be a small filtered category, w.l.o.g. a directed poset. Let $X : \I \times \J \to \PMet$ be a diagram. We need to show that the canonical map $\colim_{j \in \J} \lim_{i \in \I} X(i,j) \to \lim_{i \in \I} \colim_{j \in \J} X(i,j)$ is an isomorphism. It is bijective since the forgetful functor to $\Set$ preserves finite limits and filtered colimits and since $\Set$ has exact filtered colimits. That the map is isometric can easily be reduced to the following lemma: If $d_{i,j} \in \IR_{\geq 0}$ are numbers for $i \in \I$, $j \in \J$ with $j \leq k \implies d_{i,k} \leq d_{i,j}$, then $\inf_j \sup_i d_{i,j} = \sup_i \inf_j d_{i,j}$. This can be proven directly. Alternatively, use that the thin category $(\IR_{\geq 0} \cup \{\infty\},\leq)$ is isomorphic to $([0,1],\leq)$, and we already know that it has exact filtered colimits.' + dependencies: + - id: Set + type: category + property: exact filtered colimits + satisfied: true - property: ℵ₁-cofiltered limits proof: The proof is identical to the one for $\Met$. + dependencies: + - id: Met + type: category + property: ℵ₁-cofiltered limits + satisfied: true unsatisfied_properties: - property: skeletal @@ -77,6 +107,11 @@ unsatisfied_properties: - property: Malcev proof: Take any counterexample in $\Set$ and equip it with the zero pseudo-metric. + dependencies: + - id: Set + type: category + property: Malcev + satisfied: false - property: cartesian closed proof: This is proven in MSE/5131457. @@ -95,6 +130,11 @@ unsatisfied_properties: - property: effective cocongruences proof: 'The proof is similar to the one for $\Top$: Equip a two-point set with the zero metric; this pseudo-metric space represents the functor taking a pseudo-metric space to the pairs of points with $d(x,y) = 0$. In this case, once you conclude $Z = \varnothing$, the map $h : Z \to 1$ does not have any cokernel pair, since that would have to be a coproduct $1+1$, which does not exist.' + dependencies: + - id: Top + type: category + property: effective cocongruences + satisfied: false - property: regular proof: 'We can adapt Example 3.14 at the nLab (which disproves regularity for $\Pos$ and related categories) as follows: Consider the subspaces $X = \{0,1,2,3\}$ and $Y = \{0,1,2\}$ of $\IR$ with the usual metric. Define a surjective map $p : X \to Y$ by $p(0)=0$, $p(1)=p(2)=1$, and $p(3)=2$. Clearly, $p$ is non-expansive. Moreover, one can check that $p$ satisfies the universal property in $\PMet$ of a coequalizer of the two maps $1,2 : \{\ast\} \rightrightarrows X$. Thus, $p$ is a regular epimorphism. Now consider the subspace $Z = \{0,2\}$ of $Y$. As a set, the pullback $X \times_Y Z$ is $p^*(Z) = \{0,3\}$. Using the definition of the product metric, one can verify that $d(0,3) = 3$ in this pullback. The projection $X \times_Y Z \to Z$ identifies with the evident bijective and non-expansive map $\{0,3\} \to \{0,2\}$. It is a monomorphism and not an isomorphism (the distances do not match), hence cannot be a regular epimorphism.' diff --git a/database/data/categories/Pos.yaml b/database/data/categories/Pos.yaml index a8cfd553..a7bdda05 100644 --- a/database/data/categories/Pos.yaml +++ b/database/data/categories/Pos.yaml @@ -17,6 +17,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Pos \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: locally finitely presentable proof: See Adamek-Rosicky, Example 1.10. @@ -35,6 +40,11 @@ satisfied_properties: - property: infinitary extensive proof: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : P \to \coprod_i Q_i$ corresponds to a decomposition $P = \coprod_i P_i$ (as sets) with maps $f_i : P_i \to Q_i$. Endow $P_i$ with the induced order. If $f$ is order-preserving, the elements in different $P_i$ cannot be comparable (since their $f$-images are not comparable), so that $P = \coprod_i P_i$ as posets, and each $f_i$ is order-preserving.' + dependencies: + - id: Set + type: category + property: infinitary extensive + satisfied: true - property: coregular proof: See MSE/5130295. diff --git a/database/data/categories/PreOrd.yaml b/database/data/categories/PreOrd.yaml index 2bd97f7b..6cf2b6e4 100644 --- a/database/data/categories/PreOrd.yaml +++ b/database/data/categories/PreOrd.yaml @@ -16,9 +16,19 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\PreOrd \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: locally finitely presentable proof: The same proof as for $\Pos$ works, cf. Adamek-Rosicky, Example 1.10. + dependencies: + - id: Pos + type: category + property: locally finitely presentable + satisfied: true - property: cartesian closed proof: For preordered sets $P,Q$ we endow $\Hom(P,Q)$ with the preorder in which $f \leq g$ holds iff $f(p) \leq g(p)$ for all $p \in P$. The universal evaluation map is $\Hom(P,Q) \times P \to Q$, $(f,p) \mapsto f(p)$, it is order-preserving, and it satisfies the universal property. @@ -34,6 +44,11 @@ satisfied_properties: - property: infinitary extensive proof: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : P \to \coprod_i Q_i$ corresponds to a decomposition $P = \coprod_i P_i$ (as sets) with maps $f_i : P_i \to Q_i$. Endow $P_i$ with the induced order. If $f$ is order-preserving, the elements in different $P_i$ cannot be comparable (since their $f$-images are not comparable), so that $P = \coprod_i P_i$ as preordered sets, and each $f_i$ is order-preserving.' + dependencies: + - id: Set + type: category + property: infinitary extensive + satisfied: true - property: coregular proof: See MSE/5130295. @@ -53,6 +68,11 @@ unsatisfied_properties: - property: cofiltered-limit-stable epimorphisms proof: We know that $\Set$ does not have this property. Now use the contrapositive of the dual of Lemma 2 here applied to the functor $\Set \to \PreOrd$ that equips a set with the chaotic preorder. + dependencies: + - id: Set + type: category + property: cofiltered-limit-stable epimorphisms + satisfied: false - property: effective cocongruences proof: 'Consider the preordered set $E \coloneqq \{ a, b \}$ with the chaotic preorder. This represents the functor which sends a preordered set to the pairs of elements $x,y$ with $x \le y$ and $y \le x$. Therefore, it defines a cocongruence $1 \rightrightarrows E$, where the maps are the two possible functions. However, this cannot be effective: for any map $h : Z \to 1$ which equalizes the two functions, $Z$ must be empty. But that means the cokernel pair of $h$ is the two-element preordered set with the trivial preorder.' diff --git a/database/data/categories/R-Mod.yaml b/database/data/categories/R-Mod.yaml index 83c27ab0..b13e06a8 100644 --- a/database/data/categories/R-Mod.yaml +++ b/database/data/categories/R-Mod.yaml @@ -19,6 +19,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $R{-}\Mod \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: abelian proof: This is standard, see Mac Lane, Ch. VIII. diff --git a/database/data/categories/R-Mod_div.yaml b/database/data/categories/R-Mod_div.yaml index 39b2b779..819c9f47 100644 --- a/database/data/categories/R-Mod_div.yaml +++ b/database/data/categories/R-Mod_div.yaml @@ -16,6 +16,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $R{-}\Mod \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: split abelian proof: It is a standard fact that the category of $R$-modules is abelian for any ring $R$, see Mac Lane, Ch. VIII. If $R$ is a division ring, then by linear algebra every $R$-module has a basis, hence is projective, so that every short exact sequence splits. diff --git a/database/data/categories/Rel.yaml b/database/data/categories/Rel.yaml index e01269cb..d2b28792 100644 --- a/database/data/categories/Rel.yaml +++ b/database/data/categories/Rel.yaml @@ -27,8 +27,13 @@ satisfied_properties: proof: One checks that the the one-point set is a generator. - property: coproducts - proof: It is an easy exercise to deduce this from the corresponding fact for sets and that sets form a distributive category. + proof: It is an easy exercise to deduce this from the corresponding fact for sets and that sets form an infinitary distributive category. check_redundancy: false + dependencies: + - id: Set + type: category + property: infinitary distributive + satisfied: true - property: biproducts proof: This is a consequence of the description of coproducts and products, both are disjoint unions (even for infinite families). diff --git a/database/data/categories/Ring.yaml b/database/data/categories/Ring.yaml index 3e074365..ed1ce3e1 100644 --- a/database/data/categories/Ring.yaml +++ b/database/data/categories/Ring.yaml @@ -20,6 +20,11 @@ comments: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Ring \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: finitary algebraic proof: Take the algebraic theory of a ring. @@ -29,6 +34,11 @@ satisfied_properties: - property: Malcev proof: This follows in the same way as for $\Grp$, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. + dependencies: + - id: Grp + type: category + property: Malcev + satisfied: true - property: disjoint finite products proof: 'To show that $A \sqcup_{A \times B} B$ is trivial, let $R$ be a ring which admits homomorphisms $f : A \to R$, $g : B \to R$ with $f(p_1(a,b))=g(p_2(a,b))$ for all $(a,b) \in A \times B$, i.e. $f(a)=g(b)$. Applying this to $a=0$, $b=1$ yields $1=0$ in $R$.' @@ -42,6 +52,11 @@ unsatisfied_properties: - property: semi-strongly connected proof: This is because already the full subcategory $\CRing$ does not have this property. + dependencies: + - id: CRing + type: category + property: semi-strongly connected + satisfied: false - property: cogenerating set proof: 'We apply this lemma to the collection of fields: If $F$ is a field and $R$ is a non-trivial ring, any ring homomorphism $F \to R$ 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).' @@ -57,6 +72,11 @@ unsatisfied_properties: - property: regular quotient object classifier proof: We may copy the proof for $\CRing$ (since the proof there did not use that $P$ is commutative). Alternatively, any regular quotient object classifier in $\Ring$ would produce one in $\CRing$ by Lemma 1 here (dualized). + dependencies: + - id: CRing + type: category + property: regular quotient object classifier + satisfied: false - property: cocartesian cofiltered limits proof: >- @@ -66,6 +86,11 @@ unsatisfied_properties: - property: cofiltered-limit-stable epimorphisms proof: We know that $\CRing$ does not have this property. Now use the contrapositive of the dual of Lemma 2 here applied to the forgetful functor $\CRing \to \Ring$. It preserves epimorphisms by MSE/5133488. + dependencies: + - id: CRing + type: category + property: cofiltered-limit-stable epimorphisms + satisfied: false - property: effective cocongruences proof: See MO/510744. diff --git a/database/data/categories/Rng.yaml b/database/data/categories/Rng.yaml index c7b20f43..0ccfb64f 100644 --- a/database/data/categories/Rng.yaml +++ b/database/data/categories/Rng.yaml @@ -19,6 +19,11 @@ comments: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Rng \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: finitary algebraic proof: Take the algebraic theory of a rng. @@ -28,6 +33,11 @@ satisfied_properties: - property: Malcev proof: This follows in the same way as for $\Grp$, see also Example 2.2.5 in Malcev, protomodular, homological and semi-abelian categories. + dependencies: + - id: Grp + type: category + property: Malcev + satisfied: true unsatisfied_properties: - property: skeletal @@ -57,9 +67,19 @@ unsatisfied_properties: - property: coregular proof: 'We can copy the proof for $\Ring$. In short, the inclusion of diagonal matrices $\IQ^2 \hookrightarrow M_2(\IQ)$ is a regular monomorphism, but becomes zero after taking the pushout with $p_1 : \IQ^2 \twoheadrightarrow \IQ$ because $M_2(\IQ)$ is simple.' + dependencies: + - id: Ring + type: category + property: coregular + satisfied: false - property: regular quotient object classifier proof: 'Assume that $\Rng$ has a regular quotient object classifier $P$. Consider the functor $N : \Ab \to \Rng$ that equips an abelian group with zero multiplication. It is fully faithful and has a left adjoint mapping a rng $R$ to the abelian group $R/R^2$. If $R$ is a rng with zero multiplication and $R \to S$ is a surjective homomorphism, then $S$ has zero multiplication. Therefore, the assumptions of Lemma 1 here (dualized) apply and we conclude that $P/P^2$ is a regular quotient object classifier of $\Ab$. But we already know that $\Ab$ has no such object (in fact, the only additive categories with such an object are trivial by MSE/4086192).' + dependencies: + - id: Ab + type: category + property: regular quotient object classifier + satisfied: false - property: cocartesian cofiltered limits proof: >- @@ -69,6 +89,11 @@ unsatisfied_properties: - property: cofiltered-limit-stable epimorphisms proof: 'We know that $\Ring$ does not have this property. Now use the contrapositive of the dual of Lemma 2 here applied to the forgetful functor $\Ring \to \Rng$. We only need to verify that it preserves epimorphisms: Let $f : R \to S$ be an epimorphism in $\Ring$ and let $g,h : S \rightrightarrows T$ be two homomorphisms of rngs with $gf = hf$. The element $e = g(1) = h(1) \in T$ is idempotent, and $g,h$ become homomorphisms of rings $S \rightrightarrows eTe$. Hence, $g=h$.' + dependencies: + - id: Ring + type: category + property: cofiltered-limit-stable epimorphisms + satisfied: false - property: effective cocongruences proof: >- @@ -79,6 +104,11 @@ unsatisfied_properties: via $$p \mapsto \begin{pmatrix} 1 & 0 \\ 0 & 0 \end{pmatrix}, \quad q \mapsto \begin{pmatrix} 1 & 1 \\ 0 & 0 \end{pmatrix}.$$ From here, the rest of the proof is similar to the one for $\Ring$. + dependencies: + - id: Ring + type: category + property: effective cocongruences + satisfied: false special_objects: initial object: diff --git a/database/data/categories/Sch_R.yaml b/database/data/categories/Sch_R.yaml index 7269a7dd..f556b45d 100644 --- a/database/data/categories/Sch_R.yaml +++ b/database/data/categories/Sch_R.yaml @@ -21,6 +21,11 @@ comments: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Sch_R \to \LRS_R$ and $\LRS_R$ is locally small. + dependencies: + - id: LRS_R + type: category + property: locally small + satisfied: true - property: terminal object proof: The scheme $\Spec(R)$ is terminal. @@ -33,6 +38,11 @@ satisfied_properties: - property: infinitary extensive proof: One uses the same proof as for locally ringed spaces, using that open subspaces of schemes are also schemes. + dependencies: + - id: LRS_R + type: category + property: infinitary extensive + satisfied: true unsatisfied_properties: - property: skeletal @@ -49,9 +59,19 @@ unsatisfied_properties: - property: semi-strongly connected proof: This is because already the full subcategory of affine $R$-schemes is not semi-strongly connected, because its dual $\CAlg(R)$ is not semi-strongly connected. + dependencies: + - id: CAlg(R) + type: category + property: semi-strongly connected + satisfied: false - property: generating set proof: If $S$ is a generating set of $R$-schemes, then the set of affine open subsets of the schemes in $S$ would also be a generating set. This is then also a generating set in the category of affine $R$-schemes, corresponding to a cogenerating set in $\CAlg(R)$, which we know does not exist. + dependencies: + - id: CAlg(R) + type: category + property: cogenerating set + satisfied: false - property: quotients of congruences proof: If $\Sch_R$ had quotients of congruences, then by this lemma it would also have pushouts of monomorphisms, contradicting the fact that the span $\IA^1_K \leftarrow \Spec(K(t)) \rightarrow \IA^1_K$ has no pushout where $K$ is a residue field of $R$; see MO/9961. diff --git a/database/data/categories/SemiGrp.yaml b/database/data/categories/SemiGrp.yaml index d7c90468..2c772a12 100644 --- a/database/data/categories/SemiGrp.yaml +++ b/database/data/categories/SemiGrp.yaml @@ -16,6 +16,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\SemiGrp \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: finitary algebraic proof: Take the algebraic theory of a semigroup. @@ -61,15 +66,30 @@ unsatisfied_properties: The proof is similar to the proof for $\Grp$. Assume that there is a cogenerating set $S$. There is an infinite simple group $G$ larger than all the semigroups in $S$ (such as an alternating group). Since $\id_G, 1 : G \rightrightarrows G$ are different, there is a semigroup $H \in S$ and a homomorphism of semigroups $f : G \to H$ with $f \neq f \circ 1$. Then $$N \coloneqq \{g \in G : f(g) = f(1)\}$$ is a normal subgroup of $G$. It is proper, and hence trivial. But then $f$ is injective, which is a contradiction. + dependencies: + - id: Grp + type: category + property: cogenerating set + satisfied: false - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property (by this result). Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \SemiGrp$ that equips a set with the multiplication $a \cdot b \coloneqq a$. + dependencies: + - id: Set + type: category + property: cofiltered-limit-stable epimorphisms + satisfied: false - property: effective cocongruences proof: >- The proof is similar to $\Mon$, i.e. we adapt the counterexample from MO/510744. Namely, consider the semigroups $$\begin{align*} X & \coloneqq \langle p \mid p^2 = p \rangle,\\ E & \coloneqq \langle p, q \mid p^2 = p,\, q^2 = q,\, pq = q,\, qp = p \rangle, \end{align*}$$ whose underlying sets are $\{p\}$ and $\{p,q\}$, respectively. Then $X$ represents the functor sending a semigroup $A$ to its idempotents, and $E$ represents the relation on idempotents $a, b$ of $A$ that $ab = b$, $ba = a$. It is easy to check that this defines an equivalence relation (see MO/510744 for details). Since $p \ne q$ in $E$, the equalizer of the two maps $X \rightrightarrows E$ is the empty semigroup. Therefore, if $E$ were effective, it would be isomorphic to the coproduct $X \sqcup X$, whose underlying set consists of non-empty words in $p,q$ with $p,q$ strictly alternating. In particular, in this coproduct, $pq \ne q$. + dependencies: + - id: Mon + type: category + property: effective cocongruences + satisfied: false - property: natural numbers object proof: >- @@ -95,9 +115,19 @@ unsatisfied_properties: There is a canonical homomorphism $\iota : F \to M$, which is the equalizer of the two canonical homomorphisms $M \rightrightarrows N$ defined by $s \mapsto s_i$. We define $F \to K$ by $a \mapsto x$, $b \mapsto x$, $c \mapsto c$, $d \mapsto d$. Then $$K \sqcup_F M \cong \langle x,c,d,s : x s = c,\, x s = d \rangle$$ shows that $c,d \in K$ have the same image in the pushout. + dependencies: + - id: Mon + type: category + property: coregular + satisfied: false - property: regular subobject classifier proof: 'Assume that a regular subobject classifier $\Omega$ exists in $\SemiGrp$. The universal regular monomorphism $\top : 1 \to \Omega$ corresponds to an idempotent element $e \in \Omega$. It follows that $e \Omega e$ is a monoid with neutral element $e$. We claim that it is a regular subobject classifier in $\Mon$, which we know does not exist. Indeed, let $\iota : A \to B$ be a regular monomorphism of monoids. Since the forgetful functor $\Mon \to \SemiGrp$ preserves limits, we can also see $\iota$ as a regular monomorphism of semigroups. Hence, there is a unique homomorphism of semigroups $f : B \to \Omega$ with $\iota(A) = \{b \in B : f(b) = e\}$. Since $1 \in \iota(A)$, we have $f(1) = e$. Then $f$ corresponds to a homomorphism of monoids $f : B \to e \Omega e$ with kernel $\iota$, which proves our claim.' + dependencies: + - id: Mon + type: category + property: regular subobject classifier + satisfied: false special_objects: initial object: diff --git a/database/data/categories/Set_arrow.yaml b/database/data/categories/Set_arrow.yaml index 56b73135..4b486080 100644 --- a/database/data/categories/Set_arrow.yaml +++ b/database/data/categories/Set_arrow.yaml @@ -24,11 +24,21 @@ related: satisfied_properties: - property: locally small - proof: This is easy. + proof: There is a forgetful functor $\Set^{\rightarrow} \to \Set$, and \Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: semi-strongly connected proof: >- Consider two objects $(X, Y, f)$ and $(X', Y', f')$. If $X'$ is non-empty with element $x'$, we can construct a morphism $(\ell, r) : (X, Y, f) \to (X', Y', f')$ where $\ell$ is the constant function with value $x'$, and $r$ is the constant function with value $f'(x')$; and similarly if $X$ is non-empty we can construct a morphism $(X', Y', f') \to (X, Y, f)$. Otherwise, if $X$ and $X'$ are both empty, we can reduce to the fact that $\Set$ is semi-strongly connected to find $r$ in one direction, and fill in $\ell$ as the unique function $\varnothing \to \varnothing$. + dependencies: + - id: Set + type: category + property: semi-strongly connected + satisfied: true - property: Grothendieck topos proof: It is equivalent to the category of presheaves on the walking morphism. diff --git a/database/data/categories/Set_c.yaml b/database/data/categories/Set_c.yaml index ae626057..a93a8120 100644 --- a/database/data/categories/Set_c.yaml +++ b/database/data/categories/Set_c.yaml @@ -16,7 +16,12 @@ related: satisfied_properties: - property: locally small - proof: The collection of maps between two (countable) sets $X,Y$ is a subset of $X \times Y$ and therefore a set. + proof: It is a full subcategory of $\Set$, which is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: essentially small proof: Every countable set is isomorphic to a subset of $\IN$. @@ -24,13 +29,28 @@ satisfied_properties: - property: finitely complete proof: The embedding $\Set_\c \hookrightarrow \Set$ is closed under finite products and equalizers, hence under finite limits. check_redundancy: false + dependencies: + - id: Set + type: category + property: finitely complete + satisfied: true - property: finitely cocomplete proof: The embedding $\Set_\c \hookrightarrow \Set$ is closed under finite coproducts and coequalizers, hence under finite colimits. check_redundancy: false + dependencies: + - id: Set + type: category + property: finitely cocomplete + satisfied: true - property: subobject classifier proof: This is because $\{0,1\}$ is a subobject classifier in $\Set$, which is countable, and the monomorphisms coincide. + dependencies: + - id: Set + type: category + property: subobject classifier + satisfied: true - property: generator proof: The one-point set is clearly a generator. @@ -40,21 +60,51 @@ satisfied_properties: - property: semi-strongly connected proof: This is because the larger category $\Set$ has this property. + dependencies: + - id: Set + type: category + property: semi-strongly connected + satisfied: true - property: extensive proof: The same proof as for $\Set$ applies. Actually, the category is "countably extensive". + dependencies: + - id: Set + type: category + property: extensive + satisfied: true - property: countably distributive proof: By elementary set theory, a countable (disjoint) union of countable sets is again countable. Hence, countable coproducts exist in $\Set_\c$, and we already saw that finite products exist. The distributivity morphism is an isomorphism since this is the case in $\Set$ and the forgetful functor $\Set_\c \to \Set$ preserves finite products and countable coproducts. + dependencies: + - id: Set + type: category + property: countably distributive + satisfied: true - property: effective congruences proof: 'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\c$. Then using $1$ as a test object, we see that this induces an equivalence relation on $X$. We already know that $\Set$ has effective congruences (as does every topos). Using this result, we see that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set$. Also, the quotient $(X/E)_{\Set}$ is countable; and the forgetful functor $\Set_\c \to \Set$ is fully faithful and therefore reflects limits. Thus, we conclude that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set_\c$ as well.' + dependencies: + - id: Set + type: category + property: effective congruences + satisfied: true - property: regular proof: From the other properties we know that the category is finitely complete and that it has coequalizers. The regular epimorphisms are stable under pullback since this holds in $\Set$ and both regular epimorphisms (they are surjective maps) and pullbacks coincide. + dependencies: + - id: Set + type: category + property: regular + satisfied: true - property: coregular proof: From the other properties we know that the category is finitely cocomplete and that it has equalizers. The regular monomorphisms are stable under pushout since this holds in $\Set$ and both regular monomorphisms (they are injective maps) and pushouts coincide. + dependencies: + - id: Set + type: category + property: coregular + satisfied: true unsatisfied_properties: - property: small diff --git a/database/data/categories/Set_f.yaml b/database/data/categories/Set_f.yaml index 0f17ebb2..4c9fb82d 100644 --- a/database/data/categories/Set_f.yaml +++ b/database/data/categories/Set_f.yaml @@ -16,6 +16,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Set_\f \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: generator proof: The singleton set (which is not terminal) is a generator as it represents the forgetful functor $\Set_\f \to \Set$. @@ -28,9 +33,19 @@ satisfied_properties: - property: extensive proof: 'We first show that finite coproducts exist. The empty set is clearly initial. The disjoint union $X+Y$ of two sets $X,Y$ with the inclusion maps $X \rightarrow X+Y \leftarrow Y$ is a coproduct: The inclusions are injective, hence finite-to-one. If $f : X \to T$, $g : Y \to T$ are finite-to-one maps, the induced map $(f;g) : X + Y \to T$ is finite-to-one since the fiber of $t \in T$ is $f^*(\{t\}) + g^*(\{t\})$, which is finite. Hence, finite coproducts exist. A map $A \to X + Y$ yields a decomposition $A = A_X + A_Y$ with maps $A_X \to X$, $A_Y \to Y$ (since $\Set$ is extensive). Here, $A \to X + Y$ is finite-to-one iff $A_X \to X$ and $A_Y \to Y$ are finite-to-one.' + dependencies: + - id: Set + type: category + property: extensive + satisfied: true - property: equalizers proof: 'Equalizers can be constructed as in $\Set$ because of the following trivial observation: if $f : X \to Y$ is a finite-to-one map and $E \subseteq Y$ is a subset with $f(X) \subseteq E$, then the induced map $f^E : X \to E$ is also finite-to-one.' + dependencies: + - id: Set + type: category + property: equalizers + satisfied: true - property: epi-regular proof: 'If $f : X \to Y$ is an epimorphism in $\Set_\f$, i.e. a surjective finite-to-one map, it is a coequalizer of the two maps $p_1, p_2 : X \times_Y Y \rightrightarrows Y$ in $\Set$. These maps are finite-to-one since $p_i^*(\{y\}) \cong f^*(\{y\})$ for $i=1,2$, and their coequalizer is also $f$ in $\Set_\f$: It suffices to observe that if $h : Y \to T$ is a map such that $h \circ f$ is finite-to-one, then $h$ is finite-to-one as well. In fact, surjectivity of $f$ implies $h^*(\{t\}) = f_*((h \circ f)^*(\{t\}))$ for $t \in T$.' @@ -43,18 +58,42 @@ satisfied_properties: - property: effective congruences proof: 'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\f$. From the proof on quotients of congruences in $\Set_\f$, we have a quotient map $p : X \to X/E$ in $\Set_\f$, and $E$ is the kernel pair of $p$ in $\Set$. It remains to see that $E$ is also the kernel pair of $p$ in $\Set_f$. Thus, suppose we have $x_1, x_2 : T \rightrightarrows X$ with $p \circ x_1 = p \circ x_2$. Then there is a unique $e : T \to E$ in $\Set$ with $x_1 = f\circ e$ and $x_2 = g\circ e$. Since $f\circ e$ is finite-to-one, we must have $e$ is finite-to-one as well.' + dependencies: + - id: Set_f + type: category + property: quotients of congruences + satisfied: true - property: effective cocongruences proof: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Set_f$. Then it is a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences, that implies $E$ is the cokernel pair of some function $h : Z \to X$ in $\Set$. By the dual of this result, if $\inc_Y : Y \hookrightarrow X$ is the equalizer of $f$ and $g$, then $E$ is also the cokernel pair of $\inc_Y$ in $\Set$. It remains to see that $E$ is the cokernel pair of $\inc_Y$ in $\Set_\f$ as well. Thus, suppose $a, b : X \rightrightarrows T$ are such that $a |_Y = b |_Y$. Then there is a unique $c : E\to T$ in $\Set$ with $a = c\circ f$ and $b = c\circ g$. Since $(f;g) : X + X \to E$ is surjective and $c \circ (f;g) = (a;b)$ is finite-to-one, we see $c$ is finite-to-one as well.' + dependencies: + - id: Set + type: category + property: co-Malcev + satisfied: true + - id: Set + type: category + property: effective cocongruences + satisfied: true - property: locally cartesian closed proof: If $X$ is a set, the equivalence $\Set/X \simeq \Set^X$, $f \mapsto (f^*(\{x\}))_{x \in X}$ restricts to an equivalence $\Set_\f / X \simeq \FinSet^X$. This category is cartesian closed since $\FinSet$ is cartesian closed and products of cartesian closed categories are cartesian closed. + dependencies: + - id: FinSet + type: category + property: cartesian closed + satisfied: true - property: ℵ₁-accessible proof: 'We first show that $\aleph_1$-directed colimits exist and are preserved by the forgetful functor to $\Set$. Let $(X_i)_{i \in I}$ be a diagram in $\Set_\f$ indexed by a $\aleph_1$-directed poset $I$. Let $(u_i : X_i \to X)$ be the colimit in $\Set$. Each map $u_i$ is finite-to-one: Otherwise, some fiber $u_i^*(\{x\}) \subseteq X_i$ contains infinitely many elements $a_1,a_2,\dotsc$. For every $n \geq 1$ we find $i_n \geq i$ such that $a_1,a_n$ have the same image in $X_{i_n}$. Let $i_\infty \in I$ be an upper bound of all $i_n$. Then all $a_n$ have the same image in $X_{i_\infty}$. This is a contradiction since $X_i \to X_{i_\infty}$ is finite-to-one. Now if $f : X \to Y$ is a map such that each $f \circ u_i$ is finite-to-one, then $f$ is finite-to-one as well: If a fiber $f^*(\{y\})$ contains infinitely many distinct elements $x_1,x_2,\dotsc$, there is some index $i$ such that all have a preimage in $X_i$, but then $(f \circ u_i)^*(\{y\})$ would be infinite. This concludes the proof that $\aleph_1$-directed colimits exist. In $\Set$, every set $X$ is the $\aleph_1$-directed colimit of its countable subsets. This remains true in $\Set_\f$ because a map $X \to Y$ is finite-to-one as long as each restriction to a countable subset of $X$ is finite-to-one. Moreover, every countable set is $\aleph_1$-presentable in $\Set$, but also in $\Set_\f$.' - property: ℵ₁-cofiltered limits proof: 'We derive this from the fact that $\FinSet$ is closed under $\aleph_1$-cofiltered limits in $\Set$. Let $D : \I \to \Set_\f$ be an $\aleph_1$-cofiltered diagram. Let $(p_i : L \to D(i))_{i \in \I}$ be the limit cone in $\Set$. Each $p_i$ is finite-to-one, because the fiber over $d \in D(i)$ is the limit of the $\aleph_1$-cofiltered diagram $\tilde{D} : I/i \to \FinSet$ which maps $j \to i$ to $D(j \to i)^*(\{d\})$. To verify the universal property, let $(f_i : T \to D(i))_{i \in \I}$ be a cone in $\Set_\f$. There is a unique map $f : T \to L$ such that $p_i f = f_i$ for every $i \in \I$, and it remains to prove that $f$ is finite-to-one. Choose any $i \in \I$. Then for every $x \in L$ we have $f^*(\{x\}) \subseteq f_i^*(\{p_i(x)\})$, and the latter set is finite.' + dependencies: + - id: FinSet + type: category + property: ℵ₁-cofiltered limits + satisfied: true unsatisfied_properties: - property: skeletal @@ -65,6 +104,11 @@ unsatisfied_properties: - property: strongly connected proof: Already $\Set$ is not strongly connected. + dependencies: + - id: Set + type: category + property: strongly connected + satisfied: false - property: binary powers proof: 'More generally, if $X,Y$ are two non-empty sets such that $X \times Y$ exists in $\Set_\f$, then both $X$ and $Y$ must be finite. In fact, the forgetful functor to $\Set$ is representable, so it must preserve products. This means we can assume $X \times Y$ is the usual cartesian product with the usual projections. Since $p_1 : X \times Y \to X$ is finite-to-one and $X$ is non-empty, $Y$ is finite. By symmetry, also $X$ is finite. (Conversely, if $X$ and $Y$ are finite, or one of them is empty, then indeed $X \times Y$ exists.)' diff --git a/database/data/categories/Set_pointed.yaml b/database/data/categories/Set_pointed.yaml index c34cc04d..d57ed7d6 100644 --- a/database/data/categories/Set_pointed.yaml +++ b/database/data/categories/Set_pointed.yaml @@ -16,6 +16,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Set_* \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: pointed proof: The singleton set is a zero object. @@ -33,9 +38,19 @@ satisfied_properties: - property: coregular proof: From the other properties we know that (co-)limits exist and that monomorphisms coincide with injective pointed maps. So it suffices to prove that these maps are stable under pushouts. This follows from the corresponding fact for $\Set$ and the observation that the forgetful functor $\Set_* \to \Set$ preserves pushouts. check_redundancy: false + dependencies: + - id: Set + type: category + property: coregular + satisfied: true - property: co-Malcev proof: Malcev categories are closed under slice categories by Prop. 2.2.14 in Malcev, protomodular, homological and semi-abelian categories. It follows that co-Malcev categories are closed under coslice categories, and $\Set_*$ is a coslice category of $\Set$, which is co-Malcev since every elementary topos is co-Malcev. + dependencies: + - id: Set + type: category + property: co-Malcev + satisfied: true - property: cocartesian cofiltered limits proof: |- @@ -65,6 +80,11 @@ unsatisfied_properties: - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \Set_*$ that freely adds a base point. + dependencies: + - id: Set + type: category + property: cofiltered-limit-stable epimorphisms + satisfied: false special_objects: initial object: diff --git a/database/data/categories/Setne.yaml b/database/data/categories/Setne.yaml index 353a88b2..ddd90ffe 100644 --- a/database/data/categories/Setne.yaml +++ b/database/data/categories/Setne.yaml @@ -14,7 +14,12 @@ related: satisfied_properties: - property: locally small - proof: There is a forgetful functor $\Setne \to \Set$ and $\Set$ is locally small. + proof: It is a full subcategory of $\Set$, which is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: generator proof: The one-point set is clearly a generator. @@ -25,36 +30,86 @@ satisfied_properties: - property: products proof: Take the product of non-empty sets inside of $\Set$ and observe that it is non-empty by the axiom of choice. + dependencies: + - id: Set + type: category + property: products + satisfied: true - property: cartesian closed proof: This follows as for $\Set$, since for non-empty sets $X,Y$ there is at least one function $X \to Y$. + dependencies: + - id: Set + type: category + property: cartesian closed + satisfied: true - property: binary coproducts proof: The disjoint union of two non-empty sets is non-empty. + dependencies: + - id: Set + type: category + property: binary coproducts + satisfied: true - property: mono-regular proof: This follows as for $\Set$. + dependencies: + - id: Set + type: category + property: mono-regular + satisfied: true - property: epi-regular proof: This follows as for $\Set$. + dependencies: + - id: Set + type: category + property: epi-regular + satisfied: true - property: strongly connected proof: Use constant maps. - property: finitely accessible proof: Since the inclusion $\Setne \hookrightarrow \Set$ is closed under non-empty colimits, it is also closed under filtered colimits. Therefore, non-empty finite sets are still finitely presentable in $\Setne$, and every non-empty set is written as a filtered colimit of them. + dependencies: + - id: Set + type: category + property: finitely accessible + satisfied: true - property: generalized variety proof: Since the inclusion $\Setne \hookrightarrow \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 $\Setne$, and every non-empty set is written as a sifted colimit of them. + dependencies: + - id: Set + type: category + property: generalized variety + satisfied: true - property: natural numbers object proof: Any natural numbers object in $\Set$, such as $(\IN,0,n \mapsto n+1)$, is clearly also one in $\Setne$. + dependencies: + - id: Set + type: category + property: natural numbers object + satisfied: true - property: multi-complete proof: Let $D$ be a diagram in $\Setne$, and let $L$ be a limit of $D$ in $\Set$. If $L$ is non-empty, it gives a limit in $\Setne$ as well. If $L$ is the empty set, there is no cone over $D$ in $\Setne$; hence the empty set of cones gives a multi-limit of $D$ in $\Setne$. + dependencies: + - id: Set + type: category + property: complete + satisfied: true - property: effective congruences proof: 'If a congruence $E \rightrightarrows X$ is the kernel pair of $h : X \to Z$, with both $E$ and $X$ non-empty, then certainly $Z$ must also be non-empty.' + dependencies: + - id: Set + type: category + property: effective congruences + satisfied: true unsatisfied_properties: - property: skeletal @@ -77,6 +132,11 @@ unsatisfied_properties: - property: coaccessible proof: If $\Setne$ is coaccessible, then by the dual of Cor. 2.44 in Adamek-Rosicky also the coslice category $\{\ast\} / \Setne$ would be coaccessible. But this category is isomorphic to $\Set_*$, from which we know that it is not coaccessible (namely, because of Thm. 1.64 in loc. cit.). + dependencies: + - id: Set_* + type: category + property: coaccessible + satisfied: false special_objects: terminal object: diff --git a/database/data/categories/Sh(X).yaml b/database/data/categories/Sh(X).yaml index 6aac48ba..2fc3316c 100644 --- a/database/data/categories/Sh(X).yaml +++ b/database/data/categories/Sh(X).yaml @@ -30,11 +30,16 @@ satisfied_properties: unsatisfied_properties: - property: skeletal proof: Consider constant sheaves for isomorphic but non-equal sets. + dependencies: + - id: Set + type: category + property: skeletal + satisfied: false - property: generator proof: >- Suppose $\Sh(X)$ had a generator. Then by this result, every subterminal object would be either initial or terminal. On the other hand, the subterminal objects of $\Sh(X)$ are of the form $y_U \coloneqq \Hom({-}, U)$ for $U$ open. (Alternative descriptions of $y_U$ include: - $$y_U(V) = \begin{cases} 1, & V \subseteq U; \\ \varnothing & \mathrm{otherwise} \end{cases}$$ + $$y_U(V) = \begin{cases} 1, & V \subseteq U; \\ \varnothing & \text{otherwise} \end{cases}$$ with the unique restriction maps; and $y_U$ represents the functor $\Gamma(U, {-})$ of sections over $U$.) Therefore, the lemma implies that every open set of $X$ is either $\varnothing$ or $X$, contradicting our assumption that $X$ does not have the indiscrete topology. special_objects: diff --git a/database/data/categories/Sh(X,Ab).yaml b/database/data/categories/Sh(X,Ab).yaml index 5fc15918..3752e9e8 100644 --- a/database/data/categories/Sh(X,Ab).yaml +++ b/database/data/categories/Sh(X,Ab).yaml @@ -27,9 +27,19 @@ satisfied_properties: unsatisfied_properties: - property: skeletal proof: Consider constant sheaves for isomorphic but non-equal abelian groups. + dependencies: + - id: Ab + type: category + property: skeletal + satisfied: false - property: split abelian proof: 'Choose a point $x \in X$. The functor $x_* : \Ab \to \Sh(X,\Ab)$ (skyscraper sheaf) is exact, and its left adjoint $x^* : \Sh(X,\Ab) \to \Ab$ (stalk) satisfies $x^* x_* \cong \id_{\Ab}$. Now, since $\Ab$ is not split abelian, there is a short exact sequence of abelian groups $0 \to A \to B \to C \to 0$ that does not split. Then $0 \to x_* A \to x_* B \to x_* C \to 0$ is also exact, but it does not split: Otherwise it would also be split after applying $x^*$, which however gives the original sequence in $\Ab$.' + dependencies: + - id: Ab + type: category + property: split abelian + satisfied: false special_objects: initial object: diff --git a/database/data/categories/Sp.yaml b/database/data/categories/Sp.yaml index c7e4c47f..c3625bb7 100644 --- a/database/data/categories/Sp.yaml +++ b/database/data/categories/Sp.yaml @@ -16,18 +16,42 @@ related: satisfied_properties: - property: essentially small proof: This holds because $\FinSet$ and $\IB$ are essentially small. + dependencies: + - id: FinSet + type: category + property: essentially small + satisfied: true + - id: B + type: category + property: essentially small + satisfied: true - property: elementary topos proof: The category is equivalent to $\prod_{n \geq 0} \Sigma_n{-}\FinSet$ (where $\Sigma_n$ denotes the symmetric group of order $n$), and each $\Sigma_n{-}\FinSet$ is an elementary topos since is $\FinSet$ an elementary topos and $\Sigma_n$ is a finite group, cf. Johnstone, Part B, Corollary 2.3.18. + dependencies: + - id: FinSet + type: category + property: elementary topos + satisfied: true - property: cogenerator proof: '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: ℵ₁-accessible proof: We know that $\FinSet$ has $\aleph_1$-filtered colimits and that every object is $\aleph_1$-presentable. It follows that for every $n \in \IN$ also $\Sigma_n{-}\FinSet$ has $\aleph_1$-filtered colimits and that every object is $\aleph_1$-presentable. From this it follows formally that $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$ also has these properties. In particular, $\Sp$ is $\aleph_1$-accessible. + dependencies: + - id: FinSet + type: category + property: ℵ₁-accessible + satisfied: true - property: ℵ₁-cofiltered limits proof: Since $\FinSet$ has $\aleph_1$-cofiltered limits, also $\Sigma_n{-}\FinSet$ has $\aleph_1$-cofiltered limits for every $n \geq 0$. Hence, $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$ has $\aleph_1$-cofiltered limits. + dependencies: + - id: FinSet + type: category + property: ℵ₁-cofiltered limits + satisfied: true unsatisfied_properties: - property: skeletal diff --git a/database/data/categories/Top.yaml b/database/data/categories/Top.yaml index c4d961e2..ece8d70f 100644 --- a/database/data/categories/Top.yaml +++ b/database/data/categories/Top.yaml @@ -18,13 +18,28 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Top \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: complete proof: Take the limit of the underlying sets and endow it with the coarsest topology making all projections continuous. + dependencies: + - id: Set + type: category + property: complete + satisfied: true - property: cocomplete proof: Take the colimit of the underlying sets and endow it with the finest topology making all inclusions continuous. check_redundancy: false + dependencies: + - id: Set + type: category + property: cocomplete + satisfied: true - property: well-powered proof: This is clear from the classification of monomorphisms as injective continuous maps. @@ -43,6 +58,11 @@ satisfied_properties: - property: infinitary extensive proof: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : Y \to \coprod_i X_i$ corresponds to a decomposition $Y = \coprod_i Y_i$ (as sets) with maps $f_i : Y_i \to X_i$. Endow $Y_i$ with the subspace topology. If $f$ is continuous, each $Y_i = f^{-1}(X_i)$ is open in $Y$, so that $Y = \coprod_i Y_i$ holds as topological spaces, and each $f_i$ is continuous.' + dependencies: + - id: Set + type: category + property: infinitary extensive + satisfied: true - property: regular subobject classifier proof: The indiscrete two-point space $\{0,1\}$ is a regular subobject classifier since continuous maps $X \to \{0,1\}$ correspond to subsets of $X$. @@ -71,15 +91,25 @@ unsatisfied_properties: - property: coaccessible proof: 'Assume $\Top$ is coaccessible. Let $p : 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 $\Set$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\Set$ is not coaccessible, this is a contradiction.' + dependencies: + - id: Set + type: category + property: coaccessible + satisfied: false - property: co-Malcev proof: 'See MO/509548. We can also phrase the proof as follows: Consider the forgetful functor $U : \Top \to \Set$ and the relation $R \subseteq U^2$ defined by $R(X) \coloneqq \{(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.' - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \Top$ which equips a set with the indiscrete topology. + dependencies: + - id: Set + type: category + property: cofiltered-limit-stable epimorphisms + satisfied: false - property: effective cocongruences - proof: 'Consider the indiscrete topological space $I$ on two points. This represents the functor which takes a topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $1 \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: if we have $h : Z\to 1$ which equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete space on two points.' + proof: 'Consider the indiscrete topological space $I$ on two points. This represents the functor which takes a topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $1 \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: if we have $h : Z \to 1$ which equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete space on two points.' special_objects: initial object: diff --git a/database/data/categories/Top_pointed.yaml b/database/data/categories/Top_pointed.yaml index 5528583d..54182d0d 100644 --- a/database/data/categories/Top_pointed.yaml +++ b/database/data/categories/Top_pointed.yaml @@ -16,6 +16,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Top_* \to \Set_*$ and $\Set_*$ is locally small. + dependencies: + - id: Set_* + type: category + property: locally small + satisfied: true - property: pointed proof: The singleton space $\{0\}$ with base point $0$ is a zero object. @@ -24,14 +29,29 @@ satisfied_properties: - property: complete proof: This follows from $\Top_* \cong 1 / \Top$ and the fact that $\Top$ is complete. Concretely, the limit of pointed spaces $(X_i,x_i)$ is the limit of the underlying spaces $X_i$ equipped with the base point that projects down to each $x_i$. check_redundancy: false + dependencies: + - id: Top + type: category + property: complete + satisfied: true - property: coequalizers proof: This follows immediately from the fact that $\Top$ has coequalizers. check_redundancy: false + dependencies: + - id: Top + type: category + property: coequalizers + satisfied: true - property: coproducts proof: This follows from $\Top_* \cong 1 / \Top$ and the fact that $\Top$ has wide pushouts. check_redundancy: false + dependencies: + - id: Top + type: category + property: wide pushouts + satisfied: true - property: well-powered proof: This is clear from the classification of monomorphisms as injective pointed continuous maps. @@ -52,19 +72,40 @@ satisfied_properties: proof: Since embeddings are regular monomorphisms in this category (see below) and hence strong monomorphisms, it suffices to prove that the canonical morphism $X \vee Y \hookrightarrow X \times Y$ is an embedding. For a proof, see MSE/4055988. - property: CIP - proof: This follows since $\Set_*$ has this property and the forgetful functor preserves products and coproducts. + proof: This follows since $\Set_*$ has this property, the forgetful functor preserves products and coproducts, and the forgetful functor reflects monomorphisms. + + dependencies: + - id: Set_* + type: category + property: CIP + satisfied: true - property: cocartesian cofiltered limits proof: >- We continue the proof for $\Set_*$ by showing that the natural bijective map $$\textstyle \alpha : X \vee \lim_i Y_i \to \lim_i (X \vee Y_i)$$ is open. It suffices to consider open sets of two types: (1) If $U \subseteq X$ is open, the $\alpha$-image of $U \vee \lim_i Y_i$ is $p_{i_0}^{-1}(U \vee Y_{i_0})$ for any chosen index $i_0$, hence open. (2) If $i$ is an index and $V_i \subseteq Y_i$ is open, then the $\alpha$-image of $X \vee (p_i^{-1}(V_i) \cap \lim_i Y_i)$ is $p_i^{-1}(X \vee V_i)$, hence open. + dependencies: + - id: Set_* + type: category + property: cocartesian cofiltered limits + satisfied: true - property: filtered-colimit-stable monomorphisms proof: This follows from Lemma 2 here applied to the forgetful functor to $\Set$. + dependencies: + - id: Set + type: category + property: filtered-colimit-stable monomorphisms + satisfied: true - property: coregular proof: Regular monomorphisms coincide with the embeddings (see below). Since $\Top$ is coregular, they are stable under pushouts, and pushouts in $\Top_*$ are the same. + dependencies: + - id: Top + type: category + property: coregular + satisfied: true unsatisfied_properties: - property: skeletal @@ -84,6 +125,11 @@ unsatisfied_properties: - property: co-Malcev proof: 'We can adjust the proof for $\Top$ as follows: Consider the forgetful functor $U : \Top_* \to \Set$ and the relation $R \subseteq U^2$ defined by $R(X) \coloneqq \{(x,y) \in U(X)^2 : x \in \overline{\{y\}} \}$. Both are representable: $U$ by the discrete space $\{0,1\}$ with base point $0$ and $R$ by the Sierpinski space with an isolated base point added. It is clear that $R$ is reflexive, but not symmetric.' + dependencies: + - id: Top + type: category + property: co-Malcev + satisfied: false - property: unital proof: 'The joint image of $X \to X \times Y \leftarrow Y$ is just $\{(x,0) : x \in X\} \cup \{(0,y) : y \in Y\}$ (where $0$ denotes the base point), which is clearly a proper subset of $X \times Y$ when both $X,Y$ are non-trivial.' @@ -94,18 +140,49 @@ unsatisfied_properties: - property: regular quotient object classifier proof: We can recycle the proof for $\Set_*$ using discrete topological spaces. + dependencies: + - id: Set_* + type: category + property: regular quotient object classifier + satisfied: false + # FIXME! + # with_proof: true - property: coaccessible proof: 'We can adjust the proof for $\Top$ as follows: Assume $\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 : 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 $\Set_*$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\Set_*$ is not coaccessible, this is a contradiction.' + dependencies: + - id: Top + type: category + property: coaccessible + satisfied: false + - id: Set_* + type: category + property: coaccessible + satisfied: false - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set_*$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set_* \to \Top_*$ that equips a pointed set with the indiscrete topology. + dependencies: + - id: Set_* + type: category + property: cofiltered-limit-stable epimorphisms + satisfied: false - property: effective congruences proof: Suppose that $\Top_*$ had effective congruences. Then by this result, $\Top$ would also have effective congruences, which we know is not the case. + dependencies: + - id: Top + type: category + property: effective congruences + satisfied: false - property: effective cocongruences proof: 'This counterexample is adapted from the counterexample for $\Top$. Consider the pointed topological space $I \coloneqq \{ *, a, b \}$ with topology $\{ \varnothing, \{ * \}, \{ a, b \}, \{ *, a, b \} \}$. This represents the functor which sends a pointed topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $\{ *, a \} \rightrightarrows I$ on the discrete space $\{ *, a \}$, where the maps are $*\mapsto *, a\mapsto a$ and $*\mapsto *, a\mapsto b$ respectively. However, this cannot be effective: if we have $h : Z \to \{ *, a \}$ which equalizes the cocongruence, then $h$ must be the constant function with value $*$. But that means the cokernel pair of $h$ is the discrete space on $\{ *, a, b \}$.' + dependencies: + - id: Top + type: category + property: effective cocongruences + satisfied: false special_objects: initial object: diff --git a/database/data/categories/TorsAb.yaml b/database/data/categories/TorsAb.yaml index a2ce9462..c342c0c0 100644 --- a/database/data/categories/TorsAb.yaml +++ b/database/data/categories/TorsAb.yaml @@ -16,27 +16,62 @@ related: satisfied_properties: - property: locally small - proof: There is a forgetful functor $\TorsAb \to \Ab$ and $\Ab$ is locally small. + proof: It is a full subcategory of $\Ab$, which is locally small. + dependencies: + - id: Ab + type: category + property: locally small + satisfied: true - property: cocomplete proof: The embedding $\TorsAb \hookrightarrow \Ab$ is closed under colimits and $\Ab$ is cocomplete. check_redundancy: false + dependencies: + - id: Ab + type: category + property: cocomplete + satisfied: true - property: complete proof: The embedding $\TorsAb \hookrightarrow \Ab$ has a right adjoint, sending an abelian group $A$ to its torsion subgroup $T(A)$. Since $\Ab$ is complete, $\TorsAb$ is complete as well. The limit of a diagram of torsion abelian groups is the torsion subgroup of the limit of the underlying abelian groups. Notice that the torsion subgroup is not required in the case of equalizers, since a subgroup of a torsion abelian group is already torsion. Also, a finite product of torsion abelian groups is already torsion. check_redundancy: false + dependencies: + - id: Ab + type: category + property: complete + satisfied: true - property: preadditive proof: It is a full subcategory of the preadditive category $\Ab$. + dependencies: + - id: Ab + type: category + property: preadditive + satisfied: true - property: normal proof: 'If $f : A \to B$ is a monomorphism, it is injective (see below). In $\Ab$ it is then the kernel of $B \to B/f(A)$. Since $B/f(A)$ is torsion, it is also the kernel in $\TorsAb$.' + dependencies: + - id: Ab + type: category + property: normal + satisfied: true - property: conormal proof: 'If $f : A \to B$ is an epimorphism, it is surjective (see below). In $\Ab$ it is then the cokernel of its kernel $K \hookrightarrow A$. Since $K$ is torsion, it is also the cokernel in $\TorsAb$.' + dependencies: + - id: Ab + type: category + property: conormal + satisfied: true - property: finitely accessible proof: We already know that (filtered) colimits exist and are preserved by the forgetful functor to $\Ab$. Every torsion abelian group is the filtered colimit of its finitely generated subgroups (which are finite). These are finitely presentable in $\Ab$, hence also in $\TorsAb$. + dependencies: + - id: Ab + type: category + property: finitely accessible + satisfied: true unsatisfied_properties: - property: skeletal diff --git a/database/data/categories/TorsFreeAb.yaml b/database/data/categories/TorsFreeAb.yaml index 1bc8bd9c..2d705135 100644 --- a/database/data/categories/TorsFreeAb.yaml +++ b/database/data/categories/TorsFreeAb.yaml @@ -16,21 +16,46 @@ related: satisfied_properties: - property: locally small - proof: There is a forgetful functor $\TorsFreeAb \to \Ab$ and $\Ab$ is locally small. + proof: It is a full subcategory of $\Ab$, which is locally small. + dependencies: + - id: Ab + type: category + property: locally small + satisfied: true - property: complete proof: The embedding $\TorsFreeAb \hookrightarrow \Ab$ is closed under limits and $\Ab$ is complete. check_redundancy: false + dependencies: + - id: Ab + type: category + property: complete + satisfied: true - property: cocomplete proof: 'The embedding $\TorsFreeAb \hookrightarrow \Ab$ has a left adjoint, sending an abelian group $A$ to its torsion-free reflection $A/T(A)$, where $T(A)$ is the torsion subgroup of $A$. Since $\Ab$ is cocomplete, $\TorsFreeAb$ is cocomplete as well. The colimit of a diagram of torsion-free abelian groups is the torsion-free reflection of the colimit of the underlying abelian groups. Notice that the reflection is not required in the case of coproducts: the direct sum of torsion-free abelian groups is again torsion-free. It is also not required for filtered colimits.' check_redundancy: false + dependencies: + - id: Ab + type: category + property: cocomplete + satisfied: true - property: finitely accessible proof: We already saw that filtered colimits exist and are preserved by the forgetful functor to $\Ab$. Every torsion-free abelian group is the filtered colimit of its finitely generated subgroups, which are in fact free. Finitely generated free abelian groups are finitely presentable in $\Ab$ and therefore also in $\TorsFreeAb$. + dependencies: + - id: Ab + type: category + property: finitely accessible + satisfied: true - property: preadditive proof: It is a full subcategory of the preadditive category $\Ab$. + dependencies: + - id: Ab + type: category + property: preadditive + satisfied: true - property: cogenerator proof: The additive group $\IQ$ is a cogenerator since every torsion-free abelian group $A$ embeds into $A \otimes \IQ$, which is a vector space over $\IQ$, and by linear algebra $K$ is a cogenerator in the category of vector spaces over $K$. @@ -43,6 +68,11 @@ satisfied_properties: It suffices to prove that regular monomorphisms (which are classified below) are stable under pushouts. Let $i : A \to B$ be a regular monomorphism in $\TorsFreeAb$, i.e. $i$ is injective and its $\Ab$-cokernel $B/i(A)$ is torsion-free, and let $f : B \to C$ be any morphism in $\TorsFreeAb$. Their $\Ab$-pushout is $$P = (B \times C)/\{(i(a),-f(a)): a \in A\}.$$ It is torsion-free: If $n \in \IZ \setminus \{0\}$ and $n (b,c) = (i(a),-f(a))$, there is some $a' \in A$ with $b = i(a')$ since $B/i(A)$ is torsion-free. It follows $n a' = a$, and then $c = -f(a')$ since $C$ is torsion-free. Thus, $(b,c) = (i(a'),-f(a'))$, which proves our claim. Therefore, $P$ is also the pushout in $\TorsFreeAb$. The homomorphism $j : C \to P$, $j(c) = [0,c]$ is injective (since $\Ab$ is coregular, but a direct proof is also easy), and by the universal property of $P$ its $\Ab$-cokernel is isomorphic to the $\Ab$-cokernel of $i$, which is torsion-free. + dependencies: + - id: Ab + type: category + property: coregular + satisfied: true unsatisfied_properties: - property: skeletal diff --git a/database/data/categories/Vect.yaml b/database/data/categories/Vect.yaml index 2bc65497..244a4fa9 100644 --- a/database/data/categories/Vect.yaml +++ b/database/data/categories/Vect.yaml @@ -21,6 +21,11 @@ related: satisfied_properties: - property: locally small proof: There is a forgetful functor $\Vect \to \Set$ and $\Set$ is locally small. + dependencies: + - id: Set + type: category + property: locally small + satisfied: true - property: split abelian proof: That $\Vect$ is abelian is a standard fact, see Mac Lane, Ch. VIII. Furthermore, it is a fact from linear algebra that every subspace has a complement, which is why every short exact sequence splits. diff --git a/database/data/categories/Z.yaml b/database/data/categories/Z.yaml index 81cac005..c4b67636 100644 --- a/database/data/categories/Z.yaml +++ b/database/data/categories/Z.yaml @@ -17,26 +17,61 @@ related: satisfied_properties: - property: complete proof: This follows immediately from the fact for $\Set$. + dependencies: + - id: Set + type: category + property: complete + satisfied: true - property: cocomplete proof: This follows immediately from the fact for $\Set$. check_redundancy: false + dependencies: + - id: Set + type: category + property: cocomplete + satisfied: true - property: infinitary extensive proof: This follows immediately from the fact for $\Set$. + dependencies: + - id: Set + type: category + property: infinitary extensive + satisfied: true - property: exact filtered colimits proof: This follows immediately from the fact for $\Set$. + dependencies: + - id: Set + type: category + property: exact filtered colimits + satisfied: true - property: regular proof: This follows immediately from the fact for $\Set$. + dependencies: + - id: Set + type: category + property: regular + satisfied: true - property: coregular proof: This follows immediately from the fact for $\Set$. + dependencies: + - id: Set + type: category + property: coregular + satisfied: true - property: co-Malcev proof: This follows immediately from the fact for $\Set$. check_redundancy: false + dependencies: + - id: Set + type: category + property: co-Malcev + satisfied: true - property: effective congruences proof: 'If we have a congruence $E \rightrightarrows X$ in $[\CRing, \Set]$, then evaluating at any commutative ring gives a congruence in $\Set$. Defining $Y$ pointwise to be the quotient of this congruence, we get a morphism of functors $h : X \to Y$, and by this result applied pointwise, the kernel pair of $h$ is $E$.' @@ -51,9 +86,19 @@ unsatisfied_properties: - property: Malcev proof: Any counterexample for $\Set$ (i.e., any non-symmetric reflexive relation) yields one for this category by taking constant functors. + dependencies: + - id: Set + type: category + property: Malcev + satisfied: false - property: semi-strongly connected proof: This is because already the full subcategory of representable functors is not semi-strongly connected, because $\CRing$ is not semi-strongly connected. Specifically, there is no morphism between $\Hom(\IF_2,-)$ and $\Hom(\IF_3,-)$. + dependencies: + - id: CRing + type: category + property: semi-strongly connected + satisfied: false - property: locally essentially small proof: See MO/390611 for example. @@ -66,6 +111,11 @@ unsatisfied_properties: - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to [\CRing, \Set]$ that maps a set to its constant functor. + dependencies: + - id: Set + type: category + property: cofiltered-limit-stable epimorphisms + satisfied: false special_objects: initial object: diff --git a/database/data/categories/Z_div.yaml b/database/data/categories/Z_div.yaml index e51985d6..28fc33c6 100644 --- a/database/data/categories/Z_div.yaml +++ b/database/data/categories/Z_div.yaml @@ -24,7 +24,7 @@ satisfied_properties: check_redundancy: false - property: distributive - proof: 'We need to prove $\lcm_i \gcd(a, b_i) \cong \gcd(a, \lcm_i b_i)$ for finite families. If $x$ denotes the LHS and $y$ denotes the RHS, the relation $x \mid y$ is formal. If $v_p(-) : \IZ \to \IN_{\infty}$ denotes the multiplicity of a prime $p$, then $v_p(x)$ equals $\max_i \min(v_p(a),v_p(b_i))$, and $v_p(y)$ equals $\min(v_p(a), \max_i v_p(b_i))$. Since our family is finite, there is some $i_0$ with $\max_i v_p(b_i) = v_p(b_{i_0})$. Then $v_p(x) \geq \min(v_p(a),v_p(b_{i_0})) = v_p(y)$. This proves $y \mid x$.' + proof: 'We need to prove $\lcm_i \gcd(a, b_i) \cong \gcd(a, \lcm_i b_i)$ for finite families. If $x$ denotes the LHS and $y$ denotes the RHS, the relation $x \mid y$ is formal. If $v_p(-) : \IZ \to \IN_{\infty}$ denotes the multiplicity of a prime $p$, then $v_p(x)$ equals $\max_i \min(v_p(a),v_p(b_i))$, and $v_p(y)$ equals $\min(v_p(a), \max_i v_p(b_i))$. Since our family is finite, there is some $i_0$ with $\max_i v_p(b_i) = v_p(b_{i_0})$. Then $v_p(x) \geq \min(v_p(a),v_p(b_{i_0})) = v_p(y)$. This proves $y \mid x$.' - property: locally ℵ₁-presentable proof: Every $\aleph_1$-directed diagram is eventually constant. diff --git a/database/data/categories/sSet.yaml b/database/data/categories/sSet.yaml index 96cf00bf..c2817dfb 100644 --- a/database/data/categories/sSet.yaml +++ b/database/data/categories/sSet.yaml @@ -17,6 +17,11 @@ related: satisfied_properties: - property: locally small proof: This follows from the general fact that $[\C,\D]$ is locally small when $\C$ is small and $\D$ is locally small, here applied to $\C = \Delta^{\op}$ and $\D = \Set$. + dependencies: + - id: Delta + type: category + property: small + satisfied: true - property: Grothendieck topos proof: This is clear from the definitions. diff --git a/database/data/categories/walking_commutative_square.yaml b/database/data/categories/walking_commutative_square.yaml index f2163d5c..2a30ad21 100644 --- a/database/data/categories/walking_commutative_square.yaml +++ b/database/data/categories/walking_commutative_square.yaml @@ -30,9 +30,19 @@ satisfied_properties: - property: locally cartesian closed proof: This is because the walking morphism has this property. + dependencies: + - id: walking_morphism + type: category + property: locally cartesian closed + satisfied: true - property: locally strongly finitely presentable proof: This is because the walking morphism has this property. Alternatively, we may represent this category as the category of algebras for the finitary algebraic theory with two sorts $S_1,S_2$, the equation $x=y$ for $x,y \in S_1$, and the equation $x=y$ for $x,y \in S_2$. + dependencies: + - id: walking_morphism + type: category + property: locally strongly finitely presentable + satisfied: true unsatisfied_properties: - property: semi-strongly connected diff --git a/database/data/categories/walking_coreflexive_pair.yaml b/database/data/categories/walking_coreflexive_pair.yaml index ee084f04..a0695a2d 100644 --- a/database/data/categories/walking_coreflexive_pair.yaml +++ b/database/data/categories/walking_coreflexive_pair.yaml @@ -31,6 +31,11 @@ satisfied_properties: - property: terminal object proof: The object $[0]$ is terminal since it is already terminal in $\Delta$. + dependencies: + - id: Delta + type: category + property: terminal object + satisfied: true - property: generator proof: The object $[0]$ is generator since this is already true in $\Delta$. A direct proof is also possible. @@ -46,9 +51,19 @@ satisfied_properties: - property: coequalizers proof: 'We already know that the $\Delta$ has coequalizers, and the proof has shown that the cardinality does not increase, so we are done. But a direct proof is also possible: There are four non-equal parallel pairs: $(i,j)$, $(ip,jp)$, $(\id,ip)$, and $(\id,jp)$. The first two have the same coequalizer (if it exists) since $p$ is an epimorphism, the last two are symmetric, and we already remarked that $p$ is a coequalizer of $(\id,ip)$. So it suffices to check that $p$ is a coequalizer of $i,j$, which is easy.' + dependencies: + - id: Delta + type: category + property: coequalizers + satisfied: true - property: cosifted proof: Our proof that the $\Delta$ is cosifted has only used $[0],[1]$ as auxiliary objects and therefore also shows that $\Delta^{\leq 1}$ is cosifted. + dependencies: + - id: Delta + type: category + property: cosifted + satisfied: true - property: generalized variety proof: This actually holds for every truncated simplex category $\Delta^{\leq n}$. See MO/510760 for a proof that sifted colimits exist. See MO/510827 for a proof that every object is strongly finitely presentable. diff --git a/database/data/categories/walking_fork.yaml b/database/data/categories/walking_fork.yaml index 628071e5..2232e498 100644 --- a/database/data/categories/walking_fork.yaml +++ b/database/data/categories/walking_fork.yaml @@ -46,6 +46,19 @@ satisfied_properties: - property: locally cartesian closed proof: We need to check that every slice category is cartesian closed. The slice category over $0$ is the trivial category. The slice category over $1$ is the walking morphism. Finally, the slice category over $2$ ist the walking commutative square. All of these are cartesian closed, see their pages for details. + dependencies: + - id: '1' + type: category + property: cartesian closed + satisfied: true + - id: walking_morphism + type: category + property: cartesian closed + satisfied: true + - id: walking_commutative_square + type: category + property: cartesian closed + satisfied: true unsatisfied_properties: - property: strongly connected diff --git a/database/data/categories/walking_span.yaml b/database/data/categories/walking_span.yaml index 3f75f772..49790347 100644 --- a/database/data/categories/walking_span.yaml +++ b/database/data/categories/walking_span.yaml @@ -36,6 +36,15 @@ satisfied_properties: - property: locally cartesian closed proof: The slice category over $0$ is the trivial category, and the slice category over $1$ is the walking morphism, which is cartesian closed. The same holds for $2$ by symmetry. + dependencies: + - id: '1' + type: category + property: cartesian closed + satisfied: true + - id: walking_morphism + type: category + property: cartesian closed + satisfied: true unsatisfied_properties: - property: sifted diff --git a/database/data/categories/walking_splitting.yaml b/database/data/categories/walking_splitting.yaml index e4f76405..f0aa85aa 100644 --- a/database/data/categories/walking_splitting.yaml +++ b/database/data/categories/walking_splitting.yaml @@ -42,6 +42,11 @@ satisfied_properties: - property: preadditive proof: 'We can define $\id_1 + \id_1 \coloneqq ip$ (and it is clear how to add zero morphisms) and then verify that the axioms of a preadditive category hold. Alternatively, it suffices to find a preadditive category which is isomorphic to the walking splitting: Consider the full subcategory of $\Vect_{\IF_2}$ that consists only of the trivial vector space $\{0\}$ and $\IF_2$. Since $\Vect_{\IF_2}$ is preadditive, it is preadditive as well. It has two objects, two identities, the morphisms $i : \{0\} \to \IF_2$, $p : \IF_2 \to \{0\}$, and the zero morphism $ip : \IF_2 \to \IF_2$. Clearly, $pi$ is the identity.' + dependencies: + - id: Vect + type: category + property: preadditive + satisfied: true - property: sifted colimits proof: |- @@ -49,6 +54,11 @@ satisfied_properties: Every element in $X_\infty$ is a finite sum of elements of the form $u_i(x_i)$ with $x_i \in X_i$. Choose an object $k$ with morphisms $i \to k$ for every occurring $i$. If $y_i \in X_k$ denotes the image of $x_i$, we get $\sum_i u_i(x_i) = \sum_i u_k(y_i) = u_k(\sum_i y_i)$. Therefore, every element of $X_\infty$ has the form $u_i(x_i)$ for some $i \in \I$ and $x_i \in X_i$. Moreover, for finitely many elements in $X_\infty$ the index $i$ may be chosen uniformly. Now, if $X_\infty$ has dimension $> d$, it would have linearly independent vectors $v_0,\dotsc,v_d$, all of which have a preimage in $X_i$ for some $i \in \I$. But then these preimages would be linearly independent as well, which contradicts $\dim(X_i) \leq d$. check_redundancy: false + dependencies: + - id: Vect + type: category + property: sifted colimits + satisfied: true - property: generalized variety proof: Again we work with $\Vect^{\leq 1}_{\IF_2}$. We already know that it has sifted colimits and that the embedding to $\Vect_{\IF_2}$ preserves them. The object $0$ is initial and hence strongly finitely presentable. The object $\IF_2$ is strongly finitely presentable in $\Vect^{\leq 1}_{\IF_2}$ since its hom-functor is the composition of the embedding and the forgetful functor $\Vect_{\IF_2} \to \Set$, and the latter preserves sifted colimits by [AR01, Lemma 3.3] applied to $\IF_2 \in \Vect_{\IF_2}$. diff --git a/database/data/functors/abelianization.yaml b/database/data/functors/abelianization.yaml index 2bd13824..f10e15ab 100644 --- a/database/data/functors/abelianization.yaml +++ b/database/data/functors/abelianization.yaml @@ -16,6 +16,11 @@ related: [] satisfied_properties: - property: reflector proof: 'This functor is left adjoint to the forgetful functor $U_{\Ab,\Grp} : \Ab \hookrightarrow \Grp$, which is fully faithful.' + dependencies: + - id: forget_abelian + type: functor + property: fully faithful + satisfied: true - property: preserves finite products proof: See MO/386144. diff --git a/database/data/functors/binary_coproduct_sets.yaml b/database/data/functors/binary_coproduct_sets.yaml index ab981434..619ede0e 100644 --- a/database/data/functors/binary_coproduct_sets.yaml +++ b/database/data/functors/binary_coproduct_sets.yaml @@ -31,6 +31,11 @@ satisfied_properties: - property: cofinitary proof: We already know that $\Set$ has cocartesian cofiltered limits; this is a consequence of this result. + dependencies: + - id: Set + type: category + property: cocartesian cofiltered limits + satisfied: true unsatisfied_properties: - property: preserves terminal objects @@ -44,3 +49,8 @@ unsatisfied_properties: - property: reflector proof: 'Its right adjoint, the diagonal functor $\Delta : \Set \to \Set \times \Set$, is faithful, but not full.' + dependencies: + - id: diagonal_sets + type: functor + property: full + satisfied: false diff --git a/database/data/functors/binary_product_sets.yaml b/database/data/functors/binary_product_sets.yaml index 00ba6d45..b68c0cdf 100644 --- a/database/data/functors/binary_product_sets.yaml +++ b/database/data/functors/binary_product_sets.yaml @@ -44,6 +44,20 @@ unsatisfied_properties: - property: preserves coequalizers proof: 'Since the diagonal functor $\Delta : \Set \to \Set \times \Set$ preserves coequalizers (in fact, all colimits), it would follow that the composition $\Set \to \Set$, $X \mapsto X^2$ preserves coequalizers. But this is the squaring functor, from we already know that it does not preserve coequalizers.' + dependencies: + - id: diagonal_sets + type: functor + property: cocontinuous + satisfied: true + - id: squaring_sets + type: functor + property: preserves coequalizers + satisfied: false - property: coreflector proof: 'Its left adjoint, the diagonal functor $\Delta : \Set \to \Set \times \Set$, is faithful, but not full.' + dependencies: + - id: diagonal_sets + type: functor + property: full + satisfied: false diff --git a/database/data/functors/continuous-functions.yaml b/database/data/functors/continuous-functions.yaml index 20a1942d..ee92be9e 100644 --- a/database/data/functors/continuous-functions.yaml +++ b/database/data/functors/continuous-functions.yaml @@ -15,6 +15,7 @@ related: [] satisfied_properties: - property: continuous proof: 'Since the forgetful functor $U : \CAlg(\IR) \to \Set$ is conservative and continuous, it suffices to prove that $U \circ C : \Top^{\op} \to \Set$ is continuous. But this functor is representable.' + # TODO: add proof dependencies when these functors are added - property: preserves initial objects proof: The initial object in $\Top^{\op}$ is the singleton space, which is mapped to $\IR$, the initial commutative $\IR$-algebra. diff --git a/database/data/functors/forget_abelian.yaml b/database/data/functors/forget_abelian.yaml index ea6c02a8..0bd1edc6 100644 --- a/database/data/functors/forget_abelian.yaml +++ b/database/data/functors/forget_abelian.yaml @@ -30,6 +30,16 @@ satisfied_properties: - property: finitary proof: 'Since the forgetful functor $U_{\Grp} : \Grp \to \Set$ is finitary and conservative, it suffices to prove that the composition $U_{\Grp} \circ U_{\Ab,\Grp} : \Ab \to \Set$ is finitary. This is just the forgetful functor $U_{\Ab} : \Ab \to \Set$ and therefore finitary.' + dependencies: + - id: forget_group + type: functor + property: finitary + satisfied: true + - id: forget_group + type: functor + property: finitary + satisfied: true + # TODO: add dependencies on U_Ab once this functor is added unsatisfied_properties: - property: preserves finite coproducts diff --git a/database/data/functors/forget_addition.yaml b/database/data/functors/forget_addition.yaml index a954e4a8..ea410cf2 100644 --- a/database/data/functors/forget_addition.yaml +++ b/database/data/functors/forget_addition.yaml @@ -20,12 +20,29 @@ satisfied_properties: - property: conservative proof: 'This is because even the composition $U_{\Mon} \circ U_{\Ring,\Mon} : \Ring \to \Set$, namely the forgetful functor $U_{\Ring} : \Ring \to \Set$, is conservative.' + dependencies: + - id: forget_ring + type: functor + property: conservative + satisfied: true - property: finitary proof: 'Since the forgetful functor $U_{\Mon} : \Mon \to \Set$ is finitary and conservative, it suffices to prove that the composition $U_{\Mon} \circ U_{\Ring,\Mon} : \Ring \to \Set$ is finitary. This is just the forgetful functor $U_{\Ring} : \Ring \to \Set$ and is therefore finitary.' + # TODO: add proof dependencies on U_Mon once this functor is added + dependencies: + - id: forget_ring + type: functor + property: finitary + satisfied: true - property: preserves reflexive coequalizers proof: 'Since the forgetful functor $U_{\Mon} : \Mon \to \Set$ preserves reflexive coequalizers (by Theorem 2.5 at the nLab) and is conservative, it suffices to prove that the composition $U_{\Mon} \circ U_{\Ring,\Mon} : \Ring \to \Set$ preserves reflexive coequalizers. This is just the forgetful functor $U_{\Ring} : \Ring \to \Set$ and therefore preserves reflexive coequalizers (by loc.cit.).' + # TODO: add proof dependency on U_Mon once this functor is added + dependencies: + - id: forget_ring + type: functor + property: preserves reflexive coequalizers + satisfied: true unsatisfied_properties: - property: preserves initial objects diff --git a/database/data/functors/forget_group_pointed.yaml b/database/data/functors/forget_group_pointed.yaml index 776ca0eb..106482f9 100644 --- a/database/data/functors/forget_group_pointed.yaml +++ b/database/data/functors/forget_group_pointed.yaml @@ -21,12 +21,28 @@ satisfied_properties: - property: conservative proof: 'We already know that the forgetful functor $U_{\Grp} : \Grp \to \Set$ is conservative.' + dependencies: + - id: forget_group + type: functor + property: conservative + satisfied: true - property: finitary proof: 'Since the forgetful functor $U_{\Set_*} : \Set_* \to \Set$ is finitary and conservative, it suffices to prove that the composition $U_{\Set_*} \circ U_{\Grp,\Set_*} : \Grp \to \Set$ is finitary. This is just the forgetful functor $U_{\Grp} : \Grp \to \Set$ and therefore finitary.' + # TODO: add other proof dependencies when the functor Set_* -> Set is added + dependencies: + - id: forget_group + type: functor + property: finitary + satisfied: true - property: preserves reflexive coequalizers proof: 'It suffices to prove that $U_{\Grp} : \Grp \to \Set$ preserves them, which follows from Theorem 2.5 at the nLab.' + dependencies: + - id: forget_group + type: functor + property: preserves reflexive coequalizers + satisfied: true - property: essentially surjective proof: Let $(X,x_0)$ be a pointed set. If $X$ is finite, we can endow $X$ with a cyclic group structure in which $x_0$ is the identity element. If $X$ is infinite, there is a bijection between $X$ and the set $P_{<\aleph_0}(X)$ of finite subsets of $X$, and we may assume that $x_0$ is mapped to $\varnothing$. Since $P_{<\aleph_0}(X)$ carries a group structure with identity element $\varnothing$ (it is the underlying set of the vector space $\IF_2^{\oplus X}$), $X$ also carries a group structure with identity element $x_0$. diff --git a/database/data/functors/forget_ring.yaml b/database/data/functors/forget_ring.yaml index 36ac9247..12ed2a20 100644 --- a/database/data/functors/forget_ring.yaml +++ b/database/data/functors/forget_ring.yaml @@ -21,9 +21,11 @@ satisfied_properties: proof: This functor is represented by the polynomial ring $\IZ[T]$. - property: monadic + # TODO: add reference (also to similar functors) proof: For every algebraic category the forgetful functor to the category of sets is monadic. - property: finitary + # TODO: add reference (also to similar functors) proof: For every algebraic category the forgetful functor to the category of sets preserves filtered colimits. - property: preserves reflexive coequalizers diff --git a/database/data/functors/group_units.yaml b/database/data/functors/group_units.yaml index ad6f6312..5c187f38 100644 --- a/database/data/functors/group_units.yaml +++ b/database/data/functors/group_units.yaml @@ -18,6 +18,15 @@ satisfied_properties: - property: finitary proof: 'There is a direct way to prove this, but here is an abstract argument: Since the forgetful functor $\Grp \to \Set$ is conservative and finitary, it suffices to prove that the composition $\Mon \to \Set$, which maps a monoid to its set of units, is finitary. This functor is represented by the monoid $\langle x,y : xy = yx = 1 \rangle \cong \IZ$. It has a finite presentation and hence is finitely presentable in the categorical sense (Corollary 3.13 in Adamek-Rosicky).' + dependencies: + - id: forget_group + type: functor + property: conservative + satisfied: true + - id: forget_group + type: functor + property: finitary + satisfied: true - property: preserves coproducts proof: >- diff --git a/database/data/functors/pi_0.yaml b/database/data/functors/pi_0.yaml index 32fa83be..99eb412c 100644 --- a/database/data/functors/pi_0.yaml +++ b/database/data/functors/pi_0.yaml @@ -47,4 +47,4 @@ unsatisfied_properties: proof: 'Consider the spaces $X_n = [n,\infty) \subseteq \IR$ and the inclusion maps $X_{n+1} \hookrightarrow X_n$. Then $\lim_n X_n = \varnothing$ and hence $\pi_0(\lim_n X_n) = \varnothing$. However, each $\pi_0(X_n) = \{X_n\}$ is a singleton, so that also $\lim_n \pi_0(X_n)$ is a singleton.' - property: finitary - proof: 'Let $A_n = \{1/k : k \geq n\}$ for $n \geq 1$. Let $X_n$ be the interval $[0,1]$ equipped with the topology generated by the Euclidean topology and all the singletons $\{a\}$ for $a \in A_n$. The identity maps $X_n \to X_{n+1}$ are continuous since $A_{n+1} \subseteq A_n$, and we have continuous identity maps $X_n \to [0,1]$. Using $\bigcap_{n \geq 1} A_n = \varnothing$, one can show that $\operatorname{colim}_n X_n = [0,1]$ with the Euclidean topology, which is path connected. In particular, $[0]=[1]$ in $\pi_0(\operatorname{colim}_n X_n)$. However, this equation does not hold in $\operatorname{colim}_n \pi_0(X_n)$. Otherwise, there is some $n$ such that it holds in $\pi_0(X_n)$, i.e. there is a path $\gamma : [0,1] \to X_n$ with $\gamma(0)=0$ and $\gamma(1)=1$. By the intermediate value theorem applied to the composition with the map $X_n \to [0,1]$, the element $1/n$ lies in its image. But $\{1/n\}$ is open and closed in $X_n$. Hence, its preimage is $[0,1]$, which means that the path is constant. This is a contradiction.' + proof: 'Let $A_n = \{1/k : k \geq n\}$ for $n \geq 1$. Let $X_n$ be the interval $[0,1]$ equipped with the topology generated by the Euclidean topology and all the singletons $\{a\}$ for $a \in A_n$. The identity maps $X_n \to X_{n+1}$ are continuous since $A_{n+1} \subseteq A_n$, and we have continuous identity maps $X_n \to [0,1]$. Using $\bigcap_{n \geq 1} A_n = \varnothing$, one can show that $\colim_n X_n = [0,1]$ with the Euclidean topology, which is path connected. In particular, $[0]=[1]$ in $\pi_0(\colim_n X_n)$. However, this equation does not hold in $\colim_n \pi_0(X_n)$. Otherwise, there is some $n$ such that it holds in $\pi_0(X_n)$, i.e. there is a path $\gamma : [0,1] \to X_n$ with $\gamma(0)=0$ and $\gamma(1)=1$. By the intermediate value theorem applied to the composition with the map $X_n \to [0,1]$, the element $1/n$ lies in its image. But $\{1/n\}$ is open and closed in $X_n$. Hence, its preimage is $[0,1]$, which means that the path is constant. This is a contradiction.' diff --git a/database/data/functors/trivial_groups.yaml b/database/data/functors/trivial_groups.yaml index b26d6ea2..ba708550 100644 --- a/database/data/functors/trivial_groups.yaml +++ b/database/data/functors/trivial_groups.yaml @@ -16,12 +16,27 @@ related: satisfied_properties: - property: coreflector proof: 'The constant functor $1 \to \Grp$ with value the trivial group is a left adjoint of $! : \Grp \to 1$ and fully faithful; this is because the trivial group is an initial object of $\Grp$.' + dependencies: + - id: Grp + type: category + property: initial object + satisfied: true - property: reflector proof: 'The constant functor $1 \to \Grp$ with value the trivial group is a right adjoint of $! : \Grp \to 1$ and fully faithful; this is because the trivial group is a terminal object of $\Grp$.' + dependencies: + - id: Grp + type: category + property: terminal object + satisfied: true - property: full proof: This follows easily from the fact that $\Grp$ is strongly connected. + dependencies: + - id: Grp + type: category + property: strongly connected + satisfied: true unsatisfied_properties: - property: essentially injective diff --git a/database/data/functors/trivial_sets.yaml b/database/data/functors/trivial_sets.yaml index adedbc55..c362e4ef 100644 --- a/database/data/functors/trivial_sets.yaml +++ b/database/data/functors/trivial_sets.yaml @@ -16,9 +16,19 @@ related: satisfied_properties: - property: coreflector proof: 'The constant functor $1 \to \Set$ with value $\varnothing$ is a left adjoint of $! : \Set \to 1$ and fully faithful; this is because $\varnothing$ is an initial object of $\Set$.' + dependencies: + - id: Set + type: category + property: initial object + satisfied: true - property: reflector proof: 'The constant functor $1 \to \Set$ with value $\{\ast\}$ is a right adjoint of $! : \Set \to 1$ and fully faithful; this is because $\{\ast\}$ is a terminal object of $\Set$.' + dependencies: + - id: Set + type: category + property: terminal object + satisfied: true unsatisfied_properties: - property: faithful diff --git a/database/data/morphisms/baer-specker-relations.yaml b/database/data/morphisms/baer-specker-relations.yaml index 557e207d..16fdfc7b 100644 --- a/database/data/morphisms/baer-specker-relations.yaml +++ b/database/data/morphisms/baer-specker-relations.yaml @@ -16,4 +16,5 @@ satisfied_properties: unsatisfied_properties: - property: regular monomorphism + # TODO: check this via a new feature in proof dependencies proof: 'We know that a monomorphism $f : A \to B$ in $\FreeAb$ is regular if and only if the quotient (taken in $\Ab$) $B/f(A)$ is free abelian. But $F/K \cong \IZ^\IN$ is the Baer-Specker group, which is not free abelian.' diff --git a/database/data/morphisms/multiply-2.yaml b/database/data/morphisms/multiply-2.yaml index a38b08e4..27775903 100644 --- a/database/data/morphisms/multiply-2.yaml +++ b/database/data/morphisms/multiply-2.yaml @@ -15,6 +15,7 @@ satisfied_properties: proof: The map is clearly injective. - property: epimorphism + # TODO: check this via a new feature in proof dependencies proof: 'We know that a homomorphism $f : A \to B$ in $\TorsFreeAb$ is an epimorphism if and only if $B/f(A)$ is torsion. Since $\IZ/2$ is torsion, the claim follows.' unsatisfied_properties: diff --git a/database/schema/002_properties.sql b/database/schema/002_properties.sql index fab1a896..be4d7908 100644 --- a/database/schema/002_properties.sql +++ b/database/schema/002_properties.sql @@ -55,6 +55,21 @@ CREATE TABLE property_assignments ( CREATE INDEX idx_property_assigned ON property_assignments (property_id); +CREATE TABLE required_property_assignments ( + id INTEGER PRIMARY KEY, + required_for TEXT NOT NULL, + structure_id TEXT NOT NULL, + property_id TEXT NOT NULL, + type TEXT NOT NULL, + is_satisfied INTEGER NOT NULL CHECK (is_satisfied in (TRUE, FALSE)), + with_proof INTEGER CHECK (with_proof in (TRUE, FALSE)), + FOREIGN KEY (required_for) REFERENCES structures (id) ON DELETE CASCADE, + FOREIGN KEY (structure_id, type) + REFERENCES structures (id, type) ON DELETE CASCADE, + FOREIGN KEY (property_id, type) + REFERENCES properties (id, type) ON DELETE CASCADE +); + CREATE TABLE property_tags ( id INTEGER PRIMARY KEY, tag TEXT NOT NULL, diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index b305bee3..2d0b1014 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -82,6 +82,7 @@ function clear_all_tables() { db.prepare(`DELETE FROM implications`).run() db.prepare(`DELETE FROM property_assignments`).run() + db.prepare(`DELETE FROM required_property_assignments`).run() db.prepare(`DELETE FROM related_properties`).run() db.prepare(`DELETE FROM property_tag_assignments`).run() db.prepare(`DELETE FROM property_tags`).run() @@ -225,6 +226,13 @@ function seed_structures({ ) VALUES (?, ?, ?, ?, ?, ?)` ) + const required_property_assignment_insert = db.prepare( + `INSERT INTO required_property_assignments ( + required_for, structure_id, property_id, + type, is_satisfied, with_proof + ) VALUES (?, ?, ?, ?, ?, ?)` + ) + function insert_property_assignments( structure_id: string, entries: PropertyEntry[], @@ -239,6 +247,17 @@ function seed_structures({ entry.proof, entry.check_redundancy === false ? 0 : 1 ) + + for (const dep of entry.dependencies ?? []) { + required_property_assignment_insert.run( + structure_id, + dep.id, + dep.property, + dep.type, + Number(dep.satisfied), + dep.with_proof !== undefined ? Number(dep.with_proof) : null + ) + } } } diff --git a/database/scripts/test.ts b/database/scripts/test.ts index 9708df81..3444951a 100644 --- a/database/scripts/test.ts +++ b/database/scripts/test.ts @@ -57,6 +57,9 @@ function execute_tests() { test_positivity('id_G', 'morphism') test_decided_structures(decided_morphisms, 'morphism') + + devlog('\n--- Test proof dependencies ---') + test_proof_dependencies() } catch (err) { if (err instanceof Error) { console.error(err.message) @@ -288,3 +291,56 @@ function check_link_targets_exist() { devlog(`✅ Link targets exist`) } + +/** + * Tests if the dependencies in the proofs of properties are actually true. + */ +function test_proof_dependencies() { + const count = db + .prepare<[], number>(`SELECT COUNT(*) FROM required_property_assignments`) + .pluck() + .get() + + const rows = db + .prepare< + [], + { + required_for: string + structure_id: string + property_id: string + is_satisfied: number + with_proof: number | null + } + >( + `SELECT + r.required_for, + r.structure_id, + r.property_id, + r.is_satisfied, + r.with_proof + FROM required_property_assignments r + WHERE NOT EXISTS ( + SELECT 1 FROM property_assignments a + WHERE a.structure_id = r.structure_id + AND a.property_id = r.property_id + AND a.type = r.type + AND a.is_satisfied = r.is_satisfied + AND (r.with_proof IS NULL OR r.with_proof != a.is_deduced) + )` + ) + .all() + + if (!rows.length) { + devlog(`✅ ${count} Proof dependencies are validated`) + return + } + + for (const row of rows) { + const { required_for, structure_id, property_id, is_satisfied, with_proof } = row + console.error( + `❌ ${required_for} expects ${structure_id} to ${is_satisfied === 1 ? '' : 'not '}have property "${property_id}" ${with_proof === 1 ? '(with proof)' : ''}, which could not be deduced` + ) + } + + throw new Error(`Found ${rows.length} invalid proof dependencies`) +} diff --git a/database/scripts/utils/seed.types.ts b/database/scripts/utils/seed.types.ts index fe33f69b..73be70f2 100644 --- a/database/scripts/utils/seed.types.ts +++ b/database/scripts/utils/seed.types.ts @@ -32,6 +32,13 @@ export type PropertyEntry = { property: string proof: string check_redundancy?: boolean + dependencies?: { + id: string + type: string + property: string + satisfied: boolean + with_proof?: boolean + }[] } type ObjectEntry = {