Replace all lemmas with markdown-generated content pages

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

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:
 

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. <span class="qed">$\square$</span>

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$. <span class="qed">$\square$</span>

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. <span class="qed">$\square$</span>

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*}
+$$
+
+<span class="qed">$\square$</span>

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. <span class="qed">$\square$</span>

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$. <span class="qed">$\square$</span>

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$. <span class="qed">$\square$</span>

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. <span class="qed">$\square$</span>

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$. <span class="qed">$\square$</span>

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. <span class="qed">$\square$</span>

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}$. <span class="qed">$\square$</span>

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 <i>unique</i>: 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*}
+$$
+
+<span class="qed">$\square$</span>

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$. <span class="qed">$\square$</span>