diff --git a/database/data/categories/Alg(R).yaml b/database/data/categories/Alg(R).yaml index d352aa82..1ac7ca03 100644 --- a/database/data/categories/Alg(R).yaml +++ b/database/data/categories/Alg(R).yaml @@ -50,7 +50,7 @@ unsatisfied_properties: - property: co-Malcev proof: 'See MO/509552: Consider the forgetful functor $U : \Alg(R) \to \Set$ and the relation $S \subseteq U^2$ defined by $S(A) \coloneqq \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $R[X]$ and $S$ by $R \langle X,Y \rangle / \langle XY-X^2 \rangle$. It is clear that $S$ is reflexive, but not symmetric.' - - property: coregular + - property: pushout-stable regular monomorphisms proof: '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.' label: alg_not_coregular diff --git a/database/data/categories/Ban.yaml b/database/data/categories/Ban.yaml index 3895bd54..89248ff3 100644 --- a/database/data/categories/Ban.yaml +++ b/database/data/categories/Ban.yaml @@ -37,16 +37,16 @@ satisfied_properties: proof: >- The Hahn-Banach theorem implies that $\IC$ is a cogenerator. We claim that it is in fact an extremal cogenerator. Thus, suppose $f : X \to Y$ is a morphism such that ${-} \circ f : \Hom(Y, \IC) \to \Hom(X, \IC)$ is bijective on the underlying sets. Then for any non-zero $x \in X$, by the Hahn-Banach theorem, there exists $\varphi \in X^*$ such that $|\varphi| = 1$ and $\varphi(x) = |x|$. Since $|\varphi| = 1$, we see that $\varphi$ is a morphism $X \to \IC$ in $\Ban$; so by the assumption, there exists a morphism $\psi : Y \to \IC$ such that $\varphi = \psi \circ f$. Therefore, $|x| = |\psi(f(x))| \le |f(x)|$; and conversely, since $f$ is a morphism, $|f(x)| \le |x|$. On the other hand, if $x = 0$, then certainly $|f(x)| = |x| = 0$. This shows that $f$ is isometric and therefore a regular monomorphism (see below). On the other hand, since $\IC$ is a cogenerator and ${-} \circ f$ is injective, we have $f$ is also an epimorphism. Hence, $f$ is an isomorphism. - - property: regular + - property: pullback-stable regular epimorphisms proof: >- - It suffices to prove that regular epimorphisms are stable under pullbacks. We will use their classification via open unit balls below. + We will use the classification of regular epimorphisms via open unit balls below. So let $f : X \to Y$ be a regular epimorphism and let $g : T \to Y$ be any morphism. We need to show that the projection $X \times_Y T \to X$ is a regular epimorphism. Let $t \in T$ be an element of norm $<1$. Since $g$ is a linear contraction, $g(t)$ has norm $<1$. Since $f$ is a regular epimorphism, there is some $x \in X$ with norm $<1$ and $f(x) = g(t)$. Then $(x,t) \in X \times_Y T$ is a preimage of $t$ with norm $\max(|x|,|t|) < 1$. - - property: coregular + - property: pushout-stable regular monomorphisms proof: >- - It suffices to prove that regular monomorphisms are stable under pushouts. We will use their classification as isometric linear maps below. + We will use the classification of regular monomorphisms as isometric linear maps below. So let $i : X \to Y$ be an isometric linear map and let $f : X \to T$ be any morphism. We need to show that the linear contraction $\iota : T \to T \sqcup_X Y$ is isometric as well. The pushout can be constructed as the quotient of the direct sum $T \oplus Y$, equipped with the $1$-norm, modulo the closure of the subspace containing all $(-f(x),i(x))$ for $x \in X$. Using that $i$ is an isometry, it is easily checked that this subspace is already closed. For $t \in T$ the norm of $\iota(t) = [(t,0)]$ is the infimum of the norms of $(t,0) + (-f(x),i(x)) = (t - f(x), i(x))$ for $x \in X$. By taking $x=0$ we see that the infimum is $\leq |t|$. diff --git a/database/data/categories/Cat.yaml b/database/data/categories/Cat.yaml index 11fd7d2c..329ba132 100644 --- a/database/data/categories/Cat.yaml +++ b/database/data/categories/Cat.yaml @@ -47,11 +47,11 @@ unsatisfied_properties: - property: cogenerating set proof: 'Assume that $S$ is a cogenerating set in $\Cat$. Then one checks that the set of monoids $\{\End(X) : X \in \C \in S\}$ is a cogenerating set in $\Mon$, which we know does not exist.' - - property: regular + - property: pullback-stable regular epimorphisms proof: See Example 3.14 at the nLab. - - property: coregular - proof: 'We already know that $\Mon$ is not coregular; in fact we have shown that there is a regular monomorphism $M \to N$ of monoids and a morphism $M \to K$ such that $K \to K \sqcup_M N$ is not a monomorphism. The delooping functor $B : \Mon \to \Cat$ has a left adjoint (MSE/574745), hence it preserves regular monomorphisms. It also preserves pushouts (MSE/5130854), and it reflects monomorphisms since it is faithful. Therefore, $B(M) \to B(N)$ provides the desired counterexample of a non-stable regular monomorphism of categories.' + - property: pushout-stable regular monomorphisms + proof: 'We already know that $\Mon$ has a regular monomorphism $M \to N$ and a morphism $M \to K$ such that $K \to K \sqcup_M N$ is not a monomorphism. The delooping functor $B : \Mon \to \Cat$ has a left adjoint (MSE/574745), hence it preserves regular monomorphisms. It also preserves pushouts (MSE/5130854), and it reflects monomorphisms since it is faithful. Therefore, $B(M) \to B(N)$ provides the desired counterexample of a non-stable regular monomorphism of categories.' references: - mon_not_coregular diff --git a/database/data/categories/CompHaus.yaml b/database/data/categories/CompHaus.yaml index 63db0ea2..fe5d3890 100644 --- a/database/data/categories/CompHaus.yaml +++ b/database/data/categories/CompHaus.yaml @@ -42,15 +42,15 @@ satisfied_properties: - property: Barr-exact proof: The forgetful functor from $\CompHaus$ to $\Set$ is monadic; see for example nLab. Therefore, by this result, $\CompHaus$ is Barr-exact. - - property: coregular - proof: - 'It suffices to show that pushouts preserve (regular) monomorphisms in $\CompHaus$. Thus, suppose we have a pushout square + - property: pushout-stable regular monomorphisms + proof: >- + Suppose we have a pushout square $$\begin{CD} A @> i >> B \\ @V f VV @VV g V \\ C @>> j > D, \end{CD}$$ - with $i : A \hookrightarrow B$ a monomorphism. Then for any pair of distinct elements $c, c'' \in C$, by Urysohn''s lemma there exists $\gamma : C \to [0, 1]$ with $\gamma(c) = 0$ and $\gamma(c'') = 1$. Also, by Tietze''s extension theorem, there exists $\beta : B \to [0, 1]$ such that $\beta \circ i = \gamma \circ f$. By the pushout property, there is a unique $\delta : D \to [0, 1]$ such that $\delta \circ g = \beta$ and $\delta \circ j = \gamma$. Since $\delta(j(c)) \ne \delta(j(c''))$, we conclude that $j(c) \ne j(c'')$. This shows that $j$ is injective, so it is a regular monomorphism.' + with $i : A \hookrightarrow B$ a monomorphism. Then for any pair of distinct elements $c, c' \in C$, by Urysohn's lemma there exists $\gamma : C \to [0, 1]$ with $\gamma(c) = 0$ and $\gamma(c') = 1$. Also, by Tietze's extension theorem, there exists $\beta : B \to [0, 1]$ such that $\beta \circ i = \gamma \circ f$. By the pushout property, there is a unique $\delta : D \to [0, 1]$ such that $\delta \circ g = \beta$ and $\delta \circ j = \gamma$. Since $\delta(j(c)) \ne \delta(j(c'))$, we conclude that $j(c) \ne j(c')$. This shows that $j$ is injective, so it is a regular monomorphism. - property: extensive proof: This follows from Lemma 11 here since $\Top$ is infinitary extensive and its full subcategory $\CompHaus$ is closed under pullbacks and finite coproducts in $\Top$. diff --git a/database/data/categories/FiltVect.yaml b/database/data/categories/FiltVect.yaml index 4501bd65..201b5663 100644 --- a/database/data/categories/FiltVect.yaml +++ b/database/data/categories/FiltVect.yaml @@ -78,18 +78,18 @@ satisfied_properties: $$F_{< N}^n(V) \coloneqq \begin{cases} F^n(V) & n < N \\ 0 & n \geq N. \end{cases}$$ Indeed, we have $F_{< N} \subseteq F_{< N+1}$, so that $\id_V : (V,F_{- - It remains to prove that regular epimorphisms are stable under pullbacks. This follows immediately from their classification below, from the fact that $F^n$ preserves limits, and from the regularity of $\Vect$. + This follows immediately from the classification of regular epimorphisms below, from the fact that $F^n$ preserves limits, and from the corresponding property of $\Vect$. In more detail, if $(V,F) \to (W,F)$ is a regular epimorphism and $(U,F) \to (W,F)$ is any morphism, then $(V,F) \times_{(W,F)} (U,F) \to (U,F)$ is a regular epimorphism, since $V \times_W U \to U$ is surjective and, for every $n \in \IZ$, the restricted map $$F^n(V \times_W U) = F^n(V) \times_{F^n(W)} F^n(U) \to F^n(U)$$ is surjective. - - property: coregular + - property: pushout-stable regular monomorphisms proof: >- - It remains to prove that regular monomorphisms (as classified below) are stable under pushouts. Let $i : (U,F) \to (V,F)$ be a regular monomorphism, i.e. $i$ is injective and $F^n(U) = i^*(F^n(V))$. Let $f : (U,F) \to (W,F)$ be any morphism. We must prove that the canonical morphism $(W,F) \to (V,F) \oplus_{(U,F)} (W,F)$ is a regular monomorphism. It is certainly injective, since the forgetful functor to $\Vect$ preserves colimits and $\Vect$ is abelian, and hence coregular. Now suppose that $w \in W$ is an element whose image $[0,w] \in V \oplus_U W$ lies in $F^n(V \oplus_U W)$; we must show that $w \in F^n(W)$. + Let $i : (U,F) \to (V,F)$ be a regular monomorphism, i.e. $i$ is injective and $F^n(U) = i^*(F^n(V))$. Let $f : (U,F) \to (W,F)$ be any morphism. We must prove that the canonical morphism $(W,F) \to (V,F) \oplus_{(U,F)} (W,F)$ is a regular monomorphism. It is certainly injective since the forgetful functor to $\Vect$ preserves colimits and $\Vect$ has the claimed property. Now suppose that $w \in W$ is an element whose image $[0,w] \in V \oplus_U W$ lies in $F^n(V \oplus_U W)$; we must show that $w \in F^n(W)$. Since, by the construction of colimits in $\FiltVect$, the subspace $F^n(V \oplus_U W)$ is the sum of the images of $F^n(V)$ and $F^n(W)$, there exist $v \in F^n(V)$ and $w' \in F^n(W)$ such that $[0,w] = [v,w']$. This means that there exists some $u \in U$ with $v = i(u)$ and $w = f(u) + w'$. Then $u \in F^n(U)$ because $i(u) \in F^n(V)$. Hence $f(u) \in F^n(W)$, and therefore $w = f(u) + w' \in F^n(W)$. unsatisfied_properties: diff --git a/database/data/categories/Grp.yaml b/database/data/categories/Grp.yaml index a117d21d..c1c1e4b3 100644 --- a/database/data/categories/Grp.yaml +++ b/database/data/categories/Grp.yaml @@ -58,8 +58,8 @@ unsatisfied_properties: proof: '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).' label: grp_no_cogenerator - - property: coregular - proof: This is because injective group homomorphisms are not stable under pushouts, see e.g. MSE/601463 or MSE/5088032. + - property: pushout-stable regular monomorphisms + proof: See MSE/601463 or MSE/5088032. - property: counital proof: The canonical morphism $F_2 = \IZ \sqcup \IZ \to \IZ \times \IZ$ is not a monomorphism since $F_2$ is not abelian. diff --git a/database/data/categories/Grp_c.yaml b/database/data/categories/Grp_c.yaml index 19222b46..468f51b9 100644 --- a/database/data/categories/Grp_c.yaml +++ b/database/data/categories/Grp_c.yaml @@ -88,8 +88,8 @@ unsatisfied_properties: references: - grp_no_regular_quotient_object_classifier - - property: coregular - proof: Pushouts of injective homomorphisms between countable groups do not need to be injective, see MSE/5088032. + - property: pushout-stable regular monomorphisms + proof: See MSE/5088032. - property: cogenerator proof: 'Assume that a cogenerator $Q$ exists in $\Grp_\c$. There are only countably many finitely generated subgroups of $Q$. But there are continuum many finitely generated simple groups; this follows from Corollary 1.5 in Finitely generated infinite simple groups of homeomorphisms of the real line by J. Hyde and Y. Lodha. Hence, there is a finitely generated (and hence countable) simple group $H$ which does not embed into $Q$. Since $H$ is simple, any homomorphism $H \to Q$ must be trivial then. But then $\id_H, 1 : H \rightrightarrows H$ are not separated by a homomorphism $H \to Q$.' diff --git a/database/data/categories/Haus.yaml b/database/data/categories/Haus.yaml index 328fb032..31b38a1d 100644 --- a/database/data/categories/Haus.yaml +++ b/database/data/categories/Haus.yaml @@ -82,7 +82,7 @@ unsatisfied_properties: - property: regular proof: 'The regular epimorphisms are precisely the surjective quotient maps of Hausdorff spaces (see below). In a regular category, for every regular epimorphism $X \to Y$ and every object $Z$, the induced morphism $X \times Z \to Y \times Z$ is again a regular epimorphism. This is not the case in $\Haus$ (or $\Top$, for that matter). The standard example is the quotient map $\IR \to \IR / \IZ^+$, for which the induced map $\IR \times \IQ \to \IR/\IZ^+ \times \IQ$ is not a quotient map (MSE/1907972).' - - property: coregular + - property: pushout-stable regular monomorphisms proof: >- Let $\Gamma$ be the Moore plane. Its underlying set is $\{(x,y) \in \IR^2 : y \geq 0 \}$. The open neighborhoods of points $(x,y)$ with $y > 0$ are those of $\IR^2$ (intersected with $\Gamma$), and the basic open neighborhoods of a point $(x,0)$ are open disks centered at $(x,\varepsilon)$ with radius $\varepsilon$ for some $\varepsilon > 0$. Then $\Gamma$ is Hausdorff, and the $x$-axis $A \coloneqq \{(x,0) : x \in \IR\}$ is a closed discrete subspace of $\Gamma$. In particular, by the classification of regular monomorphisms below, the inclusion map $i : A \to \Gamma$ is a regular monomorphism. Consider the two subsets $A_1 \coloneqq \{(x,0) : x \in \IQ \}$ and $A_2 \coloneqq \{(x,0) : x \in \IR \setminus \IQ \}$ of $A$. They are closed in $A$ (since $A$ is closed and discrete), disjoint, but cannot be separated by disjoint open neighborhoods in $\Gamma$; this is part of the proof of the well-known fact that $\Gamma$ is not normal (MSE/2528435). diff --git a/database/data/categories/Meas.yaml b/database/data/categories/Meas.yaml index af5336c0..e10dfa5b 100644 --- a/database/data/categories/Meas.yaml +++ b/database/data/categories/Meas.yaml @@ -39,11 +39,11 @@ satisfied_properties: proof: Take the colimit of the underlying sets and take the largest $\sigma$-algebra making all inclusions measurable. That is, a set is measurable iff its preimage under each inclusion is measurable. check_redundancy: false - - property: coregular + - property: pushout-stable regular monomorphisms proof: >- - The proof is similar to the proof for $\Top$. We already know that (finite) colimits and equalizers exist, and that they are preserved by the forgetful functor to $\Set$. It remains to show that regular monomorphisms, i.e. embeddings, are stable under pushouts. Thus, let $i : A \to X$ be an embedding and let $f : A \to Y$ be any measurable map. We claim that the induced measurable map + The proof is similar to the proof for $\Top$. Let $i : A \to X$ be an embedding and let $f : A \to Y$ be any measurable map. We claim that the induced measurable map $$j : Y \to Y \sqcup_A X$$ - is again an embedding. It is certainly injective, since $\Set$ is coregular. More precisely, the underlying set of $Y \sqcup_A X$ can be identified with $Y \sqcup (X \setminus \im(i))$. Now let $T \subseteq Y$ be a measurable subset. Then its preimage $f^*(T) \subseteq A$ is measurable. Since $i$ is an embedding, there exists a measurable subset $S \subseteq X$ such that $i^*(S) = f^*(T)$. Let $u : X \to Y \sqcup_A X$ denote the canonical map, so that $u \circ i = j \circ f$, and consider the subset + is again an embedding. It is certainly injective, since $\Set$ has the claimed property. More precisely, the underlying set of $Y \sqcup_A X$ can be identified with $Y \sqcup (X \setminus \im(i))$. Now let $T \subseteq Y$ be a measurable subset. Then its preimage $f^*(T) \subseteq A$ is measurable. Since $i$ is an embedding, there exists a measurable subset $S \subseteq X$ such that $i^*(S) = f^*(T)$. Let $u : X \to Y \sqcup_A X$ denote the canonical map, so that $u \circ i = j \circ f$, and consider the subset $$M \coloneqq j_*(T) \cup u_*(S \setminus \im(i))$$ of the pushout. It is straightforward to verify that $j^*(M) = T$ and $u^*(M) = S$. Since both $T$ and $S$ are measurable, it follows that $M$ is measurable. Finally, the equality $j^*(M) = T$ shows that every measurable subset of $Y$ is the preimage of a measurable subset of the pushout. Hence $j$ is an embedding, as claimed. references: diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index 3415d557..7234c33a 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -160,7 +160,7 @@ unsatisfied_properties: 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$. label: met_no_effective_cocongruences - - property: regular + - property: pullback-stable regular epimorphisms proof: We can take the same counterexample as for $\PMet$. references: - pmet_not_regular diff --git a/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml index 0b432668..61883815 100644 --- a/database/data/categories/Met_c.yaml +++ b/database/data/categories/Met_c.yaml @@ -121,5 +121,21 @@ special_morphisms: description: continuous maps with dense image proof: See MSE/937387. regular monomorphisms: - description: embeddings of closed subspaces - proof: A reference is Example 7.58 (3) in Joy of Cats, but a proof is missing there. + description: closed embeddings + proof: 'Regular monomorphisms are closed embeddings by the concrete construction of equalizers and the fact that metric spaces are Hausdorff. Conversely, let $A$ be a closed subset of a metric space $X$. If $A$ is empty, then it is the equalizer of the two constant maps $0,1 : X \rightrightarrows \IR$. If $A$ is non-empty, then it is the equalizer of the function $d(A,-) : X \to \IR$, $x \mapsto \inf_{a \in A} d(a,x)$, and the zero function $0 : X \to \IR$. The function $d(A,-)$ is non-expansive and hence continuous.' + regular epimorphisms: + description: 'A continuous map $f : X \to Y$ of metric spaces is a regular epimorphism if and only if $f$ is surjective and $Y$ carries the "final metric topology" with respect to $f$; by this we mean that, for every metric space $Z$ (not necessarily every topological space) and every set map $g : Y \to Z$ such that $g \circ f$ is continuous, $g$ is continuous. Furthermore, it is sufficient to demand this for $Z = \IR$.' + proof: >- + Assume first that $f$ is surjective and that $Y$ carries the final metric topology. Then it is straightforward to check, using the corresponding fact for $\Set$, that $f$ is the coequalizer of its kernel pair $X \times_Y X \rightrightarrows X$. + + Conversely, assume that $f : X \to Y$ is the coequalizer of $u,v : U \rightrightarrows X$. Let $Y' \subseteq Y$ be the image of $f$, equipped with the metric induced from $Y$. Then $f$ factors as $i \circ g$, where $g : X \to Y'$ is a surjective continuous map and $i : Y' \to Y$ is the inclusion. Since + $$i \circ g \circ u = f \circ u = f \circ v = i \circ g \circ v$$ + and $i$ is a monomorphism, we have $g \circ u = g \circ v$. Hence, there is a continuous map $\tilde{g} : Y \to Y'$ such that $\tilde{g} \circ f = g$. Thus + $$i \circ \tilde{g} \circ f = i \circ g = f = \id_Y \circ f.$$ + Since $f$ is an epimorphism, it follows that $i \circ \tilde{g} = \id_Y$. Therefore, $i$ is surjective, so $f$ is surjective as well. + + Finally, let $g : Y \to Z$ be a set map into a metric space $Z$, not assumed to be continuous, such that $g \circ f : X \to Z$ is continuous. Since $f \circ u = f \circ v$, we have + $$(g \circ f) \circ u = (g \circ f) \circ v.$$ + Hence, there is a continuous map $h : Y \to Z$ such that $g \circ f = h \circ f$. Since $f$ is surjective, this implies $g = h$. Therefore, $g$ is continuous, as claimed. + + That $Z = \IR$ suffices as a test space is a consequence of the general and elementary lemma that a map $X \to Y$ between metric spaces is continuous when for every continuous map $Y \to \IR$ the composition $X \to \IR$ is continuous. diff --git a/database/data/categories/Met_oo.yaml b/database/data/categories/Met_oo.yaml index b394ac65..f431f4c3 100644 --- a/database/data/categories/Met_oo.yaml +++ b/database/data/categories/Met_oo.yaml @@ -70,7 +70,7 @@ unsatisfied_properties: references: - met_no_effective_cocongruences - - property: regular + - property: pullback-stable regular epimorphisms proof: We can take the same counterexample as for $\PMet$. references: - pmet_not_regular diff --git a/database/data/categories/Mon.yaml b/database/data/categories/Mon.yaml index f34a7288..13435c70 100644 --- a/database/data/categories/Mon.yaml +++ b/database/data/categories/Mon.yaml @@ -53,7 +53,7 @@ unsatisfied_properties: - property: CSP proof: If $M \to N$ is an epimorphism in $\Mon$ and $M$ is infinite, then $\card(N) \leq \card(M)$ (see MO/510431). This implies that in $\Mon$ the canonical homomorphism $\coprod_{n \geq 0} \IN \to \prod_{n \geq 0} \IN$ is not an epimorphism because its domain is countable and its codomain is uncountable. - - property: coregular + - property: pushout-stable regular monomorphisms proof: 'Consider the monoid $M \coloneqq \langle x_0, x_1, s : x_0 s = x_1 s = 1 \rangle$. Notice that every element in $M$ has a unique expression as $s^k \cdot u$ with $k \in \IN$ and $u \in \langle x_0,x_1 \rangle_M$. Moreover, the canonical homomorphism $\iota : \langle x_0, x_1 \rangle \to M$ (from the free monoid) is injective. We will prove that it is a regular monomorphism, which however is not stable under pushouts. Consider $N \coloneqq \langle x_0, x_1, s_0, s_1 : x_i s_j = 1 \rangle$ and define $f_i : M \to N$ for $i=0,1$ by $f_i(x_j) = x_j$ and $f_i(s) = s_i$. Then $\iota$ is the equalizer of $f_0,f_1$. Now consider $g : \langle x_0,x_1 \rangle \to \langle y_0 \rangle$ defined by $g(x_0) = y_0$, $g(x_1) = 1$. The pushout of $\iota$ with $g$ is given by $\langle x_0, x_1, s, y_0 : x_0 s = x_1 s = 1 , \, x_0 = y_0, \, x_1 = 1 \rangle$, which simplifies to $\langle x_0, s : x_0 s = s = 1 \rangle$, which is trivial.' label: mon_not_coregular diff --git a/database/data/categories/PMet.yaml b/database/data/categories/PMet.yaml index 4635ae69..a9a0e47d 100644 --- a/database/data/categories/PMet.yaml +++ b/database/data/categories/PMet.yaml @@ -118,8 +118,8 @@ unsatisfied_properties: references: - top_no_effective_cocongruences - - property: regular - proof: 'We can adapt Example 3.14 at the nLab (which disproves regularity for $\Pos$ and related categories) as follows: Consider the subspaces $X = \{0,1,2,3\}$ and $Y = \{0,1,2\}$ of $\IR$ with the usual metric. Define a surjective map $p : X \to Y$ by $p(0)=0$, $p(1)=p(2)=1$, and $p(3)=2$. Clearly, $p$ is non-expansive. Moreover, one can check that $p$ satisfies the universal property in $\PMet$ of a coequalizer of the two maps $1,2 : \{\ast\} \rightrightarrows X$. Thus, $p$ is a regular epimorphism. Now consider the subspace $Z = \{0,2\}$ of $Y$. As a set, the pullback $X \times_Y Z$ is $p^*(Z) = \{0,3\}$. Using the definition of the product metric, one can verify that $d(0,3) = 3$ in this pullback. The projection $X \times_Y Z \to Z$ identifies with the evident bijective and non-expansive map $\{0,3\} \to \{0,2\}$. It is a monomorphism and not an isomorphism (the distances do not match), hence cannot be a regular epimorphism.' + - property: pullback-stable regular epimorphisms + proof: 'We can adapt Example 3.14 at the nLab (which provides non-stable regular epimorphisms in $\Pos$ and related categories) as follows: Consider the subspaces $X = \{0,1,2,3\}$ and $Y = \{0,1,2\}$ of $\IR$ with the usual metric. Define a surjective map $p : X \to Y$ by $p(0)=0$, $p(1)=p(2)=1$, and $p(3)=2$. Clearly, $p$ is non-expansive. Moreover, one can check that $p$ satisfies the universal property in $\PMet$ of a coequalizer of the two maps $1,2 : \{\ast\} \rightrightarrows X$. Thus, $p$ is a regular epimorphism. Now consider the subspace $Z = \{0,2\}$ of $Y$. As a set, the pullback $X \times_Y Z$ is $p^*(Z) = \{0,3\}$. Using the definition of the product metric, one can verify that $d(0,3) = 3$ in this pullback. The projection $X \times_Y Z \to Z$ identifies with the evident bijective and non-expansive map $\{0,3\} \to \{0,2\}$. It is a monomorphism and not an isomorphism (the distances do not match), hence cannot be a regular epimorphism.' label: pmet_not_regular special_objects: diff --git a/database/data/categories/Pos.yaml b/database/data/categories/Pos.yaml index 8353be37..f3b6f285 100644 --- a/database/data/categories/Pos.yaml +++ b/database/data/categories/Pos.yaml @@ -53,7 +53,7 @@ unsatisfied_properties: - property: balanced proof: The inclusion $\{0,1\} \to \{0 < 1\}$ provides a counterexample (where in the domain there is no relation between $0$ and $1$). - - property: regular + - property: pullback-stable regular epimorphisms proof: See Example 3.14 at the nLab. - property: Malcev diff --git a/database/data/categories/PreOrd.yaml b/database/data/categories/PreOrd.yaml index 360b6cc7..28c6e109 100644 --- a/database/data/categories/PreOrd.yaml +++ b/database/data/categories/PreOrd.yaml @@ -32,7 +32,7 @@ satisfied_properties: - property: infinitary extensive proof: 'This can be deduced from the infinitary extensivity of $\Set$ as follows. We already know that coproducts and pullbacks exist, and these are preserved by the forgetful functor to $\Set$. More concretely, coproducts are disjoint unions of the underlying sets equipped with the evident partial order that leaves the distinct summands incomparable. Since coproducts are disjoint in $\Set$ and the empty set has a unique preorder, it follows immediately that coproducts are disjoint in $\PreOrd$ as well. It remains to show that coproducts are stable under pullbacks. Let $(P_i)_{i \in I}$ be a family of preordered sets and let $f : T \to \coprod_{i \in I} P_i$ be an order-preserving map. Consider the pullbacks $T_i \coloneqq f^*(P_i)$. These are just the preimages of $P_i$ under $f$, with the partial order induced from $T$. Since coproducts in $\Set$ are stable under pullbacks, the canonical order-preserving map $\coprod_{i \in I} T_i \to T$ is bijective. It remains to show that it is order-reflecting. Since each $T_i \to T$ is order-reflecting, this amounts to proving that, for $x \in T_i$ and $y \in T_j$ with $i \neq j$, we never have $x \leq y$ in $T$. But such a relation would imply $f(x) \leq f(y)$ in $\coprod_{i \in I} P_i$, where $f(x) \in P_i$ and $f(y) \in P_j$, which contradicts the concrete description of the coproduct.' - - property: coregular + - property: pushout-stable regular monomorphisms proof: See MSE/5130295. - property: regular subobject classifier @@ -51,7 +51,7 @@ satisfied_properties: Finally, by this result, we can conclude that the product of $\{0,1\}_c$ and $\{0<1\}$ is an extremal cogenerator. unsatisfied_properties: - - property: regular + - property: pullback-stable regular epimorphisms proof: See Example 3.14 at the nLab. - property: skeletal diff --git a/database/data/categories/Rng.yaml b/database/data/categories/Rng.yaml index dea398ba..4172e04f 100644 --- a/database/data/categories/Rng.yaml +++ b/database/data/categories/Rng.yaml @@ -59,8 +59,8 @@ unsatisfied_properties: - property: CSP proof: Assume that $\coprod_n \IZ \to \prod_n \IZ$ is an epimorphism in $\Rng$. Then $((\coprod_n \IZ)^+)^{\ab} \to \prod_n \IZ$ would be an epimorphism in $\CRing$, where $(-)^+$ denotes the unitalization and $(-)^{\ab}$ the abelianization. But if $R \to S$ is an epimorphism of commutative rings, then $\card(S) \leq \card(R)$ by SP/04W0. Since $((\coprod_n \IZ)^+)^{\ab}$ is countable and $\prod_n \IZ$ is not, we get a contradiction. - - property: coregular - proof: 'We can copy the proof for $\Ring$, i.e. the proof for $\Alg(R)$. 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: pushout-stable regular monomorphisms + proof: 'We can copy the proof for $\Ring$, i.e. the proof for $\Alg(R)$ for $R = \IZ$. 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.' references: - alg_not_coregular diff --git a/database/data/categories/SemiGrp.yaml b/database/data/categories/SemiGrp.yaml index d9899349..7d593827 100644 --- a/database/data/categories/SemiGrp.yaml +++ b/database/data/categories/SemiGrp.yaml @@ -88,7 +88,7 @@ unsatisfied_properties: $$\alpha(x_0 y_1) = \alpha(y_0 x_1),$$ where $x_i$ (resp. $y_i$) denotes the image of $x$ (resp. $y$) in the copy $A_i$. This shows that $\alpha$ is not injective. - - property: coregular + - property: pushout-stable regular monomorphisms proof: >- We will find a regular monomorphism $\iota : F \to M$ of semigroups and a homomorphism $F \to K$ such that $K \to K \sqcup_F M$ is not injective. It is similar to our example for $\Mon$. Consider these semigroups defined by generators and relations: $$\begin{align*} diff --git a/database/data/categories/Set_ff.yaml b/database/data/categories/Set_ff.yaml index f9ffe948..735689b5 100644 --- a/database/data/categories/Set_ff.yaml +++ b/database/data/categories/Set_ff.yaml @@ -26,6 +26,11 @@ satisfied_properties: - property: equalizers proof: 'Equalizers can be constructed as in $\Set$ because of the following trivial observation: if $f : X \to Y$ is a finite-to-one map and $E \subseteq Y$ is a subset with $f(X) \subseteq E$, then the induced map $f^E : X \to E$ is also finite-to-one.' + - property: pullbacks + proof: 'Pullbacks can be constructed as in $\Set$. Namely, for two finite-to-one maps $f : X \to S$ and $g : Y \to S$, the projections from $X \times_S Y = \{(x,y) \in X \times Y : f(x)=g(y)\}$ to $X$ resp. $Y$ are finite-to-one since the fiber over $x \in X$ identifies with $g^*(\{f(x)\})$ and the fiber over $y \in Y$ identifies with $f^*(\{g(y)\})$. Moreover, if $h : T \to X \times_S Y$ is a map whose components $h_X : T \to X$ and $h_Y : T \to Y$ are finite-to-one, then $h$ is finite-to-one because of $h^*(\{x\}) = (h_X)^*(\{(x,y)\}) \cap (h_Y)^*(\{y\})$ for $(x,y) \in X \times_S Y$.' + check_redundancy: false + label: Set_ff_pullbacks + - property: locally cartesian closed proof: If $X$ is a set, the equivalence $\Set/X \simeq \Set^X$, $f \mapsto (f^*(\{x\}))_{x \in X}$ restricts to an equivalence $\Set_\ff / X \simeq \FinSet^X$. This category is cartesian closed since $\FinSet$ is cartesian closed and products of cartesian closed categories are cartesian closed. @@ -43,7 +48,16 @@ satisfied_properties: 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. - property: epi-regular - proof: 'If $f : X \to Y$ is an epimorphism in $\Set_\ff$, i.e. a surjective finite-to-one map, it is a coequalizer of the two maps $p_1, p_2 : X \times_Y Y \rightrightarrows Y$ in $\Set$. These maps are finite-to-one since $p_i^*(\{y\}) \cong f^*(\{y\})$ for $i=1,2$, and their coequalizer is also $f$ in $\Set_\ff$: It suffices to observe that if $h : Y \to T$ is a map such that $h \circ f$ is finite-to-one, then $h$ is finite-to-one as well. In fact, surjectivity of $f$ implies $h^*(\{t\}) = f_*((h \circ f)^*(\{t\}))$ for $t \in T$.' + proof: 'If $f : X \to Y$ is an epimorphism in $\Set_\ff$, i.e. a surjective finite-to-one map, it is a coequalizer of the two maps $p_1, p_2 : X \times_Y Y \rightrightarrows Y$ in $\Set$. These maps are finite-to-one (see the proof that pullbacks exist), and their coequalizer is also $f$ in $\Set_\ff$: It suffices to observe that if $h : Y \to T$ is a map such that $h \circ f$ is finite-to-one, then $h$ is finite-to-one as well. In fact, surjectivity of $f$ implies $h^*(\{t\}) = f_*((h \circ f)^*(\{t\}))$ for $t \in T$.' + label: Set_ff_epi_regular + references: + - Set_ff_pullbacks + + - property: pullback-stable regular epimorphisms + proof: We have seen that a morphism is a regular epimorphism if and only if it is surjective and that pullbacks can be constructed just like in $\Set$. Therefore, the claim follows from the corresponding property of $\Set$. + references: + - Set_ff_epi_regular + - Set_ff_pullbacks - property: well-copowered proof: This is clear since the epimorphisms are surjective. diff --git a/database/data/categories/Setne.yaml b/database/data/categories/Setne.yaml index f1df54cc..3493187a 100644 --- a/database/data/categories/Setne.yaml +++ b/database/data/categories/Setne.yaml @@ -48,6 +48,9 @@ satisfied_properties: - property: epi-regular proof: This follows easily from the fact that $\Set$ is epi-regular. + - property: pushout-stable regular monomorphisms + proof: This follows easily from the fact that $\Set$ has this property. + - property: strongly connected proof: Use constant maps. diff --git a/database/data/categories/Top.yaml b/database/data/categories/Top.yaml index 488ce0d5..84ad72a4 100644 --- a/database/data/categories/Top.yaml +++ b/database/data/categories/Top.yaml @@ -59,8 +59,8 @@ satisfied_properties: - property: infinitary extensive proof: 'This can be deduced from the infinitary extensivity of $\Set$ as follows. We already know that coproducts and pullbacks exist, and these are preserved by the forgetful functor to $\Set$. More concretely, coproducts are disjoint unions of the underlying sets whose open subsets are unions of open subsets of the summands. Since coproducts are disjoint in $\Set$ and the empty set has a unique topology, it follows immediately that coproducts are disjoint in $\Top$ as well. It remains to show that coproducts are stable under pullbacks. Let $(X_i)_{i \in I}$ be a family of topological spaces and let $f : T \to \coprod_{i \in I} X_i$ be a continuous map. Consider the pullbacks $T_i \coloneqq f^*(X_i)$. These are just the preimages of $X_i$ under $f$, with the topology induced from $T$. Since coproducts in $\Set$ are stable under pullbacks, the canonical continuous map $\coprod_{i \in I} T_i \to T$ is bijective. It remains to show that it is an open map. By the concrete description of open subsets in the disjoint union, it suffices to prove that each $T_i \to T$ is an open map. But this is the inclusion of a subspace, which is open since $X_i$ is open in $\coprod_{i \in I} X_i$.' - - property: coregular - proof: 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. Another proof can be found in MSE/2016945. + - property: pushout-stable regular monomorphisms + proof: We need to show that embeddings are stable under pushouts. For a proof see e.g. Lemma 3.6 at the nLab. Another proof can be found in MSE/2016945. label: top_coregular unsatisfied_properties: @@ -77,7 +77,7 @@ unsatisfied_properties: - property: cartesian filtered colimits proof: 'The functor $\IQ \times - : \Top \to \Top$ does not preserve sequential colimits, see MSE/1255678.' - - property: regular + - property: pullback-stable regular epimorphisms proof: See Example 3.14 at the nLab. - property: coaccessible diff --git a/database/data/categories/Top_pointed.yaml b/database/data/categories/Top_pointed.yaml index db00dfea..ea0bac56 100644 --- a/database/data/categories/Top_pointed.yaml +++ b/database/data/categories/Top_pointed.yaml @@ -77,7 +77,7 @@ unsatisfied_properties: - property: skeletal proof: This is trivial. - - property: regular + - property: pullback-stable regular epimorphisms proof: See Example 3.14 at the nLab. The proof also works for pointed spaces (resp. posets) by using the base points $a$ and $0$. - property: cartesian filtered colimits diff --git a/database/data/categories/TorsFreeAb.yaml b/database/data/categories/TorsFreeAb.yaml index 1f0b5b6c..1fd6c235 100644 --- a/database/data/categories/TorsFreeAb.yaml +++ b/database/data/categories/TorsFreeAb.yaml @@ -36,11 +36,11 @@ satisfied_properties: - property: regular 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 + - property: pushout-stable regular monomorphisms proof: >- - It suffices to prove that regular monomorphisms (which are classified below) are stable under pushouts. Let $i : A \to B$ be a regular monomorphism in $\TorsFreeAb$, i.e. $i$ is injective and its $\Ab$-cokernel $B/i(A)$ is torsion-free, and let $f : B \to C$ be any morphism in $\TorsFreeAb$. Their $\Ab$-pushout is + Let $i : A \to B$ be a regular monomorphism in $\TorsFreeAb$, i.e. $i$ is injective and its $\Ab$-cokernel $B/i(A)$ is torsion-free, and let $f : B \to C$ be any morphism in $\TorsFreeAb$. Their $\Ab$-pushout is $$P = (B \times C)/\{(i(a),-f(a)): a \in A\}.$$ - It is torsion-free: If $n \in \IZ \setminus \{0\}$ and $n (b,c) = (i(a),-f(a))$, there is some $a' \in A$ with $b = i(a')$ since $B/i(A)$ is torsion-free. It follows $n a' = a$, and then $c = -f(a')$ since $C$ is torsion-free. Thus, $(b,c) = (i(a'),-f(a'))$, which proves our claim. Therefore, $P$ is also the pushout in $\TorsFreeAb$. The homomorphism $j : C \to P$, $j(c) = [0,c]$ is injective (since $\Ab$ is coregular, but a direct proof is also easy), and by the universal property of $P$ its $\Ab$-cokernel is isomorphic to the $\Ab$-cokernel of $i$, which is torsion-free. + It is torsion-free: If $n \in \IZ \setminus \{0\}$ and $n (b,c) = (i(a),-f(a))$, there is some $a' \in A$ with $b = i(a')$ since $B/i(A)$ is torsion-free. It follows $n a' = a$, and then $c = -f(a')$ since $C$ is torsion-free. Thus, $(b,c) = (i(a'),-f(a'))$, which proves our claim. Therefore, $P$ is also the pushout in $\TorsFreeAb$. The homomorphism $j : C \to P$, $j(c) = [0,c]$ is injective (since $\Ab$ has pushout-stable regular monomorphisms, but a direct proof is also easy), and by the universal property of $P$ its $\Ab$-cokernel is isomorphic to the $\Ab$-cokernel of $i$, which is torsion-free. - property: extremal cogenerating set proof: >- diff --git a/database/data/category-implications/congruences.yaml b/database/data/category-implications/congruences.yaml index 5803dd83..74c8b6de 100644 --- a/database/data/category-implications/congruences.yaml +++ b/database/data/category-implications/congruences.yaml @@ -1,29 +1,4 @@ -# results on congruences and regular categories - -- id: regular_def - assumptions: - - regular - conclusions: - - finitely complete - - coequalizers of kernel pairs - proof: This holds by definition of a regular category. - -- id: regular_well-powered_well-copowered - assumptions: - - regular - - epi-regular - - well-powered - conclusions: - - well-copowered - proof: The regularity condition gives a bijection between the collection of quotients of $X$ and the collection of effective congruences on $X$, where the latter is a subcollection of the collection of subobjects of $X\times X$. - -- id: regular_balanced_epi-regular - assumptions: - - regular - - balanced - conclusions: - - epi-regular - proof: 'Given any epimorphism $f : X \twoheadrightarrow Y$ in a regular category, we have the factorization into a regular epimorphism $X \twoheadrightarrow \im(f)$ followed by a monomorphism $\im(f) \hookrightarrow Y$. Because the composition is an epimorphism, the monomorphism $\im(f) \hookrightarrow Y$ must also be an epimorphism, and therefore an isomorphism. It follows that $f$ is in fact a regular epimorphism.' +# results on congruences - id: congruence_quotients_are_reflexive_coequalizers assumptions: @@ -97,14 +72,6 @@ proof: >- Let $i : Y \hookrightarrow X$ be a monomorphism. Then we define a relation on $X$ via $E \coloneqq X \times Y$ with maps $f, g : E \rightrightarrows X$ defined by $f : (x, y) \mapsto x+i(y)$ and $g : (x, y) \mapsto x$. It is straightforward to check that $f$ and $g$ are jointly monomorphic. Now $E$ is a congruence because for generalized elements $x_1, x_2 \in X(T)$, $(x_1, x_2)$ factors through $E$ if and only if $x_1 - x_2$ factors through $Y$. In other words, the relation on $X(T)$ is exactly $x_1 \equiv x_2 \pmod{Y(T)}$, which is an equivalence relation on $X(T)$ (and in fact a congruence in $\Ab$). Now by assumption, $E$ is the kernel pair of some morphism $h : X \to Z$; in other words, $(x_1, x_2)$ factors through $E$ if and only if $h(x_1) = h(x_2)$. In particular, for $x \in X(T)$, $x$ factors through $Y$ if and only if $(x, 0)$ factors through $E$, which is equivalent to $h(x) = h(0) = 0$. We have thus shown that $Y$ is the kernel of $h$. -- id: regular_effective_congruences_implies_quotients - assumptions: - - effective congruences - - regular - conclusions: - - quotients of congruences - proof: We assume that every congruence is effective, and the regularity condition implies that every effective congruence has a quotient. - - id: regular_epi-regular_extensive_consequences assumptions: - epi-regular @@ -143,12 +110,3 @@ g(y) & = \alpha(y)', & g(y') & = \alpha(y), \end{align*}$$ on generalized elements. Extensivity can be used to show that $f, g$ are jointly monomorphic. Clearly, the pair $f, g$ is reflexive and symmetric. For transitivity, one once again uses extensivity. By assumption, there is a morphism $h : B + B' \to C$ such that $f, g$ is the kernel pair of $h$, that is, two generalized elements $x, y \in B + B'$ satisfy $h(x) = h(y)$ if and only if $x = f(e)$, $y = g(e)$ for some $e \in E$. In particular, for $x \in B$, we have $h(x) = h(x')$ if and only if $x = f(e)$, $x' = g(e)$ for some $e \in E$. By disjointness of coproducts, we must necessarily have $e \in A$, and $x = \alpha(e)$. This shows that $\alpha$ is the equalizer of $h \circ i_1, h \circ i_2 : B \rightrightarrows C$. - -- id: Barr-exact_definition - assumptions: - - Barr-exact - conclusions: - - regular - - effective congruences - proof: This holds by definition. - is_equivalence: true diff --git a/database/data/category-implications/regular.yaml b/database/data/category-implications/regular.yaml new file mode 100644 index 00000000..e0b7079c --- /dev/null +++ b/database/data/category-implications/regular.yaml @@ -0,0 +1,44 @@ +# results on regular categories and related notions + +- id: regular_def + assumptions: + - regular + conclusions: + - finitely complete + - coequalizers of kernel pairs + - pullback-stable regular epimorphisms + proof: This is the definition of a regular category. + is_equivalence: true + +- id: pullback-stable-requires-pullbacks + assumptions: + - pullback-stable regular epimorphisms + conclusions: + - pullbacks + proof: This holds by definition. + +- id: regular_well-powered_well-copowered + assumptions: + - regular + - epi-regular + - well-powered + conclusions: + - well-copowered + proof: The regularity condition gives a bijection between the collection of quotients of $X$ and the collection of effective congruences on $X$, where the latter is a subcollection of the collection of subobjects of $X\times X$. + +- id: regular_balanced_epi-regular + assumptions: + - regular + - balanced + conclusions: + - epi-regular + proof: 'Given any epimorphism $f : X \twoheadrightarrow Y$ in a regular category, we have the factorization into a regular epimorphism $X \twoheadrightarrow \im(f)$ followed by a monomorphism $\im(f) \hookrightarrow Y$. Because the composition is an epimorphism, the monomorphism $\im(f) \hookrightarrow Y$ must also be an epimorphism, and therefore an isomorphism. It follows that $f$ is in fact a regular epimorphism.' + +- id: Barr-exact_definition + assumptions: + - Barr-exact + conclusions: + - regular + - effective congruences + proof: This holds by definition. + is_equivalence: true diff --git a/database/data/category-implications/subobject-trivial.yaml b/database/data/category-implications/subobject-trivial.yaml index e701a27e..6c941a6e 100644 --- a/database/data/category-implications/subobject-trivial.yaml +++ b/database/data/category-implications/subobject-trivial.yaml @@ -63,3 +63,11 @@ conclusions: - trivial proof: 'For any object $X$, the coequalizer of the two coprojections $X \rightrightarrows X \sqcup X$ is the codiagonal $\nabla : X \sqcup X \to X$. Therefore, these two coprojections are equal. But their equalizer is also the unique morphism $! : 0 \to X$. It follows that $! : 0 \to X$ is an isomorphism.' + +- id: isos_are_stable + assumptions: + - regular-quotient-trivial + - pullbacks + conclusions: + - pullback-stable regular epimorphisms + proof: Regular epimorphisms are isomorphisms by assumption, and isomorphisms are clearly stable under pullback. diff --git a/database/data/category-properties/pullback-stable regular epimorphisms.yaml b/database/data/category-properties/pullback-stable regular epimorphisms.yaml new file mode 100644 index 00000000..2fd78aab --- /dev/null +++ b/database/data/category-properties/pullback-stable regular epimorphisms.yaml @@ -0,0 +1,14 @@ +id: pullback-stable regular epimorphisms +relation: has +description: A category has pullback-stable regular epimorphisms if it has pullbacks and, for every regular epimorphism $X \to Y$ and every morphism $Z \to Y$, the induced morphism $X \times_Y Z \to Z$ is also a regular epimorphism. This property is one of the requirements for a category to be regular. +nlab_link: https://ncatlab.org/nlab/show/stability+under+pullback +dual: pushout-stable regular monomorphisms +invariant_under_equivalences: true + +related: + - pullbacks + - regular + +tags: + - limit–colimit interaction + - morphism behavior diff --git a/database/data/category-properties/pushout-stable regular monomorphisms.yaml b/database/data/category-properties/pushout-stable regular monomorphisms.yaml new file mode 100644 index 00000000..46d9b103 --- /dev/null +++ b/database/data/category-properties/pushout-stable regular monomorphisms.yaml @@ -0,0 +1,14 @@ +id: pushout-stable regular monomorphisms +relation: has +description: A category has pushout-stable regular monomorphisms if it has pushouts and, for every regular monomorphism $X \to Y$ and every morphism $X \to Z$, the induced morphism $Z \to Z \sqcup_X Y$ is also a regular monomorphism. This property is one of the requirements for a category to be coregular. +nlab_link: https://ncatlab.org/nlab/show/stability+under+pushout +dual: pullback-stable regular epimorphisms +invariant_under_equivalences: true + +related: + - pushouts + - coregular + +tags: + - limit–colimit interaction + - morphism behavior diff --git a/database/schema/002_properties.sql b/database/schema/002_properties.sql index d751a682..439aaae8 100644 --- a/database/schema/002_properties.sql +++ b/database/schema/002_properties.sql @@ -78,7 +78,7 @@ CREATE TABLE proof_references ( property_id TEXT NOT NULL, type TEXT NOT NULL, reference TEXT NOT NULL, - PRIMARY KEY (structure_id, property_id), + PRIMARY KEY (structure_id, property_id, reference), FOREIGN KEY (structure_id, type) REFERENCES structures (id, type) ON DELETE CASCADE, FOREIGN KEY (property_id, type) diff --git a/database/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json index df68bb2c..5cb4caf0 100644 --- a/database/scripts/expected-data/Ab.json +++ b/database/scripts/expected-data/Ab.json @@ -125,6 +125,8 @@ "cokernel pairs": true, "equalizers of cokernel pairs": true, "coequalizers of kernel pairs": true, + "pullback-stable regular epimorphisms": true, + "pushout-stable regular monomorphisms": 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 e405c63d..0e9bfd48 100644 --- a/database/scripts/expected-data/Set.json +++ b/database/scripts/expected-data/Set.json @@ -123,6 +123,8 @@ "cokernel pairs": true, "equalizers of cokernel pairs": true, "coequalizers of kernel pairs": true, + "pullback-stable regular epimorphisms": true, + "pushout-stable regular monomorphisms": true, "Grothendieck abelian": false, "Malcev": false, diff --git a/database/scripts/expected-data/Top.json b/database/scripts/expected-data/Top.json index b5aefcc9..b3d97fbf 100644 --- a/database/scripts/expected-data/Top.json +++ b/database/scripts/expected-data/Top.json @@ -88,6 +88,7 @@ "cokernel pairs": true, "equalizers of cokernel pairs": true, "coequalizers of kernel pairs": true, + "pushout-stable regular monomorphisms": true, "abelian": false, "additive": false, @@ -184,5 +185,6 @@ "regular-quotient-trivial": false, "core-connected": false, "extremal generator": false, - "extremal generating set": false + "extremal generating set": false, + "pullback-stable regular epimorphisms": false }