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..09a124b8 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_fg + type: category + property: essentially small + 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..ac669297 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,19 @@ 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 - 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 @@ -39,6 +54,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 +71,23 @@ 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 - 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). + dependencies: + - id: CRing + type: category + property: regular quotient object classifier + satisfied: false + - id: CAlg(R) + type: category + property: regular quotient object classifier + satisfied: false - property: cocartesian cofiltered limits proof: >- @@ -62,10 +96,20 @@ 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 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..a170e81e 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,11 @@ 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 - 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..c3a27a50 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,19 @@ 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: One can use the same proof as for $\CRing$. + dependencies: + - id: CRing + type: category + property: coextensive + satisfied: true unsatisfied_properties: - property: skeletal @@ -55,6 +70,11 @@ 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 - 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/schema/002_properties.sql b/database/schema/002_properties.sql index fab1a896..6615030f 100644 --- a/database/schema/002_properties.sql +++ b/database/schema/002_properties.sql @@ -55,6 +55,20 @@ 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 CHECK (is_satisfied 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..88680f6d 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,12 @@ 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 + ) VALUES (?, ?, ?, ?, ?)` + ) + function insert_property_assignments( structure_id: string, entries: PropertyEntry[], @@ -239,6 +246,16 @@ 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) + ) + } } } diff --git a/database/scripts/test.ts b/database/scripts/test.ts index 9708df81..e29e972a 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,52 @@ 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 + } + >( + `SELECT + r.required_for, + r.structure_id, + r.property_id, + r.is_satisfied + 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 + )` + ) + .all() + + if (!rows.length) { + devlog(`✅ ${count} Proof dependencies are validated`) + return + } + + for (const { required_for, structure_id, property_id, is_satisfied } of rows) { + console.error( + `❌ ${required_for} expects ${structure_id} to ${is_satisfied === 1 ? '' : 'not '}have property "${property_id}", 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..777d49aa 100644 --- a/database/scripts/utils/seed.types.ts +++ b/database/scripts/utils/seed.types.ts @@ -32,6 +32,12 @@ export type PropertyEntry = { property: string proof: string check_redundancy?: boolean + dependencies?: { + id: string + type: string + property: string + satisfied: boolean + }[] } type ObjectEntry = {