Add proof dependencies (WIP)

database/data/categories/Ab.yaml

@@ -22,6 +22,11 @@ related:
 satisfied_properties:
   - property: locally small
     proof: There is a forgetful functor $\Ab \to \Set$ and $\Set$ is locally small.
+    dependencies:
+      - id: Set
+        type: category
+        property: locally small
+        satisfied: true
 
   - property: abelian
     proof: This is standard, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. VIII.

database/data/categories/Ab_fg.yaml

@@ -17,9 +17,19 @@ related:
 satisfied_properties:
   - property: locally small
     proof: There is a forgetful functor $\FinAb \to \Set$ and $\Set$ is locally small.
+    dependencies:
+      - id: Set
+        type: category
+        property: locally small
+        satisfied: true
 
   - property: abelian
     proof: This follows from the fact for abelian groups and the fact that subgroups of finitely generated abelian groups are also finitely generated.
+    dependencies:
+      - id: Ab
+        type: category
+        property: abelian
+        satisfied: true
 
   - property: generator
     proof: The group $\IZ$ is a generator since it represents the forgetful functor to $\Set$.
@@ -29,6 +39,11 @@ satisfied_properties:
 
   - property: ℵ₁-accessible
     proof: The inclusion $\Ab_{\fg} \hookrightarrow \Ab$ is closed under $\aleph_1$-filtered colimits by <a href="https://mathoverflow.net/questions/400763/" target="_blank">MO/400763</a>. In particular, $\Ab_{\fg}$ has $\aleph_1$-filtered colimits. Since $\Ab_{\fg}$ is essentially small, there is a set $G$ such that every f.g. abelian group is isomorphic to one in $G$. So trivially it is also a $\aleph_1$-filtered colimit of such objects (take the constant diagram). Finally, every object is $\Ab_{\fg} = \Ab_{\fp}$ is finitely presentable in $\Ab$ and hence also in $\Ab_{\fg}$, a fortiori $\aleph_1$-presentable.
+    dependencies:
+      - id: Ab_fg
+        type: category
+        property: essentially small
+        satisfied: true
 
   - property: ℵ₁-cofiltered limits
     proof: A proof can be found <a href="/content/aleph1-cofiltered-limits-fg-groups">here</a>.

database/data/categories/Alg(R).yaml

@@ -17,6 +17,11 @@ related:
 satisfied_properties:
   - property: locally small
     proof: There is a forgetful functor $\Alg(R) \to \Set$ and $\Set$ is locally small.
+    dependencies:
+      - id: Set
+        type: category
+        property: locally small
+        satisfied: true
 
   - property: finitary algebraic
     proof: Take the algebraic theory of an $R$-algebra.
@@ -26,9 +31,19 @@ satisfied_properties:
 
   - property: disjoint finite products
     proof: One can take the same proof as for <a href="/category/Ring">$\Ring$</a>.
+    dependencies:
+      - id: Ring
+        type: category
+        property: disjoint finite products
+        satisfied: true
 
   - property: Malcev
     proof: This follows in the same way as for <a href="/category/Grp">$\Grp$</a>, see also Example 2.2.5 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>.
+    dependencies:
+      - id: Grp
+        type: category
+        property: Malcev
+        satisfied: true
 
 unsatisfied_properties:
   - property: skeletal
@@ -39,6 +54,11 @@ unsatisfied_properties:
 
   - property: semi-strongly connected
     proof: This is because already the full subcategory <a href="/category/CAlg(R)">$\CAlg(R)$</a> of commutative algebras is not semi-strongly connected.
+    dependencies:
+      - id: CAlg(R)
+        type: category
+        property: semi-strongly connected
+        satisfied: false
 
   - property: cogenerating set
     proof: 'We apply <a href="/content/missing_cogenerating_sets">this lemma</a> to the collection of $R$-algebras which are fields: If $F$ is an $R$-algebra that is also a field and $A$ is a non-trivial $R$-algebra, any algebra homomorphism $F \to A$ is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables over some residue field of $R$ has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).'
@@ -51,9 +71,23 @@ unsatisfied_properties:
 
   - property: coregular
     proof: 'We just need to tweak the proof for <a href="/category/Ring">$\Ring$</a>. 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 (<a href="https://math.stackexchange.com/questions/22629" target="_blank">proof</a>) or via a direct calculation with elementary matrices.'
