diff --git a/.cspell.json b/.cspell.json index df0c55dd..50979502 100644 --- a/.cspell.json +++ b/.cspell.json @@ -193,6 +193,7 @@ "morphisms", "Multialgébriques", "naturality", + "Nekoma", "Neves", "Niefield", "nilradical", diff --git a/content/Meas_not_regular.md b/content/Meas_not_regular.md new file mode 100644 index 00000000..b4f8e72c --- /dev/null +++ b/content/Meas_not_regular.md @@ -0,0 +1,28 @@ +--- +title: The category of measurable spaces is not regular +description: An example of a quotient measurable map is given whose product with itself is not a quotient map anymore. +author: Nekoma +--- + +## $\Meas$ is not regular + +::: Claim +The category $\Meas$ of measurable spaces and measurable maps is not regular. +::: + +_Proof._ +In a regular category, regular epimorphisms are stable under pullbacks and compositions (see Prop. 3.7 at the [nLab](https://ncatlab.org/nlab/show/regular+epimorphism)), which implies that for every regular epimorphism $f : X \to Y$ also $f \times f : X \times X \to Y \times Y$ is a regular epimorphism. We will show that this fails in $\Meas$. + +Let $X \coloneqq [0, 1)$ equipped with the standard Borel $\sigma$-algebra $\B$. Consider the equivalence relation $x \sim y \iff x-y \in \IQ$, let $Y \coloneqq X /{\sim}$ be the set of equivalence classes, and $f: X \to Y$ be the natural projection map. Equip $Y$ with the quotient $\sigma$-algebra $\Sigma_Y$, so that $f$ is a regular epimorphism. + +Now consider the diagonal in the quotient space $\Delta_Y \coloneqq \{(y, y) \mid y \in Y\}$. Then +$$\textstyle (f \times f)^{-1}(\Delta_Y) = \{(x_1, x_2) \in [0, 1)^2 \mid x_1 - x_2 \in \IQ\} \eqqcolon \bigcup_{q \in \IQ} L_q$$ +where each $L_q$ is the intersection of the diagonal level sets of $x_1 - x_2$ with $[0, 1)^2$. Because each line is closed in $\IR^2$, its intersection with $[0, 1)^2$ is a Borel set in $X \times X$. Since a countable union of Borel sets is Borel, $(f \times f)^{-1}(\Delta_Y) \in \B \otimes \B$. + +Now take any set $B \in \Sigma_Y$. Its preimage $f^{-1}(B)$ is a Borel set in $[0, 1)$ that is invariant under rational translations modulo 1. Because the action of $\IQ / \IZ$ on $[0, 1)$ is ergodic, the Lebesgue measure $\lambda(f^{-1}(B))$ must be exactly $0$ or $1$. Assume for contradiction that $\Sigma_Y$ is countably separated, i.e. there exists a countable sequence of measurable sets $(B_n)_{n \geq 1}$ in $\Sigma_Y$ that separates the points of $Y$. Let $A_n \coloneqq f^{-1}(B_n)$. Every $A_n$ has $\lambda(A_n) = 0$ or $\lambda(A_n) = 1$. + +Define a "bad set" $N \subseteq [0, 1)$ as +$$\textstyle N \coloneqq \left( \bigcup_{\lambda(A_n)=0} A_n \right) \cup \left( \bigcup_{\lambda(A_n)=1} A_n^c \right)$$ +Because $N$ is a countable union of sets with measure $0$, we have $\lambda(N) = 0$, and thus $\lambda([0, 1) \setminus N)=1$. For any two points $x, y \in [0, 1) \setminus N$, clearly $x \in A_n \iff y \in A_n$ for every $n$. Consequently, the sequence $(B_n)$ fails to separate $f(x)$ and $f(y)$. Hence, $x \sim y$. Since $[0, 1) \setminus N$ has measure $1$, it is uncountable. Because each equivalence class is only countable, these uncountably many points must belong to uncountably many different equivalence classes. Thus, we can easily pick $x, y \in [0, 1) \setminus N$ where $x \not\sim y$. Thus $\Sigma_Y$ is not countably separated. + +Hence by Theorem 6.5.7 in Bogachev's [Measure theory](https://link.springer.com/book/10.1007/978-3-540-34514-5) $\Delta_Y \notin \Sigma_Y \otimes \Sigma_Y$. We have identified a non-measurable subset of $Y \times Y$ whose preimage under $f \times f$ is measurable. Therefore, $f \times f$ is not a regular epimorphism. $\square$ diff --git a/content/aleph1-filtered-colimits-in-deloopings.md b/content/aleph1-filtered-colimits-in-deloopings.md new file mode 100644 index 00000000..45d618cb --- /dev/null +++ b/content/aleph1-filtered-colimits-in-deloopings.md @@ -0,0 +1,119 @@ +--- +title: ℵ₁-filtered colimits in deloopings +description: We give a detailed proof that the delooping of the monoid of natural numbers, and likewise the delooping of the large monoid of ordinal numbers, has colimits indexed by ℵ₁-filtered categories. +author: Martin Brandenburg +--- + +# $\aleph_1$-filtered colimits in deloopings + +Every (possibly large) monoid $M$ induces a category $BM$ with just one object. We will show that this category has $\aleph_1$-filtered colimits in the cases $M = \IN$ and $M = \On$ (both respect to addition). + +::: Proposition 1 +The category $B\IN$ has $\aleph_1$-filtered colimits. +::: + +_Proof._ +Let $D : \I \to B\IN$ be an $\aleph_1$-filtered diagram. Every two parallel morphisms $i \rightrightarrows j$ are mapped to the same morphism in $B \IN$, because they are coequalized by some morphism and $(\IN,+)$ is cancellative. Hence, $D$ factors through the preorder reflection of $\I$, and we may therefore assume that $\I$ itself is a preorder. Thus, the diagram consists of numbers $D(i,j) \in \IN$ for all $i \leq j$ satisfying + +$$D(j,k) + D(i,j) = D(i,k)$$ + +for all $i \leq j \leq k$. In particular, $D(i,j) \leq D(i,k)$. + +Let $i \in \I$. The set of natural numbers $\{D(i,k) : k \geq i\}$ is bounded above. Otherwise, for every $n \in \IN$ we could find $k_n \in \I$ with $k_n \geq i$ and $D(i,k_n) \geq n$. Since $\I$ is $\aleph_1$-filtered, the family $(k_n)_{n \in \IN}$ has an upper bound $k_\infty \in \I$. But then + +$$D(i, k_\infty) = D(k_n,k_\infty) + D(i, k_n) \geq D(i, k_n) \geq n$$ + +for all $n \in \IN$, contradicting the fact that $D(i,k_\infty) \in \IN$. + +Therefore, the maximum + +$$u_i \coloneqq \max \{D(i,k) : k \geq i\} \in \IN$$ + +is well-defined, which we regard as a morphism in $B\IN$. For $i \leq j$ we compute + +$$ +\begin{align*} +u_i & = \max \{D(i,k) : k \geq i\} \\ +& = \max \{D(i,k) : k \geq j\} \\ +& = \max \{ D(j,k) + D(i,j) : k \geq j\} \\ +& = \max \{D(j,k) : k \geq j\} + D(i,j)\\ +& = u_j + D(i,j), +\end{align*} +$$ + +showing that $(u_i)$ defines a cocone. It is universal: let $(v_i)$ be another cocone, i.e. $v_i \in \IN$ and $v_i = v_j + D(i,j)$ for all $i \leq j$. Then $v_i \geq D(i,j)$ for all $i \leq j$, hence $v_i \geq u_i$. Write $v_i = w_i + u_i$ for some uniquely determined $w_i \in \IN$. For $i \leq j$ we compute + +$$w_j + u_j + D(i,j) = v_j + D(i,j) = v_i = w_i + u_i = w_i + u_j + D(i,j),$$ + +hence $w_j = w_i$. Therefore, the $w_i$ are constant, and the required factorization follows. $\square$ + +::: Proposition 2 +The category $B\IN$ is $\aleph_1$-accessible. +::: + +_Proof._ +Based on Proposition 1, it remains to show that the unique object $*$ is $\aleph_1$-presentable, i.e. that for every diagram $D : \I \to B\IN$ as above, the canonical map + +$$\alpha : \colim_{i \in \I} \Hom(*,D(i)) \to \Hom(*,\colim_{i \in \I} D(i))$$ + +is bijective. On objects, we necessarily have $D(i)=*$ and $\colim_{i \in \I} D(i)=*$. Hence, the codomain of $\alpha$ is simply $\IN$, while the domain consists of equivalence classes $[i,n]$ of pairs $(i,n) \in \I \times \IN$, where $(i,n) \sim (j,m)$ iff there exists some $k \geq i,j$ such that + +$$D(i,k) + n = D(j,k) + m.$$ + +By the construction of the colimit cocone, we have + +$$\alpha([i,n]) = u_i + n = \max \{D(i,j) : j \geq i\} + n.$$ + +(1) **The map $\alpha$ is surjective:** Pick some $i \in \I$. Choose $j \geq i$ such that $u_i = D(i,j)$. For all $k \geq j$ we then have + +$$u_i \geq D(i,k) = D(j,k) + D(i,j) = D(j,k) + u_i,$$ + +hence $D(j,k)=0$. Therefore, $u_j=0$, and thus $\alpha([j,n]) = n$ for all $n \in \IN$. + +(2) **The map $\alpha$ is injective:** Assume that $[i,n]$ and $[j,m]$ have the same image. Since $\I$ is filtered, we may assume $i=j$. The condition then becomes $u_i + n = u_i + m$, and therefore $n=m$. This completes the proof. $\square$ + +::: Proposition 3 +The category $B\On$ has $\aleph_1$-filtered colimits. +::: + +_Proof._ +The proof is similar to $B\IN$. Let $\I$ be an $\aleph_1$-filtered small category and $D : \I \to B\On$ a diagram. A cocone $\lambda = (\lambda_i)_{i \in \I}$ for $D$ is a family of ordinals satisfying $\lambda_i = \lambda_j + D(f)$ for every morphism $f: i \to j$ in $\I$. + +We first observe that $D$ factors uniquely through the preorder reflection of $\I$. Indeed, any two parallel morphisms in $\I$ are coequalized by some morphism, and $B\On$ is left cancellative. Thus, we may assume that $\I$ is a preorder. Each inequality $i \leq j$ in $\I$ is mapped to an ordinal number $\alpha_{i,j} \coloneqq D(i \to j)$, and these numbers satisfy +$$\alpha_{i,k} = \alpha_{j,k} + \alpha_{i,j}$$ +for all $i \leq j \leq k$. In particular, $\alpha_{i,j} \leq \alpha_{i,k}$. + +For fixed $i \in \I$, the collection $\{\alpha_{i,j} : j \geq i\}$ is a set of ordinals because $\I$ is small, hence bounded above in $\On$. We claim that it has a maximum element. Otherwise, we can find a countable chain $i = j_0 \leq j_1 \leq j_2 \leq \dotsc$ in $\I$ such that $\alpha_{i,j_n} < \alpha_{i,j_{n+1}}$ for all $n \in \IN$. Since $\I$ is $\aleph_1$-filtered, there is an upper bound $j_\infty \in \I$ of $(j_n)_{n \in \IN}$. For each $n \in \IN$, the equation +$$\alpha_{i,j_{n+1}} = \alpha_{j_n,j_{n+1}} + \alpha_{i,j_n}$$ +implies that $\alpha_{j_n,j_{n+1}} > 0$. Hence, +$$\alpha_{j_n,j_\infty} = \alpha_{j_{n+1},j_\infty} + \alpha_{j_n,j_{n+1}} > \alpha_{j_{n+1},j_\infty},$$ +so $(\alpha_{j_n,j_\infty})_{n \in \IN}$ is a strictly decreasing infinite sequence of ordinals, contradicting the well-foundedness of $\On$. Thus, the maximum +$$u_i \coloneqq \max \{ \alpha_{i,j} : j \geq i \}$$ +is a well-defined ordinal number, which we regard as a morphism in $B\On$. The family $(u_i)_{i \in \I}$ forms a cocone for $D$, since for all $i \leq j$ we have + +$$ +\begin{align*} +u_i & = \max \{ \alpha_{i,k} : k \geq i \} \\ +& = \max \{ \alpha_{i,k} : k \geq j \} \\ +& = \max \{ \alpha_{j,k} + \alpha_{i,j} : k \geq j \} \\ +& = \max \{ \alpha_{j,k} : k \geq j \} + \alpha_{i,j} \\ +& = u_j + \alpha_{i,j}. +\end{align*} +$$ + +To establish the universal property, let $(\lambda_i)_{i \in \I}$ be any cocone for $D$, so that $\lambda_i = \lambda_j + \alpha_{i,j}$ for all $i \leq j$. The cocone relation $u_i = u_j + \alpha_{i,j}$ implies that $u_i \geq u_j$ whenever $i \leq j$. By the well-foundedness of $\On$, there exists $i_0 \in \I$ such that $u_j = u_{i_0}$ for all $j \geq i_0$. For such $j$, the relation +$$u_{i_0} = u_j + \alpha_{i_0,j} = u_{i_0} + \alpha_{i_0,j}$$ +forces $\alpha_{i_0,j} = 0$. Consequently, +$$u_{i_0} = \max \{ \alpha_{i_0,j} : j \geq i_0 \} = 0.$$ +Define the mediating morphism to be the ordinal $\kappa \coloneqq \lambda_{i_0}$. We must show that $\lambda_i = \kappa + u_i$ for all $i \in \I$. Choose $j \in \I$ with $j \geq i$ and $j \geq i_0$. Since $j \geq i_0$, we have $u_j = 0$ and $\alpha_{i_0,j} = 0$. The cocone condition for $\lambda$ gives +$$\kappa = \lambda_{i_0} = \lambda_j + \alpha_{i_0,j} = \lambda_j.$$ +Applying the cocone conditions for $u$ and $\lambda$ to $i \leq j$, we obtain +$$u_i = u_j + \alpha_{i,j} = 0 + \alpha_{i,j} = \alpha_{i,j}$$ +and +$$\lambda_i = \lambda_j + \alpha_{i,j} = \kappa + \alpha_{i,j} = \kappa + u_i.$$ +This proves the existence of the mediating morphism. + +For uniqueness, suppose $\kappa'$ is any ordinal satisfying $\lambda_i = \kappa' + u_i$ for all $i \in \I$. Evaluating at $i_0$ yields +$$\lambda_{i_0} = \kappa' + u_{i_0} = \kappa' + 0 = \kappa',$$ +hence $\kappa' = \kappa$. Therefore, the cocone $(u_i)_{i \in \I}$ is the colimit of $D$ in $B\On$. +$\square$ diff --git a/content/thin_algebraic_categories.md b/content/thin_algebraic_categories.md index b48b5ff7..13b1f5b4 100644 --- a/content/thin_algebraic_categories.md +++ b/content/thin_algebraic_categories.md @@ -7,8 +7,8 @@ author: Martin Brandenburg ## Algebraic categories are "never" thin ::: Lemma -Let $\C$ be a [thin](/category-property/thin) and [finitary algebraic](/category-property/finitary_algebraic) category. Then $\C \simeq 1$ or $\C \simeq \{0 < 1\}$. +Let $\C$ be a [thin](/category-property/thin) and [finitary algebraic](/category-property/finitary_algebraic) category. Then $\C \simeq 1$ or $\C \simeq I$, where $I$ is the walking morphism. ::: _Proof._ -Let $F : \Set \to \C$ denote the free algebra functor. Every object $A \in \C$ admits a regular epimorphism $F(X) \twoheadrightarrow A$ for some set $X$. But since $\C$ is thin, every regular epimorphism must be an isomorphism. Thus, $A \cong F(X)$. Also, $F(X)$ is a coproduct of copies of $F(1)$, which means it is either the initial object $0$ or $F(1)$ itself (since $\C$ is thin). If $F(1) \cong 0$, then every object is isomorphic to the initial object $0$, and hence $\C$ is trivial. If not, then $\C$ has exactly two objects up to isomorphism, $0$ and $F(1)$, there is a morphism $0 \to F(1)$, but no morphism $F(1) \to 0$. Since $\C$ is thin, we conclude $\C \simeq \{0 \to 1\}$. $\square$ +Let $F : \Set \to \C$ denote the free algebra functor. Every object $A \in \C$ admits a regular epimorphism $F(X) \twoheadrightarrow A$ for some set $X$. But since $\C$ is thin, every regular epimorphism must be an isomorphism. Thus, $A \cong F(X)$. Also, $F(X)$ is a coproduct of copies of $F(1)$, which means it is either the initial object $0$ or $F(1)$ itself (since $\C$ is thin). If $F(1) \cong 0$, then every object is isomorphic to the initial object $0$, and hence $\C$ is trivial. If not, then $\C$ has exactly two objects up to isomorphism, $0$ and $F(1)$, there is a morphism $0 \to F(1)$, but no morphism $F(1) \to 0$. Since $\C$ is thin, we conclude $\C \simeq I$. $\square$ diff --git a/databases/catdat/data/categories/BN.yaml b/databases/catdat/data/categories/BN.yaml index 75f0954a..44a1b7c1 100644 --- a/databases/catdat/data/categories/BN.yaml +++ b/databases/catdat/data/categories/BN.yaml @@ -40,44 +40,8 @@ satisfied_properties: - property: locally cartesian closed proof: The slice category $B\IN / *$ is isomorphic to the poset $(\IN,\geq)$ (not to $(\IN,\leq)$). This category is thin and and semi-strongly connected, hence cartesian closed. - - property: ℵ₁-filtered colimits - proof: >- - Let $D : \I \to B\IN$ be an $\aleph_1$-filtered diagram. Every two parallel morphisms $i \rightrightarrows j$ are mapped to the same morphism in $B \IN$, because they are coequalized by some morphism and $(\IN,+)$ is cancellative. Hence, $D$ factors through the preorder reflection of $\I$, and we may therefore assume that $\I$ itself is a preorder. Thus, the diagram consists of numbers $D(i,j) \in \IN$ for all $i \leq j$ satisfying - $$D(j,k) + D(i,j) = D(i,k)$$ - for all $i \leq j \leq k$. In particular, $D(i,j) \leq D(i,k)$. - - Let $i \in \I$. The set of natural numbers $\{D(i,k) : k \geq i\}$ is bounded above. Otherwise, for every $n \in \IN$ we could find $k_n \in \I$ with $k_n \geq i$ and $D(i,k_n) \geq n$. Since $\I$ is $\aleph_1$-filtered, the family $(k_n)_{n \in \IN}$ has an upper bound $k_\infty \in \I$. But then - $$D(i, k_\infty) = D(k_n,k_\infty) + D(i, k_n) \geq D(i, k_n) \geq n$$ - for all $n \in \IN$, contradicting the fact that $D(i,k_\infty) \in \IN$. - - Therefore, the maximum - $$u_i \coloneqq \max \{D(i,k) : k \geq i\} \in \IN$$ - is well-defined, which we regard as a morphism in $B\IN$. For $i \leq j$ we compute - $$\begin{align*} - u_i & = \max \{D(i,k) : k \geq i\} \\ - & = \max \{D(i,k) : k \geq j\} \\ - & = \max \{ D(j,k) + D(i,j) : k \geq j\} \\ - & = \max \{D(j,k) : k \geq j\} + D(i,j)\\ - & = u_j + D(i,j), - \end{align*}$$ - showing that $(u_i)$ defines a cocone. It is universal: let $(v_i)$ be another cocone, i.e. $v_i \in \IN$ and $v_i = v_j + D(i,j)$ for all $i \leq j$. Then $v_i \geq D(i,j)$ for all $i \leq j$, hence $v_i \geq u_i$. Write $v_i = w_i + u_i$ for some uniquely determined $w_i \in \IN$. For $i \leq j$ we compute - $$w_j + u_j + D(i,j) = v_j + D(i,j) = v_i = w_i + u_i = w_i + u_j + D(i,j),$$ - hence $w_j = w_i$. Therefore, the $w_i$ are constant, and the required factorization follows. - check_redundancy: false - - property: ℵ₁-accessible - proof: >- - We continue the proof that $\aleph_1$-filtered colimits exist. It remains to show that the unique object $*$ is $\aleph_1$-presentable, i.e. that for every diagram $D : \I \to B\IN$ as above, the canonical map - $$\alpha : \colim_{i \in \I} \Hom(*,D(i)) \to \Hom(*,\colim_{i \in \I} D(i))$$ - is bijective. On objects, we necessarily have $D(i)=*$ and $\colim_{i \in \I} D(i)=*$. Hence, the codomain of $\alpha$ is simply $\IN$, while the domain consists of equivalence classes $[i,n]$ of pairs $(i,n) \in \I \times \IN$, where $(i,n) \sim (j,m)$ iff there exists some $k \geq i,j$ such that - $$D(i,k) + n = D(j,k) + m.$$ - By the construction of the colimit cocone, we have - $$\alpha([i,n]) = u_i + n = \max \{D(i,j) : j \geq i\} + n.$$ - (1) The map $\alpha$ is surjective: Pick some $i \in \I$. Choose $j \geq i$ such that $u_i = D(i,j)$. For all $k \geq j$ we then have - $$u_i \geq D(i,k) = D(j,k) + D(i,j) = D(j,k) + u_i,$$ - hence $D(j,k)=0$. Therefore, $u_j=0$, and thus $\alpha([j,n]) = n$ for all $n \in \IN$. - - (2) The map $\alpha$ is injective: Assume that $[i,n]$ and $[j,m]$ have the same image. Since $\I$ is filtered, we may assume $i=j$. The condition then becomes $u_i + n = u_i + m$, and therefore $n=m$. This completes the proof. + proof: A proof can be found here as Proposition 2. unsatisfied_properties: - property: one-way diff --git a/databases/catdat/data/categories/BOn.yaml b/databases/catdat/data/categories/BOn.yaml index 5d8f0899..04ee602d 100644 --- a/databases/catdat/data/categories/BOn.yaml +++ b/databases/catdat/data/categories/BOn.yaml @@ -45,45 +45,7 @@ satisfied_properties: proof: In fact, it is $\kappa$-cofiltered for every cardinal $\kappa$. By the dual of Theorem 2.2 at the nLab it suffices to prove any set of objects has a cone (which is trivial in a one-object category) and that any set of parallel morphisms is equalized by some morphism. Here, this means that for every set of ordinals $A$ there is some ordinal $\beta$ such that $\alpha + \beta$ for $\alpha \in A$ does not depend on $\alpha$. Take $\beta$ to be any ordinal larger than $\sup(A)$ of the form $\omega^\gamma$. It is well-known that $\omega^\gamma$ has the property that $\alpha + \omega^\gamma = \omega^\gamma$ for all $\alpha < \omega^\gamma$ (Kunen's Set Theory, Exercise I.9.53), from which the claim follows. - property: ℵ₁-filtered colimits - proof: >- - The proof is similar to $B\IN$. Let $\I$ be an $\aleph_1$-filtered small category and $D : \I \to B\On$ a diagram. A cocone $\lambda = (\lambda_i)_{i \in \I}$ for $D$ is a family of ordinals satisfying $\lambda_i = \lambda_j + D(f)$ for every morphism $f: i \to j$ in $\I$. - - - We first observe that $D$ factors uniquely through the preorder reflection of $\I$. Indeed, any two parallel morphisms in $\I$ are coequalized by some morphism, and $B\On$ is left cancellative. Thus, we may assume that $\I$ is a preorder. Each inequality $i \leq j$ in $\I$ is mapped to an ordinal number $\alpha_{i,j} \coloneqq D(i \to j)$, and these numbers satisfy - $$\alpha_{i,k} = \alpha_{j,k} + \alpha_{i,j}$$ - for all $i \leq j \leq k$. In particular, $\alpha_{i,j} \leq \alpha_{i,k}$. - - - For fixed $i \in \I$, the collection $\{\alpha_{i,j} : j \geq i\}$ is a set of ordinals because $\I$ is small, hence bounded above in $\On$. We claim that it has a maximum element. Otherwise, we can find a countable chain $i = j_0 \leq j_1 \leq j_2 \leq \dotsc$ in $\I$ such that $\alpha_{i,j_n} < \alpha_{i,j_{n+1}}$ for all $n \in \IN$. Since $\I$ is $\aleph_1$-filtered, there is an upper bound $j_\infty \in \I$ of $(j_n)_{n \in \IN}$. For each $n \in \IN$, the equation - $$\alpha_{i,j_{n+1}} = \alpha_{j_n,j_{n+1}} + \alpha_{i,j_n}$$ - implies that $\alpha_{j_n,j_{n+1}} > 0$. Hence, - $$\alpha_{j_n,j_\infty} = \alpha_{j_{n+1},j_\infty} + \alpha_{j_n,j_{n+1}} > \alpha_{j_{n+1},j_\infty},$$ - so $(\alpha_{j_n,j_\infty})_{n \in \IN}$ is a strictly decreasing infinite sequence of ordinals, contradicting the well-foundedness of $\On$. Thus, the maximum - $$u_i \coloneqq \max \{ \alpha_{i,j} : j \geq i \}$$ - is a well-defined ordinal number, which we regard as a morphism in $B\On$. The family $(u_i)_{i \in \I}$ forms a cocone for $D$, since for all $i \leq j$ we have - $$\begin{align*} - u_i & = \max \{ \alpha_{i,k} : k \geq i \} \\ - & = \max \{ \alpha_{i,k} : k \geq j \} \\ - & = \max \{ \alpha_{j,k} + \alpha_{i,j} : k \geq j \} \\ - & = \max \{ \alpha_{j,k} : k \geq j \} + \alpha_{i,j} \\ - & = u_j + \alpha_{i,j}. - \end{align*}$$ - To establish the universal property, let $(\lambda_i)_{i \in \I}$ be any cocone for $D$, so that $\lambda_i = \lambda_j + \alpha_{i,j}$ for all $i \leq j$. The cocone relation $u_i = u_j + \alpha_{i,j}$ implies that $u_i \geq u_j$ whenever $i \leq j$. By the well-foundedness of $\On$, there exists $i_0 \in \I$ such that $u_j = u_{i_0}$ for all $j \geq i_0$. For such $j$, the relation - $$u_{i_0} = u_j + \alpha_{i_0,j} = u_{i_0} + \alpha_{i_0,j}$$ - forces $\alpha_{i_0,j} = 0$. Consequently, - $$u_{i_0} = \max \{ \alpha_{i_0,j} : j \geq i_0 \} = 0.$$ - Define the mediating morphism to be the ordinal $\kappa \coloneqq \lambda_{i_0}$. We must show that $\lambda_i = \kappa + u_i$ for all $i \in \I$. Choose $j \in \I$ with $j \geq i$ and $j \geq i_0$. Since $j \geq i_0$, we have $u_j = 0$ and $\alpha_{i_0,j} = 0$. The cocone condition for $\lambda$ gives - $$\kappa = \lambda_{i_0} = \lambda_j + \alpha_{i_0,j} = \lambda_j.$$ - Applying the cocone conditions for $u$ and $\lambda$ to $i \leq j$, we obtain - $$u_i = u_j + \alpha_{i,j} = 0 + \alpha_{i,j} = \alpha_{i,j}$$ - and - $$\lambda_i = \lambda_j + \alpha_{i,j} = \kappa + \alpha_{i,j} = \kappa + u_i.$$ - This proves the existence of the mediating morphism. - - - For uniqueness, suppose $\kappa'$ is any ordinal satisfying $\lambda_i = \kappa' + u_i$ for all $i \in \I$. Evaluating at $i_0$ yields - $$\lambda_{i_0} = \kappa' + u_{i_0} = \kappa' + 0 = \kappa',$$ - hence $\kappa' = \kappa$. Therefore, the cocone $(u_i)_{i \in \I}$ is the colimit of $D$ in $B\On$. + proof: A proof can be found here as Proposition 3. unsatisfied_properties: - property: initial object diff --git a/databases/catdat/data/categories/Cat.yaml b/databases/catdat/data/categories/Cat.yaml index bd8767aa..3d1f40ef 100644 --- a/databases/catdat/data/categories/Cat.yaml +++ b/databases/catdat/data/categories/Cat.yaml @@ -28,7 +28,7 @@ satisfied_properties: proof: Every non-empty category is weakly terminal (by using constant functors). - property: generator - proof: 'The interval category $\{0 \to 1\}$ is a generator: Assume that $F,G : \C \rightrightarrows \D$ are functors that agree when being precomposed with any functor from $\{0 \to 1\}$. This means that $F(f) = G(f)$ for all morphisms $f : X \to Y$ in $\C$. By comparing the domains and applying this to $f = \id_X$, we see that $F(X) = G(X)$ for all objects $X$. And we just saw that $F,G$ also agree on morphisms.' + proof: 'The walking morphism $I$ is a generator: Assume that $F,G : \C \rightrightarrows \D$ are functors that agree when being precomposed with any functor from $I$. This means that $F(f) = G(f)$ for all morphisms $f : X \to Y$ in $\C$. By comparing the domains and applying this to $f = \id_X$, we see that $F(X) = G(X)$ for all objects $X$. And we just saw that $F,G$ also agree on morphisms.' - property: infinitary extensive proof: '[Sketch] This is straight forward from the fact that $\Set$ is infinitary extensive: A functor $\C \to \coprod_i \D_i$ yields full subcategories $\C_i \subseteq \C$ (the preimages of $\D_i)$ with $\C = \coprod_i \C_i$.' diff --git a/databases/catdat/data/categories/Meas.yaml b/databases/catdat/data/categories/Meas.yaml index 6200cb0a..c9710ff5 100644 --- a/databases/catdat/data/categories/Meas.yaml +++ b/databases/catdat/data/categories/Meas.yaml @@ -69,27 +69,7 @@ unsatisfied_properties: proof: 'The proof is similar to the one for $\Top$: Use the trivial $\sigma$-algebra on a two-point set.' - property: regular - proof: >- - In a regular category, regular epimorphisms are stable under pullbacks and compositions (see Prop. 3.7 at the nLab), which implies that for every regular epimorphism $f : X \to Y$ also $f \times f : X \times X \to Y \times Y$ is a regular epimorphism. We will show that this fails in $\Meas$. - - - Let $X \coloneqq [0, 1)$ equipped with the standard Borel $\sigma$-algebra $\B$. Consider the equivalence relation $x \sim y \iff x-y \in \IQ$, let $Y \coloneqq X /{\sim}$ be the set of equivalence classes, and $f: X \to Y$ be the natural projection map. Equip $Y$ with the quotient $\sigma$-algebra $\Sigma_Y$, so that $f$ is a regular epimorphism. - - - Now consider the diagonal in the quotient space $\Delta_Y \coloneqq \{(y, y) \mid y \in Y\}$. Then - $$\textstyle (f \times f)^{-1}(\Delta_Y) = \{(x_1, x_2) \in [0, 1)^2 \mid x_1 - x_2 \in \IQ\} \eqqcolon \bigcup_{q \in \IQ} L_q$$ - where each $L_q$ is the intersection of the diagonal level sets of $x_1 - x_2$ with $[0, 1)^2$. Because each line is closed in $\IR^2$, its intersection with $[0, 1)^2$ is a Borel set in $X \times X$. Since a countable union of Borel sets is Borel, $(f \times f)^{-1}(\Delta_Y) \in \B \otimes \B$. - - - Now take any set $B \in \Sigma_Y$. Its preimage $f^{-1}(B)$ is a Borel set in $[0, 1)$ that is invariant under rational translations modulo 1. Because the action of $\IQ / \IZ$ on $[0, 1)$ is ergodic, the Lebesgue measure $\lambda(f^{-1}(B))$ must be exactly $0$ or $1$. Assume for contradiction that $\Sigma_Y$ is countably separated, i.e. there exists a countable sequence of measurable sets $(B_n)_{n \geq 1}$ in $\Sigma_Y$ that separates the points of $Y$. Let $A_n \coloneqq f^{-1}(B_n)$. Every $A_n$ has $\lambda(A_n) = 0$ or $\lambda(A_n) = 1$. - - - Define a "bad set" $N \subseteq [0, 1)$ as - $$\textstyle N \coloneqq \left( \bigcup_{\lambda(A_n)=0} A_n \right) \cup \left( \bigcup_{\lambda(A_n)=1} A_n^c \right)$$ - Because $N$ is a countable union of sets with measure $0$, we have $\lambda(N) = 0$, and thus $\lambda([0, 1) \setminus N)=1$. For any two points $x, y \in [0, 1) \setminus N$, clearly $x \in A_n \iff y \in A_n$ for every $n$. Consequently, the sequence $(B_n)$ fails to separate $f(x)$ and $f(y)$. Hence, $x \sim y$. Since $[0, 1) \setminus N$ has measure $1$, it is uncountable. Because each equivalence class is only countable, these uncountably many points must belong to uncountably many different equivalence classes. Thus, we can easily pick $x, y \in [0, 1) \setminus N$ where $x \not\sim y$. Thus $\Sigma_Y$ is not countably separated. - - - Hence by Theorem 6.5.7 in Bogachev's Measure theory $\Delta_Y \notin \Sigma_Y \otimes \Sigma_Y$. We have identified a non-measurable subset of $Y \times Y$ whose preimage under $f \times f$ is measurable. Therefore, $f \times f$ is not a regular epimorphism. + proof: A proof can be found here. special_objects: initial object: diff --git a/databases/catdat/data/categories/Set_f.yaml b/databases/catdat/data/categories/Set_f.yaml index 6e3b749d..7b70263f 100644 --- a/databases/catdat/data/categories/Set_f.yaml +++ b/databases/catdat/data/categories/Set_f.yaml @@ -67,7 +67,7 @@ unsatisfied_properties: proof: Already $\Set$ is not strongly connected. - property: binary powers - proof: 'More generally, if $X,Y$ are two non-empty sets such that $X \times Y$ exists in $\Set_\f$, then both $X$ and $Y$ must be finite. In fact, the forgetful functor to $\Set$ is representable, so it must preserve products. This means we can assume $X \times Y$ is the usual cartesian product with the usual projections. Since $p_1 : X \times Y \to X$ is finite-to-one and $X$ is non-empty, $Y$ is finite. By symmetric, also $X$ is finite. (Conversely, if $X$ and $Y$ are finite, or one of them is empty, then indeed $X \times Y$ exists.)' + proof: 'More generally, if $X,Y$ are two non-empty sets such that $X \times Y$ exists in $\Set_\f$, then both $X$ and $Y$ must be finite. In fact, the forgetful functor to $\Set$ is representable, so it must preserve products. This means we can assume $X \times Y$ is the usual cartesian product with the usual projections. Since $p_1 : X \times Y \to X$ is finite-to-one and $X$ is non-empty, $Y$ is finite. By symmetry, also $X$ is finite. (Conversely, if $X$ and $Y$ are finite, or one of them is empty, then indeed $X \times Y$ exists.)' - property: countable copowers proof: 'Assume that the copower $X \coloneqq \IN \otimes 1$ exists, where $1$ is the singleton set. This is a set with a map $i : \IN \to X$ (not necessarily finite-to-one) such that for every other such map $j : \IN \to Y$ there is a unique finite-to-one map $f : X \to Y$ with $f \circ i = j$. Applying this to $j : \IN \to 1$, we see that $X$ is finite. Applying the universal property to maps $j : \IN \to \{0,1\}$, we see that for every subset $E \subseteq \IN$ there is a unique finite subset $F \subseteq X$ with $i^*(F) = E$. But finiteness of $F$ is automatic, so $i^* : P(X) \to P(\IN)$ is bijective. But then $P(\IN)$ is finite, which is absurd.' diff --git a/databases/catdat/data/categories/walking_commutative_square.yaml b/databases/catdat/data/categories/walking_commutative_square.yaml index aa593661..7b6eab27 100644 --- a/databases/catdat/data/categories/walking_commutative_square.yaml +++ b/databases/catdat/data/categories/walking_commutative_square.yaml @@ -1,12 +1,12 @@ id: walking_commutative_square name: walking commutative square -notation: $\{0 \to 1\}^2$ +notation: $\Square$ objects: four objects $a,b,c,d$ morphisms: morphisms $a \to b$, $b \to d$, $a \to c$, $c \to d$, identities, and one morphism $a \to d$ description: >- This category consists of a commutative square: $$\begin{CD} a @>>> b \\ @VVV @VVV \\ c @>>> d \end{CD}$$ - Its name comes from the fact that a functor out of it is the same as a commutative square in the target category. Notice that the category is isomorphic to the product category $\{0 \to 1\} \times \{0 \to 1\}$ of the walking morphism with itself. Hence, most (but not all) properties are inherited from it. It is also isomorphic to the partial order of positive divisors of $6$. + Its name comes from the fact that a functor $\Square \to \C$ is the same as a commutative square in $\C$. Notice that the category is isomorphic to the product category $I \times I$ of the walking morphism with itself. Hence, most (but not all) properties are inherited from it. nlab_link: https://ncatlab.org/nlab/show/commutative+square tags: - category theory diff --git a/databases/catdat/data/categories/walking_composable_pair.yaml b/databases/catdat/data/categories/walking_composable_pair.yaml index c5fb2cf4..928c5005 100644 --- a/databases/catdat/data/categories/walking_composable_pair.yaml +++ b/databases/catdat/data/categories/walking_composable_pair.yaml @@ -1,11 +1,13 @@ id: walking_composable_pair name: walking composable pair -notation: $\{ 0 \to 1 \to 2 \}$ +notation: $\Comp$ objects: three objects $0,1,2$ morphisms: a single morphism from each natural number to one greater than or equal to it -description: The name of this category comes from the fact that a functor out of it is the same as a composable pair of morphisms. +description: >- + This category can be pictured as: + $$\{ 0 \to 1 \to 2 \}$$ + Its name comes from the fact that a functor $\Comp \to \C$ is the same as a composable pair of morphisms in $\C$. nlab_link: https://ncatlab.org/nlab/show/composable+pair - tags: - category theory - finite diff --git a/databases/catdat/data/categories/walking_coreflexive_pair.yaml b/databases/catdat/data/categories/walking_coreflexive_pair.yaml index f30255b5..f8973452 100644 --- a/databases/catdat/data/categories/walking_coreflexive_pair.yaml +++ b/databases/catdat/data/categories/walking_coreflexive_pair.yaml @@ -6,7 +6,7 @@ morphisms: 'the identities, two morphisms $i,j : [0] \rightrightarrows [1]$, a m description: >- This category is equal to the truncated simplex category $\Delta^{\leq 1}$, i.e. the full subcategory of $\Delta$ spanned by $[0] = \{0\}$ and $[1] = \{0 < 1\}$; this also explains our notation of the category and its objects. $$[0] \begin{array}{c} \xhookrightarrow{~~i~~} \\ \xtwoheadleftarrow{~~p~~} \\ \xhookrightarrow{~~j~~} \end{array} [1]$$ - The morphisms $i,j$ are the two inclusions, $p$ is their unique retraction, and $ip,jp : [1] \to [1]$ are the two constant maps. The name of this category comes from the fact that a functor out of it is the same as a coreflexive pair in the target category. Its dual is therefore the walking reflexive pair. + The morphisms $i,j$ are the two inclusions, $p$ is their unique retraction, and $ip,jp : [1] \to [1]$ are the two constant maps. The name of this category comes from the fact that a functor $\Delta^{\leq 1} \to \C$ is the same as a coreflexive pair in $\C$. Its dual is therefore the walking reflexive pair. nlab_link: null tags: - category theory diff --git a/databases/catdat/data/categories/walking_fork.yaml b/databases/catdat/data/categories/walking_fork.yaml index 248a32d8..85ba7edf 100644 --- a/databases/catdat/data/categories/walking_fork.yaml +++ b/databases/catdat/data/categories/walking_fork.yaml @@ -1,11 +1,13 @@ id: walking_fork name: walking fork -notation: $\{0 \to 1 \rightrightarrows 2\}$ +notation: $\Fork$ objects: three objects $0,1,2$ morphisms: 'one morphism $i : 0 \to 1$, two morphisms $f,g : 1 \rightrightarrows 2$, one morphism $0 \to 2$ (namely, $f \circ i = g \circ i$), and the identities' -description: The name of this category comes from the fact that a functor out of it is the same as a fork. +description: >- + This category can be pictured as: + $$\{0 \to 1 \rightrightarrows 2\}$$ + Its name comes from the fact that a functor $\Fork \to \C$ is the same as a fork in $\C$. nlab_link: null - tags: - category theory - finite diff --git a/databases/catdat/data/categories/walking_idempotent.yaml b/databases/catdat/data/categories/walking_idempotent.yaml index 8d9f1033..41e1cefc 100644 --- a/databases/catdat/data/categories/walking_idempotent.yaml +++ b/databases/catdat/data/categories/walking_idempotent.yaml @@ -3,7 +3,7 @@ name: walking idempotent notation: $\Idem$ objects: a single object $0$ morphisms: 'two morphisms $\id_0,e : 0 \to 0$ with $e^2=e$' -description: The name of this category comes from the fact that a functor out of it is the same as an idempotent morphism in the target category. It can also be seen as the delooping of the monoid $\{1,e\}$ in which $e^2=e$. +description: The name of this category comes from the fact that a functor $\Idem \to \C$ is the same as an idempotent morphism in $\C$. It can also be seen as the delooping of the monoid $\{1,e\}$ in which $e^2=e$. nlab_link: null tags: diff --git a/databases/catdat/data/categories/walking_isomorphism.yaml b/databases/catdat/data/categories/walking_isomorphism.yaml index 1e831a32..b2e58e6e 100644 --- a/databases/catdat/data/categories/walking_isomorphism.yaml +++ b/databases/catdat/data/categories/walking_isomorphism.yaml @@ -1,11 +1,13 @@ id: walking_isomorphism name: walking isomorphism -notation: $\{0 \rightleftarrows 1\}$ +notation: $\Isom$ objects: two objects $0$ and $1$ morphisms: identities, and two morphisms $0 \to 1$ and $1 \to 0$ that are mutually inverse -description: The name of this category comes from the fact that it consists of two objects and an isomorphism between them, and a functor out of this category is the same as an isomorphism in the target category. The walking isomorphism is actually equivalent to the trivial category. +description: >- + This category can be pictured as: + $$\{0 \rightleftarrows 1\}$$ + Its name comes from the fact that a functor $\Isom \to \C$ is the same as an isomorphism in $\C$. The walking isomorphism is actually equivalent to the trivial category. nlab_link: https://ncatlab.org/nlab/show/walking+isomorphism - tags: - category theory - finite @@ -24,7 +26,7 @@ satisfied_properties: proof: This is trivial. - property: trivial - proof: The inclusion $\{0\} \hookrightarrow \{0 \to 1\}$ is an equivalence. + proof: The inclusion $\{0\} \hookrightarrow \Isom$ is an equivalence. unsatisfied_properties: - property: skeletal diff --git a/databases/catdat/data/categories/walking_morphism.yaml b/databases/catdat/data/categories/walking_morphism.yaml index 56178970..f03f6e87 100644 --- a/databases/catdat/data/categories/walking_morphism.yaml +++ b/databases/catdat/data/categories/walking_morphism.yaml @@ -1,11 +1,13 @@ id: walking_morphism name: walking morphism -notation: $\{0 \to 1\}$ +notation: $I$ objects: $0$, $1$ morphisms: the two identities and a single morphism from $0$ to $1$ -description: This is also known as the interval category. It has the property that functors $\{0 \to 1\} \to \C$ are the same as morphisms in $\C$. +description: >- + This is also known as the interval category and can be pictured as: + $$\{0 \to 1\}$$ + It has the property that functors $I \to \C$ are the same as morphisms in $\C$, which explains its name. nlab_link: https://ncatlab.org/nlab/show/interval+category - tags: - category theory - finite @@ -37,7 +39,7 @@ satisfied_properties: proof: This is trivial. - property: finitary algebraic - proof: Take the algebraic theory with no operations but with the equation $x=y$ that is supposed to hold for all elements $x,y$. The algebras for this theory are the empty set and the singleton set, hence we get the equivalence to $\{0 \to 1\}$. + proof: Take the algebraic theory with no operations but with the equation $x=y$ that is supposed to hold for all elements $x,y$. The algebras for this theory are the empty set and the singleton set, hence we get the equivalence to $I$. unsatisfied_properties: - property: trivial diff --git a/databases/catdat/data/categories/walking_pair.yaml b/databases/catdat/data/categories/walking_pair.yaml index 72502a12..86e2b597 100644 --- a/databases/catdat/data/categories/walking_pair.yaml +++ b/databases/catdat/data/categories/walking_pair.yaml @@ -1,11 +1,13 @@ id: walking_pair name: walking parallel pair -notation: $\{0 \rightrightarrows 1 \}$ +notation: $\Pair$ objects: two objects $0$ and $1$ morphisms: the two identities and two parallel morphisms from $0$ to $1$ -description: The name of this category comes from the fact that it consists of two parallel morphisms, and a functor out of this category is the same as a parallel pair of morphisms in the target category. +description: >- + This category can be pictured as: + $$\{0 \rightrightarrows 1 \}$$ + Its name comes from the fact that a functor $\Pair \to \C$ is the same as a parallel pair of morphisms in $\C$. nlab_link: https://ncatlab.org/nlab/show/walking+structure - tags: - category theory - finite diff --git a/databases/catdat/data/categories/walking_span.yaml b/databases/catdat/data/categories/walking_span.yaml index 6e6d1faf..a6a74142 100644 --- a/databases/catdat/data/categories/walking_span.yaml +++ b/databases/catdat/data/categories/walking_span.yaml @@ -1,11 +1,13 @@ id: walking_span name: walking span -notation: $\{1 \leftarrow 0 \rightarrow 2\}$ +notation: $\Span$ objects: $0,1,2$ morphisms: $0 \to 1$, $0 \to 2$, and the identities -description: The name of this category comes from the fact that a functor out of it is the same as a span in the target category. It is isomorphic to the partial order of proper positive divisors of $6$. +description: >- + This category can be pictured as: + $$\{1 \leftarrow 0 \rightarrow 2\}$$ + Its name comes from the fact that a functor $\Span \to \C$ is the same as a span in $\C$. nlab_link: https://ncatlab.org/nlab/show/span#the_walking_span - tags: - category theory - finite diff --git a/databases/catdat/data/macros.yaml b/databases/catdat/data/macros.yaml index d4ac1641..ad9f648f 100644 --- a/databases/catdat/data/macros.yaml +++ b/databases/catdat/data/macros.yaml @@ -111,3 +111,9 @@ \CoAlg: \mathbf{CoAlg} \Cone: \mathbf{Cone} \SemiGrp: \mathbf{SemiGrp} +\Square: \mathbf{Square} +\Comp: \mathbf{Comp} +\Fork: \mathbf{Fork} +\Isom: \mathbf{Isom} +\Pair: \mathbf{Pair} +\Span: \mathbf{Span} diff --git a/databases/catdat/scripts/seed.ts b/databases/catdat/scripts/seed.ts index 14e8e144..713ca4e6 100644 --- a/databases/catdat/scripts/seed.ts +++ b/databases/catdat/scripts/seed.ts @@ -10,6 +10,7 @@ import type { FunctorImplicationYaml, FunctorPropertyYaml, FunctorYaml, + ProofWarning, } from './seed.types' import { create_schema_hash, get_saved_schema_hash } from './utils/schema' @@ -17,6 +18,14 @@ const db = get_client() const data_folder = path.resolve('databases', 'catdat', 'data') +/** + * Proofs longer than this value raise a warning + * that suggests to use content pages instead. + */ +const PROOF_LENGTH_THRESHOLD = 1200 + +const proof_length_warnings: ProofWarning[] = [] + seed() /** @@ -43,6 +52,8 @@ function seed() { seed_functor_properties() seed_functor_implications() seed_functors() + + print_proof_length_warnings() } function read_yaml_file(...parts: string[]): T { @@ -239,6 +250,14 @@ function seed_categories() { entry.proof, entry.check_redundancy === false ? 0 : 1, ) + + if (entry.proof.length >= PROOF_LENGTH_THRESHOLD) { + proof_length_warnings.push({ + structure_id: category.id, + property: entry.property, + length: entry.proof.length, + }) + } } for (const entry of category.unsatisfied_properties) { @@ -249,6 +268,14 @@ function seed_categories() { entry.proof, entry.check_redundancy === false ? 0 : 1, ) + + if (entry.proof.length >= PROOF_LENGTH_THRESHOLD) { + proof_length_warnings.push({ + structure_id: category.id, + property: entry.property, + length: entry.proof.length, + }) + } } for (const entry of category.undecidable_properties ?? []) { @@ -259,6 +286,14 @@ function seed_categories() { entry.proof, entry.check_redundancy === false ? 0 : 1, ) + + if (entry.proof.length >= PROOF_LENGTH_THRESHOLD) { + proof_length_warnings.push({ + structure_id: category.id, + property: entry.property, + length: entry.proof.length, + }) + } } } @@ -594,6 +629,14 @@ function seed_functors() { entry.proof, entry.check_redundancy === false ? 0 : 1, ) + + if (entry.proof.length >= PROOF_LENGTH_THRESHOLD) { + proof_length_warnings.push({ + structure_id: functor.id, + property: entry.property, + length: entry.proof.length, + }) + } } for (const entry of functor.unsatisfied_properties) { @@ -604,6 +647,14 @@ function seed_functors() { entry.proof, entry.check_redundancy === false ? 0 : 1, ) + + if (entry.proof.length >= PROOF_LENGTH_THRESHOLD) { + proof_length_warnings.push({ + structure_id: functor.id, + property: entry.property, + length: entry.proof.length, + }) + } } for (const entry of functor.undecidable_properties ?? []) { @@ -614,6 +665,14 @@ function seed_functors() { entry.proof, entry.check_redundancy === false ? 0 : 1, ) + + if (entry.proof.length >= PROOF_LENGTH_THRESHOLD) { + proof_length_warnings.push({ + structure_id: functor.id, + property: entry.property, + length: entry.proof.length, + }) + } } } @@ -635,3 +694,12 @@ function seed_functors() { process.exit(1) } } + +function print_proof_length_warnings() { + proof_length_warnings.sort((a, b) => b.length - a.length) + for (const { structure_id, property, length } of proof_length_warnings) { + console.warn( + `🟡 The proof for (${structure_id}, ${property}) has ${length} characters. Consider moving it to a content page.`, + ) + } +} diff --git a/databases/catdat/scripts/seed.types.ts b/databases/catdat/scripts/seed.types.ts index 92bd3205..2c1b7b3e 100644 --- a/databases/catdat/scripts/seed.types.ts +++ b/databases/catdat/scripts/seed.types.ts @@ -106,3 +106,9 @@ export type FunctorYaml = { undecidable_properties?: PropertyEntry[] comments?: string[] } + +export type ProofWarning = { + structure_id: string + property: string + length: number +} diff --git a/src/components/Header.svelte b/src/components/Header.svelte index 63777e94..9cbdd953 100644 --- a/src/components/Header.svelte +++ b/src/components/Header.svelte @@ -47,11 +47,10 @@ diff --git a/src/components/NavMobile.svelte b/src/components/NavMobile.svelte index f6b2d584..82b16f7f 100644 --- a/src/components/NavMobile.svelte +++ b/src/components/NavMobile.svelte @@ -3,6 +3,7 @@ import type { StructureType } from '$lib/commons/types' import { faXmark } from '@fortawesome/free-solid-svg-icons' import Fa from 'svelte-fa' + import StructureSelector from './StructureSelector.svelte' type Props = { close: () => void @@ -17,6 +18,10 @@ +
+ +
+