diff --git a/database/data/categories/Ab.yaml b/database/data/categories/Ab.yaml index 6ce6a016..95490952 100644 --- a/database/data/categories/Ab.yaml +++ b/database/data/categories/Ab.yaml @@ -3,8 +3,9 @@ name: category of abelian groups notation: $\Ab$ objects: abelian groups morphisms: group homomorphisms -description: This is the prototype of an abelian category. +description: This category is the prototype of an abelian category. It is the special case of $R{-}\Mod$ where $R = \IZ$. nlab_link: https://ncatlab.org/nlab/show/Ab +parent: R-Mod_non_ss tags: - algebra @@ -15,31 +16,15 @@ related: - FinAb - FreeAb - Grp - - R-Mod - TorsAb - TorsFreeAb -satisfied_properties: - - property: locally small - proof: There is a forgetful functor $\Ab \to \Set$ and $\Set$ is locally small. - - - property: abelian - proof: This is standard, see Mac Lane, Ch. VIII. - label: ab_abelian - - - property: finitary algebraic - proof: Take the algebraic theory of a commutative group. +satisfied_properties: [] unsatisfied_properties: - - property: skeletal - proof: This is trivial. - - property: split abelian proof: The short exact sequence $0 \xrightarrow{} \IZ \xrightarrow{p} \IZ \xrightarrow{} \IZ/p \xrightarrow{} 0$ does not split. - - property: CSP - proof: The canonical homomorphism $\bigoplus_{n \geq 0} \IZ \to \prod_{n \geq 0} \IZ$ is not surjective, hence no epimorphism. - special_objects: initial object: description: trivial group @@ -53,4 +38,4 @@ special_objects: special_morphisms: epimorphisms: description: surjective morphisms - proof: 'For the non-trivial direction, if $f : A \to B$ is an epimorphism, then $p \circ f = 0$ for the projection $p : B \to B/f(A)$ implies that $p = 0$, so that $B = f(A)$.' + proof: 'For the non-trivial direction, if $f : A \to B$ is an epimorphism, then $p \circ f = 0$ for the projection $p : B \to B/f(A)$ implies that $p = 0$, so that $B = f(A)$.' diff --git a/database/data/categories/Ab_fg.yaml b/database/data/categories/Ab_fg.yaml index 41588e5b..daa552fa 100644 --- a/database/data/categories/Ab_fg.yaml +++ b/database/data/categories/Ab_fg.yaml @@ -3,7 +3,7 @@ name: category of finitely generated abelian groups notation: $\Ab_{\fg}$ objects: finitely generated abelian groups morphisms: group homomorphisms -description: null +description: This is the full subcategory of $\Ab$ that consists of the finitely generated abelian groups. nlab_link: https://ncatlab.org/nlab/show/finitely+generated+module tags: diff --git a/database/data/categories/Alg(R).yaml b/database/data/categories/Alg(R).yaml index 41b81a5d..ab5ecf39 100644 --- a/database/data/categories/Alg(R).yaml +++ b/database/data/categories/Alg(R).yaml @@ -3,7 +3,7 @@ name: category of algebras notation: $\Alg(R)$ objects: algebras over a commutative ring $R \neq 0$ morphisms: maps preserving the ring and module structure -description: This is a generalization of the category of rings, which we get for $R = \IZ$. We assume our rings (and algebras) to be unital. For $R = 0$ we would get the trivial category, which is why we exclude this here. +description: This category is a generalization of the category of rings, which we get for $R = \IZ$. We assume our rings (and algebras) to be unital. For $R = 0$ we would get the trivial category, which is why we exclude this here. nlab_link: https://ncatlab.org/nlab/show/Alg tags: @@ -12,7 +12,6 @@ tags: related: - CAlg(R) - R-Mod - - Ring satisfied_properties: - property: locally small @@ -25,9 +24,7 @@ satisfied_properties: proof: 'If $f : 0 \to A$ is an algebra homomorphism, then $A$ satisfies $1=f(1)=f(0)=0$, so that $A=0$.' - property: disjoint finite products - proof: One can take the same proof as for $\Ring$. - references: - - ring_disjoint_finite_products + proof: 'Let $A,B$ be two $R$-algebras. To show that $A \sqcup_{A \times B} B$ is trivial, let $T$ be an $R$-algebra which admits homomorphisms $f : A \to T$, $g : B \to T$ 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=1$, $b=0$ yields $1=0$ in $T$. Hence, $T = 0$.' - 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. @@ -54,9 +51,8 @@ unsatisfied_properties: proof: 'See MO/509552: Consider the forgetful functor $U : \Alg(R) \to \Set$ and the relation $S \subseteq U^2$ defined by $S(A) \coloneqq \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $R[X]$ and $S$ by $R \langle X,Y \rangle / \langle XY-X^2 \rangle$. It is clear that $S$ is reflexive, but not symmetric.' - 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.' - references: - - ring_not_coregular + proof: '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.' + label: alg_not_coregular - property: regular quotient object classifier 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). @@ -65,7 +61,7 @@ unsatisfied_properties: - property: cocartesian cofiltered limits proof: >- - Consider the ring $A = R[X]$ and the sequence of rings $B_n = R[Y]/(Y^{n+1})$ with projections $B_{n+1} \to B_n$, whose limit is $R[[Y]]$. Every element in the coproduct of rings $R[X] \sqcup R[[Y]]$ has a finite "free product" length. Now consider the elements + Consider the algebra $A = R[X]$ and the sequence of algebras $B_n = R[Y]/(Y^{n+1})$ with projections $B_{n+1} \to B_n$, whose limit is $R[[Y]]$. Every element in the coproduct of algebras $R[X] \sqcup R[[Y]]$ has a finite "free product" length. Now consider the elements $$w_n = (1 + XY) (1+XY^2) \cdots (1+X Y^n) \in A \sqcup B_n.$$ 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. @@ -73,15 +69,13 @@ unsatisfied_properties: 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. - 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)$.' - references: - - ring_no_effective_cocongruences + proof: 'MO/510744 presents a counterexample for $\Ring$, and it can be easily generalized to $\Alg(R)$: 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)$.' special_objects: initial object: description: $R$ terminal object: - description: trivial algebra + description: zero algebra coproducts: description: see MSE/625874 products: diff --git a/database/data/categories/BG.yaml b/database/data/categories/BG.yaml new file mode 100644 index 00000000..e1ecdf50 --- /dev/null +++ b/database/data/categories/BG.yaml @@ -0,0 +1,51 @@ +id: BG +name: delooping of a group +notation: $BG$ +objects: a single object $*$ +morphisms: the elements of $G$ +description: Every group $G$ yields a groupoid $BG$ with a single object $*$, morphisms given by the elements of $G$, and composition given by the group operation. We assume that $G$ is non-trivial, since otherwise we get the trivial category. +nlab_link: https://ncatlab.org/nlab/show/delooping#delooping_of_a_group_to_a_groupoid + +tags: + - algebra + - category theory + +related: + - BN + +satisfied_properties: + - property: small + proof: This is trivial. + + - property: groupoid + proof: This is trivial. + + - property: core-connected + proof: The category has exactly one object. + + - property: skeletal + proof: The category has exactly one object. + +unsatisfied_properties: + - property: thin + proof: This is because $G$ is not trivial, so there are at least two morphisms $* \rightrightarrows *$. + +undecidable_properties: + - property: essentially countable + proof: This holds if and only if $G$ is countable. + + - property: countable + proof: This holds if and only if $G$ is countable. + + - property: finite + proof: This holds if and only if $G$ is finite. + + - property: locally finite + proof: This holds if and only if $G$ is finite. + + - property: essentially finite + proof: This holds if and only if $G$ is finite. + +special_objects: {} + +special_morphisms: {} diff --git a/database/data/categories/BG_c.yaml b/database/data/categories/BG_c.yaml index a5b31312..5192d70e 100644 --- a/database/data/categories/BG_c.yaml +++ b/database/data/categories/BG_c.yaml @@ -1,39 +1,26 @@ id: BG_c name: delooping of an infinite countable group notation: $BG$ -objects: a single object +objects: a single object $*$ morphisms: the elements of an infinite countable group $G$ -description: Every group $G$ yields a groupoid $BG$ with a single object $*$, morphisms given by the elements of $G$, and composition given by the group operation. In this example, we consider the case of an infinite countable group $G$ (such as $G = \IZ$). -nlab_link: https://ncatlab.org/nlab/show/delooping +description: This is the special case of $BG$ where $G$ is an infinite countable group $G$ (such as $G = \IZ$). +nlab_link: https://ncatlab.org/nlab/show/delooping#delooping_of_a_group_to_a_groupoid +parent: BG tags: - algebra - category theory related: - - BG_f - - BG_u - BN satisfied_properties: - - property: small - proof: This is trivial. - - - property: groupoid - proof: This is trivial. - - - property: core-connected - proof: The category has exactly one object. - - - property: skeletal - proof: The category has exactly one object. - - property: countable - proof: This is because $G$ is countable. + proof: This is because $G$ is countable by assumption. unsatisfied_properties: - property: locally finite - proof: This is because we choose $G$ to be infinite. + proof: This is because $G$ is infinite by assumption. special_objects: {} diff --git a/database/data/categories/BG_f.yaml b/database/data/categories/BG_f.yaml index 5bf6633e..5a1ca411 100644 --- a/database/data/categories/BG_f.yaml +++ b/database/data/categories/BG_f.yaml @@ -1,39 +1,24 @@ id: BG_f name: delooping of a non-trivial finite group notation: $BG$ -objects: a single object +objects: a single object $*$ morphisms: the elements of a non-trivial finite group $G$ -description: Every group $G$ yields a groupoid $BG$ with a single object $*$, morphisms given by the elements of $G$, and composition given by the group operation. In this example, we consider the case of a non-trivial finite group $G$ (such as $G = C_2$). -nlab_link: https://ncatlab.org/nlab/show/delooping +description: This is the special case of $BG$ where $G$ is a non-trivial finite group $G$ (such as $G = C_2$). +nlab_link: https://ncatlab.org/nlab/show/delooping#delooping_of_a_group_to_a_groupoid +parent: BG tags: - algebra - category theory related: - - BG_c - - BG_u - BN satisfied_properties: - property: finite - proof: This is trivial. + proof: This is because $G$ is finite by assumption. - - property: small - proof: This is trivial. - - - property: groupoid - proof: This is trivial. - - - property: core-connected - proof: The category has exactly one object. - - - property: skeletal - proof: The category has exactly one object. - -unsatisfied_properties: - - property: trivial - proof: This is trivial. +unsatisfied_properties: [] special_objects: {} diff --git a/database/data/categories/BG_u.yaml b/database/data/categories/BG_u.yaml index b90f5df5..a8c4ff7b 100644 --- a/database/data/categories/BG_u.yaml +++ b/database/data/categories/BG_u.yaml @@ -1,39 +1,27 @@ id: BG_u name: delooping of an infinite uncountable group notation: $BG$ -objects: a single object +objects: a single object $*$ morphisms: the elements of an infinite uncountable group $G$ -description: Every group $G$ yields a groupoid $BG$ with a single object $*$, morphisms given by the elements of $G$, and composition given by the group operation. In this example, we consider the case of an uncountable group $G$ (such as $G = \IR$). -nlab_link: https://ncatlab.org/nlab/show/delooping +description: This is the special case of $BG$ where $G$ is an infinite uncountable group $G$ (such as $G = \IR$). +nlab_link: https://ncatlab.org/nlab/show/delooping#delooping_of_a_group_to_a_groupoid +parent: BG tags: - algebra - category theory related: - - BG_f - - BG_c - BN -satisfied_properties: - - property: small - proof: This is trivial. - - - property: groupoid - proof: This is trivial. - - - property: core-connected - proof: The category has exactly one object. - - - property: skeletal - proof: The category has exactly one object. +satisfied_properties: [] unsatisfied_properties: - property: locally finite - proof: This is because we choose $G$ to be infinite. + proof: This is because $G$ is infinite by assumption. - property: essentially countable - proof: This is because we choose $G$ to be uncountable. + proof: This is because $G$ is uncountable by assumption. special_objects: {} diff --git a/database/data/categories/CAlg(R).yaml b/database/data/categories/CAlg(R).yaml index 9a4d1984..d9eecee9 100644 --- a/database/data/categories/CAlg(R).yaml +++ b/database/data/categories/CAlg(R).yaml @@ -3,7 +3,7 @@ name: category of commutative algebras notation: $\CAlg(R)$ objects: commutative algebras over a commutative ring $R \neq 0$ morphisms: maps preserving the ring and module structure -description: This is a generalization of the category of commutative rings, which we get for $R = \IZ$. In general, $\CAlg(R) \cong R \,/\, \CRing$. We assume our rings (and algebras) to be unital. For $R = 0$ we would get the trivial category, which is why we exclude this here. +description: This category is a generalization of the category of commutative rings, which we get for $R = \IZ$. In general, $\CAlg(R) \cong R \,/\, \CRing$. We assume our rings (and algebras) to be unital. For $R = 0$ we would get the trivial category, which is why we exclude this here. nlab_link: https://ncatlab.org/nlab/show/CommAlg tags: @@ -11,7 +11,6 @@ tags: related: - Alg(R) - - CRing - R-Mod satisfied_properties: @@ -19,10 +18,10 @@ satisfied_properties: proof: There is a forgetful functor $\CAlg(R) \to \Set$ and $\Set$ is locally small. - property: finitary algebraic - proof: Take the algebraic theory of a commutative ring. + proof: Take the algebraic theory of a commutative algebra. - property: strict terminal object - proof: 'If $f : 0 \to R$ is a homomorphism, then $R$ satisfies $1=f(1)=f(0)=0$, so that $R=0$.' + proof: 'If $f : 0 \to A$ is a homomorphism of $R$-algebras, then $A$ satisfies $1=f(1)=f(0)=0$, so that $A=0$.' check_redundancy: false - property: Malcev @@ -31,9 +30,23 @@ satisfied_properties: - grp_malcev - property: coextensive - proof: One can use the same proof as for $\CRing$. - references: - - cring_coextensive + proof: >- + We already know that $\CAlg(R)$ has products and pushouts, since it is finitary algebraic. Concretely, the pushout of a span $A \leftarrow S \rightarrow B$ can be constructed as the tensor product $A \otimes_S B$ with the obvious multiplication. Finite products are disjoint because the projection $p_1 : A \times B \to A$ is clearly surjective, hence an epimorphism, and the tensor product $A \otimes_{p_1,A \times B,p_2} B = 0$ is the zero ring (the terminal object), since + $$a \otimes b = a \cdot p_1(1,0) \otimes b = a \otimes p_2(1,0) \cdot b = a \otimes 0 = 0.$$ + It remains to check that finite products are stable under pushouts. Let + $$f : A \times B \to T$$ + be an algebra homomorphism, and consider the pushouts + $$\begin{align*} + T_A & := A \otimes_{p_1,A \times B,f} T \\ + T_B & := B \otimes_{p_2,A \times B,f} T. + \end{align*}$$ + We need to prove that the canonical homomorphism + $$T \to T_A \times T_B$$ + is an isomorphism. Since $p_1 : A \times B \to A$ is surjective with kernel $0 \times B = \langle (0,1) \rangle$, we have $T_A = T/\langle f(1,0)\rangle$, and likewise, $T_B = T/\langle f(0,1) \rangle$. The elements $f(1,0)$ and $f(0,1)$ are orthogonal idempotents in $T$. Therefore, the claim follows from the well-known result in commutative algebra that if $A$ is a commutative algebra and $e \in A$ is an idempotent, then the canonical homomorphism + $$A \to A/\langle e \rangle \times A/\langle 1-e \rangle$$ + is an isomorphism. One can also deduce this from the Chinese Remainder Theorem. + + An alternative proof, which we only sketch, uses the category of locally ringed spaces $\LRS_R$ over $R$, which is infinitary extensive. It follows that the category of affine $R$-schemes is extensive by Lemma 11 here, and this category is anti-equivalent to $\CAlg(R)$. This argument is not circular since our proof of extensivity of $\LRS_R$ does not use coextensivity of $\CAlg(R)$. unsatisfied_properties: - property: skeletal @@ -58,13 +71,18 @@ unsatisfied_properties: proof: 'See MO/509552: Consider the forgetful functor $U : \CAlg(R) \to \Set$ and the relation $S \subseteq U^2$ defined by $S(A) \coloneqq \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $R[X]$ and $S$ by $R[X,Y] / \langle XY-X^2 \rangle$. It is clear that $S$ is reflexive, but not symmetric.' - 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.' + proof: '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.' label: calg_no_regular_quotient_object_classifier - references: - - cring_no_regular_quotient_object_classifier - 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. + proof: >- + Let $K$ be a field over $R$. Consider the epimorphism of sequences + $$\begin{CD} + \cdots @>>> K[X] @>>> K[X] @>>> K[X] \\ + @. @VVV @VVV @VVV \\ + \cdots @>>> K[X]/\langle X^3 \rangle @>>> K[X]/\langle X^2 \rangle @>>> K[X]/\langle X \rangle + \end{CD}$$ + In the limit, it induces the inclusion $K[X] \hookrightarrow K[[X]]$, where $K[[X]]$ is the algebra of formal power series over $K$. 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. special_objects: initial object: diff --git a/database/data/categories/CMon.yaml b/database/data/categories/CMon.yaml index 5a861ffb..bd4a9a07 100644 --- a/database/data/categories/CMon.yaml +++ b/database/data/categories/CMon.yaml @@ -3,7 +3,7 @@ name: category of commutative monoids notation: $\CMon$ objects: commutative monoids morphisms: monoid homomorphisms -description: null +description: This is the full subcategory of $\Mon$ that consists of commutative monoids. It is a typical example of a finitary algebraic category and the "non-additive version" of $\CRing$. nlab_link: https://ncatlab.org/nlab/show/category+of+monoids tags: diff --git a/database/data/categories/CRing.yaml b/database/data/categories/CRing.yaml index dc2f9b31..78c1ae79 100644 --- a/database/data/categories/CRing.yaml +++ b/database/data/categories/CRing.yaml @@ -3,82 +3,33 @@ name: category of commutative rings notation: $\CRing$ objects: commutative rings morphisms: ring homomorphisms -description: null +description: This category is the special case of $\CAlg(R)$ where $R = \IZ$. nlab_link: https://ncatlab.org/nlab/show/CRing +parent: CAlg(R) tags: - algebra related: - - CAlg(R) - Ring - Rng + - CMon comments: - Regular monomorphisms are discussed in MSE/695685, but probably they cannot be classified. -satisfied_properties: - - property: locally small - proof: There is a forgetful functor $\CRing \to \Set$ and $\Set$ is locally small. - - - property: finitary algebraic - proof: Take the algebraic theory of a commutative ring. - - - property: strict terminal object - proof: 'If $f : 0 \to R$ is a homomorphism, then $R$ satisfies $1=f(1)=f(0)=0$, so that $R=0$.' - check_redundancy: false - - - 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. - references: - - grp_malcev - - - property: coextensive - proof: >- - We already know that $\CRing$ has products and pushouts, since it is finitary algebraic. Concretely, the pushout of a span $A \leftarrow R \rightarrow B$ can be constructed as the tensor product $A \otimes_R B$ with the obvious multiplication. Finite products are disjoint because the projection $p_1 : A \times B \to A$ is clearly surjective, hence an epimorphism, and the tensor product $A \otimes_{p_1,A \times B,p_2} B = 0$ is the zero ring (the terminal object), since - $$a \otimes b = a \cdot p_1(1,0) \otimes b = a \otimes p_2(1,0) \cdot b = a \otimes 0 = 0.$$ - It remains to check that finite products are stable under pushouts. Let - $$f : A \times B \to T$$ - be a ring homomorphism, and consider the pushouts - $$\begin{align*} - T_A & := A \otimes_{p_1,A \times B,f} T \\ - T_B & := B \otimes_{p_2,A \times B,f} T. - \end{align*}$$ - We need to prove that the canonical homomorphism - $$T \to T_A \times T_B$$ - is an isomorphism. Since $p_1 : A \times B \to A$ is surjective with kernel $0 \times B = \langle (0,1) \rangle$, we have $T_A = T/\langle f(1,0)\rangle$, and likewise, $T_B = T/\langle f(0,1) \rangle$. The elements $f(1,0)$ and $f(0,1)$ are orthogonal idempotents in $T$. Therefore, the claim follows from the well-known result in commutative algebra that if $R$ is a commutative ring and $e \in R$ is an idempotent, then $R \to R/\langle e \rangle \times R/\langle 1-e \rangle$ is an isomorphism. One can also deduce this from the Chinese Remainder Theorem. - - An alternative proof, which we only sketch, uses the category of locally ringed spaces $\LRS$, which is infinitary extensive. It follows that the category of affine schemes is extensive by Lemma 11 here, and this category is anti-equivalent to $\CRing$. This argument is not circular since our proof of extensivity of $\LRS$ does not use coextensivity of $\CRing$. - label: cring_coextensive +satisfied_properties: [] unsatisfied_properties: - - property: skeletal - proof: This is trivial. - - property: semi-strongly connected + # This can be deduced from the parent CAlg(R), but we keep it because + # the proof for general R is more complicated. proof: There is no homomorphism between $\IF_2$ and $\IF_3$. label: cring_no_semi_strongly_connected - - property: balanced - proof: The inclusion $\IZ \hookrightarrow \IQ$ is a counterexample. - - - property: cogenerating set - proof: 'We apply this lemma to the collection of fields: If $F$ is a field and $R$ is a non-trivial commutative 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).' - - - property: countably codistributive - proof: 'The canonical homomorphism $\IQ \otimes \IZ^{\IN} \to (\IQ \otimes \IZ)^{\IN} = \IQ^{\IN}$ is not an isomorphism: its image consists of those sequences of rational numbers whose denominators can be bounded.' - - - property: coregular - proof: See MSE/3745302. - - - property: co-Malcev - proof: 'See MO/509552: Consider the forgetful functor $U : \CRing \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) \coloneqq \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $\IZ[X]$ and $R$ by $\IZ[X,Y] / \langle XY-X^2 \rangle$. It is clear that $R$ is reflexive, but not symmetric.' - - - property: regular quotient object classifier - proof: 'Assume that $P \to \IZ$ is a regular quotient object classifier. If $J$ denotes its kernel, this means that every ideal $I \subseteq A$ of any commutative ring 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 ring of $\sigma$. But then $I$ is generated by elements in the fixed ring. This fails for $A = \IZ[X]$, $I = \langle X \rangle$, $\sigma(X)=-X$. The fixed ring is $\IZ[X^2]$, and if $I$ was generated by elements $f \in \IZ[X^2] \cap I$, they would be multiples of $X^2$, but $X$ is not a multiple of $X^2$.' - label: cring_no_regular_quotient_object_classifier - - property: cofiltered-limit-stable epimorphisms + # This can be deduced from the parent CAlg(R), but the proof for CRing is + # instructive, so we keep it. proof: 'For a prime $p$ consider the sequence of projections $\cdots \to \IZ/p^2 \to \IZ/p$ and the constant sequence $\cdots \to \IZ \to \IZ$. The surjective homomorphisms $\IZ \to \IZ/p^n$ induce the homomorphism $\IZ \to \IZ_p$ in the limit, where $\IZ_p$ is the ring of $p$-adic integers. It is not surjective since $\IZ_p$ is uncountable, but this is not sufficient (at least, for this category): We need to use SP/04W0 to conclude that it is no epimorphism in $\CRing$.' special_objects: diff --git a/database/data/categories/FinAb.yaml b/database/data/categories/FinAb.yaml index 98ca4405..f3185a07 100644 --- a/database/data/categories/FinAb.yaml +++ b/database/data/categories/FinAb.yaml @@ -3,7 +3,7 @@ name: category of finite abelian groups notation: $\FinAb$ objects: finite abelian groups morphisms: group homomorphisms -description: null +description: This is the full subcategory of $\Ab$ that consists of the finite abelian groups. nlab_link: https://ncatlab.org/nlab/show/finite+abelian+group tags: diff --git a/database/data/categories/FinGrp.yaml b/database/data/categories/FinGrp.yaml index 2e3b8fa8..b1c0d7aa 100644 --- a/database/data/categories/FinGrp.yaml +++ b/database/data/categories/FinGrp.yaml @@ -3,7 +3,7 @@ name: category of finite groups notation: $\FinGrp$ objects: finite groups morphisms: group homomorphisms -description: null +description: This is the full subcategory of $\Grp$ that consists of the finite groups. nlab_link: https://ncatlab.org/nlab/show/finite+group tags: diff --git a/database/data/categories/FinSet.yaml b/database/data/categories/FinSet.yaml index a981bf27..3b723fef 100644 --- a/database/data/categories/FinSet.yaml +++ b/database/data/categories/FinSet.yaml @@ -3,7 +3,7 @@ name: category of finite sets notation: $\FinSet$ objects: finite sets morphisms: maps -description: null +description: This is the full subcategory of $\Set$ that consists of the finite sets. nlab_link: https://ncatlab.org/nlab/show/FinSet tags: diff --git a/database/data/categories/FinVect.yaml b/database/data/categories/FinVect.yaml new file mode 100644 index 00000000..dcf12144 --- /dev/null +++ b/database/data/categories/FinVect.yaml @@ -0,0 +1,76 @@ +id: FinVect +name: category of finite-dimensional vector spaces +notation: $\FinVect_K$ +objects: finite-dimensional vector spaces over a field $K$ +morphisms: linear maps +description: This is the full subcategory of $\Vect_K$ consisting of finite-dimensional vector spaces. Every object is isomorphic to $K^n$ for a unique $n \in \IN$. +nlab_link: https://ncatlab.org/nlab/show/FinDimVect + +tags: + - algebra + +related: + - Vect + - Ab_fg + +satisfied_properties: + - property: locally small + proof: There is a forgetful functor $\FinVect_K \to \Vect_K$, and $\Vect_K$ is locally small. + + - 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. + + - property: extremal generator + proof: The one-dimensional vector space $K$ is an extremal generator even in $\Vect_K$. Now apply Lemma 10 here. + references: + - vect_extremal_generator + + - property: split abelian + proof: This follows directly from the corresponding fact for $\Vect_K$. + + - 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. + + - property: ℵ₁-accessible + proof: 'The inclusion $\FinVect_K \hookrightarrow \Vect_K$ is closed under $\aleph_1$-filtered colimits by MO/400763. In particular, $\FinVect_K$ has $\aleph_1$-filtered colimits. Moreover, every object in $\FinVect_K$ is $\aleph_1$-presentable: it is isomorphic to some $K^n$, which is finitely presentable in $\Vect_K$, hence $\aleph_1$-presentable in $\Vect_K$, and therefore also $\aleph_1$-presentable in $\FinVect_K$.' + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: small + proof: This is trivial. + + - property: countable + proof: This is trivial. + + - property: thin + proof: This is clear. + +undecidable_properties: + - property: essentially countable + proof: This depends on the countability of $K$. + + - property: locally finite + proof: This depends on the finiteness of $K$. + +special_objects: + initial object: + description: the trivial vector space + terminal object: + description: the trivial vector space + coproducts: + description: '[finite case] direct sums' + products: + description: '[finite case] direct products with pointwise operations' + +special_morphisms: + isomorphisms: + description: bijective linear maps + proof: It is a full subcategory of $\Vect_K$, for which we know that isomorphisms are bijective linear maps. + monomorphisms: + description: injective linear maps + proof: For the non-trivial direction, the forgetful functor $\FinVect_K \to \Set$ is representable (by $K$), and therefore preserves monomorphisms. + epimorphisms: + description: surjective linear maps + proof: 'For the non-trivial direction, it suffices to observe that every epimorphism in $\FinVect_K$ is also an epimorphism in $\Vect_K$, where epimorphisms are already classified. Namely, let $f : V \to W$ be an epimorphism in $\FinVect_K$ and let $g : W \to T$ be a linear map with $g \circ f = 0$. Then $g$ factors as $g = i \circ h$, where $i : \im(g) \hookrightarrow T$ is the inclusion of the image and $h : W \twoheadrightarrow \im(g)$ is the corestriction of $g$. Then $h \circ f = 0$, and since $\im(g)$ is finite-dimensional, it follows that $h = 0$. Hence $g = 0$.' diff --git a/database/data/categories/FinVect_c.yaml b/database/data/categories/FinVect_c.yaml index 763d15a3..57d73dd5 100644 --- a/database/data/categories/FinVect_c.yaml +++ b/database/data/categories/FinVect_c.yaml @@ -1,72 +1,27 @@ -# TODO: fix duplication with FinVect_u and FinVect_f id: FinVect_c name: category of finite-dimensional vector spaces [countable field] notation: $\FinVect_K$ objects: finite-dimensional vector spaces over a countably infinite field $K$ morphisms: linear maps -description: This is the full subcategory of $\Vect_K$ consisting of finite-dimensional vector spaces. Every object is isomorphic to $K^n$ for a unique $n \in \IN$. In this entry, we assume that $K$ is countably infinite (e.g. $K = \IQ$) in order to determine all properties of this category. +description: This is the special case of $\FinVect_K$ where $K$ is a countably infinite field (e.g. $K = \IQ$). We use this assumption in order to determine all properties of this category. nlab_link: https://ncatlab.org/nlab/show/FinDimVect +parent: FinVect tags: - algebra related: - Vect - - FinVect_u - - FinVect_f - Ab_fg satisfied_properties: - - property: locally small - proof: There is a forgetful functor $\FinVect_K \to \Vect_K$, and $\Vect_K$ is locally small. - - 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. - - - property: extremal generator - proof: The one-dimensional vector space $K$ is an extremal generator even in $\Vect_K$. Now apply Lemma 10 here. - references: - - vect_extremal_generator - - - property: split abelian - proof: This follows directly from the corresponding fact for $\Vect_K$. - - - 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. - - - property: ℵ₁-accessible - proof: 'The inclusion $\FinVect_K \hookrightarrow \Vect_K$ is closed under $\aleph_1$-filtered colimits by MO/400763. In particular, $\FinVect_K$ has $\aleph_1$-filtered colimits. Moreover, every object in $\FinVect_K$ is $\aleph_1$-presentable: it is isomorphic to some $K^n$, which is finitely presentable in $\Vect_K$, hence $\aleph_1$-presentable in $\Vect_K$, and therefore also $\aleph_1$-presentable in $\FinVect_K$.' + 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 because $K$ is countable by assumption. unsatisfied_properties: - - property: skeletal - proof: This is trivial. - - - property: small - proof: This is trivial. - - - property: countable - proof: This is trivial. - - property: locally finite proof: The hom-set $\Hom(K,K) \cong K$ is infinite by assumption. -special_objects: - initial object: - description: the trivial vector space - terminal object: - description: the trivial vector space - coproducts: - description: '[finite case] direct sums' - products: - description: '[finite case] direct products with pointwise operations' +special_objects: {} -special_morphisms: - isomorphisms: - description: bijective linear maps - proof: It is a full subcategory of $\Vect_K$, for which we know that isomorphisms are bijective linear maps. - monomorphisms: - description: injective linear maps - proof: For the non-trivial direction, the forgetful functor $\FinVect_K \to \Set$ is representable (by $K$), and therefore preserves monomorphisms. - epimorphisms: - description: surjective linear maps - proof: 'For the non-trivial direction, it suffices to observe that every epimorphism in $\FinVect_K$ is also an epimorphism in $\Vect_K$, where epimorphisms are already classified. Namely, let $f : V \to W$ be an epimorphism in $\FinVect_K$ and let $g : W \to T$ be a linear map with $g \circ f = 0$. Then $g$ factors as $g = i \circ h$, where $i : \im(g) \hookrightarrow T$ is the inclusion of the image and $h : W \twoheadrightarrow \im(g)$ is the corestriction of $g$. Then $h \circ f = 0$, and since $\im(g)$ is finite-dimensional, it follows that $h = 0$. Hence $g = 0$.' +special_morphisms: {} diff --git a/database/data/categories/FinVect_f.yaml b/database/data/categories/FinVect_f.yaml index c994ef71..a3aef1d0 100644 --- a/database/data/categories/FinVect_f.yaml +++ b/database/data/categories/FinVect_f.yaml @@ -1,72 +1,28 @@ -# TODO: fix duplication with FinVect_u and FinVect_c id: FinVect_f name: category of finite-dimensional vector spaces [finite field] notation: $\FinVect_K$ -objects: finite-dimensional vector spaces over a countably infinite field $K$ +objects: finite-dimensional vector spaces over a finite field $K$ morphisms: linear maps -description: This is the full subcategory of $\Vect_K$ consisting of finite-dimensional vector spaces. Every object is isomorphic to $K^n$ for a unique $n \in \IN$. In this entry, we assume that $K$ is finite (e.g. $K = \IF_2$) in order to determine all properties of this category. +description: This is the special case of $\FinVect_K$ where $K$ is a finite field (e.g. $K = \IF_2$). We use this assumption in order to determine all properties of this category. nlab_link: https://ncatlab.org/nlab/show/FinDimVect +parent: FinVect tags: - algebra related: - Vect - - FinVect_u - - FinVect_c - Ab_fg satisfied_properties: - - property: locally small - proof: There is a forgetful functor $\FinVect_K \to \Vect_K$, and $\Vect_K$ is locally small. - - 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. + 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 finite by assumption, hence a countable set. - property: locally finite proof: Each hom-set $\Hom(K^n,K^m) \cong M_{m \times n}(K)$ is finite by assumption. - - property: extremal generator - proof: The one-dimensional vector space $K$ is an extremal generator even in $\Vect_K$. Now apply Lemma 10 here. - references: - - vect_extremal_generator - - - property: split abelian - proof: This follows directly from the corresponding fact for $\Vect_K$. - - - 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. - -unsatisfied_properties: - - property: skeletal - proof: This is trivial. - - - property: small - proof: This is trivial. - - - property: countable - proof: This is trivial. - - - property: thin - proof: This is trivial. +unsatisfied_properties: [] -special_objects: - initial object: - description: the trivial vector space - terminal object: - description: the trivial vector space - coproducts: - description: '[finite case] direct sums' - products: - description: '[finite case] direct products with pointwise operations' +special_objects: {} -special_morphisms: - isomorphisms: - description: bijective linear maps - proof: It is a full subcategory of $\Vect_K$, for which we know that isomorphisms are bijective linear maps. - monomorphisms: - description: injective linear maps - proof: For the non-trivial direction, the forgetful functor $\FinVect_K \to \Set$ is representable (by $K$), and therefore preserves monomorphisms. - epimorphisms: - description: surjective linear maps - proof: 'For the non-trivial direction, it suffices to observe that every epimorphism in $\FinVect_K$ is also an epimorphism in $\Vect_K$, where epimorphisms are already classified. Namely, let $f : V \to W$ be an epimorphism in $\FinVect_K$ and let $g : W \to T$ be a linear map with $g \circ f = 0$. Then $g$ factors as $g = i \circ h$, where $i : \im(g) \hookrightarrow T$ is the inclusion of the image and $h : W \twoheadrightarrow \im(g)$ is the corestriction of $g$. Then $h \circ f = 0$, and since $\im(g)$ is finite-dimensional, it follows that $h = 0$. Hence $g = 0$.' +special_morphisms: {} diff --git a/database/data/categories/FinVect_u.yaml b/database/data/categories/FinVect_u.yaml index 0329565e..bd20868b 100644 --- a/database/data/categories/FinVect_u.yaml +++ b/database/data/categories/FinVect_u.yaml @@ -1,72 +1,28 @@ -# TODO: fix duplication with FinVect_c and FinVect_f id: FinVect_u name: category of finite-dimensional vector spaces [uncountable field] notation: $\FinVect_K$ objects: finite-dimensional vector spaces over an uncountable field $K$ morphisms: linear maps -description: This is the full subcategory of $\Vect_K$ consisting of finite-dimensional vector spaces. Every object is isomorphic to $K^n$ for a unique $n \in \IN$. In this entry, we assume that $K$ is uncountable (e.g. $K = \IR$) in order to determine all properties of this category. +description: This is the special case of $\FinVect_K$ where $K$ is an uncountable field (e.g. $K = \IR$). We use this assumption in order to determine all properties of this category. nlab_link: https://ncatlab.org/nlab/show/FinDimVect +parent: FinVect tags: - algebra related: - Vect - - FinVect_c - - FinVect_f - Ab_fg -satisfied_properties: - - property: locally small - proof: There is a forgetful functor $\FinVect_K \to \Vect_K$, and $\Vect_K$ is locally small. - - - 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. - - - property: extremal generator - proof: The one-dimensional vector space $K$ is an extremal generator even in $\Vect_K$. Now apply Lemma 10 here. - references: - - vect_extremal_generator - - - property: split abelian - proof: This follows directly from the corresponding fact for $\Vect_K$. - - - 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. - - - property: ℵ₁-accessible - proof: 'The inclusion $\FinVect_K \hookrightarrow \Vect_K$ is closed under $\aleph_1$-filtered colimits by MO/400763. In particular, $\FinVect_K$ has $\aleph_1$-filtered colimits. Moreover, every object in $\FinVect_K$ is $\aleph_1$-presentable: it is isomorphic to some $K^n$, which is finitely presentable in $\Vect_K$, hence $\aleph_1$-presentable in $\Vect_K$, and therefore also $\aleph_1$-presentable in $\FinVect_K$.' +satisfied_properties: [] unsatisfied_properties: - - property: skeletal - proof: This is trivial. - - - property: small - proof: This is trivial. - - property: essentially countable proof: The hom-set $\Hom(K,K) \cong K$ is uncountable by assumption. - property: locally finite proof: The hom-set $\Hom(K,K) \cong K$ is infinite by assumption. -special_objects: - initial object: - description: the trivial vector space - terminal object: - description: the trivial vector space - coproducts: - description: '[finite case] direct sums' - products: - description: '[finite case] direct products with pointwise operations' +special_objects: {} -special_morphisms: - isomorphisms: - description: bijective linear maps - proof: It is a full subcategory of $\Vect_K$, for which we know that isomorphisms are bijective linear maps. - monomorphisms: - description: injective linear maps - proof: For the non-trivial direction, the forgetful functor $\FinVect_K \to \Set$ is representable (by $K$), and therefore preserves monomorphisms. - epimorphisms: - description: surjective linear maps - proof: 'For the non-trivial direction, it suffices to observe that every epimorphism in $\FinVect_K$ is also an epimorphism in $\Vect_K$, where epimorphisms are already classified. Namely, let $f : V \to W$ be an epimorphism in $\FinVect_K$ and let $g : W \to T$ be a linear map with $g \circ f = 0$. Then $g$ factors as $g = i \circ h$, where $i : \im(g) \hookrightarrow T$ is the inclusion of the image and $h : W \twoheadrightarrow \im(g)$ is the corestriction of $g$. Then $h \circ f = 0$, and since $\im(g)$ is finite-dimensional, it follows that $h = 0$. Hence $g = 0$.' +special_morphisms: {} diff --git a/database/data/categories/Fld.yaml b/database/data/categories/Fld.yaml index 946d2732..48040e5b 100644 --- a/database/data/categories/Fld.yaml +++ b/database/data/categories/Fld.yaml @@ -3,7 +3,7 @@ name: category of fields notation: $\Fld$ objects: fields morphisms: field homomorphisms (i.e., ring homomorphisms) -description: This is a typical example of a bad category of good objects. +description: This category is a typical example of a bad category of good objects. nlab_link: https://ncatlab.org/nlab/show/Field tags: diff --git a/database/data/categories/FreeAb.yaml b/database/data/categories/FreeAb.yaml index 13dc27f8..1fbd065c 100644 --- a/database/data/categories/FreeAb.yaml +++ b/database/data/categories/FreeAb.yaml @@ -3,7 +3,7 @@ name: category of free abelian groups notation: $\FreeAb$ objects: free abelian groups morphisms: group homomorphisms -description: null +description: This is the full subcategory of $\Ab$ that consists of the free abelian groups. nlab_link: null tags: diff --git a/database/data/categories/M-Set.yaml b/database/data/categories/M-Set.yaml index f14e307e..3c8713c2 100644 --- a/database/data/categories/M-Set.yaml +++ b/database/data/categories/M-Set.yaml @@ -33,6 +33,7 @@ unsatisfied_properties: undecidable_properties: - property: semi-strongly connected + # TODO: decide if we want to add separate children entries to decide this for some cases. proof: If this category is semi-strongly connected depends on the choice of $M$. For $M = 1$ it is, for $M = \IZ$ it is not. In general, if $G$ is a group, then $G{-}\Set$ is semi-strongly connected if and only if for all subgroups $H,K \subseteq G$, $H$ is subconjugated to $K$ or $K$ is subconjugated to $H$. If $G$ is abelian, this means that the poset of subgroups is linear, in which case $G$ is either isomorphic to $\IZ/p^n$ or to $\IZ/p^{\infty}$ for a prime $p$. See also MSE/5129804. special_objects: diff --git a/database/data/categories/Mon.yaml b/database/data/categories/Mon.yaml index d6b61c38..9f58e138 100644 --- a/database/data/categories/Mon.yaml +++ b/database/data/categories/Mon.yaml @@ -3,7 +3,7 @@ name: category of monoids notation: $\Mon$ objects: monoids morphisms: monoid homomorphisms -description: null +description: This category is a typical example of a finitary algebraic category. nlab_link: https://ncatlab.org/nlab/show/category+of+monoids tags: @@ -11,6 +11,7 @@ tags: related: - CMon + - Ring - Cat - Grp - SemiGrp diff --git a/database/data/categories/N.yaml b/database/data/categories/N.yaml index 45add20b..d4ee93cb 100644 --- a/database/data/categories/N.yaml +++ b/database/data/categories/N.yaml @@ -3,7 +3,9 @@ name: partially ordered set of natural numbers notation: $(\IN,\leq)$ objects: natural numbers $0, 1, 2, \dotsc$ morphisms: 'a unique morphism $(n,m) : n \to m$ if $n \leq m$' -description: This can also be seen as the path category of the infinite linear graph $\bullet \to \bullet \to \bullet \to \cdots$. +description: >- + This category can also be seen as the path category of the infinite linear graph + $$\bullet \longrightarrow \bullet \longrightarrow \bullet \longrightarrow \cdots.$$ nlab_link: null tags: diff --git a/database/data/categories/N_oo.yaml b/database/data/categories/N_oo.yaml index ddab4eba..1f60f871 100644 --- a/database/data/categories/N_oo.yaml +++ b/database/data/categories/N_oo.yaml @@ -3,7 +3,7 @@ name: partially ordered set of extended natural numbers notation: $(\IN \cup \{\infty\}, \leq)$ objects: natural numbers and $\infty$ morphisms: 'a unique morphism $(n, m) : n \to m$ if $n \leq m$, where of course $n \leq \infty$ for all $n$' -description: null +description: This category is a completed version of the thin category of natural numbers. nlab_link: null tags: diff --git a/database/data/categories/On.yaml b/database/data/categories/On.yaml index d4323b34..45fe331b 100644 --- a/database/data/categories/On.yaml +++ b/database/data/categories/On.yaml @@ -3,7 +3,7 @@ name: partially ordered collection of ordinal numbers notation: $(\On,\leq)$ objects: ordinal numbers morphisms: 'a unique morphism $(\alpha,\beta): \alpha \to \beta$ if $\alpha \leq \beta$' -description: This is a large variant of the partially ordered set of natural numbers. +description: This category is a large variant of the thin category of natural numbers. nlab_link: null tags: diff --git a/database/data/categories/R-Mod.yaml b/database/data/categories/R-Mod.yaml index 83c27ab0..411b5a45 100644 --- a/database/data/categories/R-Mod.yaml +++ b/database/data/categories/R-Mod.yaml @@ -4,16 +4,14 @@ notation: $R{-}\Mod$ objects: left $R$-modules morphisms: $R$-linear maps description: |- - This is the prototype of an abelian category. The category of right modules is the same with the opposite ring $R^{\op}$, hence not listed here. - To settle the unsatisfied properties, we make the assumption that $R$ is not semisimple: If $R$ is semisimple, then by the Artin-Wedderburn theorem, the category is equivalent to a finite direct product of categories $D{-}\Mod$ for division rings $D$, and the case of division rings is in a separate entry. In particular, $R \neq 0$ and $R$ is not a field. + This is the prototype of an abelian category. The category of right modules is the same with the opposite ring $R^{\op}$, hence not listed here. We assume $R \neq 0$ since otherwise the category would be trivial. nlab_link: https://ncatlab.org/nlab/show/module tags: - algebra related: - - Ab - M-Set - - R-Mod_div + - Ab - Vect satisfied_properties: @@ -27,15 +25,16 @@ satisfied_properties: proof: Take the algebraic theory of an $R$-module (given by the algebraic theory of an abelian group and for each $r \in R$ a unary operation). unsatisfied_properties: - - property: split abelian - proof: By assumption, $R$ is not semisimple, so that there is a non-projective $R$-module, which yields a non-split sequence. - - property: skeletal proof: This is trivial. - property: CSP proof: The canonical homomorphism $\bigoplus_{n \geq 0} R \to \prod_{n \geq 0} R$ is not surjective, hence no epimorphism. +undecidable_properties: + - property: split abelian + proof: The category $R{-}\Mod$ is split abelian if and only if $R$ is semisimple. See Theorem 2.5 in Lam's A First Course in Noncommutative Rings. For example, $\Vect_K$ is split abelian, while $\Ab$ is not. + special_objects: initial object: description: trivial module diff --git a/database/data/categories/R-Mod_div.yaml b/database/data/categories/R-Mod_div.yaml index 39b2b779..3da1ead1 100644 --- a/database/data/categories/R-Mod_div.yaml +++ b/database/data/categories/R-Mod_div.yaml @@ -3,44 +3,22 @@ name: category of left modules over a division ring notation: $R{-}\Mod$ objects: left $R$-modules morphisms: $R$-linear maps -description: Here, we assume that $R$ is a non-commutative division ring, i.e. a skew-field which is not a field. The category of modules behaves mostly the same as in the commutative case. +description: This is the special case of $R{-}\Mod$ where $R$ is a division ring (also known as a skew-field). nlab_link: https://ncatlab.org/nlab/show/module +parent: R-Mod tags: - algebra related: - - R-Mod - - Vect + - M-Set satisfied_properties: - - property: locally small - proof: There is a forgetful functor $R{-}\Mod \to \Set$ and $\Set$ is locally small. - - 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. - - property: finitary algebraic - proof: Take the algebraic theory of an $R$-module (given by the algebraic theory of an abelian group and for each $r \in R$ a unary operation). - -unsatisfied_properties: - - property: skeletal - proof: This is trivial. - - - property: CSP - proof: The canonical homomorphism $\bigoplus_{n \geq 0} R \to \prod_{n \geq 0} R$ is not surjective, hence no epimorphism. +unsatisfied_properties: [] -special_objects: - initial object: - description: trivial module - terminal object: - description: zero module - coproducts: - description: direct sums - products: - description: direct products with pointwise operations +special_objects: {} -special_morphisms: - epimorphisms: - description: surjective morphisms - proof: The forgetful functor to abelian groups is faithful and preserves colimits, hence reflects and preserves epimorphisms. Alternatively, use the same proof as for abelian groups. +special_morphisms: {} diff --git a/database/data/categories/R-Mod_non_ss.yaml b/database/data/categories/R-Mod_non_ss.yaml new file mode 100644 index 00000000..0ad4bf01 --- /dev/null +++ b/database/data/categories/R-Mod_non_ss.yaml @@ -0,0 +1,24 @@ +id: R-Mod_non_ss +name: category of left modules over a non-semisimple ring +notation: $R{-}\Mod$ +objects: left $R$-modules +morphisms: $R$-linear maps +description: This is the special case of $R{-}\Mod$ where $R$ is a ring that is not semisimple. In particular, $R \neq 0$ and $R$ is not a field. If $R$ is semisimple, then by the Artin-Wedderburn theorem, the category is equivalent to a finite direct product of categories $D{-}\Mod$ for division rings $D$, and the case of division rings is in a separate entry. +nlab_link: https://ncatlab.org/nlab/show/module +parent: R-Mod + +tags: + - algebra + +related: + - M-Set + +satisfied_properties: [] + +unsatisfied_properties: + - property: split abelian + proof: By assumption, $R$ is not semisimple, which means that there is a short exact sequence that does not split; see Theorem 2.5 in Lam's A First Course in Noncommutative Rings. + +special_objects: {} + +special_morphisms: {} diff --git a/database/data/categories/Ring.yaml b/database/data/categories/Ring.yaml index 7da17e06..2bbbaefc 100644 --- a/database/data/categories/Ring.yaml +++ b/database/data/categories/Ring.yaml @@ -3,80 +3,24 @@ name: category of rings notation: $\Ring$ objects: rings morphisms: ring homomorphisms -description: Here, rings always have a unit, and homomorphisms preserve them. +description: Here, rings always have a unit, and homomorphisms preserve them. This category is the special case of $\Alg(R)$ where $R = \IZ$. nlab_link: https://ncatlab.org/nlab/show/Ring +parent: Alg(R) tags: - algebra related: - - Alg(R) - CRing - Rng + - Mon comments: - It is likely that the epimorphisms can be described as for $\CRing$. -satisfied_properties: - - property: locally small - proof: There is a forgetful functor $\Ring \to \Set$ and $\Set$ is locally small. +satisfied_properties: [] - - property: finitary algebraic - proof: Take the algebraic theory of a ring. - - - property: strict terminal object - proof: 'If $f : 0 \to R$ is a homomorphism, then $R$ satisfies $1=f(1)=f(0)=0$, so that $R=0$.' - - - 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. - references: - - grp_malcev - - - 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$.' - label: ring_disjoint_finite_products - -unsatisfied_properties: - - property: skeletal - proof: This is trivial. - - - property: balanced - proof: The inclusion $\IZ \hookrightarrow \IQ$ is a counterexample; see also here. - label: ring_not_balanced - - - property: semi-strongly connected - proof: This is because already the full subcategory $\CRing$ does not have this property. - - - 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).' - - - property: codistributive - proof: 'If $\sqcup$ denotes the coproduct of rings (see MSE/625874 for their description) and $R$ is a ring, the canonical morphism $R \sqcup \IZ^2 \to (R \sqcup \IZ)^2 = R^2$ is usually no isomorphism. For example, for $R = \IZ[X]$ the coproduct on the LHS is not commutative, it has the ring presentation $\langle X,E : E^2=E \rangle$.' - - - property: co-Malcev - proof: 'See MO/509552: Consider the forgetful functor $U : \Ring \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) \coloneqq \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $\IZ[X]$ and $S$ by $\IZ \langle X,Y \rangle / \langle XY-X^2 \rangle$. It is clear that $R$ is reflexive, but not symmetric.' - - - property: coregular - proof: 'Let $B \coloneqq M_2(\IQ)$ and $A \coloneqq \IQ^2$. 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 & 2 \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.' - label: ring_not_coregular - - - 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). - references: - - cring_no_regular_quotient_object_classifier - - - property: cocartesian cofiltered limits - proof: >- - Consider the ring $A = \IZ[X]$ and the sequence of rings $B_n = \IZ[Y]/(Y^{n+1})$ with projections $B_{n+1} \to B_n$, whose limit is $\IZ[[Y]]$. Every element in the coproduct of rings $\IZ[X] \sqcup \IZ[[Y]]$ has a finite "free product" length. Now consider the elements - $$w_n = (1 + XY) (1+XY^2) \cdots (1+X Y^n) \in A \sqcup B_n.$$ - 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 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. - - - property: effective cocongruences - proof: See MO/510744. - label: ring_no_effective_cocongruences +unsatisfied_properties: [] special_objects: initial object: diff --git a/database/data/categories/Rng.yaml b/database/data/categories/Rng.yaml index f27986ca..37744cd0 100644 --- a/database/data/categories/Rng.yaml +++ b/database/data/categories/Rng.yaml @@ -3,7 +3,7 @@ name: category of rngs notation: $\Rng$ objects: rngs, that is, non-unital rings morphisms: maps that preserve addition and multiplication -description: null +description: This category is a typical example of a finitary algebraic category. It is an "additive version" of the category of semigroups $\SemiGrp$. nlab_link: https://ncatlab.org/nlab/show/Rng tags: @@ -13,6 +13,7 @@ related: - CRing - Ring - Ab + - SemiGrp comments: - It is likely that the epimorphisms can be described as for $\CRing$. @@ -37,9 +38,7 @@ unsatisfied_properties: proof: This is trivial. - property: balanced - proof: The inclusion $\IZ \hookrightarrow \IQ$ is a counterexample; the proof can be reduced to the unital case. - references: - - ring_not_balanced + proof: The inclusion $\IZ \hookrightarrow \IQ$ is a counterexample; the proof can be reduced to the unital case. - property: cogenerator proof: 'We apply this lemma to the collection of fields: Any non-zero rng homomorphism from a field to a rng must be injective, and for every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables has cardinality $\geq \kappa$.' @@ -61,9 +60,9 @@ unsatisfied_properties: proof: Assume that $\coprod_n \IZ \to \prod_n \IZ$ is an epimorphism in $\Rng$. Then $((\coprod_n \IZ)^+)^{\ab} \to \prod_n \IZ$ would be an epimorphism in $\CRing$, where $(-)^+$ denotes the unitalization and $(-)^{\ab}$ the abelianization. But if $R \to S$ is an epimorphism of commutative rings, then $\card(S) \leq \card(R)$ by SP/04W0. Since $((\coprod_n \IZ)^+)^{\ab}$ is countable and $\prod_n \IZ$ is not, we get a contradiction. - 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.' + proof: 'We can copy the proof for $\Ring$, i.e. the proof for $\Alg(R)$. 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.' references: - - ring_not_coregular + - alg_not_coregular - 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).' @@ -86,8 +85,6 @@ 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$. - references: - - ring_no_effective_cocongruences special_objects: initial object: diff --git a/database/data/categories/SemiGrp.yaml b/database/data/categories/SemiGrp.yaml index 022420ac..5719dfee 100644 --- a/database/data/categories/SemiGrp.yaml +++ b/database/data/categories/SemiGrp.yaml @@ -12,6 +12,7 @@ tags: related: - Grp - Mon + - Rng satisfied_properties: - property: locally small diff --git a/database/data/categories/SetxSet.yaml b/database/data/categories/SetxSet.yaml index fc1170fd..59151c09 100644 --- a/database/data/categories/SetxSet.yaml +++ b/database/data/categories/SetxSet.yaml @@ -3,7 +3,7 @@ name: category of pairs of sets notation: $\Set \times \Set$ objects: pairs $(A,B)$ of sets $A$ and $B$ morphisms: A morphism $(A,B) \to (C,D)$ consists of a map $A \to C$ and a map $B \to D$. -description: This is an example of the product of categories. It inherits most (but not all) properties from $\Set$. It can also be seen as the category $\Sh(1+1)$ of sheaves on a discrete space with two points, and also as the slice category $\Set/(1+1)$. +description: This category is an example of the product of categories. It inherits most (but not all) properties from $\Set$. It can also be seen as the category $\Sh(1+1)$ of sheaves on a discrete space with two points, and also as the slice category $\Set/(1+1)$. nlab_link: null tags: diff --git a/database/data/categories/Sh(X).yaml b/database/data/categories/Sh(X).yaml index 6aac48ba..c69c870b 100644 --- a/database/data/categories/Sh(X).yaml +++ b/database/data/categories/Sh(X).yaml @@ -17,6 +17,7 @@ related: - Sh(X,Ab) comments: + # TODO: maybe create separate entries for specific spaces X - It is likely that none of the currently remaining unknown properties (locally finitely presentable, ℵ₁-accessible, etc.) are satisfied for a generic space $X$, but we need to make this precise by adding additional requirements to $X$. Maybe we need to create separate entries for specific spaces $X$. - See MSE/5140378 in particular for conditions when $\Sh(X)$ is locally finitely presentable. diff --git a/database/data/categories/Sh(X,Ab).yaml b/database/data/categories/Sh(X,Ab).yaml index 5fc15918..868f7ff3 100644 --- a/database/data/categories/Sh(X,Ab).yaml +++ b/database/data/categories/Sh(X,Ab).yaml @@ -15,6 +15,7 @@ related: - Sh(X) comments: + # TODO: maybe create separate entries for specific spaces X - It is likely that neither of the currently remaining unknown properties (finitary algebraic, locally finitely presentable, CSP, etc.) are satisfied for a generic space $X$, but we need to make this precise by adding additional requirements to $X$. Maybe we need to create separate entries for specific spaces $X$. satisfied_properties: diff --git a/database/data/categories/TorsAb.yaml b/database/data/categories/TorsAb.yaml index f65fcd95..a80fee06 100644 --- a/database/data/categories/TorsAb.yaml +++ b/database/data/categories/TorsAb.yaml @@ -3,7 +3,7 @@ name: category of torsion abelian groups notation: $\TorsAb$ objects: torsion abelian groups morphisms: group homomorphisms -description: This is a Grothendieck abelian category containing all finite abelian groups. +description: This category is a Grothendieck abelian category containing all finite abelian groups. nlab_link: https://ncatlab.org/nlab/show/torsion+subgroup tags: @@ -31,13 +31,9 @@ satisfied_properties: - 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$.' - references: - - ab_abelian - 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$.' - references: - - ab_abelian - 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$. diff --git a/database/data/categories/TorsFreeAb.yaml b/database/data/categories/TorsFreeAb.yaml index 56130f69..dc820eb3 100644 --- a/database/data/categories/TorsFreeAb.yaml +++ b/database/data/categories/TorsFreeAb.yaml @@ -3,7 +3,7 @@ name: category of torsion-free abelian groups notation: $\TorsFreeAb$ objects: torsion-free abelian groups morphisms: group homomorphisms -description: This is a typical example of a well-behaved additive category which is not abelian. It contains the category of free abelian groups. +description: This category is a typical example of a well-behaved additive category which is not abelian. It contains the category of free abelian groups. nlab_link: https://ncatlab.org/nlab/show/torsion-free+module tags: diff --git a/database/data/categories/Vect.yaml b/database/data/categories/Vect.yaml index ff2e0869..d7045dca 100644 --- a/database/data/categories/Vect.yaml +++ b/database/data/categories/Vect.yaml @@ -3,31 +3,22 @@ name: category of vector spaces notation: $\Vect_K$ objects: vector spaces over a field $K$ morphisms: linear maps -description: This is a special case of the category of modules over a ring, where the ring is a field. It is the prototype of a split abelian category. +description: This is the special case of $R{-}\Mod$ where $R$ is a field $K$. It is the prototype of a split abelian category. nlab_link: https://ncatlab.org/nlab/show/Vect +parent: R-Mod_div tags: - algebra related: - - R-Mod - - R-Mod_div - - FinVect_f - - FinVect_c - - FinVect_u + - FinVect - FiltVect - FreeAb satisfied_properties: - - property: locally small - proof: There is a forgetful functor $\Vect \to \Set$ and $\Set$ is locally small. - - 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. - - property: finitary algebraic - proof: Take the algebraic theory of a vector space. - - property: extremal generator proof: The one-dimensional vector space $K$ is an extremal generator since it represents the forgetful functor $\Vect_K \to \Set$ which is faithful and conservative. check_redundancy: false @@ -37,12 +28,7 @@ satisfied_properties: proof: 'The one-dimensional vector space $K$ is an extremal cogenerator. To show this, using this result, since $\Vect_K$ is balanced, it suffices to show that $K$ is a cogenerator. For this, suppose we have two unequal vectors $x, y \in V$. Then $x - y \ne 0$, so there exists a functional $\varphi : V \to K$ such that $\varphi(x - y) \ne 0$. It follows that $\varphi(x) \ne \varphi(y)$.' check_redundancy: false -unsatisfied_properties: - - property: skeletal - proof: This is trivial. - - - property: CSP - proof: The canonical homomorphism $\bigoplus_{n \geq 0} K \to \prod_{n \geq 0} K$ is not surjective, hence no epimorphism. +unsatisfied_properties: [] special_objects: initial object: @@ -54,7 +40,4 @@ special_objects: products: description: direct products with pointwise operations -special_morphisms: - epimorphisms: - description: surjective morphisms - proof: The forgetful functor to abelian groups is faithful and preserves colimits, hence reflects and preserves epimorphisms. Alternatively, just use the same proof as for abelian groups. +special_morphisms: {} diff --git a/database/data/categories/Z_div.yaml b/database/data/categories/Z_div.yaml index f3c24246..2697f6ca 100644 --- a/database/data/categories/Z_div.yaml +++ b/database/data/categories/Z_div.yaml @@ -3,7 +3,7 @@ name: preordered set of integers w.r.t. divisibility notation: $(\IZ,\mid)$ objects: integers morphisms: 'a unique morphism $(a,b) : a \to b$ if $a$ divides $b$' -description: This is a preordered set, not a partially ordered set, because $a$ and $-a$ divide each other, but are not equal for $a \neq 0$. Notice that this category is equivalent (but not isomorphic) to $(\IN,\mid)$. +description: This category corresponds to a preordered set, not a partially ordered set, because $a$ and $-a$ divide each other, but are not equal for $a \neq 0$. Notice that this category is equivalent (but not isomorphic) to $(\IN,\mid)$. nlab_link: null tags: diff --git a/database/data/categories/sSet.yaml b/database/data/categories/sSet.yaml index 8412ce1d..7d7339d3 100644 --- a/database/data/categories/sSet.yaml +++ b/database/data/categories/sSet.yaml @@ -3,7 +3,7 @@ name: category of simplicial sets notation: $\sSet$ objects: simplicial sets, i.e. functors $\Delta^{\op} \to \Set$ where $\Delta$ denotes the simplex category. morphisms: natural transformations -description: null +description: The category of simplicial sets provides a fundamental combinatorial framework for representing spaces and $\infty$-categories, with applications throughout algebraic topology, higher category theory, and homological algebra. nlab_link: https://ncatlab.org/nlab/show/SimpSet tags: diff --git a/database/data/functors/trivial_BG.yaml b/database/data/functors/trivial_BG.yaml index de3af686..20503576 100644 --- a/database/data/functors/trivial_BG.yaml +++ b/database/data/functors/trivial_BG.yaml @@ -1,9 +1,9 @@ id: trivial_BG name: trivial functor from the delooping notation: $!_{BG}$ -domain: BG_f +domain: BG codomain: '1' -description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the delooping of a non-trivial finite group $G$. It is a basic example of a conservative functor which is not faithful.' +description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the delooping of a non-trivial group $G$. It is a basic example of a conservative functor which is not faithful.' nlab_link: null left_adjoint: null diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index 4de505dc..68f5d92f 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -15,9 +15,11 @@ CREATE TABLE structures ( description TEXT, nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'), dual_structure_id TEXT, + parent TEXT, UNIQUE (id, type), FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT, FOREIGN KEY (dual_structure_id, type) REFERENCES structures (id, type) ON DELETE RESTRICT + FOREIGN KEY (parent, type) REFERENCES structures (id, type) ON DELETE RESTRICT ); CREATE UNIQUE INDEX structures_lower_id_unique ON structures (lower(id)); diff --git a/database/scripts/deduce-special-morphisms.ts b/database/scripts/deduce-special-morphisms.ts index 9a73adcf..4b9cbf52 100644 --- a/database/scripts/deduce-special-morphisms.ts +++ b/database/scripts/deduce-special-morphisms.ts @@ -1,11 +1,13 @@ import { get_client } from '$shared/db' import { devlog } from '$shared/utils' +import { get_structure_parent_map } from './utils/structures' const db = get_client({ readonly: false }) export function deduce_special_morphisms() { console.info('\n--- Deduce special morphisms ---') clear_deduced_special_morphisms() + inherit_special_morphisms_from_parents() deduce_special_morphisms_by_rules() deduce_special_morphisms_of_dual_categories() } @@ -17,6 +19,58 @@ function clear_deduced_special_morphisms() { db.prepare(`DELETE FROM special_morphisms WHERE is_deduced = TRUE`).run() } +/** + * Inherit special morphism assignments from parent categories + */ +function inherit_special_morphisms_from_parents() { + type SpecialMorphism = { type: string; description: string; proof: string } + + const parent_map = get_structure_parent_map(db, 'category') + + const get_parent_special_morphisms = db.prepare<[string], SpecialMorphism>( + `SELECT type, description, proof FROM special_morphisms + WHERE category_id = ? AND is_deduced = FALSE` + ) + + const insert_special_morphism = db.prepare( + `INSERT INTO special_morphisms (category_id, type, description, proof, is_deduced) + VALUES (?, ?, ?, ?, TRUE) + ON CONFLICT (category_id, type) DO NOTHING` + ) + + let inherited_count = 0 + + for (const [category_id, parent_id] of parent_map) { + const inherited_morphisms = new Map() + let current_id = parent_id + + while (current_id) { + const parent_entries = get_parent_special_morphisms.all(current_id) + + for (const entry of parent_entries) { + if (!inherited_morphisms.has(entry.type)) { + inherited_morphisms.set(entry.type, entry) + } + } + + current_id = parent_map.get(current_id) ?? null + } + + for (const [type, entry] of inherited_morphisms) { + const proof = `This follows from the parent.` + const res = insert_special_morphism.run( + category_id, + type, + entry.description, + proof + ) + inherited_count += res.changes + } + } + + devlog(`Inherited ${inherited_count} special morphisms from parents`) +} + /** * Deduces special morphisms from the rules from the special_morphism_rules * table. We ignore duplicate assignments here because of overlaps diff --git a/database/scripts/deduce-special-objects.ts b/database/scripts/deduce-special-objects.ts index c65c5791..c99843c0 100644 --- a/database/scripts/deduce-special-objects.ts +++ b/database/scripts/deduce-special-objects.ts @@ -1,11 +1,13 @@ import { get_client } from '$shared/db' import { devlog } from '$shared/utils' +import { get_structure_parent_map } from './utils/structures' const db = get_client({ readonly: false }) export function deduce_special_objects() { console.info('\n--- Deduce special objects ---') clear_deduced_special_objects() + inherit_special_objects_from_parents() deduce_special_objects_of_dual_categories() } @@ -16,6 +18,52 @@ function clear_deduced_special_objects() { db.prepare(`DELETE FROM special_objects WHERE is_deduced = TRUE`).run() } +/** + * Inherit special object assignments from parent categories + */ +function inherit_special_objects_from_parents() { + type SpecialObject = { type: string; description: string } + + const parent_map = get_structure_parent_map(db, 'category') + + const get_parent_special_objects = db.prepare<[string], SpecialObject>( + `SELECT type, description FROM special_objects + WHERE category_id = ? AND is_deduced = FALSE` + ) + + const insert_special_object = db.prepare( + `INSERT INTO special_objects (category_id, type, description, is_deduced) + VALUES (?, ?, ?, TRUE) + ON CONFLICT (category_id, type) DO NOTHING` + ) + + let inherited_count = 0 + + for (const [category_id, parent_id] of parent_map) { + const inherited_objects = new Map() + let current_id = parent_id + + while (current_id) { + const parent_entries = get_parent_special_objects.all(current_id) + + for (const entry of parent_entries) { + if (!inherited_objects.has(entry.type)) { + inherited_objects.set(entry.type, entry) + } + } + + current_id = parent_map.get(current_id) ?? null + } + + for (const [type, entry] of inherited_objects) { + const res = insert_special_object.run(category_id, type, entry.description) + inherited_count += res.changes + } + } + + devlog(`Inherited ${inherited_count} special objects from parents`) +} + /** * Deduce special objects in dual categories. * For example, initial objects in C describe the terminal objects in C^op. diff --git a/database/scripts/deduce-structure-properties.ts b/database/scripts/deduce-structure-properties.ts index a17f331b..478a94cc 100644 --- a/database/scripts/deduce-structure-properties.ts +++ b/database/scripts/deduce-structure-properties.ts @@ -13,7 +13,12 @@ import { } from './utils/properties' import { get_contradiction_string, get_proof_string } from './utils/implications' import { type StructureType, STRUCTURE_TYPES_WITH_DUALS } from '$shared/config' -import { get_structures, is_dual_structure, type StructureMeta } from './utils/structures' +import { + get_structure_parent_map, + get_structures, + is_dual_structure, + type StructureMeta +} from './utils/structures' import { get_normalized_implications, NormalizedImplication } from '$shared/implications' import { devlog } from '$shared/utils' @@ -230,6 +235,62 @@ function delete_deduced_properties(db: Database, type: StructureType) { ).run(type) } +/** + * Inherits satisfied/unsatisfied properties from parent structures. + */ +function inherit_properties_from_parents(db: Database, type: StructureType) { + type PropertyAssignment = { property_id: string; is_satisfied: 0 | 1 } + + const parent_map = get_structure_parent_map(db, type) + + const get_assignments = db.prepare<[string], PropertyAssignment>( + `SELECT property_id, is_satisfied + FROM property_assignments + WHERE structure_id = ? AND is_satisfied IS NOT NULL + ORDER BY id` + ) + + const property_insert = db.prepare( + `INSERT INTO property_assignments + (structure_id, property_id, type, is_satisfied, proof, is_deduced) + VALUES (?, ?, ?, ?, ?, TRUE) + ON CONFLICT (structure_id, property_id) DO NOTHING` + ) + + let inherited_count = 0 + + for (const [structure_id, parent_id] of parent_map) { + const inherited_properties = new Map() + let current_id = parent_id + + while (current_id) { + const parent_assignments = get_assignments.all(current_id) + + for (const assignment of parent_assignments) { + if (!inherited_properties.has(assignment.property_id)) { + inherited_properties.set(assignment.property_id, assignment) + } + } + + current_id = parent_map.get(current_id) ?? null + } + + for (const [property_id, assignment] of inherited_properties) { + const proof = `This follows from the parent.` + const res = property_insert.run( + structure_id, + property_id, + type, + assignment.is_satisfied, + proof + ) + inherited_count += res.changes + } + } + + devlog(`Inherited ${inherited_count} properties from parents`) +} + /** * Main function: Deduce properties of structures from given ones * by using the stored implications. @@ -240,6 +301,7 @@ export function deduce_properties_for_structures(type: StructureType) { const db = get_client({ readonly: false }) delete_deduced_properties(db, type) + inherit_properties_from_parents(db, type) const implications = get_normalized_implications(db, type) const structures = get_structures(db, type) diff --git a/database/scripts/expected-data/decided-categories.json b/database/scripts/expected-data/decided-categories.json index ff088f53..f20e5e19 100644 --- a/database/scripts/expected-data/decided-categories.json +++ b/database/scripts/expected-data/decided-categories.json @@ -5,7 +5,13 @@ "Ab", "Grp", "N", + "BG", + "BG_c", + "BG_f", + "BG_u", "R-Mod", + "R-Mod_div", + "R-Mod_non_ss", "CRing", "Ring", "FinSet", @@ -16,6 +22,7 @@ "Top_op", "Top_*", "Vect", + "FinVect", "FinVect_f", "FinVect_c", "FinVect_u", diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index bba87c08..fb05670b 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -1,12 +1,11 @@ import path from 'node:path' -import { seed_file, seed_files } from './utils/seed.helpers' +import { get_property_assignments, seed_file, seed_files } from './utils/seed.helpers' import { get_client } from '$shared/db' import type { CategoryYaml, ConfigYaml, ImplicationYaml, FunctorYaml, - PropertyEntry, SpecialMorphismRuleYaml, StructureYaml, PropertyYaml, @@ -199,9 +198,9 @@ function seed_structures({ const structure_insert = db.prepare( `INSERT INTO structures ( id, type, name, notation, description, nlab_link, - dual_structure_id + dual_structure_id, parent ) - VALUES (?, ?, ?, ?, ?, ?, ?)` + VALUES (?, ?, ?, ?, ?, ?, ?, ?)` ) const tag_insert = db.prepare( @@ -232,28 +231,6 @@ function seed_structures({ ) VALUES (?, ?, ?, ?)` ) - function insert_property_assignments( - structure_id: string, - entries: PropertyEntry[], - is_satisfied: 0 | 1 | null - ) { - for (const entry of entries) { - property_assignment_insert.run( - structure_id, - entry.property, - type, - is_satisfied, - entry.proof, - entry.check_redundancy === false ? 0 : 1, - entry.label || null - ) - - for (const ref of entry.references ?? []) { - proof_reference_insert.run(structure_id, entry.property, type, ref) - } - } - } - function insert_structure(structure: T) { const properties_are_disjoint = are_disjoint( [ @@ -276,7 +253,8 @@ function seed_structures({ structure.notation, structure.description, structure.nlab_link, - structure.dual || null + structure.dual || null, + structure.parent || null ) if (!structure.tags.length) { @@ -296,13 +274,23 @@ function seed_structures({ related_insert.run(structure.id, related, type) } - insert_property_assignments(structure.id, structure.satisfied_properties, 1) - insert_property_assignments(structure.id, structure.unsatisfied_properties, 0) - insert_property_assignments( - structure.id, - structure.undecidable_properties ?? [], - null - ) + const property_assignments = get_property_assignments(structure) + + for (const entry of property_assignments) { + property_assignment_insert.run( + structure.id, + entry.property, + type, + entry.is_satisfied, + entry.proof, + entry.check_redundancy === false ? 0 : 1, + entry.label || null + ) + + for (const ref of entry.references ?? []) { + proof_reference_insert.run(structure.id, entry.property, type, ref) + } + } if (extra) extra(structure) } @@ -332,12 +320,10 @@ function insert_category(category: CategoryYaml) { category_insert.run(category.id, category.objects, category.morphisms) for (const [type, entry] of Object.entries(category.special_objects)) { - if (!entry) continue special_object_insert.run(category.id, type, entry.description) } for (const [type, entry] of Object.entries(category.special_morphisms)) { - if (!entry) continue special_morphism_insert.run(category.id, type, entry.description, entry.proof) } } diff --git a/database/scripts/utils/seed.helpers.ts b/database/scripts/utils/seed.helpers.ts index 93367516..70bf9cd2 100644 --- a/database/scripts/utils/seed.helpers.ts +++ b/database/scripts/utils/seed.helpers.ts @@ -3,6 +3,7 @@ import path from 'node:path' import fs from 'node:fs' import YAML from 'yaml' import { devlog } from '$shared/utils' +import { StructureYaml } from './seed.types' function read_yaml_file(...parts: string[]): T { const content = fs.readFileSync(path.join(...parts), 'utf8') @@ -66,3 +67,20 @@ export function seed_files( process.exit(1) } } + +export function get_property_assignments(structure: StructureYaml) { + return [ + ...structure.satisfied_properties.map((entry) => ({ + ...entry, + is_satisfied: 1 as const + })), + ...structure.unsatisfied_properties.map((entry) => ({ + ...entry, + is_satisfied: 0 as const + })), + ...(structure.undecidable_properties ?? []).map((entry) => ({ + ...entry, + is_satisfied: null + })) + ] +} diff --git a/database/scripts/utils/seed.types.ts b/database/scripts/utils/seed.types.ts index 1bf2830e..173af4f6 100644 --- a/database/scripts/utils/seed.types.ts +++ b/database/scripts/utils/seed.types.ts @@ -28,7 +28,7 @@ export type SpecialMorphismRuleYaml = { proof: string } -export type PropertyEntry = { +type PropertyEntry = { property: string proof: string check_redundancy?: boolean @@ -54,6 +54,7 @@ export type StructureYaml = { tags: string[] related: string[] dual?: string + parent?: string satisfied_properties: PropertyEntry[] unsatisfied_properties: PropertyEntry[] undecidable_properties?: PropertyEntry[] @@ -63,8 +64,8 @@ export type StructureYaml = { export type CategoryYaml = StructureYaml & { objects: string morphisms: string - special_objects: Record - special_morphisms: Record + special_objects: Record + special_morphisms: Record } export type FunctorYaml = StructureYaml & { diff --git a/database/scripts/utils/structures.ts b/database/scripts/utils/structures.ts index 17c6848e..b6b91f6f 100644 --- a/database/scripts/utils/structures.ts +++ b/database/scripts/utils/structures.ts @@ -83,3 +83,17 @@ export function is_dual_structure( ): structure is StructureMeta & { dual: string } { return Boolean(structure.dual) && structure.name.toLowerCase().startsWith('dual') } + +/** + * Returns a map that assigns to each structure its parent, if present. + */ +export function get_structure_parent_map(db: Database, type: StructureType) { + const structures = db + .prepare< + [StructureType], + { id: string; parent: string | null } + >(`SELECT id, parent FROM structures WHERE type = ?`) + .all(type) + + return new Map(structures.map((structure) => [structure.id, structure.parent])) +} diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index 21266777..8fac8bf2 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -20,6 +20,9 @@ export type StructureDisplay = { dual_structure_id: string | null dual_structure_name: string | null dual_structure_notation: string | null + parent: string | null + parent_name: string | null + parent_notation: string | null } export type MappedTypes = Record @@ -120,6 +123,7 @@ export type StructureDetails = { type: StructureType structure: StructureDisplay related_structures: RelatedStructure[] + children: RelatedStructure[] tags: string[] satisfied_properties: PropertyAssignmentDisplay[] unsatisfied_properties: PropertyAssignmentDisplay[] diff --git a/src/lib/server/fetchers/structure.ts b/src/lib/server/fetchers/structure.ts index 0aab7b5b..b4727cb3 100644 --- a/src/lib/server/fetchers/structure.ts +++ b/src/lib/server/fetchers/structure.ts @@ -23,9 +23,13 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai s.nlab_link, s.dual_structure_id, ds.name AS dual_structure_name, - ds.notation AS dual_structure_notation + ds.notation AS dual_structure_notation, + s.parent, + ps.name AS parent_name, + ps.notation AS parent_notation FROM structures s LEFT JOIN structures ds ON ds.id = s.dual_structure_id + LEFT JOIN structures ps ON ps.id = s.parent WHERE s.id = ?` ) .get(id) @@ -37,13 +41,20 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai const related_structures = db .prepare<[string], RelatedStructure>( `SELECT - c.id, - c.name, - c.notation + s.id, + s.name, + s.notation FROM related_structures r - INNER JOIN structures c ON c.id = r.related_structure_id + INNER JOIN structures s ON s.id = r.related_structure_id WHERE r.structure_id = ? - ORDER BY lower(c.name)` + ORDER BY lower(s.name)` + ) + .all(id) + + const children = db + .prepare<[string], RelatedStructure>( + `SELECT s.id, s.name, s.notation + FROM structures s WHERE s.parent = ?` ) .all(id) @@ -134,6 +145,7 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai return { type, structure, + children, related_structures, tags, satisfied_properties, diff --git a/src/pages/StructureDetailPage.svelte b/src/pages/StructureDetailPage.svelte index 4b92293d..b117af77 100644 --- a/src/pages/StructureDetailPage.svelte +++ b/src/pages/StructureDetailPage.svelte @@ -21,6 +21,7 @@ type: StructureType structure: StructureDisplay related_structures: RelatedStructure[] + children: RelatedStructure[] tags: string[] satisfied_properties: PropertyAssignmentDisplay[] unsatisfied_properties: PropertyAssignmentDisplay[] @@ -37,6 +38,7 @@ type, structure, related_structures, + children, tags, satisfied_properties, unsatisfied_properties, @@ -65,6 +67,28 @@ {@render definition?.()} + {#if structure.parent} +
  • + Parent: + + {@html structure.parent_notation} + +
    • + {/if} + + {#if children.length} +
  • + Children: + {#each children as { id, name, notation }, i} + + {@html notation} + {#if i < children.length - 1} + ,  + {/if} + {/each} +
    • + {/if} + {#if related_structures.length}
  • Related {PLURALS[type]}: diff --git a/tests/categories.spec.ts b/tests/categories.spec.ts index b3717bb9..e2886367 100644 --- a/tests/categories.spec.ts +++ b/tests/categories.spec.ts @@ -172,6 +172,32 @@ test('user may see undecidable properties', async ({ page }) => { await expect(link).toBeVisible() }) +test('user may see properties that cannot be determined in a family of categories', async ({ + page +}) => { + await page.goto('/category/BG') + + await expect( + page.getByRole('heading', { + name: 'delooping of a group', + exact: true + }) + ).toBeVisible() + + const undecidable_properties_section = page + .locator('section', { + hasText: 'Undecidable properties' + }) + .first() + + const link = undecidable_properties_section.getByRole('link', { + name: 'finite', + exact: true + }) + + await expect(link).toBeVisible() +}) + test('user can navigate to a related category', async ({ page }) => { await page.goto('/category/FinSet', { waitUntil: 'networkidle' }) @@ -225,6 +251,47 @@ test('user can navigate to the dual category if it exists in the database', asyn await expect(page).toHaveURL('/category/Set_op') }) +test('user can navigate to a child category', async ({ page }) => { + await page.goto('/category/BG', { waitUntil: 'networkidle' }) + + await page + .getByRole('link', { + name: 'delooping of a non-trivial finite group', + exact: true + }) + .click() + + await expect( + page.getByRole('heading', { + name: 'delooping of a non-trivial finite group', + exact: true + }) + ).toBeVisible() + + await expect(page).toHaveURL('/category/BG_f') +}) + +test('user can navigate to a parent category', async ({ page }) => { + await page.goto('/category/Ring', { waitUntil: 'networkidle' }) + + await page + .getByRole('link', { + name: 'category of algebras', + exact: true + }) + .first() + .click() + + await expect( + page.getByRole('heading', { + name: 'category of algebras', + exact: true + }) + ).toBeVisible() + + await expect(page).toHaveURL('/category/Alg(R)') +}) + test('user can open and close a proof for a property of a category', async ({ page }) => { await page.goto('/category/Grp', { waitUntil: 'networkidle' }) @@ -295,6 +362,38 @@ test('user can open a proof for a deduced unsatisfied property of a category', a ).toBeVisible() }) +test('user can open a proof for an inherited satisfied property of a category', async ({ + page +}) => { + await page.goto('/category/Ab', { waitUntil: 'networkidle' }) + + const claim = page.locator('li', { has: page.getByText('is abelian') }) + + await expect(claim).toBeVisible() + + await claim.locator('button').click() + + const popup = page.locator('.popup').filter({ hasText: 'Proof' }) + + await expect(popup.getByText('This follows from the parent.')).toBeVisible() +}) + +test('user can open a proof for an inherited unsatisfied property of a category', async ({ + page +}) => { + await page.goto('/category/BG_f', { waitUntil: 'networkidle' }) + + const claim = page.locator('li', { has: page.getByText('is not thin') }) + + await expect(claim).toBeVisible() + + await claim.locator('button').click() + + const popup = page.locator('.popup').filter({ hasText: 'Proof' }) + + await expect(popup.getByText('This follows from the parent.')).toBeVisible() +}) + test('user sees functors associated with the given category', async ({ page }) => { await page.goto('/category/Ab', { waitUntil: 'networkidle' })