diff --git a/.cspell.json b/.cspell.json index 70760c20..e3a2b1ce 100644 --- a/.cspell.json +++ b/.cspell.json @@ -77,6 +77,7 @@ "codistributivity", "codomain", "codomains", + "coequalize", "coequalized", "coequalizer", "coequalizers", @@ -95,6 +96,7 @@ "cogenerator", "cogenerators", "Cohomology", + "coimage", "cokernel", "cokernels", "colimit", diff --git a/content/monic_sequential_colimits.md b/content/monic_sequential_colimits.md new file mode 100644 index 00000000..aed0b8cc --- /dev/null +++ b/content/monic_sequential_colimits.md @@ -0,0 +1,46 @@ +--- +title: The colimit of a sequence of monomorphisms +description: We find conditions under which a countably extensive category has colimits of sequences of monomorphisms. +--- + +## The colimit of a sequence of monomorphisms + +::: Lemma 1 +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_0 \hookrightarrow X_1 \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 that the maps are jointly monomorphic, and again when proving transitivity, we use extensivity to split the domain of the generalized elements of $\coprod_{m,n \geq 0}^\infty E_{m,n}$ so that, without loss of generality, we may assume that each factors through one of the coproduct inclusions. Now a quotient of this congruence must be a colimit of the sequence. +::: + +::: Lemma 2 +Let $\C$ be a countably extensive category with coequalizers of kernel pairs. Assume that $X_0 \hookrightarrow X_1 \hookrightarrow \cdots$ is a sequence of monomorphisms that has a cocone $(X_n \hookrightarrow Y)$ consisting of monomorphisms. Then this sequence has a colimit. +::: + +::: Proof +We consider the morphism $\coprod_{n \geq 0} X_n \to Y$ induced by the monomorphisms $X_n \hookrightarrow Y$. By assumption, its kernel pair $\coprod_{n \geq 0} X_n \times_Y \coprod_{n \geq 0} X_n$ exists, and the two projections to $\coprod_{n \geq 0} X_n$ have a coequalizer. We will prove that this coequalizer is a colimit of the sequence $X_1 \hookrightarrow X_2 \hookrightarrow \cdots$. For this, it suffices to find a natural bijection between cocones $(h_n : X_n \to T)_{n \geq 0}$ and morphisms $h : \coprod_{n \geq 0} X_n \to T$ that coequalize the two projections, where $T \in \C$ is any object. + +A morphism $h : \coprod_{n \geq 0} X_n \to Y$ is equivalent to a family of morphisms $(h_n : X_n \to T)_{n \geq 0}$. Since $\C$ is countably extensive, the canonical morphism +$$\textstyle \coprod_{n,m \geq 0} X_n \times_Y X_m \to \coprod_{n \geq 0} X_n \times_Y \coprod_{m \geq 0} X_m$$ +is an isomorphism. Hence, $h$ coequalizes the two projections if and only if for all $n,m \geq 0$ the diagram + +$$ +\begin{CD} +X_n \times_Y X_m @>>> X_n \\ +@VVV @VVV \\ +X_m @>>> T +\end{CD} +$$ + +commutes. Without loss of generality, we may assume $n \leq m$. But then $X_n \times_Y X_m \cong X_n$, and the diagram simplifies to + +$$ +\begin{CD} +X_n @>{=}>> X_n \\ +@VVV @VVV \\ +X_m @>>> T, +\end{CD} +$$ + +which is precisely the cocone condition for $(h_n : X_n \to T)_{n \geq 0}$. +::: diff --git a/content/subcategories.md b/content/subcategories.md index d30770e4..5385297a 100644 --- a/content/subcategories.md +++ b/content/subcategories.md @@ -86,15 +86,17 @@ The forgetful functor $\C / P \to \C$ is fully faithful; it has right adjoint ${ ::: ::: Lemma 7 -Let $U : \C \to \D$ be a fully faithful functor. Assume that $\C$ has finite limits and coequalizers, and that $U$ preserves pullbacks and coequalizers. If $\D$ is regular, then so is $\C$. +Let $U : \C \to \D$ be a functor preserving pullbacks. Assume that $\D$ is regular and that $\C$ has finite limits and coequalizers of kernel pairs. If $U$ preserves and reflects regular epimorphisms, then $\C$ is regular. Moreover, this condition is satisfied when $U$ is conservative and preserves coequalizers. ::: ::: Proof -Since $\C$ has finite limits and coequalizers, the only nontrivial part of proving $\C$ is regular is to check that regular epimorphisms are stable under pullbacks in $\C$. Since $U$ preserves pullbacks and regular epimorphisms, it suffices to show that $U$ reflects regular epimorphisms. Thus, suppose $f : X \to Y$ is a morphism in $\C$ with $Uf$ a regular epimorphism. Then in $\C$ we have the diagram -$$X \times_Y X \rightrightarrows X \to \im(f) \xrightarrow{i} Y$$ -where $X \times_Y X$ is the kernel pair of $f$, and $\im(f)$ is the coequalizer. By the assumptions, the image under $U$ is equivalent to the diagram in $\D$: -$$UX \times_{UY} UX \rightrightarrows UX \to \im(Uf) \xrightarrow{Ui} UY$$ -where $UX \times_{UY} UX$ is the kernel pair of $Uf$, and $\im(Uf)$ is the coequalizer. Since $Uf$ is a regular epimorphism, we must have $Ui$ is an isomorphism. Since $U$ is fully faithful and therefore conservative, we get $i$ is an isomorphism as well, so $f$ is a regular epimorphism. +Since $\C$ has finite limits and coequalizers of kernel pairs, it remains to prove that regular epimorphisms are stable under pullbacks in $\C$. Assume first that $U$ preserves and reflects regular epimorphisms. If $X \to Y$ is a regular epimorphism and $Z \to Y$ is any morphism in $\C$, then $U(X) \to U(Y)$ is a regular epimorphism, and therefore also $U(X) \times_{U(Y)} U(Z) \to U(Z)$ is a regular epimorphism. Since $U$ preserves pullbacks, this identifies with $U(X \times_Y Z) \to U(Z)$, the image under $U$ of $X \times_Y Z \to Z$. Since $U$ reflects regular epimorphisms, it follows that $X \times_Y Z \to Z$ is a regular epimorphism, finishing the proof. + +Now assume that $U$ is conservative and preserves coequalizers. Then it clearly preserves regular epimorphisms. Conversely, suppose that $f : X \to Y$ is a morphism in $\C$ such that $U(f)$ is a regular epimorphism. Then in $\C$ we have the diagram +$$X \times_Y X \rightrightarrows X \xrightarrow{p} \im(f) \xrightarrow{i} Y$$ +where $X \times_Y X \rightrightarrows X$ is the kernel pair of $f$, and $\im(f)$ is the coequalizer. By the assumptions on $U$, its image is equivalent to the diagram in $\D$: +$$U(X) \times_{U(Y)} U(X) \rightrightarrows U(X) \xrightarrow{U(p)} U(\im(f)) \xrightarrow{U(i)} U(Y)$$ +where $U(X) \times_{U(Y)} U(X)$ is the kernel pair of $U(f)$, and $U(\im(f))$ is the coequalizer. Since $U(f)$ is a regular epimorphism and $\D$ is regular, we must have that $U(i)$ is an isomorphism. Since $U$ is conservative, $i$ is an isomorphism as well, so $f$ is a regular epimorphism. ::: ::: Lemma 8 diff --git a/database/data/categories/FinGrp.yaml b/database/data/categories/FinGrp.yaml index b1c0d7aa..69d19f30 100644 --- a/database/data/categories/FinGrp.yaml +++ b/database/data/categories/FinGrp.yaml @@ -48,7 +48,7 @@ satisfied_properties: proof: 'A proof can be found in MO/511516. It even shows that every cocongruence in $\FinGrp$ is trivial. In short, the proof goes like this: We know that $\Grp$ has effective cocongruences. Using the fact that amalgamated sums of finite groups are residually finite, one can can show that every cocongruence in $\FinGrp$ is also a cocongruence in $\Grp$.' - property: regular - proof: 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. + proof: This follows from Lemma 7 here applied to the inclusion functor $\FinGrp \hookrightarrow \Grp$ into the regular category $\Grp$ and the description of regular epimorphisms below. - property: ℵ₁-cofiltered limits proof: For $\FinSet$ know that the embedding $\FinSet \hookrightarrow \Set$ is closed under $\aleph_1$-cofiltered limits. From this and the fact that the forgetful functor $\Grp \to \Set$ preserves limits it follows that $\FinGrp \hookrightarrow \Grp$ is closed under $\aleph_1$-cofiltered limits. diff --git a/database/data/categories/Grp_c.yaml b/database/data/categories/Grp_c.yaml index 3837e698..19222b46 100644 --- a/database/data/categories/Grp_c.yaml +++ b/database/data/categories/Grp_c.yaml @@ -56,7 +56,7 @@ satisfied_properties: - grp_malcev - property: regular - proof: We already know that the category is finitely complete, and that it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks. + proof: This follows from Lemma 7 here applied to the inclusion functor $\Grp_\c \hookrightarrow \Grp$ into the regular category $\Grp$ and the description of regular epimorphisms below. - property: effective congruences proof: 'A congruence on a countable group $G$ has the form $\{(g,h) \in G^2 : g^{-1} h \in N \}$ for some normal subgroup $N \subseteq G$. It is the kernel pair of the projection $p : G \twoheadrightarrow G/N$ in $\Grp$, but also in $\Grp_\c$ since $G/N$ is countable.' diff --git a/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml index 524e22e4..0b432668 100644 --- a/database/data/categories/Met_c.yaml +++ b/database/data/categories/Met_c.yaml @@ -97,37 +97,8 @@ unsatisfied_properties: - property: ℵ₁-filtered colimits proof: See MO/511433 for a proof that the diagram $\omega_1 \to \Met_c$, $\alpha \mapsto \IR^\alpha$ does not have a colimit. - - property: regular - proof: >- - We will find a morphism $f : X \to Y$ in $\Met_c$ whose kernel pair has no coequalizer. The idea is to represent the sequential fan $S_\omega$ as such a coequalizer in $\Top$, and generalize the diagonal argument showing that it is not metrizable. - - - For $n \geq 1$ consider the subspace - $$S_n \coloneqq \{1/k : k \geq 1\} \cup \{0\}$$ - of $\IR$, so that $\Hom(S_n,Y)$ corresponds to convergent sequences in $Y$. Each $S_n$ has diameter $1$, so we can endow the coproduct space - $$X \coloneqq \textstyle\coprod_n S_n$$ - with a metric that extends the metric on each $S_n$ and in which points in $S_n$ and $S_m$ for $n \neq m$ have distance $1$. The points of $X$ will be written as $(n,x)$, where $x \in S_n$. If $p_n$ denotes the $n$th prime number, we have $\lim_{k \to \infty} p_n^{-k} = 0$ in $\IR$, so we have a continuous map $S_n \to \IR$ mapping $1/k \mapsto p_n^{-k}$ and $0 \mapsto 0$. Together, these yield a continuous map - $$f : X \to \IR, \, (n,0) \mapsto 0, \, (n,1/k) \mapsto p_n^{-k}.$$ - Let $\pi_1,\pi_2 : E \rightrightarrows X$ be the kernel pair of $f$. Since $p_n^{-k}$ completely determines $n$ and $k$, $E$ consists precisely of the diagonal and all $((n,0),(m,0))$ for $n,m \geq 1$. Thus, the coequalizer of $\pi_1,\pi_2$ in $\Top$ is the quotient of $X$ that identifies all limit points $(n,0)$ for $n \geq 1$; this space is known as the sequential fan $S_\omega$. - - - Now assume that $\pi_1,\pi_2$ have a coequalizer $q : X \to Q$ in $\Met_c$, i.e. the universal continuous map from $X$ into a metrizable space such that the point - $$0_Q \coloneqq q(n,0) \in Q$$ - does not depend on the choice of $n$. Since $Q$ is metrizable, there is a countable decreasing neighborhood basis $(B_m)_{m \geq 1}$ of $0_Q \in Q$. Then $U_m \coloneqq q^{-1}(B_m)$ is an open neighborhood of $(n,0) \in X$ for any $n$, and in particular of $(m,0)$. Hence, $U_m \cap S_m$ contains almost all points of $S_m$. In particular, we may choose a point $x_m \in U_m \cap S_m$ that is isolated in $S_m$. - - - Define the subset $A \coloneqq \{x_m : m \geq 1\}$ of $X$ and let $g : X \to \IR$ be its characteristic function, so that $g(a)=1$ for $a \in A$ and $g(x) = 0$ for $x \in X \setminus A$. To show that $g$ is continuous, it suffices to consider each restriction $g|_{S_m} : S_m \to \IR$. This is the characteristic function of the isolated point $x_m \in S_m$, hence continuous. - - - Since $g(n,0) = 0$ for all $n \geq 1$, there is a unique continuous map $\tilde{g} : Q \to \IR$ satisfying $\tilde{g} \circ q = g$. The points $q(x_m)$ in $Q$ converge to $0_Q$ because for all $k \geq m$ we have $x_k \in U_k$, hence $q(x_k) \in B_k \subseteq B_m$. Since $\tilde{g}$ is continuous, it follows that $\tilde{g}(q(x_m)) = g(x_m) = 1$ converges to $\tilde{g}(0_Q) = \tilde{g}(q(n,0)) = g(n,0) = 0$, which is a contradiction. - - - Sketch of an alternative proof: Consider the coproduct $X \coloneqq \coprod_n \IR^n$ in $\Met_c$. The canonical inclusions $\IR^n \to \ell^2$ into the Hilbert space of square-summable sequences yield a continuous map $f : X \to \ell^2$. A coequalizer of the kernel pair of $f$ would be a colimit of the sequence - $$\IR \hookrightarrow \IR^2 \hookrightarrow \IR^3 \cdots$$ - where each map appends a zero coordinate, and we have seen above that this sequential colimit does not exist. - - - property: quotients of congruences - proof: In the previous proof we have constructed a morphism whose kernel pair does not have a coequalizer, and every kernel pair is a congruence. + - property: coequalizers of kernel pairs + proof: The sequence of embeddings $\IR^1 \hookrightarrow \IR^2 \hookrightarrow \IR^3 \hookrightarrow \cdots$, where each map appends a zero coordinate, has no colimit by MO/510316. It has a cocone consisting of the embeddings $\IR^n \hookrightarrow \ell^2$, $x \mapsto (x,0,0,\dotsc)$, where $\ell^2$ is the Hilbert space of square-summable sequences. Since $\Met_c$ is infinitary extensive, it follows from Lemma 2 here that $\Met_c$ does not have coequalizers of kernel pairs. special_objects: initial object: diff --git a/database/data/categories/Sch_R.yaml b/database/data/categories/Sch_R.yaml index 4dc75ebe..aef7cd69 100644 --- a/database/data/categories/Sch_R.yaml +++ b/database/data/categories/Sch_R.yaml @@ -58,12 +58,19 @@ unsatisfied_properties: - property: cokernel pairs proof: Choose a residue field $K$ of $R$. Then the span $\IA^1_K \leftarrow \Spec(K(t)) \rightarrow \IA^1_K$ has no pushout; see MO/9961. - - property: quotients of congruences - proof: If $\Sch_R$ had quotients of congruences, then by this lemma it would also have pushouts of monomorphisms, contradicting the fact that the span $\IA^1_K \leftarrow \Spec(K(t)) \rightarrow \IA^1_K$ has no pushout where $K$ is a residue field of $R$; see MO/9961. - - property: sequential colimits proof: It is shown in MO/511944 that the diagram $$\IA^1_R \hookrightarrow \IA^2_R \hookrightarrow \IA^3_R \hookrightarrow \cdots$$ has no colimit. + - property: coequalizers of kernel pairs + proof: >- + We have a diagram of closed immersions of affine spaces + $$\begin{array}{cccc} + \IA^1_R & \to & \IA^2_R & \to ~ \cdots \\[1ex] + \downarrow & \swarrow & & \\[1ex] + \IA^\infty_R, &&& + \end{array}$$ + where $\IA^n_R = \Spec(R[X_1,\dotsc,X_n])$ and $\IA^\infty_R = \Spec(R[X_1,X_2,\dotsc])$. By MO/511944, the sequence $\IA^1_R \hookrightarrow \IA^2_R \hookrightarrow \cdots$ has no colimit. Moreover, we already know that $\Sch_R$ is infinitary extensive. Hence, Lemma 2 here implies that $\Sch_R$ does not have coequalizers of kernel pairs. Specifically, the kernel pair of $\coprod_{n \geq 0} \IA^n_R \to \IA^\infty_R$ has no coequalizer. + special_objects: initial object: description: empty scheme diff --git a/database/data/categories/Set_c.yaml b/database/data/categories/Set_c.yaml index 4dfc07bc..ba19a412 100644 --- a/database/data/categories/Set_c.yaml +++ b/database/data/categories/Set_c.yaml @@ -52,10 +52,10 @@ satisfied_properties: proof: '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 - proof: From the other properties we know that the category is finitely complete and that it has coequalizers. The regular epimorphisms are stable under pullbacks since this holds in $\Set$ and both regular epimorphisms (they are surjective maps) and pullbacks coincide. + proof: This follows from Lemma 7 here applied to the inclusion functor $\Set_\c \hookrightarrow \Set$ into the regular category $\Set$ and the description of regular epimorphisms below. - property: coregular - proof: From the other properties we know that the category is finitely cocomplete and that it has equalizers. The regular monomorphisms are stable under pushouts since this holds in $\Set$ and both regular monomorphisms (they are injective maps) and pushouts coincide. + proof: This follows from the dual of Lemma 7 here applied to the inclusion functor $\Set_\c \hookrightarrow \Set$ into the coregular category $\Set$ and the description of regular monomorphisms below. unsatisfied_properties: - property: small diff --git a/database/data/categories/Set_pointed.yaml b/database/data/categories/Set_pointed.yaml index 521a5564..b4c8e429 100644 --- a/database/data/categories/Set_pointed.yaml +++ b/database/data/categories/Set_pointed.yaml @@ -32,10 +32,6 @@ satisfied_properties: proof: The pointed set $(\{0,1\},1)$ is a cogenerator. label: set_*_cogenerator - - property: coregular - proof: From the other properties we know that (co-)limits exist and that monomorphisms coincide with injective pointed maps. So it suffices to prove that these maps are stable under pushouts. This follows from the corresponding fact for $\Set$ and the observation that the forgetful functor $\Set_* \to \Set$ preserves pushouts. - check_redundancy: false - - property: co-Malcev proof: Malcev categories are closed under slice categories by Prop. 2.2.14 in Malcev, protomodular, homological and semi-abelian categories. It follows that co-Malcev categories are closed under coslice categories, and $\Set_*$ is a coslice category of $\Set$, which is co-Malcev since every elementary topos is co-Malcev. diff --git a/database/data/categories/Setne.yaml b/database/data/categories/Setne.yaml index d8edf2e1..f1df54cc 100644 --- a/database/data/categories/Setne.yaml +++ b/database/data/categories/Setne.yaml @@ -39,6 +39,9 @@ satisfied_properties: - property: binary coproducts proof: The disjoint union of two non-empty sets is non-empty. + - property: equalizers of cokernel pairs + proof: 'Let $f : X \to Y$ be a map of non-empty sets. The cokernel pair $i_1,i_2 : Y \rightrightarrows Y \sqcup_X Y$ in $\Set$ is clearly also a cokernel pair in $\Setne$. Moreover, the equalizer of $i_1,i_2$ in $\Set$ is non-empty because it contains the elements of $X$.' + - property: mono-regular proof: This follows easily from the fact that $\Set$ is mono-regular. @@ -79,9 +82,6 @@ unsatisfied_properties: - property: coquotients of cocongruences proof: The two maps $\{0\} \rightrightarrows \{0,1\}$ form a cocongruence on $\{0\}$ — namely the cofull cocongruence on $\{0\}$ — but they do not have an equalizer. - - property: effective cocongruences - proof: The two maps $\{0\} \rightrightarrows \{0,1\}$ form a cocongruence on $\{0\}$ — namely the cofull cocongruence on $\{0\}$ — but there is no map $Z \to \{0\}$ making the required commutative diagram, much less a cocartesian square. - - property: coaccessible proof: If $\Setne$ is coaccessible, then by the dual of Cor. 2.44 in Adamek-Rosicky also the coslice category $\{\ast\} / \Setne$ would be coaccessible. But this category is isomorphic to $\Set_*$, from which we know that it is not coaccessible (namely, because of Thm. 1.64 in op. cit.). diff --git a/database/data/categories/Top_pointed.yaml b/database/data/categories/Top_pointed.yaml index 30afa0aa..db00dfea 100644 --- a/database/data/categories/Top_pointed.yaml +++ b/database/data/categories/Top_pointed.yaml @@ -63,7 +63,7 @@ satisfied_properties: proof: This follows from Lemma 2 here applied to the forgetful functor to $\Set$. - property: coregular - proof: Regular monomorphisms coincide with the embeddings (see below). Since $\Top$ is coregular, they are stable under pushouts, and pushouts in $\Top_*$ are the same. + proof: This follows from the dual of Lemma 7 here applied to the forgetful functor $\Top_* \to \Top$, using that $\Top$ is coregular and the description of regular monomorphisms below. - property: extremal cogenerator proof: >- diff --git a/database/data/categories/TorsFreeAb.yaml b/database/data/categories/TorsFreeAb.yaml index dc820eb3..1f0b5b6c 100644 --- a/database/data/categories/TorsFreeAb.yaml +++ b/database/data/categories/TorsFreeAb.yaml @@ -34,7 +34,7 @@ satisfied_properties: proof: It is a full subcategory of the preadditive category $\Ab$. - property: regular - proof: The regular epimorphisms are exactly the surjective homomorphisms (see below), and these are clearly stable under pullbacks. + proof: This follows from Lemma 7 here applied to the inclusion functor $\TorsFreeAb \hookrightarrow \Ab$ into the regular category $\Ab$ and the description of regular epimorphisms below. - property: coregular proof: >- diff --git a/database/data/category-implications/congruences.yaml b/database/data/category-implications/congruences.yaml index 7e85b8bf..5803dd83 100644 --- a/database/data/category-implications/congruences.yaml +++ b/database/data/category-implications/congruences.yaml @@ -5,6 +5,7 @@ - regular conclusions: - finitely complete + - coequalizers of kernel pairs proof: This holds by definition of a regular category. - id: regular_well-powered_well-copowered @@ -31,6 +32,22 @@ - quotients of congruences proof: A congruence $E \rightrightarrows X$ has a common section $X \to E$ given by the reflexivity morphism. +- id: congruences_include_kernel_pairs + assumptions: + - quotients of congruences + - kernel pairs + conclusions: + - coequalizers of kernel pairs + proof: This is simply because a kernel pair is a congruence. + +- id: kernel_pairs_are_effective + assumptions: + - effective congruences + - coequalizers of kernel pairs + conclusions: + - quotients of congruences + proof: Every congruence is a kernel pair, thus has a coequalizer. + - id: cokernels_via_congruence_quotients assumptions: - preadditive @@ -47,7 +64,7 @@ - preadditive conclusions: - quotients of congruences - proof: 'For any congruence $E$ on an object $X$ of a preadditive category, let $E_0$ be the kernel of $p_2 : E \to X$. The restriction of $p_1$ to $E_0$ is a monomorphism. We can then see that $E$ must be the pullback of $p_1 - p_2 : E \to X$ and $E_0 \hookrightarrow X$. Then the cokernel of $E_0 \hookrightarrow X$ is a quotient of $E$.' + proof: 'For any congruence $E$ on an object $X$ of a preadditive category, let $E_0$ be the kernel of $p_2 : E \to X$. The restriction of $p_1$ to $E_0$ is a monomorphism. We can then see that $E$ must be the pullback of $p_1 - p_2 : E \to X$ and $E_0 \hookrightarrow X$. Then the cokernel of $E_0 \hookrightarrow X$ is a quotient of $E$.' - id: core-hin_quotients assumptions: diff --git a/database/data/category-implications/pullbacks.yaml b/database/data/category-implications/pullbacks.yaml index a67ce551..797925f6 100644 --- a/database/data/category-implications/pullbacks.yaml +++ b/database/data/category-implications/pullbacks.yaml @@ -83,3 +83,10 @@ is representable. Using $w = u-v$, this functor is isomorphic to $$T \mapsto \{(u,w) \in \Hom(T,X)^2 : f \circ w = 0\}.$$ The functor $T \mapsto \{w \in \Hom(T,X) : f \circ w = 0\}$ is a retract of this functor. Since the category is Cauchy complete, every retract of a representable functor is representable. Therefore, the kernel of $f$ exists. + +- id: kernel_pairs_coequalizers_assumption + assumptions: + - coequalizers of kernel pairs + conclusions: + - kernel pairs + proof: This holds by definition. diff --git a/database/data/category-properties/coequalizers of kernel pairs.yaml b/database/data/category-properties/coequalizers of kernel pairs.yaml new file mode 100644 index 00000000..37769ea9 --- /dev/null +++ b/database/data/category-properties/coequalizers of kernel pairs.yaml @@ -0,0 +1,17 @@ +id: coequalizers of kernel pairs +relation: has +description: 'We say that a category has coequalizers of kernel pairs if every morphism $f : A \to B$ has a kernel pair $p_1, p_2 : A \times_B A \rightrightarrows A$ such that $p_1,p_2$ have a coequalizer. The coequalizer is sometimes also called the regular image of $f$.' +nlab_link: https://ncatlab.org/nlab/show/image#AsEqualizer +dual: equalizers of cokernel pairs +invariant_under_equivalences: true + +related: + - quotients of congruences + - reflexive coequalizers + - coequalizers + - kernel pairs + - regular + +tags: + - limits + - colimits diff --git a/database/data/category-properties/coequalizers.yaml b/database/data/category-properties/coequalizers.yaml index 9f39e248..6acb2f04 100644 --- a/database/data/category-properties/coequalizers.yaml +++ b/database/data/category-properties/coequalizers.yaml @@ -10,6 +10,7 @@ related: - finitely cocomplete - quotients of congruences - reflexive coequalizers + - coequalizers of kernel pairs tags: - colimits diff --git a/database/data/category-properties/cokernel pairs.yaml b/database/data/category-properties/cokernel pairs.yaml index 5a308756..bcf5c394 100644 --- a/database/data/category-properties/cokernel pairs.yaml +++ b/database/data/category-properties/cokernel pairs.yaml @@ -1,6 +1,6 @@ id: cokernel pairs relation: has -description: 'The cokernel pair of a morphism $f : X \to Y$ is the pushout $Y \sqcup_X Y$, i.e. the colimit of the span $Y \xleftarrow{f} X \xrightarrow{f} Y$. If the morphism is not clear from the context, we can write $Y \sqcup_{f,X,f} Y$ to denote the pushout. We say that a category $\C$ has cokernel pairs if every morphism has a cokernel pair. Equivalently, each coslice category $X / \C$ has binary copowers.' +description: 'The cokernel pair of a morphism $f : X \to Y$ is the pushout $Y \rightrightarrows Y \sqcup_X Y$, i.e. the colimit of the span $Y \xleftarrow{f} X \xrightarrow{f} Y$. If the morphism is not clear from the context, we can write $Y \sqcup_{f,X,f} Y$ to denote the pushout. We say that a category $\C$ has cokernel pairs if every morphism has a cokernel pair. Equivalently, each coslice category $X / \C$ has binary copowers.' nlab_link: https://ncatlab.org/nlab/show/cokernel+pair dual: kernel pairs invariant_under_equivalences: true @@ -10,6 +10,7 @@ related: - coregular - cokernels - binary copowers + - equalizers of cokernel pairs tags: - colimits diff --git a/database/data/category-properties/coquotients of cocongruences.yaml b/database/data/category-properties/coquotients of cocongruences.yaml index 1278a671..d9179b91 100644 --- a/database/data/category-properties/coquotients of cocongruences.yaml +++ b/database/data/category-properties/coquotients of cocongruences.yaml @@ -6,10 +6,10 @@ dual: quotients of congruences invariant_under_equivalences: true related: - - coregular - - effective cocongruences - equalizers + - equalizers of cokernel pairs - kernels + - effective cocongruences - Barr-coexact tags: diff --git a/database/data/category-properties/coreflexive equalizers.yaml b/database/data/category-properties/coreflexive equalizers.yaml index 2314612d..475f957c 100644 --- a/database/data/category-properties/coreflexive equalizers.yaml +++ b/database/data/category-properties/coreflexive equalizers.yaml @@ -8,6 +8,8 @@ invariant_under_equivalences: true related: - cosifted limits - equalizers + - coquotients of cocongruences + - equalizers of cokernel pairs tags: - limits diff --git a/database/data/category-properties/coregular.yaml b/database/data/category-properties/coregular.yaml index b3b0d344..367ff73b 100644 --- a/database/data/category-properties/coregular.yaml +++ b/database/data/category-properties/coregular.yaml @@ -6,10 +6,10 @@ dual: regular invariant_under_equivalences: true related: - - coquotients of cocongruences - finitely cocomplete - - Barr-coexact - cokernel pairs + - equalizers of cokernel pairs + - Barr-coexact tags: - limit–colimit interaction diff --git a/database/data/category-properties/equalizers of cokernel pairs.yaml b/database/data/category-properties/equalizers of cokernel pairs.yaml new file mode 100644 index 00000000..c53cdb38 --- /dev/null +++ b/database/data/category-properties/equalizers of cokernel pairs.yaml @@ -0,0 +1,17 @@ +id: equalizers of cokernel pairs +relation: has +description: 'We say that a category has equalizers of cokernel pairs if every morphism $f : A \to B$ has a cokernel pair $i_1, i_2 : B \rightrightarrows B \sqcup_A B$ such that $i_1,i_2$ have an equalizer. The equalizer is sometimes also called the regular coimage of $f$.' +nlab_link: https://ncatlab.org/nlab/show/image#AsEqualizer +dual: coequalizers of kernel pairs +invariant_under_equivalences: true + +related: + - coquotients of cocongruences + - coreflexive equalizers + - equalizers + - cokernel pairs + - coregular + +tags: + - limits + - colimits diff --git a/database/data/category-properties/equalizers.yaml b/database/data/category-properties/equalizers.yaml index 84050d51..9920bda9 100644 --- a/database/data/category-properties/equalizers.yaml +++ b/database/data/category-properties/equalizers.yaml @@ -10,6 +10,7 @@ related: - coreflexive equalizers - finitely complete - kernels + - equalizers of cokernel pairs tags: - limits diff --git a/database/data/category-properties/kernel pairs.yaml b/database/data/category-properties/kernel pairs.yaml index 1e346058..459bc382 100644 --- a/database/data/category-properties/kernel pairs.yaml +++ b/database/data/category-properties/kernel pairs.yaml @@ -1,6 +1,6 @@ id: kernel pairs relation: has -description: 'The kernel pair of a morphism $f : X \to Y$ is the pullback $X \times_Y X$, i.e. the limit of the cospan $X \xrightarrow{f} Y \xleftarrow{f} X$. If the morphism is not clear from the context, we can write $X \times_{f,Y,f} X$ to denote the pullback. We say that a category $\C$ has kernel pairs if every morphism has a kernel pair. Equivalently, each slice category $\C / Y$ has binary powers.' +description: 'The kernel pair of a morphism $f : X \to Y$ is the pullback $X \times_Y X \rightrightarrows X$, i.e. the limit of the cospan $X \xrightarrow{f} Y \xleftarrow{f} X$. If the morphism is not clear from the context, we can write $X \times_{f,Y,f} X$ to denote the pullback. We say that a category $\C$ has kernel pairs if every morphism has a kernel pair. Equivalently, each slice category $\C / Y$ has binary powers.' nlab_link: https://ncatlab.org/nlab/show/kernel+pair dual: cokernel pairs invariant_under_equivalences: true @@ -10,6 +10,7 @@ related: - regular - kernels - binary powers + - coequalizers of kernel pairs tags: - limits diff --git a/database/data/category-properties/quotients of congruences.yaml b/database/data/category-properties/quotients of congruences.yaml index ddc20f3d..8d2225fe 100644 --- a/database/data/category-properties/quotients of congruences.yaml +++ b/database/data/category-properties/quotients of congruences.yaml @@ -7,9 +7,9 @@ invariant_under_equivalences: true related: - coequalizers + - coequalizers of kernel pairs - cokernels - effective congruences - - regular - Barr-exact tags: diff --git a/database/data/category-properties/reflexive coequalizers.yaml b/database/data/category-properties/reflexive coequalizers.yaml index d5f0e393..dce185ed 100644 --- a/database/data/category-properties/reflexive coequalizers.yaml +++ b/database/data/category-properties/reflexive coequalizers.yaml @@ -8,6 +8,8 @@ invariant_under_equivalences: true related: - coequalizers - sifted colimits + - quotients of congruences + - coequalizers of kernel pairs tags: - colimits diff --git a/database/data/category-properties/regular.yaml b/database/data/category-properties/regular.yaml index bf002548..0ccac623 100644 --- a/database/data/category-properties/regular.yaml +++ b/database/data/category-properties/regular.yaml @@ -7,9 +7,9 @@ invariant_under_equivalences: true related: - finitely complete - - quotients of congruences - - Barr-exact - kernel pairs + - coequalizers of kernel pairs + - Barr-exact tags: - limit–colimit interaction diff --git a/database/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json index cd0fd9d6..df68bb2c 100644 --- a/database/scripts/expected-data/Ab.json +++ b/database/scripts/expected-data/Ab.json @@ -123,6 +123,8 @@ "natural numbers object": true, "kernel pairs": true, "cokernel pairs": true, + "equalizers of cokernel pairs": true, + "coequalizers of kernel pairs": true, "cartesian closed": false, "locally cartesian closed": false, diff --git a/database/scripts/expected-data/Set.json b/database/scripts/expected-data/Set.json index a35726cd..e405c63d 100644 --- a/database/scripts/expected-data/Set.json +++ b/database/scripts/expected-data/Set.json @@ -121,6 +121,8 @@ "extremal cogenerating set": true, "kernel pairs": true, "cokernel pairs": true, + "equalizers of cokernel pairs": true, + "coequalizers of kernel pairs": true, "Grothendieck abelian": false, "Malcev": false, diff --git a/database/scripts/expected-data/Top.json b/database/scripts/expected-data/Top.json index c6f80aa6..b5aefcc9 100644 --- a/database/scripts/expected-data/Top.json +++ b/database/scripts/expected-data/Top.json @@ -86,6 +86,8 @@ "extremal cogenerating set": true, "kernel pairs": true, "cokernel pairs": true, + "equalizers of cokernel pairs": true, + "coequalizers of kernel pairs": true, "abelian": false, "additive": false,