From ffa718a260c61b4661ab077d54a1ee0908aa0d1c Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 21 Aug 2026 22:41:52 +0200 Subject: [PATCH 1/9] remove redundant implication --- database/data/category-implications/congruences.yaml | 8 -------- 1 file changed, 8 deletions(-) diff --git a/database/data/category-implications/congruences.yaml b/database/data/category-implications/congruences.yaml index 5803dd832..6989b0fde 100644 --- a/database/data/category-implications/congruences.yaml +++ b/database/data/category-implications/congruences.yaml @@ -97,14 +97,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 From af82dfc1a63beafb64a8b829e5f8dd0e608563e9 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 21 Aug 2026 17:25:13 +0200 Subject: [PATCH 2/9] add properties: pullback-stable regular epis / pushout-stable regular monos --- .../category-implications/congruences.yaml | 36 +-------------- .../data/category-implications/regular.yaml | 44 +++++++++++++++++++ .../subobject-trivial.yaml | 8 ++++ .../pullback-stable regular epimorphisms.yaml | 14 ++++++ .../pushout-stable regular monomorphisms.yaml | 14 ++++++ database/scripts/expected-data/Ab.json | 2 + database/scripts/expected-data/Set.json | 2 + database/scripts/expected-data/Top.json | 4 +- 8 files changed, 88 insertions(+), 36 deletions(-) create mode 100644 database/data/category-implications/regular.yaml create mode 100644 database/data/category-properties/pullback-stable regular epimorphisms.yaml create mode 100644 database/data/category-properties/pushout-stable regular monomorphisms.yaml diff --git a/database/data/category-implications/congruences.yaml b/database/data/category-implications/congruences.yaml index 6989b0fde..74c8b6de5 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: @@ -135,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 000000000..e0b7079c2 --- /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 bf79b6338..32cd7aafb 100644 --- a/database/data/category-implications/subobject-trivial.yaml +++ b/database/data/category-implications/subobject-trivial.yaml @@ -70,3 +70,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 000000000..2fd78aab8 --- /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 000000000..46d9b1037 --- /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/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json index 6cb04cfe1..dd5181dc6 100644 --- a/database/scripts/expected-data/Ab.json +++ b/database/scripts/expected-data/Ab.json @@ -128,6 +128,8 @@ "concretizable": true, "total": true, "cototal": 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 34fdebfb0..ac9697142 100644 --- a/database/scripts/expected-data/Set.json +++ b/database/scripts/expected-data/Set.json @@ -126,6 +126,8 @@ "concretizable": true, "total": true, "cototal": 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 36e9a0b10..5e16fcbc7 100644 --- a/database/scripts/expected-data/Top.json +++ b/database/scripts/expected-data/Top.json @@ -91,6 +91,7 @@ "concretizable": true, "total": true, "cototal": true, + "pushout-stable regular monomorphisms": true, "abelian": false, "additive": false, @@ -187,5 +188,6 @@ "regular-quotient-trivial": false, "core-connected": false, "extremal generator": false, - "extremal generating collection": false + "extremal generating collection": false, + "pullback-stable regular epimorphisms": false } From ba402c8e4d1166ec64fa1b0322ac1ba3a7a5c25b Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 27 Sep 2026 12:09:04 +0200 Subject: [PATCH 3/9] multi-algebraic categories have pullback-stable regular epis in fact, the regular epis of models of an FPC-sketch are precisely the pointwise surjective morphisms --- .../data/category-implications/algebraic.yaml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/database/data/category-implications/algebraic.yaml b/database/data/category-implications/algebraic.yaml index c16702f92..4ec509afd 100644 --- a/database/data/category-implications/algebraic.yaml +++ b/database/data/category-implications/algebraic.yaml @@ -91,3 +91,19 @@ conclusions: - effective congruences proof: This is Thm. 4.0 in Yves Diers, Catégories Multialgébriques or its English translation. + +- id: multi-algebraic_classification_regular_epis + assumptions: + - multi-algebraic + conclusions: + - pullback-stable regular epimorphisms + proof: >- + Let $\C$ be a multi-algebraic category. We may assume $\C = \Mod(\A)$, where $\A$ is a small category equipped with a collection of finite discrete cones and discrete cocones, and $\Mod(\A) \subseteq \Hom(\A,\Set)$ consists of those functors that map the finite discrete cones in $\A$ to finite product cones in $\Set$ and the discrete cocones in $\A$ to coproduct cocones in $\Set$. Since finite products and coproducts commute with pullbacks in $\Set$, it is easy to check that $\Mod(\A) \subseteq \Hom(\A,\Set)$ is closed under pullbacks. Thus, pullbacks are constructed pointwise. Since surjective maps are stable under pullback in $\Set$, it remains to show, as in the case of finitary algebraic categories, that regular epimorphisms in $\C$ are precisely the pointwise surjective morphisms of models. + + + First, let $\alpha : F \to G$ be any morphism of models. For $A \in \A$, consider the image $I(A) = \im(\alpha(A)) \subseteq G(A)$. This defines a subfunctor $I \subseteq G$. It is a model because $F$ and $G$ are models and, for any family of maps of sets $(f_i : X_i \to Y_i)_{i \in I}$, we have $\im(\prod_{i \in I} f_i) = \prod_{i \in I} \im(f_i)$ and $\im(\coprod_{i \in I} f_i) = \coprod_{i \in I} \im(f_i)$. Therefore, $\alpha$ factors in $\C$ as + $$\alpha = \iota \circ \pi,$$ + where $\pi : F \to I$ is pointwise surjective and $\iota : I \to G$ is pointwise injective, hence a monomorphism. If $\alpha$ is a regular epimorphism, then it is in particular an extremal epimorphism, so $\iota$ is an isomorphism. Thus, $I = G$, and $\alpha$ is pointwise surjective. + + + Conversely, assume that $\alpha : F \to G$ is pointwise surjective. Then it is the coequalizer of its kernel pair $F \times_G F \rightrightarrows F$ in the category $\Hom(\A,\Set)$ of all functors. Since the pullback $F \times_G F$ is a model, $\alpha$ is also the coequalizer in the full subcategory of models. From 3d30834f3e6675d399a2029ac0941bcab0d809d4 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 27 Sep 2026 10:40:41 +0200 Subject: [PATCH 4/9] locally cartesian closed categories with binary products have pullback-stable regular epis --- database/data/category-implications/cartesian closed.yaml | 8 ++++++++ .../category-properties/locally cartesian closed.yaml | 2 +- 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/database/data/category-implications/cartesian closed.yaml b/database/data/category-implications/cartesian closed.yaml index 7d143bc56..125bc242e 100644 --- a/database/data/category-implications/cartesian closed.yaml +++ b/database/data/category-implications/cartesian closed.yaml @@ -104,3 +104,11 @@ conclusions: - locally cartesian closed proof: In a thin category, every object is subterminal. Thus, the result follows from Corollary 6 here. + +- id: lcc_stable_reg_epis + assumptions: + - locally cartesian closed + - binary products + conclusions: + - pullback-stable regular epimorphisms + proof: 'Let $p : X \to Y$ be a regular epimorphism in a locally cartesian closed category, and let $f : Z \to Y$ be any morphism. We may lift $p$ to a morphism in $\C / Y$ by equipping $X$ with the structure morphism $p$ and $Y$ with the structure morphism $\id_Y$. It is straightforward to check that $p$ is also a regular epimorphism in $\C / Y$. Since the base change functor $f^* : \C / Y \to \C / Z$ is a left adjoint, it preserves regular epimorphisms. Hence the morphism $X \times_Y Z \to Z$ induced by $p$ is a regular epimorphism in $\C / Z$. Finally, the underlying morphism in $\C$ is a regular epimorphism because the forgetful functor $\C / Z \to \C$ has a right adjoint, mapping $T$ to $T \times Z \to Z$, and therefore preserves regular epimorphisms.' diff --git a/database/data/category-properties/locally cartesian closed.yaml b/database/data/category-properties/locally cartesian closed.yaml index fc86a0421..fb260afb2 100644 --- a/database/data/category-properties/locally cartesian closed.yaml +++ b/database/data/category-properties/locally cartesian closed.yaml @@ -1,6 +1,6 @@ id: locally cartesian closed relation: is -description: A category is locally cartesian closed if each of its slice categories is cartesian closed. +description: 'A category $\C$ is locally cartesian closed if each of its slice categories $\C / X$ is cartesian closed. Equivalently, pullbacks exist, and for every morphism $f : X \to Y$ the base change functor $f^* : \C / Y \to \C / X$ has a right adjoint.' nlab_link: https://ncatlab.org/nlab/show/locally+cartesian+closed+category dual: locally cocartesian coclosed invariant_under_equivalences: true From d0068fdca27eddf2eda87b37163e47ea79184ce4 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 21 Aug 2026 18:05:17 +0200 Subject: [PATCH 5/9] rework regularity and coregularity proofs; use the stability properties directly --- database/data/categories/Alg(R).yaml | 2 +- database/data/categories/Ban.yaml | 8 ++++---- database/data/categories/Cat.yaml | 6 +++--- database/data/categories/CompHaus.yaml | 4 ++-- database/data/categories/FiltVect.yaml | 8 ++++---- database/data/categories/FreeAb.yaml | 4 ++-- database/data/categories/FreeAb_fg.yaml | 4 ++-- database/data/categories/Grp.yaml | 4 ++-- database/data/categories/Grp_c.yaml | 4 ++-- database/data/categories/Haus.yaml | 6 +++--- database/data/categories/Meas.yaml | 6 +++--- database/data/categories/Met.yaml | 2 +- database/data/categories/Met_oo.yaml | 2 +- database/data/categories/Mon.yaml | 2 +- database/data/categories/PMet.yaml | 4 ++-- database/data/categories/Pos.yaml | 4 ++-- database/data/categories/PreOrd.yaml | 4 ++-- database/data/categories/Rng.yaml | 4 ++-- database/data/categories/SemiGrp.yaml | 2 +- database/data/categories/Set_family_mostly_0.yaml | 6 +++--- database/data/categories/SetxSet_0_fin.yaml | 4 ++-- database/data/categories/Top.yaml | 6 +++--- database/data/categories/Top_pointed.yaml | 2 +- database/data/categories/TorsFreeAb.yaml | 6 +++--- 24 files changed, 52 insertions(+), 52 deletions(-) diff --git a/database/data/categories/Alg(R).yaml b/database/data/categories/Alg(R).yaml index 935935a1b..26b15f609 100644 --- a/database/data/categories/Alg(R).yaml +++ b/database/data/categories/Alg(R).yaml @@ -52,7 +52,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 3895bd54b..89248ff3d 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 3a0db17f6..4bad3cd43 100644 --- a/database/data/categories/Cat.yaml +++ b/database/data/categories/Cat.yaml @@ -45,11 +45,11 @@ unsatisfied_properties: - property: balanced proof: Since we know that $\Mon$ is not balanced, there is a monoid map $M \to N$ which is a monomorphism and an epimorphism which is not an isomorphism. Then $B(M) \to B(N)$ has the corresponding properties. - - 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 510ccba68..74cec97f5 100644 --- a/database/data/categories/CompHaus.yaml +++ b/database/data/categories/CompHaus.yaml @@ -43,9 +43,9 @@ 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 + - property: pushout-stable regular monomorphisms proof: >- - It suffices to show that pushouts preserve (regular) monomorphisms in $\CompHaus$. Thus, suppose we have a pushout square + Suppose we have a pushout square $$\begin{CD} A @> i >> B \\ @V f VV @VV g V \\ diff --git a/database/data/categories/FiltVect.yaml b/database/data/categories/FiltVect.yaml index a07b49a25..9c05a95ad 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/FreeAb.yaml b/database/data/categories/FreeAb.yaml index 9899d7de2..4d3048077 100644 --- a/database/data/categories/FreeAb.yaml +++ b/database/data/categories/FreeAb.yaml @@ -46,8 +46,8 @@ satisfied_properties: proof: 'Let $f : A \to B$ be a homomorphism of free abelian groups. The coequalizer of its kernel pair $A \times_B A \rightrightarrows A$ in $\Ab$ is the image $\im(f)$. As a subgroup of $B$, it is also free abelian. Then it is also the coequalizer of the kernel pair in $\FreeAb$.' check_redundancy: false - - property: regular - proof: It remains to prove that regular epimorphisms are stable under pullback. This is clear since they coincide with the surjective homomorphisms (see below). + - property: pullback-stable regular epimorphisms + proof: This is clear since regular epimorphisms coincide with the surjective homomorphisms (see below). unsatisfied_properties: - property: balanced diff --git a/database/data/categories/FreeAb_fg.yaml b/database/data/categories/FreeAb_fg.yaml index db95dc082..64cc7cc09 100644 --- a/database/data/categories/FreeAb_fg.yaml +++ b/database/data/categories/FreeAb_fg.yaml @@ -40,8 +40,8 @@ satisfied_properties: references: - proj_fg_self-dual - - property: regular - proof: We already know that the category is finitely complete and self-dual, hence also finitely cocomplete. It remains to prove that regular epimorphisms are stable under pullback. This is clear since they coincide with the surjective homomorphisms (see below). + - property: pullback-stable regular epimorphisms + proof: This is clear since regular epimorphisms coincide with the surjective homomorphisms (see below). - property: ℵ₁-accessible proof: >- diff --git a/database/data/categories/Grp.yaml b/database/data/categories/Grp.yaml index 4a536f7d4..727a26d97 100644 --- a/database/data/categories/Grp.yaml +++ b/database/data/categories/Grp.yaml @@ -62,8 +62,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 44189c860..3aa20dd50 100644 --- a/database/data/categories/Grp_c.yaml +++ b/database/data/categories/Grp_c.yaml @@ -91,8 +91,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 6b441f983..d31c5bc2d 100644 --- a/database/data/categories/Haus.yaml +++ b/database/data/categories/Haus.yaml @@ -78,10 +78,10 @@ unsatisfied_properties: references: - met_no_filtered_colimit_stable_monos - - 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: pullback-stable regular epimorphisms + proof: In a category with pullback-regular epimorphisms and products, 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, since it can be seen as $X \times_Y (Y \times Z) \to Y \times Z$. 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 fa3c0cbf3..2d9ca4934 100644 --- a/database/data/categories/Meas.yaml +++ b/database/data/categories/Meas.yaml @@ -40,11 +40,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 6c2d12260..c1614f7cd 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_oo.yaml b/database/data/categories/Met_oo.yaml index bdf90725b..9091f5524 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 289ae0bc2..2ec07acfe 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 248f6024f..6cb6b41de 100644 --- a/database/data/categories/PMet.yaml +++ b/database/data/categories/PMet.yaml @@ -121,8 +121,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 12c821e74..4797e36b2 100644 --- a/database/data/categories/Pos.yaml +++ b/database/data/categories/Pos.yaml @@ -33,7 +33,7 @@ satisfied_properties: - property: infinitary extensive proof: This follows from Lemma 11 here since $\PreOrd$ is infinitary extensive and its full subcategory $\Pos$ is closed under pullbacks and coproducts in $\PreOrd$. - - property: coregular + - property: pushout-stable regular monomorphisms proof: See MSE/5130295. - property: extremal generator @@ -56,7 +56,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 1b7e91dcb..66b3cb183 100644 --- a/database/data/categories/PreOrd.yaml +++ b/database/data/categories/PreOrd.yaml @@ -34,7 +34,7 @@ satisfied_properties: 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.' label: PreOrd_infinitary_extensive - - property: coregular + - property: pushout-stable regular monomorphisms proof: See MSE/5130295. - property: regular subobject classifier @@ -53,7 +53,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 3b1fa08fc..77fd1e747 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 4830c4d53..e6339c442 100644 --- a/database/data/categories/SemiGrp.yaml +++ b/database/data/categories/SemiGrp.yaml @@ -89,7 +89,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_family_mostly_0.yaml b/database/data/categories/Set_family_mostly_0.yaml index e7af16b91..93b4c8cad 100644 --- a/database/data/categories/Set_family_mostly_0.yaml +++ b/database/data/categories/Set_family_mostly_0.yaml @@ -58,12 +58,12 @@ satisfied_properties: - property: filtered-colimit-stable monomorphisms proof: Since filtered colimits are constructed pointwise and the monomorphisms are precisely the morphisms that are pointwise injective (see below), this property is inherited from $\Set$. + - property: pushout-stable regular monomorphisms + proof: Based on the descriptions of pushouts and regular monomorphisms, this property is inherited from $\Set$. + - property: cocartesian cofiltered limits proof: This property is inherited from $\Set$ since binary coproducts (in fact, all colimits) and cofiltered limits (in fact, all non-empty limits) are constructed pointwise. - - property: coregular - proof: It suffices to prove that regular monomorphisms are stable under pushout. This property is clearly inherited from $\Set$. - - property: well-powered proof: The monomorphisms $X \to Y$ are precisely the morphisms that are pointwise injective (see below). If $X_i \to Y_i$ is injective and $Y_i = \varnothing$, then also $X_i = \varnothing$. It follows that the collection $\Sub(Y) \cong \prod_{i \in \supp(Y)} \Sub(Y_i)$ is essentially small. check_redundancy: false diff --git a/database/data/categories/SetxSet_0_fin.yaml b/database/data/categories/SetxSet_0_fin.yaml index 1e8149f78..d9c292a83 100644 --- a/database/data/categories/SetxSet_0_fin.yaml +++ b/database/data/categories/SetxSet_0_fin.yaml @@ -53,8 +53,8 @@ satisfied_properties: - SetxSet_0_fin_equalizers - SetxSet_0_fin_finite_products - - property: regular - proof: By the previous properties, it suffices to prove that epimorphisms are stable under pullback. Since they are pairs of surjective maps and pullbacks are constructed pointwise, this follows immediately from the corresponding property of $\Set$. + - property: pullback-stable regular epimorphisms + proof: Since every epimorphism is regular, epimorphisms are pairs of surjective maps, and pullbacks are constructed pointwise, this follows immediately from the corresponding property of $\Set$. - property: effective congruences proof: Let $(R,S) \rightrightarrows (A,B)$ be a congruence in $(\Set \times \Set)_{\varnothing,\fin}$. Since finite limits are constructed pointwise, it is also a congruence in $\Set \times \Set$, and therefore a pair of congruences in $\Set$. Thus, the congruence is the kernel pair of $(A,B) \to (A/R,B/S)$ in $\Set \times \Set$. It remains to show that $(A/R,B/S)$ belongs to $(\Set \times \Set)_{\varnothing,\fin}$. If $A$ is empty, then $A/R$ is empty, and the claim holds. Otherwise, $B$ is finite, and hence $B/S$ is finite. diff --git a/database/data/categories/Top.yaml b/database/data/categories/Top.yaml index 7e4b7519f..847eb81e6 100644 --- a/database/data/categories/Top.yaml +++ b/database/data/categories/Top.yaml @@ -61,8 +61,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: @@ -79,7 +79,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 e1d65aeac..fc0ff3b11 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 069067af6..ea58173c0 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 collection proof: >- From 235d2c6251142d7fb301a2e8de2a1988bf7ff306 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 21 Aug 2026 18:26:29 +0200 Subject: [PATCH 6/9] Set_ff has pullback-stable regular epis --- database/data/categories/Set_ff.yaml | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/database/data/categories/Set_ff.yaml b/database/data/categories/Set_ff.yaml index 25f593732..19d3287d5 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. From e424a6568f28cce56ee1e9781340843181fbbf77 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 21 Aug 2026 18:32:37 +0200 Subject: [PATCH 7/9] Set_ne has pushout-stable regular monos --- database/data/categories/Setne.yaml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/database/data/categories/Setne.yaml b/database/data/categories/Setne.yaml index 8d5a2cef6..f3736e1c4 100644 --- a/database/data/categories/Setne.yaml +++ b/database/data/categories/Setne.yaml @@ -49,6 +49,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. From d580e903ce3f25d1aba67f2a67a15d3a7440a196 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 21 Aug 2026 22:12:33 +0200 Subject: [PATCH 8/9] describe regular monos and regular epis in Met_c --- database/data/categories/Met_c.yaml | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml index 081221a60..5b084bcbd 100644 --- a/database/data/categories/Met_c.yaml +++ b/database/data/categories/Met_c.yaml @@ -126,5 +126,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. From 2cc2bd04ea403556d8de223b5602e338ea9d6a82 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 27 Sep 2026 11:03:30 +0200 Subject: [PATCH 9/9] decide pushout-stable regular monos for three categories --- content/free-cocompletion.md | 6 +++--- database/data/categories/SeqSet_conn.yaml | 3 +++ database/data/categories/Set_family_mostly_1.yaml | 3 +++ .../data/categories/cocompletion-discrete-pair-join.yaml | 3 +++ 4 files changed, 12 insertions(+), 3 deletions(-) diff --git a/content/free-cocompletion.md b/content/free-cocompletion.md index 7701e4aa4..4c944349a 100644 --- a/content/free-cocompletion.md +++ b/content/free-cocompletion.md @@ -78,11 +78,11 @@ The direction $\impliedby$ is trivial in each case. For the direction $\implies$ ::: ::: Lemma 6 -If $\C$ is a locally small category, then $\widehat{\C}$ is mono-regular. Actually, every monomorphism is an effective monomorphism. Moreover, monomorphisms are stable under filtered colimits. +If $\C$ is a locally small category, then $\widehat{\C}$ is mono-regular. Actually, every monomorphism is an effective monomorphism. Moreover, monomorphisms are stable under filtered colimits and pushouts. ::: ::: Proof -The first statement is a formal consequence of the fact that every monomorphism in $\Set$ is effective and the already established facts that monomorphisms and pushouts can be understood objectwise. For similar reasons, the second statement is a formal consequence of the corresponding fact for $\Set$. +The first statement is a formal consequence of the fact that every monomorphism in $\Set$ is effective and the already established facts that monomorphisms and pushouts can be understood objectwise. For similar reasons, the second statement is a formal consequence of the corresponding facts for $\Set$. ::: ::: Lemma 7 @@ -181,7 +181,7 @@ is a weakly terminal essentially small collection in $\int E$, which is equivale $$\textstyle \coprod_{A \in K,\, a \in E(A)} \Hom(-,A) \to E$$ is an epimorphism of presheaves, as required. -Let $(X,x)$ be an object of $\int E$, i.e. $X \in \Ob(\C)$ and $x \in E(X)$. In particular, $x \in P(X)$. Thus the comma category $(X,x) \downarrow \K$ is connected, and therefore non-empty. Choose an object $f : (X,x) \to (A,a)$. Thus, $A \in K$, $a \in P(A)$, and $f : X \to A$ satisfies $f^*(a)=x$. If $a \in E(A)$, we are done. Assume otherwise and, without loss of generality, $a \in F_1(A)$. Let $b \in F_2(A) \subseteq P(A)$ be the corresponding element in the other copy of $F$. Using the flip automorphism of $P$ that fixes $E$ and exchanges $F_1$ and $F_2$, we see that $f^*(b)=x$. Thus, we also have a morphism $f' : (X,x) \to (A,b)$ with the same underlying morphism $f : X \to A$. +Let $(X,x)$ be an object of $\int E$, i.e. $X \in \Ob(\C)$ and $x \in E(X)$. In particular, $x \in P(X)$. Thus the comma category $(X,x) \downarrow \K$ is connected, and therefore non-empty. Choose an object $f : (X,x) \to (A,a)$. Thus, $A \in K$, $a \in P(A)$, and $f : X \to A$ satisfies $f^_(a)=x$. If $a \in E(A)$, we are done. Assume otherwise and, without loss of generality, $a \in F_1(A)$. Let $b \in F_2(A) \subseteq P(A)$ be the corresponding element in the other copy of $F$. Using the flip automorphism of $P$ that fixes $E$ and exchanges $F_1$ and $F_2$, we see that $f^_(b)=x$. Thus, we also have a morphism $f' : (X,x) \to (A,b)$ with the same underlying morphism $f : X \to A$. Since $(X,x) \downarrow \K$ is connected, the two morphisms $f$ and $f'$ are connected to each other. Thus, there are morphisms $(X,x) \to (A_i,a_i)$ with $A_i \in K$, $a_i \in P(A_i)$, starting with $f$ and ending with $f'$, such that for each pair of adjacent indices $i,i+1$, there is a morphism $(A_i,a_i) \to (A_{i+1},a_{i+1})$ or a morphism $(A_{i+1},a_{i+1}) \to (A_i,a_i)$. If any $a_i$ is contained in $E(A_i)$, we would be done. Assume, for a contradiction, that this is not the case. diff --git a/database/data/categories/SeqSet_conn.yaml b/database/data/categories/SeqSet_conn.yaml index 8aa9b664e..9032ba06f 100644 --- a/database/data/categories/SeqSet_conn.yaml +++ b/database/data/categories/SeqSet_conn.yaml @@ -37,6 +37,9 @@ satisfied_properties: - property: exact filtered colimits proof: Since the subcategory of connected sequences is closed under filtered colimits and finite limits, this follows from the corresponding property of the category of sequences of sets. + - property: pushout-stable regular monomorphisms + proof: Based on the pointwise descriptions of regular monomorphisms and pushouts, this follows from the corresponding property of $\Set$. + - property: regular proof: We already know that the category has finite limits and coequalizers, and that the inclusion functor into the regular category of sequences of sets is fully faithful and preserves finite limits and coequalizers. Thus, the claim follows from Lemma 7 here. diff --git a/database/data/categories/Set_family_mostly_1.yaml b/database/data/categories/Set_family_mostly_1.yaml index f44224039..ce8c631bc 100644 --- a/database/data/categories/Set_family_mostly_1.yaml +++ b/database/data/categories/Set_family_mostly_1.yaml @@ -43,6 +43,9 @@ satisfied_properties: - property: mono-regular proof: We claim that every monomorphism $X \to Y$ is the equalizer of its cokernel pair $Y \rightrightarrows Y \sqcup_X Y$. This is because every component $X_i \to Y_i$ is injective (see the classification of monomorphisms below), the statement holds in $\Set$, and equalizers and pushouts are constructed pointwise. + - property: pushout-stable regular monomorphisms + proof: Based on the pointwise descriptions of regular monomorphisms and pushouts, this follows from the corresponding property of $\Set$. + - property: well-copowered proof: The epimorphisms $X \to Y$ are precisely the morphisms that are pointwise surjective (see below). If $X_i \to Y_i$ is surjective and $X_i \cong 1$, then also $Y_i \cong 1$. It follows that the collection $\Quot(X) \cong \prod_{i \in S(X)} \Quot(X_i)$ is essentially small. diff --git a/database/data/categories/cocompletion-discrete-pair-join.yaml b/database/data/categories/cocompletion-discrete-pair-join.yaml index 7f5e86e96..48ee7d352 100644 --- a/database/data/categories/cocompletion-discrete-pair-join.yaml +++ b/database/data/categories/cocompletion-discrete-pair-join.yaml @@ -55,6 +55,9 @@ satisfied_properties: - property: filtered-colimit-stable monomorphisms proof: This holds for the free cocompletion of every locally small category. See Lemma 6 here. + - property: pushout-stable regular monomorphisms + proof: This holds for the free cocompletion of every locally small category. See Lemma 6 here. + - property: infinitary extensive proof: This holds for the free cocompletion of every locally small category. See Lemma 7 here.