From b0c39047249f91711e067fd1719c20e1493e3c24 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 17 May 2026 11:59:58 +0200 Subject: [PATCH 1/2] replace all lemmas with markdown-generated content pages --- CONTRIBUTING.md | 2 - DATABASE.md | 1 - content/cogenerators_in_product_categories.md | 13 ++++++ content/coslice-effective-congruences.md | 24 +++++++++++ content/effective-congruence-quotients.md | 21 ++++++++++ content/exact_filtered_colimits_descend.md | 26 ++++++++++++ content/filtered-monos.md | 16 ++++++++ content/generator_construction.md | 13 ++++++ content/limits_in_factor_categories.md | 16 ++++++++ content/missing_cogenerating_sets.md | 19 +++++++++ content/missing_cogenerator.md | 20 ++++++++++ ...ntial-colimits-via-congruence-quotients.md | 14 +++++++ content/nno_distributive_criterion.md | 32 +++++++++++++++ content/preadditive_structure_unique.md | 36 +++++++++++++++++ ...houts-of-monos-via-congruence-quotients.md | 14 +++++++ content/special_sequential_colimits.md | 21 ++++++++++ content/subobject_classifiers_coreflection.md | 14 +++++++ content/thin_algebraic_categories.md | 14 +++++++ databases/catdat/data/categories/Alg(R).yaml | 6 +-- databases/catdat/data/categories/CAlg(R).yaml | 2 +- databases/catdat/data/categories/CRing.yaml | 2 +- databases/catdat/data/categories/Cat.yaml | 2 +- databases/catdat/data/categories/FinGrp.yaml | 6 +-- databases/catdat/data/categories/Fld.yaml | 2 +- databases/catdat/data/categories/Grp.yaml | 4 +- databases/catdat/data/categories/Haus.yaml | 2 +- databases/catdat/data/categories/Man.yaml | 4 +- databases/catdat/data/categories/Meas.yaml | 4 +- databases/catdat/data/categories/Met.yaml | 2 +- databases/catdat/data/categories/Met_c.yaml | 2 +- databases/catdat/data/categories/Met_oo.yaml | 2 +- databases/catdat/data/categories/Mon.yaml | 6 +-- databases/catdat/data/categories/N_oo.yaml | 2 +- databases/catdat/data/categories/Pos.yaml | 2 +- databases/catdat/data/categories/Prost.yaml | 2 +- databases/catdat/data/categories/Ring.yaml | 6 +-- databases/catdat/data/categories/Rng.yaml | 6 +-- databases/catdat/data/categories/Sch.yaml | 2 +- databases/catdat/data/categories/SemiGrp.yaml | 4 +- databases/catdat/data/categories/Set_c.yaml | 2 +- databases/catdat/data/categories/Set_f.yaml | 2 +- .../catdat/data/categories/Set_pointed.yaml | 2 +- databases/catdat/data/categories/Setne.yaml | 2 +- databases/catdat/data/categories/Sp.yaml | 4 +- databases/catdat/data/categories/Top.yaml | 4 +- .../catdat/data/categories/Top_pointed.yaml | 6 +-- databases/catdat/data/categories/Z.yaml | 6 +-- databases/catdat/data/categories/sSet.yaml | 2 +- .../walking_commutative_square.yaml | 2 +- .../categories/walking_composable_pair.yaml | 2 +- .../data/category-implications/topos.yaml | 2 +- .../data/category-properties/additive.yaml | 2 +- .../cogenerators_in_product_categories.yaml | 7 ---- .../lemmas/coslice-effective-congruences.yaml | 14 ------- .../effective-congruence-quotients.yaml | 16 -------- .../exact_filtered_colimits_descend.yaml | 15 ------- .../catdat/data/lemmas/filtered-monos.yaml | 10 ----- .../data/lemmas/generator_construction.yaml | 7 ---- .../lemmas/limits_in_factor_categories.yaml | 9 ----- .../lemmas/missing_cogenerating_sets.yaml | 12 ------ .../data/lemmas/missing_cogenerator.yaml | 13 ------ ...ial-colimits-via-congruence-quotients.yaml | 7 ---- .../lemmas/nno_distributive_criterion.yaml | 27 ------------- .../lemmas/preadditive_structure_unique.yaml | 26 ------------ ...uts-of-monos-via-congruence-quotients.yaml | 7 ---- .../lemmas/special_sequential_colimits.yaml | 15 ------- .../subobject_classifiers_coreflection.yaml | 7 ---- .../lemmas/thin_algebraic_categories.yaml | 7 ---- databases/catdat/schema/013_lemmas.sql | 6 --- ...comments.sql => 013_property_comments.sql} | 0 databases/catdat/scripts/seed.ts | 36 ----------------- databases/catdat/scripts/seed.types.ts | 7 ---- src/lib/commons/types.ts | 7 ---- src/routes/category-implications/+page.svelte | 5 --- src/routes/lemma/[id]/+page.server.ts | 40 ------------------- src/routes/lemma/[id]/+page.svelte | 39 ------------------ src/routes/lemmas/+page.server.ts | 14 ------- src/routes/lemmas/+page.svelte | 24 ----------- 78 files changed, 367 insertions(+), 434 deletions(-) create mode 100644 content/cogenerators_in_product_categories.md create mode 100644 content/coslice-effective-congruences.md create mode 100644 content/effective-congruence-quotients.md create mode 100644 content/exact_filtered_colimits_descend.md create mode 100644 content/filtered-monos.md create mode 100644 content/generator_construction.md create mode 100644 content/limits_in_factor_categories.md create mode 100644 content/missing_cogenerating_sets.md create mode 100644 content/missing_cogenerator.md create mode 100644 content/monic-sequential-colimits-via-congruence-quotients.md create mode 100644 content/nno_distributive_criterion.md create mode 100644 content/preadditive_structure_unique.md create mode 100644 content/pushouts-of-monos-via-congruence-quotients.md create mode 100644 content/special_sequential_colimits.md create mode 100644 content/subobject_classifiers_coreflection.md create mode 100644 content/thin_algebraic_categories.md delete mode 100644 databases/catdat/data/lemmas/cogenerators_in_product_categories.yaml delete mode 100644 databases/catdat/data/lemmas/coslice-effective-congruences.yaml delete mode 100644 databases/catdat/data/lemmas/effective-congruence-quotients.yaml delete mode 100644 databases/catdat/data/lemmas/exact_filtered_colimits_descend.yaml delete mode 100644 databases/catdat/data/lemmas/filtered-monos.yaml delete mode 100644 databases/catdat/data/lemmas/generator_construction.yaml delete mode 100644 databases/catdat/data/lemmas/limits_in_factor_categories.yaml delete mode 100644 databases/catdat/data/lemmas/missing_cogenerating_sets.yaml delete mode 100644 databases/catdat/data/lemmas/missing_cogenerator.yaml delete mode 100644 databases/catdat/data/lemmas/monic-sequential-colimits-via-congruence-quotients.yaml delete mode 100644 databases/catdat/data/lemmas/nno_distributive_criterion.yaml delete mode 100644 databases/catdat/data/lemmas/preadditive_structure_unique.yaml delete mode 100644 databases/catdat/data/lemmas/pushouts-of-monos-via-congruence-quotients.yaml delete mode 100644 databases/catdat/data/lemmas/special_sequential_colimits.yaml delete mode 100644 databases/catdat/data/lemmas/subobject_classifiers_coreflection.yaml delete mode 100644 databases/catdat/data/lemmas/thin_algebraic_categories.yaml delete mode 100644 databases/catdat/schema/013_lemmas.sql rename databases/catdat/schema/{014_property_comments.sql => 013_property_comments.sql} (100%) delete mode 100644 src/routes/lemma/[id]/+page.server.ts delete mode 100644 src/routes/lemma/[id]/+page.svelte delete mode 100644 src/routes/lemmas/+page.server.ts delete mode 100644 src/routes/lemmas/+page.svelte diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 9ac21ba65..9defc2033 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -128,8 +128,6 @@ When contributing new data (categories, functors, properties, implications), ple - **Simplify Implications**: When adding a new implication, check if it simplifies existing implications and if it deduces some previously non-deduced properties for categories. -- **Avoid repetition**: When the same argument is used repeatedly for various categories but cannot be added as an implication, create a lemma and refer to its page where needed. - - **New Combinations**: Add new categories that satisfy combinations of satisfied properties and unsatisfied properties and not yet in the database. For example, you may add a category that is abelian but neither cocomplete nor essentially small (if it is not already present). The [page with missing data](https://catdat.app/missing) lists consistent combinations of the form $p \land \neg q$ that are not yet witnessed by a category in the database. The same remarks apply to functors. ### Redundancy Script diff --git a/DATABASE.md b/DATABASE.md index 525cdb512..cbefe983b 100644 --- a/DATABASE.md +++ b/DATABASE.md @@ -34,7 +34,6 @@ Further tables are: - `related_category_properties` - `category_comments` - `category_property_comments` -- `lemmas` (a flexible variant of implications) For functors there are similar tables, such as: diff --git a/content/cogenerators_in_product_categories.md b/content/cogenerators_in_product_categories.md new file mode 100644 index 000000000..26f8fc5ca --- /dev/null +++ b/content/cogenerators_in_product_categories.md @@ -0,0 +1,13 @@ +--- +title: Cogenerators in product categories +description: How to construct a cogenerator in a product category +--- + +## Cogenerators in product categories + +::: Lemma +For a family of categories $(\C_i)_{i \in I}$, each having a cogenerator $Q_i$ which is weakly terminal, the object $(Q_i)_{i \in I}$ is a cogenerator in the product category $\prod_{i \in I} \C_i$. +::: + +_Proof._ +Let $(f_i: A_i \to B_i)_{i \in I}$ and $(g_i: A_i \to B_i)_{i \in I}$ be two parallel morphisms in the product category which are coequalized by any morphism $(B_i \to Q_i)_{i \in I}$. Let $i_0 \in I$. We claim that $f_{i_0},g_{i_0} : A_{i_0} \rightrightarrows B_{i_0}$ are coequalized by all morphisms $B_{i_0} \to Q_{i_0}$, and hence are equal: Indeed, for all $i \neq i_0$ we may choose some morphism $B_i \to Q_i$ since $Q_i$ is weakly terminal. Thus, the morphism $B_{i_0} \to Q_{i_0}$ extends to a morphism $(B_i \to Q_i)_{i \in I}$ in the product category. By assumption, it coequalizes $(f_i)_{i \in I}$ and $(g_i)_{i \in I}$. By looking at the $i_0$-component, we are done. $\square$ diff --git a/content/coslice-effective-congruences.md b/content/coslice-effective-congruences.md new file mode 100644 index 000000000..e8510f1dd --- /dev/null +++ b/content/coslice-effective-congruences.md @@ -0,0 +1,24 @@ +--- +title: Inheritance of effective congruences in coslice categories +description: An extensive category has effective congruences when some of its coslice categories has effective congruences. +author: Daniel Schepler +--- + +## Inheritance of effective congruences in coslice categories + +::: Lemma +Let $\C$ be an extensive category, and $A$ an object of $\C$. If the coslice category $A \backslash \C$ has effective congruences, then so does $\C$. +::: + +_Proof._ +Let $f, g : E \rightrightarrows X$ be a congruence in $\C$. We then construct a congruence on $A+X$ in $A \backslash \C$. On an intuitive level, this will be the congruence generated by $a \sim a$ for $a\in A$ and $x \sim y$ for $(x, y) \in E$. More precisely, we will show the two maps + +$$\id_A + f,\, \id_A + g : A+E \rightrightarrows A+X$$ + +form a congruence. To show the pair of maps is jointly monomorphic, we use extensivity to split the domains of the generalized elements, so without loss of generality we may assume each comes from either $A$ or $E$. Reflexivity and symmetry are straightforward; and for transitivity, we again use extensivity to split the domains of the generalized elements, and provide an argument on each subdomain where the three generalized elements all come from either $A$ or $E$. + +Now if this congruence is the kernel pair of $h : A+X \to Z$ in $A \backslash \C$, then $E$ is the kernel pair of $h \circ i_2 : X \to Z$ in $\C$. Namely, if we have two generalized elements $x_1, x_2 : T \rightrightarrows X$ such that $h \circ i_2 \circ x_1 = h \circ i_2 \circ x_2$, then we can construct a map pair + +$$\id_A + x_1,\, \id_A + x_2 : A+T \rightrightarrows A+X$$ + +in $A \backslash \C$ with $h \circ (\id_A + x_1) = h \circ (\id_A + x_2)$. Therefore, $\id_A + x_1, \id_A + x_2$ factors through $A+E$ in $A \backslash \C$, so $x_1, x_2$ factors through $A+E$ in $\C$; and using disjoint coproducts, we may conclude $x_1, x_2$ factors through $E$. $\square$ diff --git a/content/effective-congruence-quotients.md b/content/effective-congruence-quotients.md new file mode 100644 index 000000000..edaa1f185 --- /dev/null +++ b/content/effective-congruence-quotients.md @@ -0,0 +1,21 @@ +--- +title: Quotients of effective congruences are strict quotients +description: Quotients by effective congruences are characterized via a pullback +author: Daniel Schepler +--- + +## Quotients of effective congruences are strict quotients + +::: Lemma +Let $f, g : E \rightrightarrows X$ be an effective congruence. If $f, g$ have a coequalizer $p : X \to X/E$, then in fact we have a cartesian square +$$\begin{CD} E @> f >> X \\ @V g VV @VV p V \\ X @>> p > X/E. \end{CD}$$ +::: + +_Proof._ +Suppose we have $h : X \to Z$ so that we have a cartesian square +$$\begin{CD} E @> f >> X \\ @V g VV @VV h V \\ X @>> h > Z. \end{CD}$$ +Then by the universal property of the coequalizer, there is a unique morphism +$$\bar h : X/E \to Z$$ +such that $h = \bar h \circ p$. Now suppose we have generalized elements $x_1, x_2 : T \rightrightarrows X$ such that $p \circ x_1 = p \circ x_2$. Then +$$h \circ x_1 = \bar h \circ p \circ x_1 = \bar h \circ p \circ x_2 = h \circ x_2,$$ +so the pair $x_1, x_2$ factors through $f, g : E \rightrightarrows X$. The uniqueness of the factorization follows from the assumption that $E$ is a congruence, so $f, g$ are jointly monomorphic. $\square$ diff --git a/content/exact_filtered_colimits_descend.md b/content/exact_filtered_colimits_descend.md new file mode 100644 index 000000000..002fcdc00 --- /dev/null +++ b/content/exact_filtered_colimits_descend.md @@ -0,0 +1,26 @@ +--- +title: Exact filtered colimits descend to nice subcategories +description: Exact filtered colimits are inherited by reflective subcategories with a finite-limit preserving reflector. +author: Martin Brandenburg +--- + +## Exact filtered colimits descend to nice subcategories + +::: Lemma +Let $G : \C \to \D$ be a fully faithful functor with a left adjoint $F : \D \to \C$ that preserves finite limits. Assume that $\D$ has exact filtered colimits and that $\C$ has finite limits. Then $\C$ has exact filtered colimits as well. +::: + +_Proof._ +It is well-known (and easy to prove) that the colimit of a diagram $(X_j)$ in $\C$ is constructed as $F(\colim_j G(X_j))$, provided that colimit in $\D$ exists. In particular, $\C$ has filtered colimits. By assumption, it also has finite limits, and $G$ preserves these since it is a right adjoint. Now let $X : \I \times \J \to \C$ be a diagram, where $\I$ is finite and $\J$ is filtered. We compute: + +$$ +\begin{align*} +\colim_j {\lim}_i X(i,j) & \cong F(\colim_j G({\lim}_i X(i,j))) \\ +& \cong F(\colim_j {\lim}_i G(X(i,j))) \\ +& \cong F({\lim}_i \colim_j G(X(i,j))) \\ +& \cong {\lim}_i F(\colim_j G(X(i,j))) \\ +& \cong {\lim}_i \colim_j X(i,j) +\end{align*} +$$ + +$\square$ diff --git a/content/filtered-monos.md b/content/filtered-monos.md new file mode 100644 index 000000000..5e839a230 --- /dev/null +++ b/content/filtered-monos.md @@ -0,0 +1,16 @@ +--- +title: Detection of filtered-colimit-stable monomorphisms +description: A useful result to prove (and disprove) filtered-colimit-stable monomorphisms for several categories based on other categories +author: Martin Brandenburg +--- + +## Detection of filtered-colimit-stable monomorphisms + +::: Lemma +Let $\C$ be a category with filtered colimits. Assume that $U : \C \to \D$ is a faithful functor which preserves monomorphisms and filtered colimits. If monomorphisms in $\D$ are stable under filtered colimits, then the same is true for $\C$. +::: + +For the record, here is the dual statement: Let $\C$ be a category with cofiltered limits. Assume that $U : \C \to \D$ is faithful functor which preserves epimorphisms and cofiltered limits. If epimorphisms in $\D$ are stable under cofiltered limits, then the same is true for $\C$. + +_Proof._ +Since $U$ is faithful, it reflects monomorphisms. From here the proof is straight forward. $\square$ diff --git a/content/generator_construction.md b/content/generator_construction.md new file mode 100644 index 000000000..a7cef4c68 --- /dev/null +++ b/content/generator_construction.md @@ -0,0 +1,13 @@ +--- +title: Construction of Generators +description: How to construct a generator from a generating set +author: Martin Brandenburg +--- + +## Construction of Generators + +::: Lemma +In a category let $S$ be a generating set which is [strongly connected](/category-property/strongly_connected) (between any two objects in $S$ there is a morphism). If the coproduct $U \coloneqq \coprod_{G \in S} G$ exists, then it is a generator. +::: + +_Proof._ This is a straight forward generalization of [this result](/category-implication/generator_via_coproduct). We remark that the assumption about $S$ implies that each inclusion $G \to U$ has a left inverse. Now let $f,g : A \rightrightarrows B$ be two morphisms with $f h = g h$ for all $h : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by our preliminary remark. Thus, $fh = gh$ holds for all $h : G \to A$ and $G \in S$. Since $S$ is a generating set, this implies $f = g$. $\square$ diff --git a/content/limits_in_factor_categories.md b/content/limits_in_factor_categories.md new file mode 100644 index 000000000..377024e69 --- /dev/null +++ b/content/limits_in_factor_categories.md @@ -0,0 +1,16 @@ +--- +title: Limits in factor categories +description: Limits descend to factors in a product of categories +author: Martin Brandenburg +--- + +## Limits in factor categories + +::: Lemma +Let $\C,\D$ be two categories. Assume that $\D$ is inhabited. If $\C \times \D$ has limits of a given shape, then $\C$ also has limits of this shape. +::: + +_Proof._ +Let $U \in \D$ be a fixed object. Assume that $X : \J \to \C$ is a diagram. Assume that the diagram $(X,U) : \J \to \C \times \D$ (which is constant in the second variable) has a limit cone $((p_i, u_i) : (L,V) \to (X_i,U))$, thus consisting of morphisms $p_i : L \to X_i$ and $u_i : V \to U$. Clearly, $(p_i : L \to X_i)$ is a cone over $X$. We prove that it is universal: + +Let $(f_i : T \to X_i)$ be a cone over $X$. Then $((f_i,\id_U) : (T,U) \to (X_i,U))$ is a cone over $(X,U)$. Hence, there is a unique morphism $(f,v) : (T,U) \to (L,V)$, consisting of $f : T \to L$ and $v : U \to V$, such that $(p_i,u_i) \circ (f,v) = (f_i,\id_U)$, i.e. $p_i \circ f = f_i$ and $u_i \circ v = \id_U$. If $g : T \to L$ is another morphism with $p_i \circ g = f_i$, then uniqueness applied to $(g,v)$ shows that $f = g$. $\square$ diff --git a/content/missing_cogenerating_sets.md b/content/missing_cogenerating_sets.md new file mode 100644 index 000000000..2fef33323 --- /dev/null +++ b/content/missing_cogenerating_sets.md @@ -0,0 +1,19 @@ +--- +title: Missing cogenerating sets +description: A generalization of the proof that the category of commutative rings has no cogenerating set. +author: Martin Brandenburg +--- + +## Missing cogenerating sets + +::: Lemma +Let $\C$ be a category with a faithful functor $U: \C \to \Set$. Assume there exists a collection of objects $\F \subseteq \Ob(\C)$ satisfying the following conditions: + +1. For any $X \in \F$ and any non-terminal $Y \in \C$, for every morphism $f: X \to Y$ its underlying map $U(f) : U(X) \to U(Y)$ is injective. +2. For every infinite cardinal number $\kappa$, there exists an object $X \in \F$ such that $\card(U(X)) \geq \kappa$ and such that $X$ has a non-identity endomorphism. + +Then $\C$ does not have a cogenerating set. +::: + +_Proof._ +Assume that there is a cogenerating set $S$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than all the $U(Y)$ with $Y \in S$ (w.r.t. cardinalities) and which has a non-identity endomorphism $\sigma : X \to X$. Since $S$ cogenerates, there is a morphism $f : X \to Y$ with $Y \in S$ and $f \sigma \neq f$. For this, $Y$ must be non-terminal. By (1) the map $U(f) : U(X) \to U(Y)$ is injective. This is a contradiction. $\square$ diff --git a/content/missing_cogenerator.md b/content/missing_cogenerator.md new file mode 100644 index 000000000..a59d81f79 --- /dev/null +++ b/content/missing_cogenerator.md @@ -0,0 +1,20 @@ +--- +title: Missing cogenerator +description: A generalization of the proof that the category of groups has no cogenerator. +author: Martin Brandenburg +--- + +## Missing cogenerator + +::: Lemma + +Let $\C$ be a pointed category with a faithful functor $U: \C \to \Set$. Assume there exists a collection of non-zero objects $\F \subseteq \Ob(\C)$ satisfying the following conditions: + +1. For any $X \in \F$ and any $Y \in \C$, every non-zero morphism $f: X \to Y$ is injective on underlying sets. +2. For every $Y \in \C$ there is some object $X \in \F$ such that $\card(U(X)) > \card(U(Y))$. + +Then $\C$ does not have a cogenerator. +::: + +_Proof._ +Assume that there is a cogenerator $Y$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than $U(Y)$ (w.r.t. cardinalities). Since $0,\id_X : X \rightrightarrows X$ are distinct, there is a morphism $f : X \to Y$ with $f \neq 0$. But then $U(f) : U(X) \to U(Y)$ is injective by assumption (1), which contradicts our choice of $X$. $\square$ diff --git a/content/monic-sequential-colimits-via-congruence-quotients.md b/content/monic-sequential-colimits-via-congruence-quotients.md new file mode 100644 index 000000000..9305e9fad --- /dev/null +++ b/content/monic-sequential-colimits-via-congruence-quotients.md @@ -0,0 +1,14 @@ +--- +title: Construction of a colimit of a sequence of monomorphisms as a quotient of a congruence +description: A countably extensive category with quotients of congruences has colimits of sequences of monomorphisms. +author: Daniel Schepler +--- + +## Construction of a colimit of a sequence of monomorphisms as a quotient of a congruence + +::: Lemma +Let $\C$ be a countably extensive category with quotients of congruences. Then $\C$ has colimits of sequences of monomorphisms. +::: + +_Proof._ +Suppose we have a sequence $X_1 \hookrightarrow X_2 \hookrightarrow \cdots$ with corresponding monomorphisms $f_{m,n} : X_m \hookrightarrow X_n$ for $m \le n$. Define $Y$ to be the coproduct of all $X_n$. Now for each $m\le n$, define $E_{m,n} \coloneqq X_m$ with two maps $i_m, i_n \circ f_{m,n} : E_{m,n} \rightrightarrows Y$, and similarly for $m \ge n$ define $E_{m,n} \coloneqq X_n$ with two maps $i_m \circ f_{n,m}, i_n : E_{m,n} \rightrightarrows Y$. Then the coproduct of all $E_{m,n}$, with the induced morphisms to $Y$, forms a congruence. Here to prove the maps are jointly monomorphic, and again in proving transitivity, we use extensivity to split the domain of the generalized elements of $\sum_{m,n=1}^\infty E_{m,n}$ so that without loss of generality we may assume each factors through one of the coproduct inclusions. Now a quotient of this congruence must be a colimit of the sequence. $\square$ diff --git a/content/nno_distributive_criterion.md b/content/nno_distributive_criterion.md new file mode 100644 index 000000000..cb001be9b --- /dev/null +++ b/content/nno_distributive_criterion.md @@ -0,0 +1,32 @@ +--- +title: Natural number objects indicate distributivity +description: A partial converse of the result that countably distributive categories have a NNO. +author: Martin Brandenburg +--- + +## Natural number objects indicate distributivity + +::: Lemma +Let $\C$ be a category with finite products, arbitrary copowers (denoted $\otimes$), and a natural numbers object $1 \xrightarrow{z} N \xrightarrow{s} N$. Then there is an isomorphism $N \cong \IN \otimes 1$, and for every object $A$ the natural morphism +$$\alpha : \IN \otimes A \to A \times (\IN \otimes 1)$$ +is a split monomorphism. +::: + +_Proof._ +We will use generalized elements extensively. In particular, for every element $a \in A$ and $n \in \IN$ there is an element $n \otimes a \in \IN \otimes A$, formally defined by the $n$th coproduct inclusion. The morphism $\alpha$ is defined by +$$\alpha(n \otimes a) = (a , n \otimes 1).$$ +In any category with finite products and arbitrary copowers, we can construct the non-parameterized NNO $\IN \otimes 1$ with the element $0 \otimes 1 \in \IN \otimes 1$ and the map +$$s : \IN \otimes 1 \to \IN \otimes 1, \quad s(n \otimes 1) \coloneqq (n+1) \otimes 1.$$ +Its universal property states that it is initial in the category of pairs $1 \xrightarrow{x_0} X \xrightarrow{r} X$. Hence, it is unique up to isomorphism. Since by assumption $1 \xrightarrow{z} N \xrightarrow{s} N$ is a full, parameterized NNO, it is also a non-parameterized NNO and therefore isomorphic to the one described. We will assume w.l.o.g. that it is equal to it and continue to work with $N = \IN \otimes 1$. + +Next, we apply the (parameterized) universal property of the NNO to the diagram +$$A \xrightarrow{f} \IN \otimes A \xrightarrow{g} \IN \otimes A$$ +defined by $f(a) \coloneqq 0 \otimes a$ and $g(n \otimes a) \coloneqq (n+1) \otimes a$. It tells us that there is a map +$$\Phi : A \times N \to \IN \otimes A$$ +with +$$\Phi(a,0 \otimes 1) = 0 \otimes a, \quad \Phi(a, s(m)) = g(\Phi(a,m)).$$ +For $m \coloneqq n \otimes 1 \in N$ (where $n \in \IN$) the second equation reads +$$\Phi(a, (n+1) \otimes 1) = g(\Phi(a, n \otimes 1)).$$ +By classical induction on $n \in \IN$ it follows that +$$\Phi(a, n \otimes 1) = n \otimes a,$$ +which exactly means $\Phi \circ \alpha = \id_{\IN \otimes A}$. $\square$ diff --git a/content/preadditive_structure_unique.md b/content/preadditive_structure_unique.md new file mode 100644 index 000000000..b2e79d25a --- /dev/null +++ b/content/preadditive_structure_unique.md @@ -0,0 +1,36 @@ +--- +title: Uniqueness of preadditive structures +description: In the presence of finite products, a preadditive structure on a given category is uniquely determined. +author: Martin Brandenburg +--- + +## Uniqueness of preadditive structures + +::: Lemma +Let $\C$ be a preadditive category (or more generally, a category enriched in commutative monoids) with finite products and finite coproducts. Then for all objects $X,Y$ the canonical morphism +$$\alpha : X \oplus Y \to X \times Y$$ +is an isomorphism. Moreover, the preadditive structure is unique: If $f,g : A \rightrightarrows B$ are morphisms, their sum +$$f+g : A \to B$$ +is the composite of $(f,g) : A \to B \times B$, the inverse $\alpha^{-1} : B \oplus B \to B \times B$, and the codiagonal $\nabla : B \oplus B \to B$. +::: + +_Proof._ +The morphism $\alpha : X \oplus Y \to X \times Y$ is defined by the equations +$$p_1 \circ \alpha \circ i_1 = \id_X, \quad p_2 \circ \alpha \circ i_2 = \id_Y,$$ +$$p_2 \circ \alpha \circ i_1 = 0,\quad p_1 \circ \alpha \circ i_2 = 0.$$ +It does not depend on the choice of preadditive structure since zero morphisms are unique. It is an isomorphism: Define +$$\beta \coloneqq i_1 \circ p_1 + i_2 \circ p_2 : X \times Y \to X \oplus Y.$$ +Then $\alpha \circ \beta = \id_{X \times Y}$ because +$$p_1 \circ \alpha \circ \beta = p_1 \circ \alpha \circ i_1 \circ p_1 + p_1 \circ \alpha \circ i_2 \circ p_2 = \id_1 \circ p_1 + 0 \circ p_2 = p_1$$ +and likewise $p_2 \circ \alpha \circ \beta = p_2$. We also have $\beta \circ \alpha = \id_{X \oplus Y}$ with a very similar calculation that shows $\beta \circ \alpha \circ i_1 = i_1$ and $\beta \circ \alpha \circ i_2 = i_2$. Therefore, for morphisms $f,g : A \rightrightarrows B$ the composite $A \to B$ in the claim is equal to + +$$ +\begin{align*} +\nabla \circ \beta \circ (f,g) & = \nabla \circ (i_1 \circ p_1 + i_2 \circ p_2) \circ (f,g) \\ +& = \nabla \circ i_1 \circ p_1 \circ (f,g) + \nabla \circ i_2 \circ p_2 \circ (f,g) \\ +& = p_1 \circ (f,g) + p_2 \circ (f,g) \\ +& = f + g. +\end{align*} +$$ + +$\square$ diff --git a/content/pushouts-of-monos-via-congruence-quotients.md b/content/pushouts-of-monos-via-congruence-quotients.md new file mode 100644 index 000000000..6aeb9f7c8 --- /dev/null +++ b/content/pushouts-of-monos-via-congruence-quotients.md @@ -0,0 +1,14 @@ +--- +title: Construction of a pushout of monomorphisms as a quotient of a congruence +description: An extensive category with quotients of congruences has pushouts of monomorphisms. +author: Daniel Schepler +--- + +## Construction of a pushout of monomorphisms as a quotient of a congruence + +::: Lemma +Let $\C$ be an extensive category with quotients of congruences. Then $\C$ has pushouts of monomorphisms. +::: + +_Proof._ +Let $f : S \hookrightarrow X$, $g : S \hookrightarrow Y$ be monomorphisms. We construct a congruence on $X+Y$ via the maps $p_1, p_2 : X + Y + S + S \rightrightarrows X+Y$ which act as the identity on $X+Y$, $i_1 \circ f, i_2 \circ g$ on the first copy of $S$, and $i_2 \circ g, i_1 \circ f$ on the second copy of $S$, respectively. To show that $p_1, p_2$ are jointly monomorphic, and again in proving transitivity of the congruence, we use extensivity to split the domain of the generalized elements of $X+Y+S+S$ so that without loss of generality we may assume each factors through one of the coproduct inclusions. Now a quotient of the congruence must be a pushout of $f$ and $g$. $\square$ diff --git a/content/special_sequential_colimits.md b/content/special_sequential_colimits.md new file mode 100644 index 000000000..3662bedd8 --- /dev/null +++ b/content/special_sequential_colimits.md @@ -0,0 +1,21 @@ +--- +title: Finite structures usually have no sequential colimits +description: A generalization of the proof that the category of finite groups has no filtered colimits. +author: Martin Brandenburg +--- + +## Finite structures usually have no sequential colimits + +::: Lemma +Let $\C$ be a category with finite powers, including a terminal object $1$. Let $a : 1 \to X$ be a morphism. Assume that the sequence of morphisms $(X^n,a) : X^n \to X^{n+1}$ for $n \geq 0$ admits a colimit $(i_n : X^n \to C)$. Then for every $m \geq 0$ there is a split epimorphism $C \to X^m$. In particular, if $U : \C \to \Set$ is a functor preserving finite powers and $\card(U(X)) \geq 2$, then $U(C)$ is infinite. +::: + +_Proof._ +Let $m \geq 0$ be fixed. For $n \geq 0$ we define a morphism $u_n : X^n \to X^m$ as follows: It is the projection on the first $m$ factors for $m \leq n$, and $(X^n,a^{m-n})$ for $m \geq n$ (for $m=n$ these agree). With generalized elements this says: +$$u_n(x_1,\dotsc,x_n) = \begin{cases} (x_1,\dotsc,x_m) & m \leq n \\ (x_1,\dotsc,x_n,a,\dotsc,a) & m \geq n \end{cases}$$ +We claim that $u_n = u_{n+1} \circ (X^n,a)$, i.e. +$$u_n(x_1,\dotsc,x_n) = u_{n+1}(x_1,\dotsc,x_n,a).$$ +If $m \leq n$ (hence, $m \leq n+1$), both sides are equal to $(x_1,\dotsc,x_m)$. If $m > n$, i.e. $m \geq n+1$, both sides are equal to $(x_1,\dotsc,x_n,a,\dotsc,a)$. This proves the claim. + +Hence, there is a unique morphism $\varphi : C \to X^m$ such that $\varphi \circ i_n = u_n$ for all $n \geq 0$. Since $u_m$ is the identity, $\varphi$ is a split epimorphism. +If $U$ is a functor with the mentioned properties, $U(\varphi)$ is also a split epimorphism from $U(C)$ to $U(X^m) \cong U(X)^m$, and $U(X)^m$ has $\geq 2^m$ elements. This holds for all $m$, so that $U(C)$ is infinite. $\square$ diff --git a/content/subobject_classifiers_coreflection.md b/content/subobject_classifiers_coreflection.md new file mode 100644 index 000000000..00c8795db --- /dev/null +++ b/content/subobject_classifiers_coreflection.md @@ -0,0 +1,14 @@ +--- +title: Coreflection of subobject classifiers +description: How to construct subobject classifiers in a coreflective subcategory. +author: Martin Brandenburg +--- + +## Coreflection of subobject classifiers + +::: Lemma +Let $\D$ be a category with a (regular) subobject classifier $\Omega$. Assume that $\C \to \D$ is a full subcategory such that (1) any (regular) $\D$-subobject of an object in $\C$ already lies in $\C$, (2) it is coreflective, i.e. there is a functor $R : \D \to \C$ right adjoint to the inclusion. Then $R(\Omega)$ is a (regular) subobject classifier in $\C$. +::: + +_Proof._ +If $X \in \C$, then $\Hom(X,R(\Omega)) \cong \Hom(X,\Omega)$ is isomorphic to the collection of $\D$-subobjects of $X$, which by assumption coincide with the $\C$-subobjects of $X$. $\square$ diff --git a/content/thin_algebraic_categories.md b/content/thin_algebraic_categories.md new file mode 100644 index 000000000..b48b5ff75 --- /dev/null +++ b/content/thin_algebraic_categories.md @@ -0,0 +1,14 @@ +--- +title: Algebraic categories are "never" thin +description: A proof that the only thin algebraic categories are the terminal and the interval category. +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\}$. +::: + +_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$ diff --git a/databases/catdat/data/categories/Alg(R).yaml b/databases/catdat/data/categories/Alg(R).yaml index be36dc579..872bc23fa 100644 --- a/databases/catdat/data/categories/Alg(R).yaml +++ b/databases/catdat/data/categories/Alg(R).yaml @@ -41,7 +41,7 @@ unsatisfied_properties: reason: This is because already the full subcategory $\CAlg(R)$ of commutative algebras is not semi-strongly connected. - property: cogenerating set - reason: 'We apply this lemma to the collection of $R$-algebras which are fields: If $F$ is an $R$-algebra that is also a field and $A$ is a non-trivial $R$-algebra, any algebra homomorphism $F \to A$ is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables over some residue field of $R$ has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).' + reason: 'We apply this lemma to the collection of $R$-algebras which are fields: If $F$ is an $R$-algebra that is also a field and $A$ is a non-trivial $R$-algebra, any algebra homomorphism $F \to A$ is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables over some residue field of $R$ has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).' - property: codistributive reason: 'If $\sqcup$ denotes the coproduct of $R$-algebras (see MSE/625874 for their description) and $A$ is an $R$-algebra, the canonical morphism $A \sqcup R^2 \to (A \sqcup R)^2 = A^2$ is usually no isomorphism. For example, for $A = R[X]$ the coproduct on the LHS is not commutative, it has the algebra presentation $\langle X,E : E^2=E \rangle$.' @@ -53,7 +53,7 @@ unsatisfied_properties: reason: '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.' - property: regular quotient object classifier - reason: We may copy the proof for $\CRing$ (since the proof there did not use that $P$ is commutative). Alternatively, any regular quotient object classifier in $\Alg(R)$ would produce one in $\CAlg(R)$ by this lemma (dualized). + reason: We may copy the proof for $\CRing$ (since the proof there did not use that $P$ is commutative). Alternatively, any regular quotient object classifier in $\Alg(R)$ would produce one in $\CAlg(R)$ by this lemma (dualized). - property: cocartesian cofiltered limits reason: >- @@ -62,7 +62,7 @@ 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 - reason: We already know that $\CAlg(R)$ does not have this property. Now apply the contrapositive of the dual of this lemma to the forgetful functor $\CAlg(R) \to \Alg(R)$. It preserves epimorphisms by MSE/5133488. + reason: We already know that $\CAlg(R)$ does not have this property. Now apply the contrapositive of the dual of this lemma to the forgetful functor $\CAlg(R) \to \Alg(R)$. It preserves epimorphisms by MSE/5133488. - property: effective cocongruences reason: '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)$.' diff --git a/databases/catdat/data/categories/CAlg(R).yaml b/databases/catdat/data/categories/CAlg(R).yaml index 77e873e4e..0b516d51f 100644 --- a/databases/catdat/data/categories/CAlg(R).yaml +++ b/databases/catdat/data/categories/CAlg(R).yaml @@ -39,7 +39,7 @@ unsatisfied_properties: reason: Take a prime ideal $P \subseteq R$ and consider the commutative $R$-algebra $A \coloneqq R/P$ (which is an integral domain). Then the inclusion $A \hookrightarrow Q(A)$ is a counterexample. - property: cogenerating set - reason: 'We apply this lemma to the collection of commutative $R$-algebras which are fields: If $F$ is a commutative $R$-algebra that is also a field and $A$ is a non-trivial commutative $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).' + reason: 'We apply this lemma to the collection of commutative $R$-algebras which are fields: If $F$ is a commutative $R$-algebra that is also a field and $A$ is a non-trivial commutative $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).' - property: countably codistributive reason: 'The canonical homomorphism $A \otimes_R R^{\IN} \to A^{\IN}$ is given by $a \otimes (r_n)_n \mapsto (r_n a)_n$ and does not have to be surjective: Since $R \neq 0$, there is a commutative $R$-algebra $K$ which is a field. Now take $A \coloneqq K[X]$ and consider the sequence $(X^n)_{n} \in A^{\IN}$.' diff --git a/databases/catdat/data/categories/CRing.yaml b/databases/catdat/data/categories/CRing.yaml index c5f34f4b7..0b05df17e 100644 --- a/databases/catdat/data/categories/CRing.yaml +++ b/databases/catdat/data/categories/CRing.yaml @@ -45,7 +45,7 @@ unsatisfied_properties: reason: The inclusion $\IZ \hookrightarrow \IQ$ is a counterexample. - property: cogenerating set - reason: '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).' + reason: '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 reason: '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.' diff --git a/databases/catdat/data/categories/Cat.yaml b/databases/catdat/data/categories/Cat.yaml index 70835a9be..71bfa1734 100644 --- a/databases/catdat/data/categories/Cat.yaml +++ b/databases/catdat/data/categories/Cat.yaml @@ -56,7 +56,7 @@ unsatisfied_properties: reason: 'We can adapt the proof from $\Mon$ as follows: Consider the functor $U : \Cat \to \Set^+$ sending a category $\C$ to the (large) set $\{(x,u) : x \in \Ob(\C) ,\, u \in \End(x) \}$. It is represented by $B \IN$, the one-object category associated to the free monoid in one generator. Consider the relation $R \subseteq U^2$ consisting of those pairs $((x,u),(y,v))$ where $x = y$ and $uv = u^2$. This also representable, namely be the one-object category associated to the monoid with the presentation $\langle u,v : uv = u^2 \rangle$. Clearly, $R$ is reflexive, but not symmetric.' - property: cofiltered-limit-stable epimorphisms - reason: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set \to \Cat$ that maps a set to its discrete category. + reason: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set \to \Cat$ that maps a set to its discrete category. - property: effective cocongruences reason: >- diff --git a/databases/catdat/data/categories/FinGrp.yaml b/databases/catdat/data/categories/FinGrp.yaml index 2baeab87d..ab9d68df3 100644 --- a/databases/catdat/data/categories/FinGrp.yaml +++ b/databases/catdat/data/categories/FinGrp.yaml @@ -41,7 +41,7 @@ satisfied_properties: reason: A direct argument is possible, but this can also be derived from the observation that $\FinGrp$ is the category of group objects in $(\FinSet,\times)$ and Example 2.2.16 in Malcev, protomodular, homological and semi-abelian categories. - property: effective congruences - reason: 'Suppose we have a congruence $f, g : E \rightrightarrows X$ in $\FinGrp$. Since the embedding $\FinGrp \hookrightarrow \Grp$ preserves finite limits, it is also a congruence in $\Grp$. We already know that $\Grp$ has effective congruences since it is algebraic. Using this result, we see that $E$ is the kernel pair of $X \to (X/E)_{\Grp}$ in $\Grp$. Also, the quotient $(X/E)_{\Grp}$ is finite; and the forgetful functor $\FinGrp \to \Grp$ is fully faithful and therefore reflects limits. Thus, we conclude that $E$ is the kernel pair of $X \to (X/E)_{\Grp}$ in $\FinGrp$ as well.' + reason: 'Suppose we have a congruence $f, g : E \rightrightarrows X$ in $\FinGrp$. Since the embedding $\FinGrp \hookrightarrow \Grp$ preserves finite limits, it is also a congruence in $\Grp$. We already know that $\Grp$ has effective congruences since it is algebraic. Using this result, we see that $E$ is the kernel pair of $X \to (X/E)_{\Grp}$ in $\Grp$. Also, the quotient $(X/E)_{\Grp}$ is finite; and the forgetful functor $\FinGrp \to \Grp$ is fully faithful and therefore reflects limits. Thus, we conclude that $E$ is the kernel pair of $X \to (X/E)_{\Grp}$ in $\FinGrp$ as well.' - property: regular reason: The category is Malcev and hence finitely complete, and it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks. @@ -66,13 +66,13 @@ unsatisfied_properties: reason: 'Assume that $C_2 \sqcup C_2$ exists. This is a finite group, say of order $N$, with two involutions $u,v$ such that for every finite group $G$ with two involutions $a,b$ there is a unique homomorphism $\varphi : C_2 \sqcup C_2 \to G$ with $\varphi(u)=a$ and $\varphi(v)=2$. In particular, when $G$ is generated by $a,b$, then $\ord(G) \leq N$. But then the dihedral group $G \coloneqq D_N$ of order $2N$ yields a contradiction.' - property: sequential colimits - reason: This follows from this lemma. + reason: This follows from this lemma. - property: generator reason: If $A,B$ are finite groups whose orders are coprime, then we know that $\Hom(A,B)$ is trivial. But a generator would admit a non-trivial homomorphism to any other non-trivial finite group. - property: cogenerator - reason: 'We apply this lemma to the collection of finite simple groups: Any non-trivial homomorphism from a finite simple group to a finite group must be injective, and for every $n \in \IN$ there is a finite simple group of size $\geq n$ (for example, the alternating group on $n+5$ elements).' + reason: 'We apply this lemma to the collection of finite simple groups: Any non-trivial homomorphism from a finite simple group to a finite group must be injective, and for every $n \in \IN$ there is a finite simple group of size $\geq n$ (for example, the alternating group on $n+5$ elements).' special_objects: initial object: diff --git a/databases/catdat/data/categories/Fld.yaml b/databases/catdat/data/categories/Fld.yaml index beefe4d8b..e0dc367b1 100644 --- a/databases/catdat/data/categories/Fld.yaml +++ b/databases/catdat/data/categories/Fld.yaml @@ -57,7 +57,7 @@ unsatisfied_properties: reason: Assume that $G$ is a generator, say of characteristic $p$. Then for all $q \neq p$ all homomorphisms between two fields of characteristic $q$ would be equal, which is absurd. - property: cogenerating set - reason: 'We apply this lemma to the collection of fields: Any homomorphism of fields 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).' + reason: 'We apply this lemma to the collection of fields: Any homomorphism of fields 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: binary powers reason: 'Assume that the product $P \coloneqq \IQ(\sqrt{2}) \times \IQ(\sqrt{2})$ exists. This field is isomorphic to a subfield of $\IQ(\sqrt{2})$, hence $P \cong \IQ$ or $P \cong \IQ(\sqrt{2})$. In the first case, the two projections $P \rightrightarrows \IQ(\sqrt{2})$ must be equal, which means that every two homomorphisms $K \rightrightarrows \IQ(\sqrt{2})$ are equal, which is absurd (take $K = \IQ(\sqrt{2})$ and its two automorphisms). In the second case, the projections induce for every field $K$ a bijection $\Hom(K,\IQ(\sqrt{2})) \cong \Hom(K,\IQ(\sqrt{2}))^2$, which however fails for $K = \IQ(\sqrt{2})$: the left hand side has $2$ elements, the right hand side has $4$ elements. A more general result about products in $\Fld$ can be found at MSE/359352.' diff --git a/databases/catdat/data/categories/Grp.yaml b/databases/catdat/data/categories/Grp.yaml index fb151ba35..394c9ed43 100644 --- a/databases/catdat/data/categories/Grp.yaml +++ b/databases/catdat/data/categories/Grp.yaml @@ -47,7 +47,7 @@ unsatisfied_properties: reason: Every non-normal subgroup (such as $C_2 \hookrightarrow S_3$) provides a counterexample. - property: cogenerator - reason: 'We apply this lemma to the collection of simple groups: Any non-trivial homomorphism from a simple group to a group must be injective, and for every infinite cardinal $\kappa$ there is a simple group of size $\geq \kappa$ (for example, the alternating group on $\kappa$ elements).' + reason: 'We apply this lemma to the collection of simple groups: Any non-trivial homomorphism from a simple group to a group must be injective, and for every infinite cardinal $\kappa$ there is a simple group of size $\geq \kappa$ (for example, the alternating group on $\kappa$ elements).' - property: coregular reason: This is because injective group homomorphisms are not stable under pushouts, see e.g. MSE/601463 or MSE/5088032. @@ -66,7 +66,7 @@ unsatisfied_properties: reason: 'Assume that $\Grp$ has a (regular) quotient object classifier, i.e. a group $P$ such that every surjective homomorphism $G \to H$ is the cokernel of a unique homomorphism $\varphi : P \to G$. Equivalently, every normal subgroup $N \subseteq G$ is $\langle \langle \varphi(P) \rangle \rangle$ for a unique homomorphism $\varphi : P \to G$, where $\langle \langle - \rangle \rangle$ denotes the normal closure. If $c_g : G \to G$ denotes the conjugation with $g \in G$, then the images of $\varphi$ and $c_g \circ \varphi$ have the same normal closures, so the homomorphisms must be equal. In other words, $\varphi$ factors through the center $Z(G)$. But then every normal subgroup of $G$, in particular $G$ itself, would be contained in $Z(G)$, which is wrong for every non-abelian group $G$.' - property: cofiltered-limit-stable epimorphisms - reason: We already know that $\Ab$ does not have this property. Now apply the contrapositive of the dual of this lemma to the forgetful functor $\Ab \to \Grp$ which indeed preserves epimorphisms. + reason: We already know that $\Ab$ does not have this property. Now apply the contrapositive of the dual of this lemma to the forgetful functor $\Ab \to \Grp$ which indeed preserves epimorphisms. - property: cocartesian cofiltered limits reason: >- diff --git a/databases/catdat/data/categories/Haus.yaml b/databases/catdat/data/categories/Haus.yaml index 04464bab2..0549744d8 100644 --- a/databases/catdat/data/categories/Haus.yaml +++ b/databases/catdat/data/categories/Haus.yaml @@ -66,7 +66,7 @@ unsatisfied_properties: reason: 'It is shown in MSE/1255678 that $\IQ \times - : \Top \to \Top$ does not preserve sequential colimits (so that it cannot be a left adjoint). The same example also works in $\Haus$: Surely $\IQ$ is Hausdorff, $X_n$ is Hausdorff, as is their colimit $X$, and the colimit (taken in $\Top$) of the $X_n \times \IQ$ admits a bijective continuous map to a Hausdorff space, therefore is also Hausdorff, meaning it is also the colimit taken in $\Haus$.' - property: cofiltered-limit-stable epimorphisms - reason: 'Recall the counterexample for sets: The unique maps $\IN_{\geq n} \to 1$ are surjective, but their limit $0 = \bigcap_{n \geq 0} \IN_{\geq n} \to 1$ is not. This also works in $\Haus$ by using discrete topologies. We could also apply a variant of (the dual of) this lemma to the discrete topology functor $\Set \to \Haus$, which does not preserve all cofiltered limits, but does preserve intersections.' + reason: 'Recall the counterexample for sets: The unique maps $\IN_{\geq n} \to 1$ are surjective, but their limit $0 = \bigcap_{n \geq 0} \IN_{\geq n} \to 1$ is not. This also works in $\Haus$ by using discrete topologies. We could also apply a variant of (the dual of) this lemma to the discrete topology functor $\Set \to \Haus$, which does not preserve all cofiltered limits, but does preserve intersections.' - property: filtered-colimit-stable monomorphisms reason: |- diff --git a/databases/catdat/data/categories/Man.yaml b/databases/catdat/data/categories/Man.yaml index 088103b0d..37f73027b 100644 --- a/databases/catdat/data/categories/Man.yaml +++ b/databases/catdat/data/categories/Man.yaml @@ -69,13 +69,13 @@ unsatisfied_properties: reason: See MSE/5129579 or MSE/322485. - property: sequential colimits - reason: If $\Man$ had sequential colimits, then by this lemma there would be a manifold $M$ that admits a split epimorphism $M \to \IR^n$ for every $n$. But then $M$ will have an infinite-dimensional tangent space, which is a contradiction. + reason: If $\Man$ had sequential colimits, then by this lemma there would be a manifold $M$ that admits a split epimorphism $M \to \IR^n$ for every $n$. But then $M$ will have an infinite-dimensional tangent space, which is a contradiction. - property: ℵ₁-accessible reason: 'We already know that $\Set_\c$ does not have $\aleph_1$-filtered colimits. The functor $\pi_0: \Man \to \Set_\c$ is well-defined (because manifolds are second-countable), and it admits a fully faithful right adjoint (regarding a countable set as a discrete manifold). Therefore, $\Man$ does not have $\aleph_1$-filtered colimits.' - property: quotients of congruences - reason: If $\Man$ had quotients of congruences, then by this lemma, it would have a pushout of $\IR \leftarrow \{ 0 \} \rightarrow \IR$. This contradicts MO/19916. + reason: If $\Man$ had quotients of congruences, then by this lemma, it would have a pushout of $\IR \leftarrow \{ 0 \} \rightarrow \IR$. This contradicts MO/19916. special_objects: initial object: diff --git a/databases/catdat/data/categories/Meas.yaml b/databases/catdat/data/categories/Meas.yaml index 0bfb2809c..f0caa3872 100644 --- a/databases/catdat/data/categories/Meas.yaml +++ b/databases/catdat/data/categories/Meas.yaml @@ -44,7 +44,7 @@ satisfied_properties: reason: '[Sketch] Since $\Set$ is infinitary extensive, a map $f : Y \to \coprod_i X_i \eqqcolon X$ corresponds to a decomposition $Y = \coprod_i Y_i$ (as sets) with maps $f_i : Y_i \to X_i$. Endow the measurable subset $Y_i \subseteq Y$ with the restricted $\sigma$-algebra. If $f$ is measurable, each $f_i$ is measurable, and $Y = \coprod_i Y_i$ holds as measurable spaces.' - property: filtered-colimit-stable monomorphisms - reason: This follows from this lemma applied to the forgetful functor to $\Set$. + reason: This follows from this lemma applied to the forgetful functor to $\Set$. - property: regular subobject classifier reason: The set $\{0,1\}$ with the trivial $\sigma$-algebra is a regular subobject classifier since measurable maps $X \to \{0,1\}$ correspond to subsets of $X$. @@ -63,7 +63,7 @@ unsatisfied_properties: reason: See MSE/5027218. - property: cofiltered-limit-stable epimorphisms - reason: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set \to \Meas$ which equips a set with the trivial $\sigma$-algebra. + reason: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set \to \Meas$ which equips a set with the trivial $\sigma$-algebra. - property: effective cocongruences reason: 'The proof is similar to the one for $\Top$: Use the trivial $\sigma$-algebra on a two-point set.' diff --git a/databases/catdat/data/categories/Met.yaml b/databases/catdat/data/categories/Met.yaml index 18e0362b0..cc94ad921 100644 --- a/databases/catdat/data/categories/Met.yaml +++ b/databases/catdat/data/categories/Met.yaml @@ -108,7 +108,7 @@ unsatisfied_properties: for each $x, y \in (0, 1)$. This is reflexive since $d(f(x), f(y)) \le |x-y| < x+y$, and it is clearly symmetric. For transitivity, suppose $f\sim g$ and $g\sim h$. Then for any $\varepsilon > 0$, we have $$d(f(x), h(y)) \le d(f(x), g(\varepsilon)) + d(g(\varepsilon), h(y)) \le (x + \varepsilon) + (y + \varepsilon).$$ Since this holds for every $\varepsilon > 0$, we conclude $d(f(x), h(y)) \le x+y$. - On the other hand, if this cocongruence were effective, then by the dual of this result, it would be the cokernel pair of the equalizer of the two inclusion maps. However, that equalizer is empty, so $E$ would have to be a binary copower of $(0,1)$, which does not exist in $\Met$. + On the other hand, if this cocongruence were effective, then by the dual of this result, it would be the cokernel pair of the equalizer of the two inclusion maps. However, that equalizer is empty, so $E$ would have to be a binary copower of $(0,1)$, which does not exist in $\Met$. special_objects: initial object: diff --git a/databases/catdat/data/categories/Met_c.yaml b/databases/catdat/data/categories/Met_c.yaml index f7854f0c8..3bbc433cf 100644 --- a/databases/catdat/data/categories/Met_c.yaml +++ b/databases/catdat/data/categories/Met_c.yaml @@ -70,7 +70,7 @@ unsatisfied_properties: reason: See MO/510316. - property: quotients of congruences - reason: If $\Met_c$ had quotients of congruences, then by this lemma it would have sequential colimits of sequences of monomorphisms. This contradicts MO/510316. + reason: If $\Met_c$ had quotients of congruences, then by this lemma it would have sequential colimits of sequences of monomorphisms. This contradicts MO/510316. special_objects: initial object: diff --git a/databases/catdat/data/categories/Met_oo.yaml b/databases/catdat/data/categories/Met_oo.yaml index d4d0754c4..68b40c28a 100644 --- a/databases/catdat/data/categories/Met_oo.yaml +++ b/databases/catdat/data/categories/Met_oo.yaml @@ -55,7 +55,7 @@ unsatisfied_properties: reason: We can copy the proof from $\Met$. - property: cofiltered-limit-stable epimorphisms - reason: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set \to \Met_{\infty}$ that equips a set with the discrete topology. + reason: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set \to \Met_{\infty}$ that equips a set with the discrete topology. - property: effective cocongruences reason: The same counterexample as for $\Met$ works here. The difference in this case is that a binary copower of two copies of $(0,1)$ does exist in $\Met_\infty$. However, this would assign a distance of $\infty$ between points in $(-1,0)$ and points in $(0,1)$, which does not agree with the chosen subspace metric on $(-1,0) \cup (0,1)$. diff --git a/databases/catdat/data/categories/Mon.yaml b/databases/catdat/data/categories/Mon.yaml index ecd4f46b5..bbdef26bf 100644 --- a/databases/catdat/data/categories/Mon.yaml +++ b/databases/catdat/data/categories/Mon.yaml @@ -40,7 +40,7 @@ unsatisfied_properties: reason: 'Consider the submonoid $\{(a,b) : a \leq b \}$ of $\IN^2$.' - property: cogenerator - reason: 'We apply this lemma to the collection of simple groups: Any non-trivial homomorphism $G \to M$ from a simple group $G$ to a monoid $M$ must be injective (as it corestricts to a homomorphism of groups $G \to M^{\times}$), and for every infinite cardinal $\kappa$ there is a simple group of size $\geq \kappa$ (for example, the alternating group on $\kappa$ elements).' + reason: 'We apply this lemma to the collection of simple groups: Any non-trivial homomorphism $G \to M$ from a simple group $G$ to a monoid $M$ must be injective (as it corestricts to a homomorphism of groups $G \to M^{\times}$), and for every infinite cardinal $\kappa$ there is a simple group of size $\geq \kappa$ (for example, the alternating group on $\kappa$ elements).' - property: counital reason: The canonical morphism $\IN \sqcup \IN \to \IN \times \IN$ is not a monomorphism since $\IN \sqcup \IN$ is not commutative. @@ -59,10 +59,10 @@ unsatisfied_properties: reason: 'Assume that $\Omega$ is a regular subobject classifier. Since the trivial monoid is a zero object, every regular submonoid $U \subseteq M$ of any monoid $M$ would have the form $\{m \in M : h(m) = 1 \}$ for some homomorphism $M \to \Omega$. Now take any monoid $M$ with zero that has two different homomorphisms with zero $f,g : M \rightrightarrows N$ (for example, let $M = N = \{0\} \cup \{x^n : n \geq 0\}$ be the free monoid with zero on one generator, $f(x) = 0$,and $g(x) = x$). Take their equalizer $U \subseteq M$, and choose a homomorphism $h : M \to \Omega$ with $U = \{m \in M : h(m) = 1\}$. Since $0 \in U$, we have $h(0)=1$. But then for all $m \in M$ we have $h(m) = h(m) h(0) = h(m 0) = h(0) = 1$, i.e. $U = M$, which yields the contradiction $f = g$.' - property: regular quotient object classifier - reason: We can just copy the proof for $\CMon$. Alternatively, we may use this lemma (dualized). + reason: We can just copy the proof for $\CMon$. Alternatively, we may use this lemma (dualized). - property: cofiltered-limit-stable epimorphisms - reason: We already know that $\Grp$ does not have this property. Now apply the contrapositive of the dual of this lemma to the forgetful functor $\Grp \to \Mon$. It preserves epimorphisms since it has a right adjoint, the unit group functor. + reason: We already know that $\Grp$ does not have this property. Now apply the contrapositive of the dual of this lemma to the forgetful functor $\Grp \to \Mon$. It preserves epimorphisms since it has a right adjoint, the unit group functor. - property: cocartesian cofiltered limits reason: 'We know that $\Grp$ fails to satisfy this property. The same counterexample works here since the inclusion $\Grp \hookrightarrow \Mon$ preserves limits and colimits (it has a left and a right adjoint) and is conservative. A similar counterexample is given by the free monoids $N_n = \langle x_1,\dotsc,x_n \rangle$ and the Boolean monoid $M = \langle e : e^2=e \rangle$ with the maps $N_{n+1} \to N_n$, $x_{n+1} \mapsto 1$. Then the element $(x_1 e \cdots x_n e) \in \lim_n (M \sqcup N_n)$ does not come from $M \sqcup \lim_n N_n$ because its components have unbounded free product length.' diff --git a/databases/catdat/data/categories/N_oo.yaml b/databases/catdat/data/categories/N_oo.yaml index 9f1538953..1f5cd0a63 100644 --- a/databases/catdat/data/categories/N_oo.yaml +++ b/databases/catdat/data/categories/N_oo.yaml @@ -45,7 +45,7 @@ unsatisfied_properties: reason: Consider the strictly increasing sequence $0 < 1 < 2 < \cdots$. - property: finitary algebraic - reason: This follows from this lemma. + reason: This follows from this lemma. special_objects: initial object: diff --git a/databases/catdat/data/categories/Pos.yaml b/databases/catdat/data/categories/Pos.yaml index a1eda4c8b..c16373103 100644 --- a/databases/catdat/data/categories/Pos.yaml +++ b/databases/catdat/data/categories/Pos.yaml @@ -63,7 +63,7 @@ unsatisfied_properties: - property: effective cocongruences reason: |- Let $X$ be $\IR$ with the standard (total) order, and let $E$ be the poset with underlying set $\IR \times \{ 0, 1 \}$ and partial order such that $(x, m) \le (y, n)$ if and only if $x < y$ or $(x, m) = (y, n)$. The two maps $\IR \rightrightarrows E$ will be $x \mapsto (x, 0)$ and $x \mapsto (x, 1)$ respectively. For any partial order $(\IP, \le)$, the induced equivalence relation on the set of order-preserving functions $\IR \to \IP$ is that $f \sim g$ if and only if $f(x) \le g(y)$ and $g(x) \le f(y)$ whenever $x < y$. This relation is clearly reflexive and symmetric; for transitivity, if $f \sim g$ and $g \sim h$, then whenever $x < y$, we have $f(x) \le g(\frac{x+y}{2}) \le h(y)$ and similarly $h(x) \le g(\frac{x+y}{2}) \le f(y)$, showing that $f \sim h$. - On the other hand, if this cocongruence on $\IR$ were effective, then by the dual of this result, $E$ would be the cokernel pair of the equalizer of the two maps $\IR \rightrightarrows E$. However, that equalizer is the empty poset, so $E$ would have to be the coproduct poset $\IR + \IR$, giving a contradiction. + On the other hand, if this cocongruence on $\IR$ were effective, then by the dual of this result, $E$ would be the cokernel pair of the equalizer of the two maps $\IR \rightrightarrows E$. However, that equalizer is the empty poset, so $E$ would have to be the coproduct poset $\IR + \IR$, giving a contradiction. special_objects: initial object: diff --git a/databases/catdat/data/categories/Prost.yaml b/databases/catdat/data/categories/Prost.yaml index 5c0f008a4..606062c04 100644 --- a/databases/catdat/data/categories/Prost.yaml +++ b/databases/catdat/data/categories/Prost.yaml @@ -57,7 +57,7 @@ unsatisfied_properties: reason: 'See MO/509552: Consider the forgetful functor $U : \Prost \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) \coloneqq \{(a,b) \in U(A)^2 : a \leq b\}$. Both are representable: $U$ by the singleton preordered set and $R$ by $\{0 \leq 1 \}$. It is clear that $R$ is reflexive, but not symmetric.' - property: cofiltered-limit-stable epimorphisms - reason: We know that $\Set$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the functor $\Set \to \Prost$ that equips a set with the chaotic preorder. + reason: We know that $\Set$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the functor $\Set \to \Prost$ that equips a set with the chaotic preorder. - property: effective cocongruences reason: 'Consider the proset $E \coloneqq \{ a, b \}$ with the chaotic preorder. This represents the functor which sends a proset to the pairs of elements $x,y$ with $x \le y$ and $y \le x$. Therefore, it defines a cocongruence $1 \rightrightarrows E$, where the maps are the two possible functions. However, this cannot be effective: for any map $h : Z \to 1$ which equalizes the two functions, $Z$ must be empty. But that means the cokernel pair of $h$ is the two-element proset with the trivial preorder.' diff --git a/databases/catdat/data/categories/Ring.yaml b/databases/catdat/data/categories/Ring.yaml index 13b0cc3b4..0d40e8094 100644 --- a/databases/catdat/data/categories/Ring.yaml +++ b/databases/catdat/data/categories/Ring.yaml @@ -44,7 +44,7 @@ unsatisfied_properties: reason: This is because already the full subcategory $\CRing$ does not have this property. - property: cogenerating set - reason: '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).' + reason: '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 reason: '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$.' @@ -56,7 +56,7 @@ unsatisfied_properties: reason: '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.' - property: regular quotient object classifier - reason: 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 this lemma (dualized). + reason: 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 this lemma (dualized). - property: cocartesian cofiltered limits reason: >- @@ -65,7 +65,7 @@ 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 - reason: We know that $\CRing$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the forgetful functor $\CRing \to \Ring$. It preserves epimorphisms by MSE/5133488. + reason: We know that $\CRing$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the forgetful functor $\CRing \to \Ring$. It preserves epimorphisms by MSE/5133488. - property: effective cocongruences reason: See MO/510744. diff --git a/databases/catdat/data/categories/Rng.yaml b/databases/catdat/data/categories/Rng.yaml index 34ed7537f..ab1bfbfd2 100644 --- a/databases/catdat/data/categories/Rng.yaml +++ b/databases/catdat/data/categories/Rng.yaml @@ -37,7 +37,7 @@ unsatisfied_properties: reason: The inclusion $\IZ \hookrightarrow \IQ$ is a counterexample. (The proof can be reduced to the unital case.) - property: cogenerator - reason: '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$.' + reason: '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$.' - property: counital reason: >- @@ -62,7 +62,7 @@ unsatisfied_properties: reason: '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.' - property: regular quotient object classifier - reason: '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 this lemma (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).' + reason: '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 this lemma (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).' - property: cocartesian cofiltered limits reason: >- @@ -71,7 +71,7 @@ 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 - reason: 'We know that $\Ring$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the forgetful functor $\Ring \to \Rng$. We only need to verify that it preserves epimorphisms: Let $f : R \to S$ be an epimorphism in $\Ring$ and let $g,h : S \rightrightarrows T$ be two homomorphisms of rngs with $gf = hf$. The element $e = g(1) = h(1) \in T$ is idempotent, and $g,h$ become homomorphisms of rings $S \rightrightarrows eTe$. Hence, $g=h$.' + reason: 'We know that $\Ring$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the forgetful functor $\Ring \to \Rng$. We only need to verify that it preserves epimorphisms: Let $f : R \to S$ be an epimorphism in $\Ring$ and let $g,h : S \rightrightarrows T$ be two homomorphisms of rngs with $gf = hf$. The element $e = g(1) = h(1) \in T$ is idempotent, and $g,h$ become homomorphisms of rings $S \rightrightarrows eTe$. Hence, $g=h$.' - property: effective cocongruences reason: >- diff --git a/databases/catdat/data/categories/Sch.yaml b/databases/catdat/data/categories/Sch.yaml index 535776bec..a56841135 100644 --- a/databases/catdat/data/categories/Sch.yaml +++ b/databases/catdat/data/categories/Sch.yaml @@ -54,7 +54,7 @@ unsatisfied_properties: reason: If $S$ is a generating set of schemes, then the set of affine open subsets of the schemes in $S$ would also be a generating set. This is then also a generating set in the category of affine schemes, corresponding to a cogenerating set in $\CRing$, which we know does not exist. - property: quotients of congruences - reason: If $\Sch$ had quotients of congruences, then by this lemma it would also have pushouts of monomorphisms, contradicting the fact that the span $\IA^1 \leftarrow \Spec(k(t)) \rightarrow \IA^1$ has no pushout - see MO/9961. + reason: If $\Sch$ had quotients of congruences, then by this lemma it would also have pushouts of monomorphisms, contradicting the fact that the span $\IA^1 \leftarrow \Spec(k(t)) \rightarrow \IA^1$ has no pushout - see MO/9961. special_objects: initial object: diff --git a/databases/catdat/data/categories/SemiGrp.yaml b/databases/catdat/data/categories/SemiGrp.yaml index cfab03e44..b066f7168 100644 --- a/databases/catdat/data/categories/SemiGrp.yaml +++ b/databases/catdat/data/categories/SemiGrp.yaml @@ -63,7 +63,7 @@ unsatisfied_properties: is a normal subgroup of $G$. It is proper, and hence trivial. But then $f$ is injective, which is a contradiction. - property: cofiltered-limit-stable epimorphisms - reason: We already know that $\Set$ does not have this property (by this result). Now apply the contrapositive of the dual of this lemma to the functor $\Set \to \SemiGrp$ that equips a set with the multiplication $a \cdot b \coloneqq a$. + reason: We already know that $\Set$ does not have this property (by this result). Now apply the contrapositive of the dual of this lemma to the functor $\Set \to \SemiGrp$ that equips a set with the multiplication $a \cdot b \coloneqq a$. - property: effective cocongruences reason: >- @@ -73,7 +73,7 @@ unsatisfied_properties: - property: natural numbers object reason: >- - Assume that a natural numbers object exists. Then by this result, for every semigroup $A$ the natural homomorphism + Assume that a natural numbers object exists. Then by this result, for every semigroup $A$ the natural homomorphism $$\textstyle\alpha : \coprod_{n \geq 0} A \to A \times \coprod_{n \geq 0} 1$$ is a split monomorphism. But this is not true: For each $n \geq 0$ let $A_n$ denote a copy of $A$. The elements of the coproduct in $\alpha$'s domain have a unique representation as $$x_{n_1} * \cdots * x_{n_s}$$ diff --git a/databases/catdat/data/categories/Set_c.yaml b/databases/catdat/data/categories/Set_c.yaml index 20fa28b60..e949660db 100644 --- a/databases/catdat/data/categories/Set_c.yaml +++ b/databases/catdat/data/categories/Set_c.yaml @@ -51,7 +51,7 @@ satisfied_properties: reason: By elementary set theory, a countable (disjoint) union of countable sets is again countable. Hence, countable coproducts exist in $\Set_\c$, and we already saw that finite products exist. The distributivity morphism is an isomorphism since this is the case in $\Set$ and the forgetful functor $\Set_\c \to \Set$ preserves finite products and countable coproducts. - property: effective congruences - reason: 'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\c$. Then using $1$ as a test object, we see that this induces an equivalence relation on $X$. We already know that $\Set$ has effective congruences (as does every topos). Using this result, we see that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set$. Also, the quotient $(X/E)_{\Set}$ is countable; and the forgetful functor $\Set_\c \to \Set$ is fully faithful and therefore reflects limits. Thus, we conclude that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set_\c$ as well.' + reason: 'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\c$. Then using $1$ as a test object, we see that this induces an equivalence relation on $X$. We already know that $\Set$ has effective congruences (as does every topos). Using this result, we see that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set$. Also, the quotient $(X/E)_{\Set}$ is countable; and the forgetful functor $\Set_\c \to \Set$ is fully faithful and therefore reflects limits. Thus, we conclude that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set_\c$ as well.' - property: regular reason: From the other properties we know that the category is finitely complete and that it has coequalizers. The regular epimorphisms are stable under pullback since this holds in $\Set$ and both regular epimorphisms (they are surjective maps) and pullbacks coincide. diff --git a/databases/catdat/data/categories/Set_f.yaml b/databases/catdat/data/categories/Set_f.yaml index f94ba80a3..0e4705031 100644 --- a/databases/catdat/data/categories/Set_f.yaml +++ b/databases/catdat/data/categories/Set_f.yaml @@ -45,7 +45,7 @@ satisfied_properties: reason: 'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\f$. From the proof on quotients of congruences in $\Set_\f$, we have a quotient map $p : X \to X/E$ in $\Set_\f$, and $E$ is the kernel pair of $p$ in $\Set$. It remains to see that $E$ is also the kernel pair of $p$ in $\Set_f$. Thus, suppose we have $x_1, x_2 : T \rightrightarrows X$ with $p \circ x_1 = p \circ x_2$. Then there is a unique $e : T \to E$ in $\Set$ with $x_1 = f\circ e$ and $x_2 = g\circ e$. Since $f\circ e$ is finite-to-one, we must have $e$ is finite-to-one as well.' - property: effective cocongruences - reason: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Set_f$. Then it is a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences, that implies $E$ is the cokernel pair of some function $h : Z \to X$ in $\Set$. By the dual of this result, if $\inc_Y : Y \hookrightarrow X$ is the equalizer of $f$ and $g$, then $E$ is also the cokernel pair of $\inc_Y$ in $\Set$. It remains to see that $E$ is the cokernel pair of $\inc_Y$ in $\Set_\f$ as well. Thus, suppose $a, b : X \rightrightarrows T$ are such that $a |_Y = b |_Y$. Then there is a unique $c : E\to T$ in $\Set$ with $a = c\circ f$ and $b = c\circ g$. Since $(f;g) : X + X \to E$ is surjective and $c \circ (f;g) = (a;b)$ is finite-to-one, we see $c$ is finite-to-one as well.' + reason: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Set_f$. Then it is a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences, that implies $E$ is the cokernel pair of some function $h : Z \to X$ in $\Set$. By the dual of this result, if $\inc_Y : Y \hookrightarrow X$ is the equalizer of $f$ and $g$, then $E$ is also the cokernel pair of $\inc_Y$ in $\Set$. It remains to see that $E$ is the cokernel pair of $\inc_Y$ in $\Set_\f$ as well. Thus, suppose $a, b : X \rightrightarrows T$ are such that $a |_Y = b |_Y$. Then there is a unique $c : E\to T$ in $\Set$ with $a = c\circ f$ and $b = c\circ g$. Since $(f;g) : X + X \to E$ is surjective and $c \circ (f;g) = (a;b)$ is finite-to-one, we see $c$ is finite-to-one as well.' - property: locally cartesian closed reason: If $X$ is a set, the equivalence $\Set/X \simeq \Set^X$, $f \mapsto (f^*(\{x\}))_{x \in X}$ restricts to an equivalence $\Set_\f / X \simeq \FinSet^X$. This category is cartesian closed since $\FinSet$ is cartesian closed and products of cartesian closed categories are cartesian closed. diff --git a/databases/catdat/data/categories/Set_pointed.yaml b/databases/catdat/data/categories/Set_pointed.yaml index 99e6d452f..8c6899357 100644 --- a/databases/catdat/data/categories/Set_pointed.yaml +++ b/databases/catdat/data/categories/Set_pointed.yaml @@ -67,7 +67,7 @@ unsatisfied_properties: reason: 'Every cokernel is "injective away from the base point". Formally, if $p : A \to B$ is a cokernel in $\Set_*$, it has the property that $p(x)=p(y) \neq 0$ implies $x=y$ (where $0$ denotes the base point). Clearly this is not satisfied for every surjective pointed map, consider $(\IN,0) \to (\{0,1\},0)$ defined by $0 \mapsto 0$ and $x \mapsto 1$ for $x > 0$.' - property: cofiltered-limit-stable epimorphisms - reason: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set \to \Set_*$ that freely adds a base point. + reason: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set \to \Set_*$ that freely adds a base point. special_objects: initial object: diff --git a/databases/catdat/data/categories/Setne.yaml b/databases/catdat/data/categories/Setne.yaml index dfc8e122e..79eef9fd3 100644 --- a/databases/catdat/data/categories/Setne.yaml +++ b/databases/catdat/data/categories/Setne.yaml @@ -50,7 +50,7 @@ satisfied_properties: reason: Any natural numbers object in $\Set$, such as $(\IN,0,n \mapsto n+1)$, is clearly also one in $\Setne$. - property: filtered-colimit-stable monomorphisms - reason: This follows from this lemma applied to the forgetful functor to $\Set$. + reason: This follows from this lemma applied to the forgetful functor to $\Set$. - property: multi-complete reason: Let $D$ be a diagram in $\Setne$, and let $L$ be a limit of $D$ in $\Set$. If $L$ is non-empty, it gives a limit in $\Setne$ as well. If $L$ is the empty set, there is no cone over $D$ in $\Setne$; hence the empty set of cones gives a multi-limit of $D$ in $\Setne$. diff --git a/databases/catdat/data/categories/Sp.yaml b/databases/catdat/data/categories/Sp.yaml index 22a5d9a42..62c23aeff 100644 --- a/databases/catdat/data/categories/Sp.yaml +++ b/databases/catdat/data/categories/Sp.yaml @@ -21,7 +21,7 @@ satisfied_properties: reason: The category is equivalent to $\prod_{n \geq 0} \Sigma_n{-}\FinSet$ (where $\Sigma_n$ denotes the symmetric group of order $n$), and each $\Sigma_n{-}\FinSet$ is an elementary topos since is $\FinSet$ an elementary topos and $\Sigma_n$ is a finite group, cf. Johnstone, Part B, Corollary 2.3.18. - property: cogenerator - reason: 'This follows from $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$, this lemma, and the fact that if $G$ is a (finite) group, the power set $P(G)$ with the evident $G$-action is a weakly terminal cogenerator in $G{-}\Set$ (resp. $G{-}\FinSet$). For the proof, notice that $\varnothing,G \in P(G)$ are fixed points, yielding two $G$-maps $1 \rightrightarrows P(G)$. In particular, $P(G)$ is weakly terminal. If $X$ is a $G$-set with distinct points $x,y$, we construct a $G$-map $f : X \to P(G)$ that separates $x,y$: First, $X$ is a coproduct of orbits. If $x,y$ lie in different orbits, let $f|_{Gx}$ be constant $\varnothing$, $f|_{Gy}$ be constant $G$, and, say, $f$ be constant $\varnothing$ on all other orbits. If $x,y$ lie in the same orbit, say $y = g_0 x$, define $f|_{Gx} : Gx \to P(G)$ by $f(x) = G_x$ (stabilizer), which is well-defined, and choose $f$ to be $\varnothing$ on all other orbits. Then $f(y) = g_0 G_x \neq G_x = f(x)$.' + reason: 'This follows from $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$, this lemma, and the fact that if $G$ is a (finite) group, the power set $P(G)$ with the evident $G$-action is a weakly terminal cogenerator in $G{-}\Set$ (resp. $G{-}\FinSet$). For the proof, notice that $\varnothing,G \in P(G)$ are fixed points, yielding two $G$-maps $1 \rightrightarrows P(G)$. In particular, $P(G)$ is weakly terminal. If $X$ is a $G$-set with distinct points $x,y$, we construct a $G$-map $f : X \to P(G)$ that separates $x,y$: First, $X$ is a coproduct of orbits. If $x,y$ lie in different orbits, let $f|_{Gx}$ be constant $\varnothing$, $f|_{Gy}$ be constant $G$, and, say, $f$ be constant $\varnothing$ on all other orbits. If $x,y$ lie in the same orbit, say $y = g_0 x$, define $f|_{Gx} : Gx \to P(G)$ by $f(x) = G_x$ (stabilizer), which is well-defined, and choose $f$ to be $\varnothing$ on all other orbits. Then $f(y) = g_0 G_x \neq G_x = f(x)$.' unsatisfied_properties: - property: skeletal @@ -37,7 +37,7 @@ unsatisfied_properties: reason: 'Any function $f : \IN \to \IN$ can be regarded as a combinatorial species with trivial actions, and distinct functions yield non-isomorphic species.' - property: countable powers - reason: If $\Sp \simeq \FinSet \times \prod_{n > 0} \Sigma_n{-}\FinSet$ has countable powers, then $\FinSet$ has countable powers as well by this lemma, which we already know is false. + reason: If $\Sp \simeq \FinSet \times \prod_{n > 0} \Sigma_n{-}\FinSet$ has countable powers, then $\FinSet$ has countable powers as well by this lemma, which we already know is false. - property: semi-strongly connected reason: 'For $n \geq 0$ let $E_n$ be the combinatorial species of $n$-sets: $E_n(A) = \{A\}$ when $A$ has cardinality $n$, otherwise $E_n(A) = \varnothing$. Then there is no morphism between $E_n$ and $E_m$ unless $n = m$.' diff --git a/databases/catdat/data/categories/Top.yaml b/databases/catdat/data/categories/Top.yaml index 3cb1e221a..4987813a2 100644 --- a/databases/catdat/data/categories/Top.yaml +++ b/databases/catdat/data/categories/Top.yaml @@ -50,7 +50,7 @@ satisfied_properties: reason: The category has all limits and colimits, and the regular monomorphisms are the subspace inclusions. Thus, it suffices to prove that subspace inclusions are stable under pushouts. For a proof see e.g. Lemma 3.6 at the nLab. - property: filtered-colimit-stable monomorphisms - reason: This follows from this lemma applied to the forgetful functor to $\Set$. + reason: This follows from this lemma applied to the forgetful functor to $\Set$. unsatisfied_properties: - property: skeletal @@ -78,7 +78,7 @@ unsatisfied_properties: reason: 'Assume $\Top$ is coaccessible. Let $p : S \to I$ be the identity map from the Sierpinski space to the two-element indiscrete space. Then, a topological space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete spaces, which is equivalent to $\Set$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\Set$ is not coaccessible, this is a contradiction.' - property: cofiltered-limit-stable epimorphisms - reason: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set \to \Top$ which equips a set with the indiscrete topology. + reason: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set \to \Top$ which equips a set with the indiscrete topology. - property: effective cocongruences reason: 'Consider the indiscrete topological space $I$ on two points. This represents the functor which takes a topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $1 \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: if we have $h : Z\to 1$ which equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete space on two points.' diff --git a/databases/catdat/data/categories/Top_pointed.yaml b/databases/catdat/data/categories/Top_pointed.yaml index d9f3e38ca..80a6113ad 100644 --- a/databases/catdat/data/categories/Top_pointed.yaml +++ b/databases/catdat/data/categories/Top_pointed.yaml @@ -61,7 +61,7 @@ satisfied_properties: is open. It suffices to consider open sets of two types: (1) If $U \subseteq X$ is open, the $\alpha$-image of $U \vee \lim_i Y_i$ is $p_{i_0}^{-1}(U \vee Y_{i_0})$ for any chosen index $i_0$, hence open. (2) If $i$ is an index and $V_i \subseteq Y_i$ is open, then the $\alpha$-image of $X \vee (p_i^{-1}(V_i) \cap \lim_i Y_i)$ is $p_i^{-1}(X \vee V_i)$, hence open. - property: filtered-colimit-stable monomorphisms - reason: This follows from this lemma applied to the forgetful functor to $\Set$. + reason: This follows from this lemma applied to the forgetful functor to $\Set$. - property: coregular reason: Regular monomorphisms coincide with the embeddings (see below). Since $\Top$ is coregular, they are stable under pushouts, and pushouts in $\Top_*$ are the same. @@ -99,10 +99,10 @@ unsatisfied_properties: reason: 'We can adjust the proof for $\Top$ as follows: Assume $\Top_*$ is coaccessible. Let $S_0=\{x,*\}$ be the pointed topological space such that $\{*\}$ is the only non-trivial open set, and let $S_1=\{x,*\}$ be the pointed space such that $\{x\}$ is the only non-trivial open set. Let $p_i : S_i \to \{x,*\}$ be the identity function to the two-element indiscrete pointed space. Then, a pointed topological space is discrete if and only if it is projective to the morphisms $p_0$ and $p_1$. This implies that the full subcategory spanned by all discrete pointed spaces, which is equivalent to $\Set_*$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\Set_*$ is not coaccessible, this is a contradiction.' - property: cofiltered-limit-stable epimorphisms - reason: We already know that $\Set_*$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set_* \to \Top_*$ that equips a pointed set with the indiscrete topology. + reason: We already know that $\Set_*$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set_* \to \Top_*$ that equips a pointed set with the indiscrete topology. - property: effective congruences - reason: Suppose that $\Top_*$ had effective congruences. Then by this result, $\Top$ would also have effective congruences, which we know is not the case. + reason: Suppose that $\Top_*$ had effective congruences. Then by this result, $\Top$ would also have effective congruences, which we know is not the case. - property: effective cocongruences reason: 'This counterexample is adapted from the counterexample for $\Top$. Consider the pointed topological space $I \coloneqq \{ *, a, b \}$ with topology $\{ \varnothing, \{ * \}, \{ a, b \}, \{ *, a, b \} \}$. This represents the functor which sends a pointed topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $\{ *, a \} \rightrightarrows I$ on the discrete space $\{ *, a \}$, where the maps are $*\mapsto *, a\mapsto a$ and $*\mapsto *, a\mapsto b$ respectively. However, this cannot be effective: if we have $h : Z \to \{ *, a \}$ which equalizes the cocongruence, then $h$ must be the constant function with value $*$. But that means the cokernel pair of $h$ is the discrete space on $\{ *, a, b \}$.' diff --git a/databases/catdat/data/categories/Z.yaml b/databases/catdat/data/categories/Z.yaml index 7a4f42c02..66753364e 100644 --- a/databases/catdat/data/categories/Z.yaml +++ b/databases/catdat/data/categories/Z.yaml @@ -46,10 +46,10 @@ satisfied_properties: check_redundancy: false - property: effective congruences - reason: 'If we have a congruence $E \rightrightarrows X$ in $[\CRing, \Set]$, then evaluating at any commutative ring gives a congruence in $\Set$. Defining $Y$ pointwise to be the quotient of this congruence, we get a morphism of functors $h : X \to Y$, and by this result applied pointwise, the kernel pair of $h$ is $E$.' + reason: 'If we have a congruence $E \rightrightarrows X$ in $[\CRing, \Set]$, then evaluating at any commutative ring gives a congruence in $\Set$. Defining $Y$ pointwise to be the quotient of this congruence, we get a morphism of functors $h : X \to Y$, and by this result applied pointwise, the kernel pair of $h$ is $E$.' - property: effective cocongruences - reason: 'If we have a cocongruence $X\rightrightarrows E$ in $[\CRing, \Set]$, then evaluating at any commutative gives a cocongruence in $\Set$. Defining $Y$ pointwise to be the equalizer of the pair, we get a morphism of functors $h : Y \to X$, and by the dual of this result applied pointwise, the cokernel pair of $h$ is $E$.' + reason: 'If we have a cocongruence $X\rightrightarrows E$ in $[\CRing, \Set]$, then evaluating at any commutative gives a cocongruence in $\Set$. Defining $Y$ pointwise to be the equalizer of the pair, we get a morphism of functors $h : Y \to X$, and by the dual of this result applied pointwise, the cokernel pair of $h$ is $E$.' check_redundancy: false unsatisfied_properties: @@ -72,7 +72,7 @@ unsatisfied_properties: reason: 'Consider the functor $F$ from MO/390611 for example. The collection of subobjects of $F$ is not isomorphic to a set: for each infinite cardinal $\kappa$, simply cut off the construction of $F$ at $\kappa$. This yields a different subobject for each $\kappa$.' - property: cofiltered-limit-stable epimorphisms - reason: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set \to [\CRing, \Set]$ that maps a set to its constant functor. + reason: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set \to [\CRing, \Set]$ that maps a set to its constant functor. special_objects: initial object: diff --git a/databases/catdat/data/categories/sSet.yaml b/databases/catdat/data/categories/sSet.yaml index db08c4ea2..1b6ba6455 100644 --- a/databases/catdat/data/categories/sSet.yaml +++ b/databases/catdat/data/categories/sSet.yaml @@ -25,7 +25,7 @@ satisfied_properties: reason: Let $X,Y$ be two simplicial sets. Assume that $X_0$ is empty. Then $X_n$ is empty for all $n$ since there is a morphism $[0] \to [n]$, hence a map $X_n \to X_0$. So there is a morphism $X \to Y$ for trivial reasons. If $X_0$ is non-empty, pick an element. By the Yoneda Lemma it corresponds to a morphism $\Delta^0 \to X$. Since $\Delta^0 = 1$ is terminal, there is a morphism $Y \to \Delta^0$, and these compose to a morphism $Y \to X$. - property: generator - reason: 'Let $\Delta^n \coloneqq \Hom([n],-)$ be the standard $n$-simplex for $n \geq 0$. The set $\{\Delta^n : n \geq 0\}$ is a generating set by the Yoneda Lemma. For all $n,m$ there is a morphism $[n] \to [m]$ in $\Delta$ and hence a morphism $\Delta^m \to \Delta^n$ in $\sSet$. Then by this lemma the coproduct $\coprod_{n \geq 0} \Delta^n$ is a generator in $\sSet$.' + reason: 'Let $\Delta^n \coloneqq \Hom([n],-)$ be the standard $n$-simplex for $n \geq 0$. The set $\{\Delta^n : n \geq 0\}$ is a generating set by the Yoneda Lemma. For all $n,m$ there is a morphism $[n] \to [m]$ in $\Delta$ and hence a morphism $\Delta^m \to \Delta^n$ in $\sSet$. Then by this lemma the coproduct $\coprod_{n \geq 0} \Delta^n$ is a generator in $\sSet$.' - property: locally strongly finitely presentable reason: This follows from the fact that every category of presheaves over a small category is locally strongly finitely presentable. diff --git a/databases/catdat/data/categories/walking_commutative_square.yaml b/databases/catdat/data/categories/walking_commutative_square.yaml index 273cc3ece..402481f80 100644 --- a/databases/catdat/data/categories/walking_commutative_square.yaml +++ b/databases/catdat/data/categories/walking_commutative_square.yaml @@ -41,7 +41,7 @@ unsatisfied_properties: reason: There is no morphism between $b$ and $c$ (resp., between $(0,1)$ and $(1,0)$). - property: finitary algebraic - reason: This follows from this lemma. + reason: This follows from this lemma. special_objects: initial object: diff --git a/databases/catdat/data/categories/walking_composable_pair.yaml b/databases/catdat/data/categories/walking_composable_pair.yaml index bbb13bbd5..7b1bcb158 100644 --- a/databases/catdat/data/categories/walking_composable_pair.yaml +++ b/databases/catdat/data/categories/walking_composable_pair.yaml @@ -36,7 +36,7 @@ satisfied_properties: unsatisfied_properties: - property: finitary algebraic - reason: This follows from this lemma. + reason: This follows from this lemma. special_objects: initial object: diff --git a/databases/catdat/data/category-implications/topos.yaml b/databases/catdat/data/category-implications/topos.yaml index cb2943ca4..14ef4c6da 100644 --- a/databases/catdat/data/category-implications/topos.yaml +++ b/databases/catdat/data/category-implications/topos.yaml @@ -57,7 +57,7 @@ - exact filtered colimits - infinitary extensive - locally presentable - reason: A Grothendieck topos is locally presentable by Prop. 3.4.16 in Handbook of Categorical Algebra Vol. 3, has a cogenerator (see nLab) and is infinitary extensive by Giraud's Theorem. To show that it has exact filtered colimits, first observe that this is clearly true in every presheaf topos (since $\Set$ has the property). Every Grothendieck topos is a full reflective subcategory of a presheaf topos such that the reflector preserves finite limits (nLab), so we conclude with this lemma. + reason: A Grothendieck topos is locally presentable by Prop. 3.4.16 in Handbook of Categorical Algebra Vol. 3, has a cogenerator (see nLab) and is infinitary extensive by Giraud's Theorem. To show that it has exact filtered colimits, first observe that this is clearly true in every presheaf topos (since $\Set$ has the property). Every Grothendieck topos is a full reflective subcategory of a presheaf topos such that the reflector preserves finite limits (nLab), so we conclude with this lemma. is_equivalence: false - id: topos_is_locally_cartesian_closed diff --git a/databases/catdat/data/category-properties/additive.yaml b/databases/catdat/data/category-properties/additive.yaml index f794892b1..3ea1196bf 100644 --- a/databases/catdat/data/category-properties/additive.yaml +++ b/databases/catdat/data/category-properties/additive.yaml @@ -1,6 +1,6 @@ id: additive relation: is -description: A category is additive if it is preadditive and has finite products (equivalently, finite coproducts). Note that in the context of finite products, the preadditive structure is unique. +description: A category is additive if it is preadditive and has finite products (equivalently, finite coproducts). Note that in the context of finite products, the preadditive structure is unique. nlab_link: https://ncatlab.org/nlab/show/additive+category dual_property: additive invariant_under_equivalences: true diff --git a/databases/catdat/data/lemmas/cogenerators_in_product_categories.yaml b/databases/catdat/data/lemmas/cogenerators_in_product_categories.yaml deleted file mode 100644 index 3bfa581ba..000000000 --- a/databases/catdat/data/lemmas/cogenerators_in_product_categories.yaml +++ /dev/null @@ -1,7 +0,0 @@ -id: cogenerators_in_product_categories - -title: Cogenerators in product categories - -claim: For a family of categories $(\C_i)_{i \in I}$, each having a cogenerator $Q_i$ which is weakly terminal, the object $(Q_i)_{i \in I}$ is a cogenerator in the product category $\prod_{i \in I} \C_i$. - -proof: 'Let $(f_i: A_i \to B_i)_{i \in I}$ and $(g_i: A_i \to B_i)_{i \in I}$ be two parallel morphisms in the product category which are coequalized by any morphism $(B_i \to Q_i)_{i \in I}$. Let $i_0 \in I$. We claim that $f_{i_0},g_{i_0} : A_{i_0} \rightrightarrows B_{i_0}$ are coequalized by all morphisms $B_{i_0} \to Q_{i_0}$, and hence are equal: Indeed, for all $i \neq i_0$ we may choose some morphism $B_i \to Q_i$ since $Q_i$ is weakly terminal. Thus, the morphism $B_{i_0} \to Q_{i_0}$ extends to a morphism $(B_i \to Q_i)_{i \in I}$ in the product category. By assumption, it coequalizes $(f_i)_{i \in I}$ and $(g_i)_{i \in I}$. By looking at the $i_0$-component are done.' diff --git a/databases/catdat/data/lemmas/coslice-effective-congruences.yaml b/databases/catdat/data/lemmas/coslice-effective-congruences.yaml deleted file mode 100644 index b0479b327..000000000 --- a/databases/catdat/data/lemmas/coslice-effective-congruences.yaml +++ /dev/null @@ -1,14 +0,0 @@ -id: coslice-effective-congruences - -title: Inheritance of effective congruences in coslice categories - -claim: Let $\C$ be an extensive category, and $A$ an object of $\C$. If the coslice category $A \backslash \C$ has effective congruences, then so does $\C$. - -proof: >- - Let $f, g : E \rightrightarrows X$ be a congruence in $\C$. We then construct a congruence on $A+X$ in $A \backslash \C$. On an intuitive level, this will be the congruence generated by $a \sim a$ for $a\in A$ and $x \sim y$ for $(x, y) \in E$. More precisely, we will show the two maps - $$\id_A + f,\, \id_A + g : A+E \rightrightarrows A+X$$ - form a congruence. To show the pair of maps is jointly monomorphic, we use extensivity to split the domains of the generalized elements, so without loss of generality we may assume each comes from either $A$ or $E$. Reflexivity and symmetry are straightforward; and for transitivity, we again use extensivity to split the domains of the generalized elements, and provide an argument on each subdomain where the three generalized elements all come from either $A$ or $E$. - - Now if this congruence is the kernel pair of $h : A+X \to Z$ in $A \backslash \C$, then $E$ is the kernel pair of $h \circ i_2 : X \to Z$ in $\C$. Namely, if we have two generalized elements $x_1, x_2 : T \rightrightarrows X$ such that $h \circ i_2 \circ x_1 = h \circ i_2 \circ x_2$, then we can construct a map pair - $$\id_A + x_1,\, \id_A + x_2 : A+T \rightrightarrows A+X$$ - in $A \backslash \C$ with $h \circ (\id_A + x_1) = h \circ (\id_A + x_2)$. Therefore, $\id_A + x_1, \id_A + x_2$ factors through $A+E$ in $A \backslash \C$, so $x_1, x_2$ factors through $A+E$ in $\C$; and using disjoint coproducts, we may conclude $x_1, x_2$ factors through $E$. diff --git a/databases/catdat/data/lemmas/effective-congruence-quotients.yaml b/databases/catdat/data/lemmas/effective-congruence-quotients.yaml deleted file mode 100644 index e1780f6df..000000000 --- a/databases/catdat/data/lemmas/effective-congruence-quotients.yaml +++ /dev/null @@ -1,16 +0,0 @@ -id: effective-congruence-quotients - -title: Quotients of effective congruences are strict quotients - -claim: >- - Let $f, g : E \rightrightarrows X$ be an effective congruence. If $f, g$ have a coequalizer $p : X \to X/E$, then in fact we have a cartesian square - $$\begin{CD} E @> f >> X \\ @V g VV @VV p V \\ X @>> p > X/E. \end{CD}$$ - -proof: >- - Suppose we have $h : X \to Z$ so that we have a cartesian square - $$\begin{CD} E @> f >> X \\ @V g VV @VV h V \\ X @>> h > Z. \end{CD}$$ - Then by the universal property of the coequalizer, there is a unique morphism - $$\bar h : X/E \to Z$$ - such that $h = \bar h \circ p$. Now suppose we have generalized elements $x_1, x_2 : T \rightrightarrows X$ such that $p \circ x_1 = p \circ x_2$. Then - $$h \circ x_1 = \bar h \circ p \circ x_1 = \bar h \circ p \circ x_2 = h \circ x_2,$$ - so the pair $x_1, x_2$ factors through $f, g : E \rightrightarrows X$. The uniqueness of the factorization follows from the assumption that $E$ is a congruence, so $f, g$ are jointly monomorphic. diff --git a/databases/catdat/data/lemmas/exact_filtered_colimits_descend.yaml b/databases/catdat/data/lemmas/exact_filtered_colimits_descend.yaml deleted file mode 100644 index 00fa6688c..000000000 --- a/databases/catdat/data/lemmas/exact_filtered_colimits_descend.yaml +++ /dev/null @@ -1,15 +0,0 @@ -id: exact_filtered_colimits_descend - -title: Exact filtered colimits descend to nice subcategories - -claim: 'Let $G : \C \to \D$ be a fully faithful functor with a left adjoint $F : \D \to \C$ that preserves finite limits. Assume that $\D$ has exact filtered colimits and that $\C$ has finite limits. Then $\C$ has exact filtered colimits as well.' - -proof: >- - It is well-known (and easy to prove) that the colimit of a diagram $(X_j)$ in $\C$ is constructed as $F(\colim_j G(X_j))$, provided that colimit in $\D$ exists. In particular, $\C$ has filtered colimits. By assumption, it also has finite limits, and $G$ preserves these since it is a right adjoint. Now let $X : \I \times \J \to \C$ be a diagram, where $\I$ is finite and $\J$ is filtered. We compute: - $$\begin{align*} - \colim_j {\lim}_i X(i,j) & \cong F(\colim_j G({\lim}_i X(i,j))) \\ - & \cong F(\colim_j {\lim}_i G(X(i,j))) \\ - & \cong F({\lim}_i \colim_j G(X(i,j))) \\ - & \cong {\lim}_i F(\colim_j G(X(i,j))) \\ - & \cong {\lim}_i \colim_j X(i,j) - \end{align*}$$ diff --git a/databases/catdat/data/lemmas/filtered-monos.yaml b/databases/catdat/data/lemmas/filtered-monos.yaml deleted file mode 100644 index 83736b811..000000000 --- a/databases/catdat/data/lemmas/filtered-monos.yaml +++ /dev/null @@ -1,10 +0,0 @@ -id: filtered-monos - -title: Detection of filtered-colimit-stable monomorphisms - -claim: |- - Let $\C$ be a category with filtered colimits. Assume that $U : \C \to \D$ is faithful functor which preserves monomorphisms and filtered colimits. If monomorphisms in $\D$ are stable under filtered colimits, then the same is true for $\C$. - - For the record, here is the dual statement: Let $\C$ be a category with cofiltered limits. Assume that $U : \C \to \D$ is faithful functor which preserves epimorphisms and cofiltered limits. If epimorphisms in $\D$ are stable under cofiltered limits, then the same is true for $\C$. - -proof: Since $U$ is faithful, it reflects monomorphisms. From here the proof is straight forward. diff --git a/databases/catdat/data/lemmas/generator_construction.yaml b/databases/catdat/data/lemmas/generator_construction.yaml deleted file mode 100644 index 9ca26cb2f..000000000 --- a/databases/catdat/data/lemmas/generator_construction.yaml +++ /dev/null @@ -1,7 +0,0 @@ -id: generator_construction - -title: Construction of Generators - -claim: In a category let $S$ be a generating set which is strongly connected (between any two objects in $S$ there is a morphism). If the coproduct $U \coloneqq \coprod_{G \in S} G$ exists, then it is a generator. - -proof: 'This is a straight forward generalization of this result. We remark that the assumption about $S$ implies that each inclusion $G \to U$ has a left inverse. Now let $f,g : A \rightrightarrows B$ be two morphisms with $f h = g h$ for all $h : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by our preliminary remark. Thus, $fh = gh$ holds for all $h : G \to A$ and $G \in S$. Since $S$ is a generating set, this implies $f = g$.' diff --git a/databases/catdat/data/lemmas/limits_in_factor_categories.yaml b/databases/catdat/data/lemmas/limits_in_factor_categories.yaml deleted file mode 100644 index 60e56e1aa..000000000 --- a/databases/catdat/data/lemmas/limits_in_factor_categories.yaml +++ /dev/null @@ -1,9 +0,0 @@ -id: limits_in_factor_categories - -title: Limits in factor categories - -claim: Let $\C,\D$ be two categories. Assume that $\D$ is inhabited. If $\C \times \D$ has limits of a given shape, then $\C$ also has limits of this shape. - -proof: |- - Let $U \in \D$ be a fixed object. Assume that $X : \J \to \C$ is a diagram. Assume that the diagram $(X,U) : \J \to \C \times \D$ (which is constant in the second variable) has a limit cone $((p_i, u_i) : (L,V) \to (X_i,U))$, thus consisting of morphisms $p_i : L \to X_i$ and $u_i : V \to U$. Clearly, $(p_i : L \to X_i)$ is a cone over $X$. We prove that it is universal: - Let $(f_i : T \to X_i)$ be a cone over $X$. Then $((f_i,\id_U) : (T,U) \to (X_i,U))$ is a cone over $(X,U)$. Hence, there is a unique morphism $(f,v) : (T,U) \to (L,V)$, consisting of $f : T \to L$ and $v : U \to V$, such that $(p_i,u_i) \circ (f,v) = (f_i,\id_U)$, i.e. $p_i \circ f = f_i$ and $u_i \circ v = \id_U$. If $g : T \to L$ is another morphism with $p_i \circ g = f_i$, then uniqueness applied to $(g,v)$ shows that $f = g$. diff --git a/databases/catdat/data/lemmas/missing_cogenerating_sets.yaml b/databases/catdat/data/lemmas/missing_cogenerating_sets.yaml deleted file mode 100644 index f12955d85..000000000 --- a/databases/catdat/data/lemmas/missing_cogenerating_sets.yaml +++ /dev/null @@ -1,12 +0,0 @@ -id: missing_cogenerating_sets - -title: Missing cogenerating sets - -claim: >- - Let $\C$ be a category with a faithful functor $U: \C \to \Set$. Assume there exists a collection of objects $\F \subseteq \Ob(\C)$ satisfying the following conditions:
    -
  1. For any $X \in \F$ and any non-terminal $Y \in \C$, for every morphism $f: X \to Y$ its underlying map $U(f) : U(X) \to U(Y)$ is injective.
    2. -
  2. For every infinite cardinal number $\kappa$, there exists an object $X \in \F$ such that $\card(U(X)) \geq \kappa$ and such that $X$ has a non-identity endomorphism.
    3. -
- Then $\C$ does not have a cogenerating set. - -proof: 'Assume that there is a cogenerating set $S$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than all the $U(Y)$ with $Y \in S$ (w.r.t. cardinalities) and which has a non-identity endomorphism $\sigma : X \to X$. Since $S$ cogenerates, there is a morphism $f : X \to Y$ with $Y \in S$ and $f \sigma \neq f$. For this, $Y$ must be non-terminal. By (1) the map $U(f) : U(X) \to U(Y)$ is injective. This is a contradiction.' diff --git a/databases/catdat/data/lemmas/missing_cogenerator.yaml b/databases/catdat/data/lemmas/missing_cogenerator.yaml deleted file mode 100644 index cf18830ce..000000000 --- a/databases/catdat/data/lemmas/missing_cogenerator.yaml +++ /dev/null @@ -1,13 +0,0 @@ -id: missing_cogenerator - -title: Missing cogenerator - -claim: >- - Let $\C$ be a pointed category with a faithful functor $U: \C \to \Set$. Assume there exists a collection of non-zero objects $\F \subseteq \Ob(\C)$ satisfying the following conditions: -
    -
  1. For any $X \in \F$ and any $Y \in \C$, every non-zero morphism $f: X \to Y$ is injective on underlying sets.
    2. -
  2. For every $Y \in \C$ there is some object $X \in \F$ such that $\card(U(X)) > \card(U(Y))$.
    3. -
- Then $\C$ does not have a cogenerator. - -proof: 'Assume that there is a cogenerator $Y$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than $U(Y)$ (w.r.t. cardinalities). Since $0,\id_X : X \rightrightarrows X$ are distinct, there is a morphism $f : X \to Y$ with $f \neq 0$. But then $U(f) : U(X) \to U(Y)$ is injective by assumption (1), which contradicts our choice of $X$.' diff --git a/databases/catdat/data/lemmas/monic-sequential-colimits-via-congruence-quotients.yaml b/databases/catdat/data/lemmas/monic-sequential-colimits-via-congruence-quotients.yaml deleted file mode 100644 index da44fc8f2..000000000 --- a/databases/catdat/data/lemmas/monic-sequential-colimits-via-congruence-quotients.yaml +++ /dev/null @@ -1,7 +0,0 @@ -id: monic-sequential-colimits-via-congruence-quotients - -title: Construction of a colimit of a sequence of monomorphisms as a quotient of a congruence - -claim: Let $\C$ be a countably extensive category with quotients of congruences. Then $\C$ has colimits of sequences of monomorphisms. - -proof: 'Suppose we have a sequence $X_1 \hookrightarrow X_2 \hookrightarrow \cdots$ with corresponding monomorphisms $f_{m,n} : X_m \hookrightarrow X_n$ for $m \le n$. Define $Y$ to be the coproduct of all $X_n$. Now for each $m\le n$, define $E_{m,n} \coloneqq X_m$ with two maps $i_m, i_n \circ f_{m,n} : E_{m,n} \rightrightarrows Y$, and similarly for $m \ge n$ define $E_{m,n} \coloneqq X_n$ with two maps $i_m \circ f_{n,m}, i_n : E_{m,n} \rightrightarrows Y$. Then the coproduct of all $E_{m,n}$, with the induced morphisms to $Y$, forms a congruence. Here to prove the maps are jointly monomorphic, and again in proving transitivity, we use extensivity to split the domain of the generalized elements of $\sum_{m,n=1}^\infty E_{m,n}$ so that without loss of generality we may assume each factors through one of the coproduct inclusions. Now a quotient of this congruence must be a colimit of the sequence.' diff --git a/databases/catdat/data/lemmas/nno_distributive_criterion.yaml b/databases/catdat/data/lemmas/nno_distributive_criterion.yaml deleted file mode 100644 index e1313e6d8..000000000 --- a/databases/catdat/data/lemmas/nno_distributive_criterion.yaml +++ /dev/null @@ -1,27 +0,0 @@ -id: nno_distributive_criterion - -title: Natural number objects indicate distributivity - -claim: >- - Let $\C$ be a category with finite products, arbitrary copowers (denoted $\otimes$), and a natural numbers object $1 \xrightarrow{z} N \xrightarrow{s} N$. Then there is an isomorphism $N \cong \IN \otimes 1$, and for every object $A$ the natural morphism - $$\alpha : \IN \otimes A \to A \times (\IN \otimes 1)$$ - is a split monomorphism. - -proof: >- - We will use generalized elements extensively. In particular, for every element $a \in A$ and $n \in \IN$ there is an element $n \otimes a \in \IN \otimes A$, formally defined by the $n$th coproduct inclusion. The morphism $\alpha$ is defined by - $$\alpha(n \otimes a) = (a , n \otimes 1).$$ - In any category with finite products and arbitrary copowers, we can construct the non-parameterized NNO $\IN \otimes 1$ with the element $0 \otimes 1 \in \IN \otimes 1$ and the map - $$s : \IN \otimes 1 \to \IN \otimes 1, \quad s(n \otimes 1) \coloneqq (n+1) \otimes 1.$$ - Its universal property states that it is initial in the category of pairs $1 \xrightarrow{x_0} X \xrightarrow{r} X$. Hence, it is unique up to isomorphism. Since by assumption $1 \xrightarrow{z} N \xrightarrow{s} N$ is a full, parameterized NNO, it is also a non-parameterized NNO and therefore isomorphic to the one described. We will assume w.l.o.g. that it is equal to it and continue to work with $N = \IN \otimes 1$. - - Next, we apply the (parameterized) universal property of the NNO to the diagram - $$A \xrightarrow{f} \IN \otimes A \xrightarrow{g} \IN \otimes A$$ - defined by $f(a) \coloneqq 0 \otimes a$ and $g(n \otimes a) \coloneqq (n+1) \otimes a$. It tells us that there is a map - $$\Phi : A \times N \to \IN \otimes A$$ - with - $$\Phi(a,0 \otimes 1) = 0 \otimes a, \quad \Phi(a, s(m)) = g(\Phi(a,m)).$$ - For $m \coloneqq n \otimes 1 \in N$ (where $n \in \IN$) the second equation reads - $$\Phi(a, (n+1) \otimes 1) = g(\Phi(a, n \otimes 1)).$$ - By classical induction on $n \in \IN$ it follows that - $$\Phi(a, n \otimes 1) = n \otimes a,$$ - which exactly means $\Phi \circ \alpha = \id_{\IN \otimes A}$. diff --git a/databases/catdat/data/lemmas/preadditive_structure_unique.yaml b/databases/catdat/data/lemmas/preadditive_structure_unique.yaml deleted file mode 100644 index c54461121..000000000 --- a/databases/catdat/data/lemmas/preadditive_structure_unique.yaml +++ /dev/null @@ -1,26 +0,0 @@ -id: preadditive_structure_unique - -title: Uniqueness of preadditive structures - -claim: >- - Let $\C$ be a preadditive category (or more generally, a category enriched in commutative monoids) with finite products and finite coproducts. Then for all objects $X,Y$ the canonical morphism - $$\alpha : X \oplus Y \to X \times Y$$ - is an isomorphism. Moreover, the preadditive structure is unique: If $f,g : A \rightrightarrows B$ are morphisms, their sum - $$f+g : A \to B$$ - is the composite of $(f,g) : A \to B \times B$, the inverse $\alpha^{-1} : B \oplus B \to B \times B$, and the codiagonal $\nabla : B \oplus B \to B$.' - -proof: >- - The morphism $\alpha : X \oplus Y \to X \times Y$ is defined by the equations - $$p_1 \circ \alpha \circ i_1 = \id_X, \quad p_2 \circ \alpha \circ i_2 = \id_Y,$$ - $$p_2 \circ \alpha \circ i_1 = 0,\quad p_1 \circ \alpha \circ i_2 = 0.$$ - It does not depend on the choice of preadditive structure since zero morphisms are unique. It is an isomorphism: Define - $$\beta \coloneqq i_1 \circ p_1 + i_2 \circ p_2 : X \times Y \to X \oplus Y.$$ - Then $\alpha \circ \beta = \id_{X \times Y}$ because - $$p_1 \circ \alpha \circ \beta = p_1 \circ \alpha \circ i_1 \circ p_1 + p_1 \circ \alpha \circ i_2 \circ p_2 = \id_1 \circ p_1 + 0 \circ p_2 = p_1$$ - and likewise $p_2 \circ \alpha \circ \beta = p_2$. We also have $\beta \circ \alpha = \id_{X \oplus Y}$ with a very similar calculation that shows $\beta \circ \alpha \circ i_1 = i_1$ and $\beta \circ \alpha \circ i_2 = i_2$. Therefore, for morphisms $f,g : A \rightrightarrows B$ the composite $A \to B$ in the claim is equal to - $$\begin{align*} - \nabla \circ \beta \circ (f,g) & = \nabla \circ (i_1 \circ p_1 + i_2 \circ p_2) \circ (f,g) \\ - & = \nabla \circ i_1 \circ p_1 \circ (f,g) + \nabla \circ i_2 \circ p_2 \circ (f,g) \\ - & = p_1 \circ (f,g) + p_2 \circ (f,g) \\ - & = f + g. - \end{align*}$$ diff --git a/databases/catdat/data/lemmas/pushouts-of-monos-via-congruence-quotients.yaml b/databases/catdat/data/lemmas/pushouts-of-monos-via-congruence-quotients.yaml deleted file mode 100644 index 3490c67e5..000000000 --- a/databases/catdat/data/lemmas/pushouts-of-monos-via-congruence-quotients.yaml +++ /dev/null @@ -1,7 +0,0 @@ -id: pushouts-of-monos-via-congruence-quotients - -title: Construction of a pushout of monomorphisms as a quotient of a congruence - -claim: Let $\C$ be an extensive category with quotients of congruences. Then $\C$ has pushouts of monomorphisms. - -proof: 'Let $f : S \hookrightarrow X$, $g : S \hookrightarrow Y$ be monomorphisms. We construct a congruence on $X+Y$ via the maps $p_1, p_2 : X + Y + S + S \rightrightarrows X+Y$ which act as the identity on $X+Y$, $i_1 \circ f, i_2 \circ g$ on the first copy of $S$, and $i_2 \circ g, i_1 \circ f$ on the second copy of $S$, respectively. To show that $p_1, p_2$ are jointly monomorphic, and again in proving transitivity of the congruence, we use extensivity to split the domain of the generalized elements of $X+Y+S+S$ so that without loss of generality we may assume each factors through one of the coproduct inclusions. Now a quotient of the congruence must be a pushout of $f$ and $g$.' diff --git a/databases/catdat/data/lemmas/special_sequential_colimits.yaml b/databases/catdat/data/lemmas/special_sequential_colimits.yaml deleted file mode 100644 index 91e09bcf4..000000000 --- a/databases/catdat/data/lemmas/special_sequential_colimits.yaml +++ /dev/null @@ -1,15 +0,0 @@ -id: special_sequential_colimits - -title: Finite structures usually have no sequential colimits - -claim: 'Let $\C$ be a category with finite powers, including a terminal object $1$. Let $a : 1 \to X$ be a morphism. Assume that the sequence of morphisms $(X^n,a) : X^n \to X^{n+1}$ for $n \geq 0$ admits a colimit $(i_n : X^n \to C)$. Then for every $m \geq 0$ there is a split epimorphism $C \to X^m$. In particular, if $U : \C \to \Set$ is a functor preserving finite powers and $\card(U(X)) \geq 2$, then $U(C)$ is infinite.' - -proof: >- - Let $m \geq 0$ be fixed. For $n \geq 0$ we define a morphism $u_n : X^n \to X^m$ as follows: It is the projection on the first $m$ factors for $m \leq n$, and $(X^n,a^{m-n})$ for $m \geq n$ (for $m=n$ these agree). With generalized elements this says: - $$u_n(x_1,\dotsc,x_n) = \begin{cases} (x_1,\dotsc,x_m) & m \leq n \\ (x_1,\dotsc,x_n,a,\dotsc,a) & m \geq n \end{cases}$$ - We claim that $u_n = u_{n+1} \circ (X^n,a)$, i.e. - $$u_n(x_1,\dotsc,x_n) = u_{n+1}(x_1,\dotsc,x_n,a).$$ - If $m \leq n$ (hence, $m \leq n+1$), both sides are equal to $(x_1,\dotsc,x_m)$. If $m > n$, i.e. $m \geq n+1$, both sides are equal to $(x_1,\dotsc,x_n,a,\dotsc,a)$. This proves the claim. - - Hence, there is a unique morphism $\varphi : C \to X^m$ such that $\varphi \circ i_n = u_n$ for all $n \geq 0$. Since $u_m$ is the identity, $\varphi$ is a split epimorphism. - If $U$ is a functor with the mentioned properties, $U(\varphi)$ is also a split epimorphism from $U(C)$ to $U(X^m) \cong U(X)^m$, and $U(X)^m$ has $\geq 2^m$ elements. This holds for all $m$, so that $U(C)$ is infinite. diff --git a/databases/catdat/data/lemmas/subobject_classifiers_coreflection.yaml b/databases/catdat/data/lemmas/subobject_classifiers_coreflection.yaml deleted file mode 100644 index 62cfce0cd..000000000 --- a/databases/catdat/data/lemmas/subobject_classifiers_coreflection.yaml +++ /dev/null @@ -1,7 +0,0 @@ -id: subobject_classifiers_coreflection - -title: Coreflection of subobject classifiers - -claim: 'Let $\D$ be a category with a (regular) subobject classifier $\Omega$. Assume that $\C \to \D$ is a full subcategory such that (1) any (regular) $\D$-subobject of an object in $\C$ already lies in $\C$, (2) it is coreflective, i.e. there is a functor $R : \D \to \C$ right adjoint to the inclusion. Then $R(\Omega)$ is a (regular) subobject classifier in $\C$.' - -proof: If $X \in \C$, then $\Hom(X,R(\Omega)) \cong \Hom(X,\Omega)$ is isomorphic to the collection of $\D$-subobjects of $X$, which by assumption coincide with the $\C$-subobjects of $X$. diff --git a/databases/catdat/data/lemmas/thin_algebraic_categories.yaml b/databases/catdat/data/lemmas/thin_algebraic_categories.yaml deleted file mode 100644 index aecfc4c4b..000000000 --- a/databases/catdat/data/lemmas/thin_algebraic_categories.yaml +++ /dev/null @@ -1,7 +0,0 @@ -id: thin_algebraic_categories - -title: Algebraic categories are "never" thin - -claim: Let $\C$ be a thin and finitary algebraic category. Then $\C \simeq 1$ or $\C \simeq \{0 < 1\}$. - -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. 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\}$.' diff --git a/databases/catdat/schema/013_lemmas.sql b/databases/catdat/schema/013_lemmas.sql deleted file mode 100644 index 03a027976..000000000 --- a/databases/catdat/schema/013_lemmas.sql +++ /dev/null @@ -1,6 +0,0 @@ -CREATE TABLE lemmas ( - id TEXT PRIMARY KEY, - title TEXT NOT NULL UNIQUE, - claim TEXT NOT NULL, - proof TEXT NOT NULL -); \ No newline at end of file diff --git a/databases/catdat/schema/014_property_comments.sql b/databases/catdat/schema/013_property_comments.sql similarity index 100% rename from databases/catdat/schema/014_property_comments.sql rename to databases/catdat/schema/013_property_comments.sql diff --git a/databases/catdat/scripts/seed.ts b/databases/catdat/scripts/seed.ts index 2d8b11a01..b2afb9d50 100644 --- a/databases/catdat/scripts/seed.ts +++ b/databases/catdat/scripts/seed.ts @@ -6,7 +6,6 @@ import type { CategoryYaml, ConfigYaml, CategoryPropertyYaml, - LemmaYaml, CategoryImplicationYaml, FunctorImplicationYaml, FunctorPropertyYaml, @@ -37,8 +36,6 @@ function seed() { seed_config() - seed_lemmas() - seed_category_properties() seed_category_implications() seed_categories() @@ -66,8 +63,6 @@ function clear_all_data() { db.transaction(() => { db.pragma('foreign_keys = OFF') - db.prepare(`DELETE FROM lemmas`).run() - db.prepare(`DELETE FROM category_implication_assumptions`).run() db.prepare(`DELETE FROM category_implication_conclusions`).run() db.prepare(`DELETE FROM category_implications`).run() @@ -334,37 +329,6 @@ function seed_category_properties() { } } -function seed_lemmas() { - console.info(`\nSeed lemmas ...`) - - const folder = path.join(data_folder, 'lemmas') - const files = get_yaml_files(folder) - - const lemma_insert = db.prepare( - `INSERT INTO lemmas (id, title, claim, proof) VALUES (?, ?, ?, ?)`, - ) - - function insert_lemma(lemma: LemmaYaml) { - lemma_insert.run(lemma.id, lemma.title, lemma.claim, lemma.proof) - } - - const tx = db.transaction(() => { - for (const lemma_file of files) { - console.info(`Seed: ${lemma_file}`) - - const lemma = read_yaml_file(folder, lemma_file) - insert_lemma(lemma) - } - }) - - try { - tx() - } catch (err) { - console.error(`Error seeding lemmas:`, err) - process.exit(1) - } -} - function seed_category_implications() { console.info(`\nSeed category implications ...`) diff --git a/databases/catdat/scripts/seed.types.ts b/databases/catdat/scripts/seed.types.ts index 6502df3ab..82a72bbde 100644 --- a/databases/catdat/scripts/seed.types.ts +++ b/databases/catdat/scripts/seed.types.ts @@ -62,13 +62,6 @@ export type CategoryPropertyYaml = { related_properties: string[] } -export type LemmaYaml = { - id: string - title: string - claim: string - proof: string -} - export type CategoryImplicationYaml = { id: string assumptions: string[] diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index 9382e0dcd..679f2440d 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -155,10 +155,3 @@ export type FunctorPropertyAssignment = Replace< FunctorPropertyAssignmentDB, { is_deduced: boolean } > - -export type Lemma = { - id: string - title: string - claim: string - proof: string -} diff --git a/src/routes/category-implications/+page.svelte b/src/routes/category-implications/+page.svelte index f1efce6cb..6c08c0111 100644 --- a/src/routes/category-implications/+page.svelte +++ b/src/routes/category-implications/+page.svelte @@ -77,11 +77,6 @@ well.

-

- In some cases, implications are a bit too rigid, which is why we also provide a small - collection of lemmas. -

-