diff --git a/.cspell.json b/.cspell.json index f8e7b4fc..70760c20 100644 --- a/.cspell.json +++ b/.cspell.json @@ -180,6 +180,7 @@ "Groupes", "groupoid", "groupoids", + "Hanai", "Haus", "hausdorff", "Hertweck", diff --git a/database/data/categories/BOn.yaml b/database/data/categories/BOn.yaml index 74b4a44c..ea4e8296 100644 --- a/database/data/categories/BOn.yaml +++ b/database/data/categories/BOn.yaml @@ -96,9 +96,6 @@ unsatisfied_properties: - property: sequential colimits proof: Assume that the sequence $\bullet \xrightarrow{1} \bullet \xrightarrow{1} \cdots$ has a colimit. This mounts to a (universal) sequence of ordinals $\alpha_n$ with $\alpha_n = \alpha_{n+1} + 1$. But then $\alpha_{n+1} < \alpha_n$, contradicting the fact that $\alpha_0$ is well-ordered. - - property: pushouts - proof: Assume that $1,\omega$ have a pushout. This is a (universal) pair of ordinals $\alpha,\beta$ with $\alpha + 1 = \beta + \omega$. But $\beta + \omega$ is a limit ordinal, while $\alpha + 1$ is not. - - property: cofiltered-limit-stable epimorphisms proof: The epimorphisms are the finite ordinals (see below), but the limit of the sequential diagram $\cdots \xrightarrow{1} * \xrightarrow{1} *$ is the ordinal $\omega$ by MSE/5129138. diff --git a/database/data/categories/Delta.yaml b/database/data/categories/Delta.yaml index e53d50ea..bc7866ad 100644 --- a/database/data/categories/Delta.yaml +++ b/database/data/categories/Delta.yaml @@ -87,6 +87,9 @@ unsatisfied_properties: - property: coreflexive equalizers proof: 'The two maps $d^0,d^1 : [0] \rightrightarrows [1]$ have a common left inverse, the unique map $s^0 : [1] \to [0]$, but are not equalized by any morphism.' + - property: cokernel pairs + proof: Assume that the inclusion $\{0\} \to \{0 < 1\}$ has a cokernel pair in $\FinOrd \setminus \{\varnothing\}$. This would be a universal finite ordered set $X$ with three elements $0,1,2$ satisfying $0 \leq 1$ and $0 \leq 2$. Assume w.l.o.g. $1 \leq 2$ (the case $2 \leq 1$ is similar). The universal property yields an order-preserving map $X \to \{a < b < c\}$ with $0 \mapsto a$, $1 \mapsto c$, $2 \mapsto b$. But then $c \leq b$, which is a contradiction. + - property: sequential colimits proof: We can just copy the proof for $\FinOrd$ to show that the sequence of inclusions $[0] \hookrightarrow [1] \hookrightarrow [2] \hookrightarrow \cdots$ has no colimit. references: @@ -100,9 +103,6 @@ unsatisfied_properties: - property: natural numbers object proof: Any natural numbers object in $\FinOrd \setminus \{\varnothing\}$ would also be a natural numbers object in $\FinOrd$, which we know does not exist. - - property: pushouts - proof: Assume that the two inclusions $\{0 < 1\} \leftarrow \{0\} \rightarrow \{0 < 2\}$ have a pushout in $\FinOrd \setminus \{\varnothing\}$. This would be a universal non-empty finite ordered set $X$ with three elements $0,1,2$ satisfying $0 \leq 1$ and $0 \leq 2$. Assume w.l.o.g. $1 \leq 2$ (the case $2 \leq 1$ is similar). The universal property yields an order-preserving map $X \to \{a < b < c\}$ with $0 \mapsto a$, $1 \mapsto c$, $2 \mapsto b$. But then $c \leq b$, which is a contradiction. - - property: multi-complete proof: >- We will prove that the multi-product of $I \coloneqq \{0 < 1\}$ with itself does not exist in $\FinOrd \setminus \{\varnothing\}$. Assume that it does, i.e. there is a family of spans diff --git a/database/data/categories/FS.yaml b/database/data/categories/FS.yaml index 374cce9d..012b10b1 100644 --- a/database/data/categories/FS.yaml +++ b/database/data/categories/FS.yaml @@ -88,9 +88,6 @@ unsatisfied_properties: - property: sequential limits proof: 'Let $X_n \coloneqq \{1,\dotsc,n\}$. We define the truncation $p_n : X_{n+1} \to X_n$ by extending the identity of $X_n$ with $p_n(n+1) \coloneqq n$. Assume the sequence of truncations $\cdots \to X_2 \to X_1$ has a limit $(f_n : X \to X_n)$ in this category. But $f_n$ is surjective, so that $\card(X) \geq n$ for all $n$. Since $X$ is finite, this is a contradiction.' - - property: pullbacks - proof: The connected component of non-empty sets has a terminal object, $1$, and it suffices to prove that it has no products. Let $X$ be a finite set with more than $1$ element. Assume that the product $P$ of $X$ with itself exists. The diagonal $X \to P$ is a split monomorphism, hence injective, but also surjective, i.e. an isomorphism. In other words, the two projections $P \rightrightarrows X$ are equal. The universal property of $P$ now implies that every two morphisms $Y \rightrightarrows X$ are equal, which is absurd. - - property: binary copowers proof: Assume that the copower $X \coloneqq 2+2$ exists. Since we have a surjective map $2 \to X$, the set $X$ has at most $2$ elements. The codiagonal $X \to 2$ shows that $X$ has at least $2$ elements. Thus, $X \cong 2$. For all finite sets $Y$ we get a bijection $\Hom(2,Y) \cong \Hom(2,Y)^2$, in particular the cardinalities are the same. For $Y=2$ this gives the contradiction $2 = 4$. diff --git a/database/data/categories/Fld.yaml b/database/data/categories/Fld.yaml index 48040e5b..2c0bb283 100644 --- a/database/data/categories/Fld.yaml +++ b/database/data/categories/Fld.yaml @@ -50,9 +50,6 @@ unsatisfied_properties: - property: multi-terminal object proof: Every field has a non-trivial extension, for instance, the rational function field over itself in one variable. Hence, a multi-terminal object never exists. - - property: pushouts - proof: 'By MSE/359352, the pushout $E \sqcup_K F$ of two field homomorphisms $E \leftarrow K \rightarrow F$ exists if and only if the tensor product $E \otimes_K F$ has a "fieldification": this means that the nilradical is a prime ideal whose quotient ring is a field. This is quite rare: Consider $E = K(X)$, $F = K(Y)$. Then $E \otimes_K F$ is isomorphic to $K[X,Y] (K[X]-\{0\})^{-1} (K[Y]-\{0\})^{-1}$, which is an integral domain but not a field: for example, $X-Y$ has no inverse.' - - property: generator proof: 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. diff --git a/database/data/categories/Man.yaml b/database/data/categories/Man.yaml index 725328cd..0a8e7546 100644 --- a/database/data/categories/Man.yaml +++ b/database/data/categories/Man.yaml @@ -81,8 +81,11 @@ unsatisfied_properties: - property: countable powers proof: 'The power $\IR^{\IN}$ does not exist. More generally, let $(M_n)_{n \geq 0}$ be a sequence of smooth manifolds of positive dimension whose product $(\pi_n : P \to M_n)_{n \geq 0}$ exists. This product cone in $\Man$ yields a product cone in $\Set$ since the forgetful functor $\Man \to \Set$ is representable, hence preserves all limits. Choose points $x_n \in M_n$ with $T_{x_n}(M_n) \neq 0$. Choose the point $x \in P$ with $\pi_n(x) = x_n$. Consider the linear map $T_x(P) \to \prod_{n \geq 0} T_{x_n}(M_n)$ induced by the derivatives $d_x(\pi_n) : T_x(P) \to T_{x_n}(M_n)$. Since $T_x(P)$ is finite-dimensional and $\prod_{n \geq 0} T_{x_n}(M_n)$ is not, it cannot be surjective. But actually, it is: Choose tangent vectors $v_n \in T_{x_n}(M_n)$. Choose smooth curves $\gamma_n : \IR \to M_n$ with $\gamma_n(0)=x_n$ and ${\gamma_n}''(0) = v_n$. By the universal property there is a unique smooth curve $\gamma : \IR \to P$ with $\pi_n \gamma = \gamma_n$. In particular, $\gamma(0) = x$. The chain rule now implies that $\gamma''(0) \in T_x(P)$ is a preimage of $(v_n)$ – a contradiction.' - - property: pullbacks - proof: See MSE/5129579 or MSE/322485. + - property: kernel pairs + proof: One can show that the map $\IR \to \IR$, $x \mapsto x^2$ does not have a kernel pair, see MSE/322485. + + - property: cokernel pairs + proof: The inclusion $\{0\} \to \IR$ does not have a cokernel pair, see MO/19916. - property: sequential colimits proof: 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. @@ -101,7 +104,7 @@ unsatisfied_properties: - setc_no_aleph1-cofiltered_limits - property: quotients of congruences - proof: 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. + proof: 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/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml index 6b5c8127..524e22e4 100644 --- a/database/data/categories/Met_c.yaml +++ b/database/data/categories/Met_c.yaml @@ -33,18 +33,23 @@ satisfied_properties: proof: See MSE/5004389. check_redundancy: false - - property: well-powered - proof: This follows easily from the fact that monomorphisms are injective in this category. - - - property: well-copowered - proof: 'If $f : X \to Y$ is an epimorphism, then $f(X)$ is dense in $Y$ (see below). Hence, there is an injective map $Y \to X^{\IN}$, which bounds the size of $Y$.' - - property: infinitary extensive proof: This follows from Lemma 11 here since $\Top$ is infinitary extensive and its full subcategory $\Met_c$ of metrizable topological spaces is closed under pullbacks and coproducts in $\Top$. + - property: cokernel pairs + proof: >- + Since metric spaces are Hausdorff, the cokernel pair of $f : Y \to X$ coincides with the cokernel pair of the inclusion $C \hookrightarrow X$, where $C$ is the closure of the image of $f$ (if it exists). Thus, it suffices to prove that for every closed subset $C \subseteq X$ of a metric space, the pushout $X \sqcup_C X$ exists. In fact, the $\Top$-pushout $X \sqcup_C X$ is metrizable. + To see this, consider the canonical continuous map $p : X \sqcup X \to X \sqcup_C X$. It is surjective and closed, and its fibers have cardinality at most $2$. In particular, its fibers are compact. Since $X \sqcup X$ is metrizable, the claim now follows from the Hanai-Morita-Stone theorem; see Theorem 4.4.17 in Engelking's book General Topology. + - property: effective cocongruences proof: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Met_c$. Then the image in $\Haus$ is a coreflexive corelation (since epimorphisms in both categories are continuous maps with dense image). By MO/509548, that implies that image is of the form $X +_S X$ for a closed subset $S$ of $X$. Since $S$ is metrizable, and the functor $\Met_c \to \Haus$ is fully faithful and therefore reflects colimits, we conclude that $E$ is effective in $\Met_c$.' + - property: well-powered + proof: This follows easily from the fact that monomorphisms are injective in this category. + + - property: well-copowered + proof: 'If $f : X \to Y$ is an epimorphism, then $f(X)$ is dense in $Y$ (see below). Hence, there is an injective map $Y \to X^{\IN}$, which bounds the size of $Y$.' + - property: extremal generator proof: 'We claim the metric space $G \coloneqq \{ 1/n : n \in \IN_{> 0} \} \cup \{ 0 \}$, with the metric inherited from $\IR$, is an extremal generator. First, the one-point metric space is a generator since it represents the forgetful functor $\Met_c \to \Set$; and since we have an epimorphism $! : G \to 1$, it follows that $G$ is a generator as well. Now, suppose we have a continuous function $f : X \to Y$ of metric spaces such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. Then since $G$ is a generator, we can conclude that $f$ is a monomorphism, i.e. injective on the underlying sets. Also, considering a constant function $G \to Y$ with image $y$, we see that $f$ is surjective on the underlying sets. Finally, the fact that $f$ induces a bijection between $\Hom(G, X)$ and $\Hom(G, Y)$ implies that a sequence $(x_n)_{n\in \IN}$ in $X$ has limit $L$ if and only if $(f(x_n))_{n\in \IN}$ has limit $f(L)$ in $Y$. This shows that $f$ is a homeomorphism.' diff --git a/database/data/categories/Rel.yaml b/database/data/categories/Rel.yaml index 47ecfb7d..3f316091 100644 --- a/database/data/categories/Rel.yaml +++ b/database/data/categories/Rel.yaml @@ -61,6 +61,9 @@ unsatisfied_properties: - property: normal proof: The construction of equalizers in $\Rel$ shows that they are injective functions, but MSE/350716 shows that monomorphisms in $\Rel$ don't have to be functions. + - property: kernel pairs + proof: 'Let $X$ be a finite set with $n$ elements. Consider the relation $R : X \to \{*\}$ corresponding to the set $\{(x,*) : x \in X\}$ (which is even a map). Assume that it has a kernel pair $E \rightrightarrows X$. Then, in particular, the set $P(E) \cong \Hom(\{*\},E)$ is isomorphic to the set of pairs $(S_1,S_2) \in \Hom(\{*\},X)^2$ such that $R \circ S_1 = R \circ S_2$. A relation $\{*\} \to X$ corresponds to a subset of $X$, and its composition with $R$ corresponds to the image of that subset under $R$, which is either $\varnothing$ or $\{*\}$, depending on whether the subset is empty or not. Therefore, the set of pairs $(S_1,S_2)$ with $R \circ S_1 = R \circ S_2$ has exactly $1 + (2^n - 1) (2^n - 1)$ elements. For $n=2$, for example, this is equal to $10$, and therefore not a power of $2$. Thus, the set cannot be isomorphic to $P(E)$ for any set $E$.' + special_objects: initial object: description: empty set diff --git a/database/data/categories/Sch_R.yaml b/database/data/categories/Sch_R.yaml index 425eca67..4dc75ebe 100644 --- a/database/data/categories/Sch_R.yaml +++ b/database/data/categories/Sch_R.yaml @@ -55,6 +55,9 @@ unsatisfied_properties: - property: generating set proof: If $S$ is a generating set of $R$-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 $R$-schemes, corresponding to a cogenerating set in $\CAlg(R)$, which we know does not exist. + - 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. diff --git a/database/data/categories/Set_ff.yaml b/database/data/categories/Set_ff.yaml index 24c936e3..f9ffe948 100644 --- a/database/data/categories/Set_ff.yaml +++ b/database/data/categories/Set_ff.yaml @@ -33,6 +33,12 @@ satisfied_properties: proof: 'The disjoint union $X+Y$ of two sets $X,Y$ with the inclusion maps $X \rightarrow X+Y \leftarrow Y$ is a coproduct: The inclusions are injective, hence finite-to-one. If $f : X \to T$, $g : Y \to T$ are finite-to-one maps, the induced map $(f;g) : X + Y \to T$ is finite-to-one since the fiber of $t \in T$ is $f^*(\{t\}) + g^*(\{t\})$, which is finite.' check_redundancy: false + - property: cokernel pairs + proof: >- + Let $f : X \to Y$ be a finite-to-one map. Consider the cokernel pair $i_1,i_2 : Y \rightrightarrows Y \sqcup_X Y$ in $\Set$. The maps $i_1,i_2$ are injective, in fact split monomorphisms in $\Set$, and therefore finite-to-one. To show that this cokernel pair is also a cokernel pair in $\Set_\ff$, it suffices to show that a map $h : Y \sqcup_X Y \to T$ is finite-to-one whenever both restrictions $h \circ i_1, h \circ i_2 : Y \rightrightarrows T$ are finite-to-one. Since $i_1,i_2$ are jointly surjective, we have + $$h^* \{y\} \subseteq (i_1)_* (h \circ i_1)^* \{y\} \cup (i_2)_* (h \circ i_2)^* \{y\},$$ + and the right-hand side is finite. + - property: extensive proof: We have already seen that finite coproducts exist in $\Set_\ff$, and pullbacks exist since the category is locally cartesian closed, although a direct argument is also possible. The forgetful functor $\Set_\ff \to \Set$ preserves finite coproducts and pullbacks, and is clearly faithful and conservative (but not full). Therefore, the claim follows from the extensivity of $\Set$ and Lemma 11 here. diff --git a/database/data/categories/Setne.yaml b/database/data/categories/Setne.yaml index 38e3275e..d8edf2e1 100644 --- a/database/data/categories/Setne.yaml +++ b/database/data/categories/Setne.yaml @@ -33,6 +33,9 @@ satisfied_properties: - property: cartesian closed proof: This is because $\Set$ is cartesian closed and since for non-empty sets $X,Y$ there is at least one function $X \to Y$. + - property: kernel pairs + proof: 'This is because $\Set$ has kernel pairs and for a map $f : X \to Y$ between non-empty sets $X,Y$ the kernel pair $\{(x,x'') \in X \times X : f(x) = f(x'')\}$ is also non-empty.' + - property: binary coproducts proof: The disjoint union of two non-empty sets is non-empty. diff --git a/database/data/categories/walking_coreflexive_pair.yaml b/database/data/categories/walking_coreflexive_pair.yaml index a0dc89c1..9998e68d 100644 --- a/database/data/categories/walking_coreflexive_pair.yaml +++ b/database/data/categories/walking_coreflexive_pair.yaml @@ -70,7 +70,7 @@ unsatisfied_properties: - property: coreflexive equalizers proof: 'The coreflexive pair $i,j : [0] \rightrightarrows [1]$ has no equalizer, in fact is not equalized by any morphism.' - - property: pushouts + - property: cokernel pairs proof: Assume that $[1] \xleftarrow{i} [0] \xrightarrow{i} [1]$ has a pushout in $\Delta^{\leq 1}$, where $i(0)=0$. This amounts to a universal totally ordered set of cardinality $\leq 2$ with elements $a,b,c$ satisfying $a \leq b$, $a \leq c$. Since a finite totally ordered set has trivial automorphism group, the automorphism defined by $a \mapsto a$, $b \mapsto c$, $c \mapsto b$ must be the identity, i.e., we have $b = c$. However, in $[1]$ the equations $0 \leq 0$, $0 \leq 1$ then show that the universal property fails. - property: natural numbers object diff --git a/database/data/categories/walking_idempotent.yaml b/database/data/categories/walking_idempotent.yaml index 8077122b..c7a02e11 100644 --- a/database/data/categories/walking_idempotent.yaml +++ b/database/data/categories/walking_idempotent.yaml @@ -44,6 +44,9 @@ unsatisfied_properties: - property: Cauchy complete proof: The idempotent $e$ does not split. + - property: kernel pairs + proof: Assume that $e$ has a kernel pair. Its underlying object must be $0$. Thus, there is a bijection between the morphisms $0 \to 0$ and the pairs of morphisms $0 \rightrightarrows 0$ that $e$ equalizes. But this holds for all pairs of morphisms. Counting these sets gives the contradiction $2 = 4$. + special_objects: {} special_morphisms: diff --git a/database/data/category-implications/pullbacks.yaml b/database/data/category-implications/pullbacks.yaml index 0169b47a..a67ce551 100644 --- a/database/data/category-implications/pullbacks.yaml +++ b/database/data/category-implications/pullbacks.yaml @@ -1,4 +1,4 @@ -# results on pullbacks and wide pullbacks +# results on pullbacks, wide pullbacks, and kernel pairs - id: pullbacks_criterion assumptions: @@ -33,3 +33,53 @@ conclusions: - wide pullbacks proof: Each slice category has finite products and is essentially finite, hence has all products by this result followed by this result. + +- id: kernel_pair_is_pullback + assumptions: + - pullbacks + conclusions: + - kernel pairs + proof: This is trivial. + +- id: kernel_pair_terminal_power + assumptions: + - kernel pairs + - terminal object + conclusions: + - binary powers + proof: If $1$ is a terminal object, then $X \times_1 X = X \times X$. + +- id: left_cancellative_kernel_pairs + assumptions: + - left cancellative + conclusions: + - kernel pairs + proof: >- + In general, the kernel pair of a monomorphism $f : X \to Y$ exists and is given by + $$\begin{CD} X @>{\id_X}>> X \\ @V{\id_X}VV @VV{f}V \\ X @>>{f}> Y. \end{CD}$$ + +- id: right_cancellative_kernel_pairs + assumptions: + - right cancellative + - kernel pairs + # TODO: rework this once we have split-mono-trivial + conclusions: + - left cancellative + proof: >- + Let $f : X \to Y$ be a morphism with kernel pair $E \rightrightarrows X$. The diagonal $X \to E$ is a split monomorphism. By assumption on the category, it is also an epimorphism. Thus, it is an isomorphism. Therefore, + $$\begin{CD} X @>{\id_X}>> X \\ @V{\id_X}VV @VV{f}V \\ X @>>{f}> Y. \end{CD}$$ + is a pullback, so $f$ is a monomorphism. + +- id: additive_kernel_pairs + assumptions: + - preadditive + - kernel pairs + - Cauchy complete + conclusions: + - kernels + proof: >- + Let $f : X \to Y$ be a morphism. Since $f$ has a kernel pair, the functor + $$\C^{\op} \to \Set^+, \quad T \mapsto \{(u,v) \in \Hom(T,X)^2 : f \circ u = f \circ v\}$$ + 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. diff --git a/database/data/category-properties/binary copowers.yaml b/database/data/category-properties/binary copowers.yaml index eab400d3..bc041869 100644 --- a/database/data/category-properties/binary copowers.yaml +++ b/database/data/category-properties/binary copowers.yaml @@ -1,13 +1,14 @@ id: binary copowers relation: has -description: A category has binary copowers when for every object $X$ and every binary set $I$ the coproduct $X \sqcup X$ exists. These objects might also be called doubles. +description: A category has binary copowers when for every object $X$ the coproduct $X \sqcup X$ exists. These objects might also be called doubles. nlab_link: https://ncatlab.org/nlab/show/copower dual: binary powers invariant_under_equivalences: true related: - finite copowers - - finite coproducts + - binary coproducts + - cokernel pairs tags: - colimits diff --git a/database/data/category-properties/binary powers.yaml b/database/data/category-properties/binary powers.yaml index da75e672..856920dd 100644 --- a/database/data/category-properties/binary powers.yaml +++ b/database/data/category-properties/binary powers.yaml @@ -1,13 +1,14 @@ id: binary powers relation: has -description: A category has binary powers when for every object $X$ the product $X \times X$ exists. These objects might also be called squares. +description: A category has binary powers when for every object $X$ the product $X \times X$ exists. These objects might also be called squares. nlab_link: https://ncatlab.org/nlab/show/powering dual: binary copowers invariant_under_equivalences: true related: - finite powers - - finite products + - binary products + - kernel pairs tags: - limits diff --git a/database/data/category-properties/cokernel pairs.yaml b/database/data/category-properties/cokernel pairs.yaml new file mode 100644 index 00000000..5a308756 --- /dev/null +++ b/database/data/category-properties/cokernel pairs.yaml @@ -0,0 +1,15 @@ +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.' +nlab_link: https://ncatlab.org/nlab/show/cokernel+pair +dual: kernel pairs +invariant_under_equivalences: true + +related: + - pushouts + - coregular + - cokernels + - binary copowers + +tags: + - colimits diff --git a/database/data/category-properties/cokernels.yaml b/database/data/category-properties/cokernels.yaml index 11f384d7..02db114d 100644 --- a/database/data/category-properties/cokernels.yaml +++ b/database/data/category-properties/cokernels.yaml @@ -10,6 +10,7 @@ related: - conormal - quotients of congruences - zero morphisms + - cokernel pairs tags: - colimits diff --git a/database/data/category-properties/coregular.yaml b/database/data/category-properties/coregular.yaml index 82571432..b3b0d344 100644 --- a/database/data/category-properties/coregular.yaml +++ b/database/data/category-properties/coregular.yaml @@ -9,6 +9,7 @@ related: - coquotients of cocongruences - finitely cocomplete - Barr-coexact + - cokernel pairs tags: - limit–colimit interaction diff --git a/database/data/category-properties/effective cocongruences.yaml b/database/data/category-properties/effective cocongruences.yaml index 81c1eeb7..6c053dd7 100644 --- a/database/data/category-properties/effective cocongruences.yaml +++ b/database/data/category-properties/effective cocongruences.yaml @@ -13,6 +13,7 @@ related: - coquotients of cocongruences - epi-regular - Barr-coexact + - cokernel pairs tags: - congruences diff --git a/database/data/category-properties/effective congruences.yaml b/database/data/category-properties/effective congruences.yaml index 351cc597..b572cb05 100644 --- a/database/data/category-properties/effective congruences.yaml +++ b/database/data/category-properties/effective congruences.yaml @@ -13,6 +13,7 @@ related: - normal - quotients of congruences - Barr-exact + - kernel pairs tags: - congruences diff --git a/database/data/category-properties/kernel pairs.yaml b/database/data/category-properties/kernel pairs.yaml new file mode 100644 index 00000000..1e346058 --- /dev/null +++ b/database/data/category-properties/kernel pairs.yaml @@ -0,0 +1,15 @@ +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.' +nlab_link: https://ncatlab.org/nlab/show/kernel+pair +dual: cokernel pairs +invariant_under_equivalences: true + +related: + - pullbacks + - regular + - kernels + - binary powers + +tags: + - limits diff --git a/database/data/category-properties/kernels.yaml b/database/data/category-properties/kernels.yaml index 246e716a..283a8ad6 100644 --- a/database/data/category-properties/kernels.yaml +++ b/database/data/category-properties/kernels.yaml @@ -10,6 +10,7 @@ related: - equalizers - normal - zero morphisms + - kernel pairs tags: - limits diff --git a/database/data/category-properties/pullbacks.yaml b/database/data/category-properties/pullbacks.yaml index 0de413d5..dee095e3 100644 --- a/database/data/category-properties/pullbacks.yaml +++ b/database/data/category-properties/pullbacks.yaml @@ -7,7 +7,9 @@ invariant_under_equivalences: true related: - binary products + - finitely complete - wide pullbacks + - kernel pairs tags: - limits diff --git a/database/data/category-properties/pushouts.yaml b/database/data/category-properties/pushouts.yaml index 8b8d97f9..516d6be0 100644 --- a/database/data/category-properties/pushouts.yaml +++ b/database/data/category-properties/pushouts.yaml @@ -7,7 +7,9 @@ invariant_under_equivalences: true related: - binary coproducts + - finitely cocomplete - wide pushouts + - cokernel pairs tags: - colimits diff --git a/database/data/category-properties/regular.yaml b/database/data/category-properties/regular.yaml index 93970f20..bf002548 100644 --- a/database/data/category-properties/regular.yaml +++ b/database/data/category-properties/regular.yaml @@ -9,6 +9,7 @@ related: - finitely complete - quotients of congruences - Barr-exact + - kernel pairs tags: - limit–colimit interaction diff --git a/database/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json index c8cc22fa..cd0fd9d6 100644 --- a/database/scripts/expected-data/Ab.json +++ b/database/scripts/expected-data/Ab.json @@ -121,6 +121,8 @@ "extremal cogenerator": true, "extremal cogenerating set": true, "natural numbers object": true, + "kernel pairs": true, + "cokernel 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 40fa66d4..a35726cd 100644 --- a/database/scripts/expected-data/Set.json +++ b/database/scripts/expected-data/Set.json @@ -119,6 +119,8 @@ "extremal generating set": true, "extremal cogenerator": true, "extremal cogenerating set": true, + "kernel pairs": true, + "cokernel pairs": true, "Grothendieck abelian": false, "Malcev": false, diff --git a/database/scripts/expected-data/Top.json b/database/scripts/expected-data/Top.json index 359a0c3d..c6f80aa6 100644 --- a/database/scripts/expected-data/Top.json +++ b/database/scripts/expected-data/Top.json @@ -84,6 +84,8 @@ "ℵ₂-small copowers": true, "extremal cogenerator": true, "extremal cogenerating set": true, + "kernel pairs": true, + "cokernel pairs": true, "abelian": false, "additive": false,