+    dependencies:
+      - id: Ring
+        type: category
+        property: coregular
+        satisfied: false
 
   - property: regular quotient object classifier
     proof: We may copy the proof for <a href="/category/CAlg(R)">$\CRing$</a> (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 <a href="/content/subcategories">here</a> (dualized).
+    dependencies:
+      - id: CRing
+        type: category
+        property: regular quotient object classifier
+        satisfied: false
+      - id: CAlg(R)
+        type: category
+        property: regular quotient object classifier
+        satisfied: false
 
   - property: cocartesian cofiltered limits
     proof: >-
@@ -62,10 +96,20 @@ unsatisfied_properties:
       Because of $w_n \equiv w_{n-1} \bmod Y^n$ these form an element $w \in \lim_n (A \sqcup B_n)$. Expanding $w_n$, the longest term is $XY XY^2 \cdots X Y^n$ of "free product" length $2n$, which is unbounded.
 
   - property: cofiltered-limit-stable epimorphisms
-    proof: We already know that <a href="/category/CRing">$\CAlg(R)$</a> does not have this property. Now apply the contrapositive of the dual of Lemma 2 <a href="/content/subcategories">here</a> to the forgetful functor $\CAlg(R) \to \Alg(R)$. It preserves epimorphisms by <a href="https://math.stackexchange.com/questions/5133488" target="_blank">MSE/5133488</a>.
+    proof: We already know that <a href="/category/CAlg(R)">$\CAlg(R)$</a> does not have this property. Now apply the contrapositive of the dual of Lemma 2 <a href="/content/subcategories">here</a> to the forgetful functor $\CAlg(R) \to \Alg(R)$. It preserves epimorphisms by <a href="https://math.stackexchange.com/questions/5133488" target="_blank">MSE/5133488</a>.
+    dependencies:
+      - id: CAlg(R)
+        type: category
+        property: cofiltered-limit-stable epimorphisms
+        satisfied: false
 
   - property: effective cocongruences
     proof: 'The counterexample is similar to the one for <a href="/category/Ring">$\Ring$</a>: Let $X \coloneqq R[p] / (p^2-p)$ with cocongruence $E \coloneqq R \langle p, q \rangle / (p^2-p, q^2-q, pq-q, qp-p)$.'
+    dependencies:
+      - id: Ring
+        type: category
+        property: effective cocongruences
+        satisfied: false
 
 special_objects:
   initial object:

database/data/categories/B.yaml

@@ -17,9 +17,19 @@ related:
 satisfied_properties:
   - property: locally small
     proof: There is a forgetful functor $\IB \to \Set$ and $\Set$ is locally small.
+    dependencies:
+      - id: Set
+        type: category
+        property: locally small
+        satisfied: true
 
   - property: locally finite
     proof: There is a faithful functor $\IB \to \FinSet$ and <a href="/category/FinSet">$\FinSet$</a> is locally finite.
+    dependencies:
+      - id: FinSet
+        type: category
+        property: locally finite
+        satisfied: true
 
   - property: inhabited
     proof: This is trivial.

database/data/categories/BN.yaml

@@ -35,6 +35,15 @@ satisfied_properties:
 
   - property: locally cartesian closed
     proof: The slice category $B\IN / *$ is isomorphic to the poset $(\IN,\geq)$ (not to $(\IN,\leq)$). This category is thin and and semi-strongly connected, <a href="/category-implication/sequential_implies_lcc">hence</a> cartesian closed.
+    dependencies:
+      - id: N
+        type: category
+        property: thin
+        satisfied: true
+      - id: N
+        type: category
+        property: semi-strongly connected
+        satisfied: true
 
   - property: ℵ₁-accessible
     proof: A proof can be found <a href="/content/aleph1-filtered-colimits-in-deloopings">here</a> as Proposition 2.

database/data/categories/BOn.yaml

@@ -33,6 +33,15 @@ satisfied_properties:
 
   - property: locally cartesian closed
     proof: The slice category $B\On / *$ is isomorphic to the poset $(\On,\geq)$ (not to $(\On,\leq)$). This category is thin and and semi-strongly connected, <a href="/category-implication/sequential_implies_lcc">hence</a> cartesian closed.
+    dependencies:
+      - id: On
+        type: category
+        property: thin
+        satisfied: true
+      - id: On
+        type: category
+        property: semi-strongly connected
+        satisfied: true
 
   - property: ℵ₁-cofiltered
     proof: In fact, it is $\kappa$-cofiltered for every cardinal $\kappa$. By the dual of Theorem 2.2 at the <a href="https://ncatlab.org/nlab/show/filtered+category">nLab</a> it suffices to prove any set of objects has a cone (which is trivial in a one-object category) and that any set of parallel morphisms is equalized by some morphism. Here, this means that for every set of ordinals $A$ there is some ordinal $\beta$ such that $\alpha + \beta$ for $\alpha \in A$ does not depend on $\alpha$. Take $\beta$ to be any ordinal larger than $\sup(A)$ of the form $\omega^\gamma$. It is well-known that $\omega^\gamma$ has the property that $\alpha + \omega^\gamma = \omega^\gamma$ for all $\alpha < \omega^\gamma$ (Kunen's <i>Set Theory</i>, Exercise I.9.53), from which the claim follows.

database/data/categories/Ban.yaml

@@ -15,6 +15,11 @@ related:
 satisfied_properties:
   - property: locally small
     proof: There is a forgetful functor $\Ban \to \Set$ and $\Set$ is locally small.
+    dependencies:
+      - id: Set
+        type: category
+        property: locally small
+        satisfied: true
 
   - property: pointed
     proof: The trivial Banach space $\{0\}$ is a zero object.
@@ -31,9 +36,19 @@ satisfied_properties:
 
   - property: cartesian filtered colimits
     proof: If $X$ is a Banach space and $(Y_i)$ is a filtered diagram of Banach spaces, the canonical map $\colim_i (X \times Y_i) \to X \times \colim_i Y_i$ is the completion of the canonical map in the category of normed vector spaces with non-expansive linear maps. Now the claim follows directly from <a href="/category/Met">$\Met$</a>.
+    dependencies:
+      - id: Met
+        type: category
+        property: cartesian filtered colimits
+        satisfied: true
 
   - property: cocartesian cofiltered limits
     proof: 'If $X$ is a Banach space and $(Y_i)$ is a cofiltered diagram of Banach spaces, the canonical map $X \oplus \lim_i Y_i \to \lim_i (X \oplus Y_i)$ is an isomorphism: Since the forgetful functor $\Ban \to \Vect$ preserves finite coproducts and all limits, and $\Vect$ has the claimed property (see <a href="/category-implication/biproducts_cartesian_filtered_colimits">here</a>), the canonical map is bijective. It remains to show that it is isometric. For $(x,y) \in X \oplus \lim_i Y_i$ the norm in the domain is $|x| + \sup_i |y_i|$, and the norm in the codomain is $\sup_i (|x| + |y_i|)$, and these clearly agree.'
+    dependencies:
+      - id: Vect
+        type: category
+        property: cocartesian cofiltered limits
+        satisfied: true
 
   - property: regular
     proof: >-
@@ -91,6 +106,11 @@ satisfied_properties:
 
 
       Since $R \hookrightarrow X \times X$ is an isometry, $R$ is a closed subspace of $X \times X$. It follows that also $U$ is a closed subspace of $X$. Finally, $R$ is the kernel pair of the projection $X \to X/U$ since this is true by construction on the level of vector spaces and the kernel pair carries the $\max$-norm, just like $R$.
+    dependencies:
+      - id: Vect
+        type: category
+        property: effective congruences
+        satisfied: true
 
 unsatisfied_properties:
   - property: skeletal
@@ -111,6 +131,11 @@ unsatisfied_properties:
       $$\Hom(\Psi,X) \to S(X), \quad f \mapsto \overline{\im(f)}$$
       is bijective. In particular, there is a morphism $f : \Psi \to X$ with dense image, i.e. an epimorphism. But this contradicts the already established fact that $\Ban$ is well-copowered (since it is locally presentable).
       Alternatively, we may use that for every cardinal $\kappa$ the Banach space $\ell^2(\kappa^+)$ has no dense subset of size $\kappa$.
+    dependencies:
+      - id: Ban
+        type: category
+        property: well-copowered
+        satisfied: true
 
   - property: unital
     proof: The canonical morphism $X \sqcup Y \to X \times Y$ is injective, and therefore a monomorphism. Hence, if it were also a strong epimorphism, it would be an isomorphism. However, for example, when $X = Y = \IC$, the norms do not agree.
@@ -120,6 +145,11 @@ unsatisfied_properties:
 
   - property: filtered-colimit-stable monomorphisms
     proof: 'The proof is similar to <a href="/category/Met">$\Met$</a>. For $n \geq 1$ let $X_n$ be the Banach space with underlying vector space $\IC$ and the norm $|x|_n \coloneqq \frac{1}{n} |x|$. For $n \leq m$ the identity map provides a morphism $X_n \to X_m$, which is clearly a monomorphism (also an epimorphism by the way, but an isomorphism iff $n=m$). Let $X$ be the colimit of all $X_n$ in the category of semi-normed vector spaces. It is constructed as the colimit in the category of vector spaces with the semi-norm $|x| \coloneqq \inf \{|x|_m : n \leq m \}$ for $x \in X_n$. So clearly, the semi-norm is zero. Hence, the colimit in the category of normed vector spaces is $0$. The colimit in the category of Banach spaces is its completion, which is also $0$. Thus, the monomorphisms $X_1 \hookrightarrow X_n$ become the zero map $X_1 \to 0$ in the colimit, which is not a monomorphism.'
+    dependencies:
+      - id: Met
+        type: category
+        property: filtered-colimit-stable monomorphisms
+        satisfied: false
 
   - property: cofiltered-limit-stable epimorphisms
     proof: 'We show that epimorphisms are not stable under sequential limits. Let $X_n = Y_n = \IC$ for all $n \geq 0$, equipped with the usual norm. The transition morphism $Y_{n+1} \to Y_n$ is the identity, and the transition morphism $X_{n+1} \to X_n$ is $x \mapsto x/2$. The morphisms $X_n \to Y_n$, $x \mapsto x/2^n$ are compatible with the transitions, and they are surjective, hence epimorphisms. Now we check $\lim_n X_n = 0$: An element $(x_n) \in \lim_n X_n$ is a family of complex numbers satisfying $x_n = x_{n+1}/2$ <i>and</i> $\sup_n |x_n| < \infty$. But then $x_n = 2^n x_0$ and this can only be bounded when $x_0=0$. Hence, $0 = \lim_n X_n \to \lim_n Y_n = \IC$ is no epimorphism.'

database/data/categories/CAlg(R).yaml

@@ -17,6 +17,11 @@ related:
 satisfied_properties:
   - property: locally small
     proof: There is a forgetful functor $\CAlg(R) \to \Set$ and $\Set$ is locally small.
+    dependencies:
+      - id: Set
+        type: category
+        property: locally small
+        satisfied: true
 
   - property: finitary algebraic
     proof: Take the algebraic theory of a commutative ring.
@@ -27,9 +32,19 @@ satisfied_properties:
 
   - property: Malcev
     proof: This follows in the same way as for <a href="/category/Grp">$\Grp$</a>, see also Example 2.2.5 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>.
+    dependencies:
+      - id: Grp
+        type: category
+        property: Malcev
+        satisfied: true
 
   - property: coextensive
     proof: One can use the same proof as for <a href="/category/CRing">$\CRing$</a>.
+    dependencies:
+      - id: CRing
+        type: category
+        property: coextensive
+        satisfied: true
 
 unsatisfied_properties:
   - property: skeletal
@@ -55,6 +70,11 @@ unsatisfied_properties:
 
   - property: regular quotient object classifier
     proof: 'The strategy is similar to the one for <a href="/category/CRing">$\CRing$</a>: Assume that $P \to R$ is a regular quotient object classifier. If $J$ denotes the kernel of $P \to R$, every ideal $I \subseteq A$ of any commutative $R$-algebra has the form $I = \langle \varphi(J) \rangle$ for a unique homomorphism $\varphi : P \to A$. If $\sigma : A \to A$ is an automorphism with $\sigma(I)=I$, then uniqueness gives us $\sigma \circ \varphi = \varphi$, which means that $\varphi(J)$ lies in $A^{\sigma}$, the fixed algebra of $\sigma$. But then $I$ is generated by elements in $A^{\sigma} \cap I$. If $K$ is a residue field of $R$, this fails for $A = K[X,Y]$, $I = \langle X,Y \rangle$, $\sigma(X)=Y$, $\sigma(Y)=X$. The fixed algebra is the subalgebra of symmetric polynomials, which is $K[X+Y,XY]$. So $\langle X,Y \rangle$ is generated by symmetric polynomials without constant term, which implies $\langle X,Y \rangle \subseteq \langle X+Y,XY \rangle$ in $K[X,Y]$. But reducing an equation like $X = a(X,Y) \cdot (X+Y) + b(X,Y) \cdot (XY)$ modulo $\langle X^2,Y^2,XY \rangle$ yields a contradiction.'
+    dependencies:
+      - id: CRing
+        type: category
+        property: regular quotient object classifier
+        satisfied: false
 
   - property: cofiltered-limit-stable epimorphisms
     proof: Let $K$ be a field over $R$. Consider the sequence of projections $\cdots \to K[X]/\langle X^2 \rangle \to K[X]/\langle X \rangle$ and the constant sequence $\cdots \to K[X] \to K[X]$. The surjective homomorphisms $K[X] \to K[X]/\langle X^n \rangle$ induce the inclusion $K[X] \hookrightarrow K[[X]]$ in the limit, where $K[[X]]$ is the algebra of formal power series. It is clearly not surjective, but this is not sufficient, we need to argue that it is not an epimorphism in $\CAlg(R)$, or equivalently, in $\CRing$. For a proof, see <a href="https://math.stackexchange.com/questions/2391187" target="_blank">MSE/2391187</a>.