Add functor properties: preserve regular epis / monos

databases/catdat/data/functor-implications/limits preservation.yaml

@@ -115,11 +115,12 @@
   proof: This is standard, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. V, Theorem 4.1.
   is_equivalence: false
 
-- id: equalizers_include_coreflexive_equalizers
+- id: equalizers_preservation_consequences
   assumptions:
     - preserves equalizers
   conclusions:
     - preserves coreflexive equalizers
+    - preserves regular monomorphisms
   proof: This is trivial.
   is_equivalence: false
 
@@ -137,13 +138,35 @@
 
 - id: mono-preserving_criterion
   assumptions:
-    - preserves equalizers
+    - preserves regular monomorphisms
   mapped_assumptions:
     source:
       - mono-regular
   conclusions:
     - preserves monomorphisms
-  proof: Any monomorphism in the domain is a regular monomorphism and is mapped to a regular monomorphism.
+  proof: This is trivial.
+  is_equivalence: false
+
+- id: regular-mono-preserving_criterion
+  assumptions:
+    - preserves monomorphisms
+  mapped_assumptions:
+    target:
+      - mono-regular
+  conclusions:
+    - preserves regular monomorphisms
+  proof: This is trivial.
+  is_equivalence: false
+
+- id: another_regular-mono-preserving_criterion
+  assumptions:
+    - preserves coreflexive equalizers
+  mapped_assumptions:
+    source:
+      - pushouts
+  conclusions:
+    - preserves regular monomorphisms
+  proof: 'Let $F : \C \to \D$ be a functor preserving coreflexive equalizers, where $\C$ has pushouts; we only need that $\C$ has cokernel pairs. Let $i : X \to Y$ be a regular monomorphism in $\C$. By Prop. 3.2 at the <a href="https://ncatlab.org/nlab/show/regular+epimorphism#MorphismsWithKernelPairsAreRegularIffEffective" target="_blank">nLab</a>, $i$ is the equalizer of the two canonical morphisms $u_1,u_2 : Y \rightrightarrows Y \sqcup_X Y$ into the cokernel pair of $i$. By the universal property of the pushout, there is a morphism $\nabla : Y \sqcup_X Y \to Y$ with $\nabla u_1 = \nabla u_2 = \id_Y$. Thus, $u_1,u_2$ is a coreflexive pair. Since $F$ preserves coreflexive equalizers by assumption, $F(i)$ is the equalizer of $F(u_1), F(u_2)$. In particular, $F(i)$ is a regular monomorphism.'
   is_equivalence: false
 
 - id: zero_preserving_condition

databases/catdat/data/functor-properties/preserves epimorphisms.yaml

@@ -8,6 +8,7 @@ invariant_under_equivalences: true
 dual_property: preserves monomorphisms
 related_properties:
   - right exact
+  - preserves regular epimorphisms
 
 tags:
   - morphism behavior

databases/catdat/data/functor-properties/preserves monomorphisms.yaml

@@ -8,6 +8,7 @@ invariant_under_equivalences: true
 dual_property: preserves epimorphisms
 related_properties:
   - left exact
+  - preserves regular monomorphisms
 
 tags:
   - morphism behavior

databases/catdat/data/functor-properties/preserves regular epimorphisms.yaml

@@ -0,0 +1,13 @@
+id: preserves regular epimorphisms
+relation: ''
+description: 'A functor $F : \C \to \D$ <i>preserves regular epimorphisms</i> if every regular epimorphism in $\C$ is mapped to a regular epimorphism in $\D$.'
+nlab_link: https://ncatlab.org/nlab/show/regular+epimorphism
+invariant_under_equivalences: true
+dual_property: preserves regular monomorphisms
+related_properties:
+  - preserves epimorphisms
+  - right exact
+  - preserves coequalizers
+
+tags:
+  - morphism behavior

databases/catdat/data/functor-properties/preserves regular monomorphisms.yaml

@@ -0,0 +1,13 @@
+id: preserves regular monomorphisms
+relation: ''
+description: 'A functor $F : \C \to \D$ <i>preserves regular monomorphisms</i> if every regular monomorphism in $\C$ is mapped to a regular monomorphism in $\D$.'
+nlab_link: https://ncatlab.org/nlab/show/regular+monomorphism
+invariant_under_equivalences: true
+dual_property: preserves regular epimorphisms
+related_properties:
+  - preserves monomorphisms
+  - left exact
+  - preserves equalizers
+
+tags:
+  - morphism behavior

databases/catdat/data/functors/binary_product_sets.yaml

@@ -21,9 +21,6 @@ satisfied_properties:
   - property: preserves initial objects
     proof: This is obvious.
 
-  - property: preserves epimorphisms
-    proof: This follows easily from the description of epimorphisms in $\Set$ as surjective maps.
-
   - property: representable
     proof: We have $X \times Y \cong \Hom_{\Set \times \Set}((1,1),(X,Y))$.
 

databases/catdat/data/functors/continuous-functions.yaml

@@ -39,11 +39,11 @@ unsatisfied_properties:
   - property: preserves finite coproducts
     proof: 'The canonical homomorphism $C(X) \otimes_{\IR} C(Y) \to C(X \times Y)$ need not be surjective. For example, for $X = Y = \IR$ one can show that $(x,y) \mapsto \exp(xy)$ is not contained in its image.'
 
-  - property: preserves reflexive coequalizers
-    proof: 'Let $i : U \hookrightarrow X$ be an open embedding such that there exists a continuous function on $U$ that does not extend to $X$; for example, $i : \IR \setminus \{0\} \hookrightarrow \IR$ together with the continuous function $x \mapsto x^{-1}$. Then $i$ is the equalizer of the two inclusions $X \rightrightarrows X +_U X$, which have common retraction $\nabla : X +_U X \to X$. But $i^* : C(X) \to C(U)$ is not a coequalizer in $\CAlg(\IR)$, since it is not surjective.'
+  - property: preserves regular epimorphisms
+    proof: 'The embedding $i : \IR \setminus \{0\} \hookrightarrow \IR$ is a regular monomorphism in $\Top$, i.e. a regular epimorphism in $\Top^{\op}$. It is mapped to the restriction map $i^* : C(\IR) \to C(\IR \setminus \{0\})$, which is not surjective, as witnessed by the map $x \mapsto x^{-1}$. Hence, $i^*$ is not a regular epimorphism.'
 
   - property: preserves epimorphisms
-    proof: 'If $i : X \to Y$ is an injective continuous map, the induced homomorphism $C(Y) \to C(X)$ need not be surjective (consider the inclusion $i : \IR \setminus \{0\} \hookrightarrow \IR$ and the map $x \mapsto x^{-1}$). However, we need an example where it is not even an epimorphism in $\CAlg(\IR)$. A simple counterexample can again be constructed using (in)discrete spaces. Namely, if $X$ is any finite set with at least two elements, we have a continuous bijection $D(X) \to I(X)$, $x \mapsto x$, where $D(X)$ (resp. $I(X)$) denotes the discrete (resp. indiscrete) space on $X$. It induces the algebra homomorphism $\IR \cong C(I(X)) \to C(D(X)) \cong \IR^X$, which is not an epimorphism since $\IR^X \otimes_\IR \IR^X \not\cong \IR^X$.'
+    proof: 'It is not sufficient to find an injective continuous map $i : X \to Y$ such that $i^* : C(Y) \to C(X)$ is not surjective, since epimorphisms in $\CAlg(\IR)$ do not need to be surjective. But a simple counterexample can again be constructed using (in)discrete spaces. Namely, if $X$ is any finite set with at least two elements, we have a continuous bijection $D(X) \to I(X)$, $x \mapsto x$, where $D(X)$ (resp. $I(X)$) denotes the discrete (resp. indiscrete) space on $X$. It induces the algebra homomorphism $\IR \cong C(I(X)) \to C(D(X)) \cong \IR^X$, which is not an epimorphism since $\IR^X \otimes_\IR \IR^X \not\cong \IR^X$.'
 
   - property: finitary
     proof: >-

databases/catdat/data/functors/enveloping_group.yaml

@@ -41,8 +41,8 @@ unsatisfied_properties:
   - property: full
     proof: 'We have $F(\IN) = \IZ$ (w.r.t. addition). The homomorphism $\IZ \to \IZ$, $x \mapsto -x$ is not induced by a homomorphism $\IN \to \IN$.'
 
-  - property: preserves monomorphisms
-    proof: 'Consider the monoid $N = \langle a,b,c : ab = ac \rangle_{\Mon}$ and the free monoid $M = \langle b,c \rangle_{\Mon}$. The canonical homomorphism $M \to N$ is injective. However, $F(M) = \langle b,c \rangle_{\Grp}$ (free group), and $b,c$ become identified in $F(N) \cong \langle a,b,c : b = c \rangle_{\Grp}$ since we may cancel $a$, so that $F(M) \to F(N)$ is not injective.'
+  - property: preserves regular monomorphisms
+    proof: 'Consider the monoid $N = \langle a,b,c : ab = ac \rangle_{\Mon}$ and the free monoid $M = \langle b,c \rangle_{\Mon}$. The canonical homomorphism $M \to N$ is injective. It is also the equalizer of the two natural maps from $N$ into $\langle a_1,a_2,b,c : a_1 b = a_1 c, \, a_2 b = a_2 c \rangle_{\Mon}$. However, $F(M) = \langle b,c \rangle_{\Grp}$ (free group), and $b,c$ become identified in $F(N) \cong \langle a,b,c : b = c \rangle_{\Grp}$ since we may cancel $a$, so that $F(M) \to F(N)$ is not injective.'
 
   - property: preserves products
     proof: >-

databases/catdat/data/functors/forget_group.yaml

@@ -27,9 +27,6 @@ satisfied_properties:
   - property: finitary
     proof: For every algebraic category the forgetful functor to the category of sets preserves filtered colimits.
 
-  - property: preserves epimorphisms
-    proof: This follows from the classifications of epimorphisms in <a href="/category/Grp">$\Grp$</a> and in <a href="/category/Set">$\Set$</a>.
-
   - property: preserves reflexive coequalizers
     proof: This follows from Theorem 2.5 at the <a href="https://ncatlab.org/nlab/show/reflexive+coequalizer" target="_blank">nLab</a>.
 

databases/catdat/data/functors/forget_group_pointed.yaml

@@ -27,9 +27,6 @@ satisfied_properties:
   - property: preserves reflexive coequalizers
     proof: 'It suffices to prove that $U_{\Grp} : \Grp \to \Set$ preserves them, which follows from Theorem 2.5 at the <a href="https://ncatlab.org/nlab/show/reflexive+coequalizer" target="_blank">nLab</a>.'
 
-  - property: preserves epimorphisms
-    proof: This follows from the classifications of epimorphisms in <a href="/category/Grp">$\Grp$</a> and in <a href="/category/Set_*">$\Set_*$</a>.
-
   - property: essentially surjective
     proof: Let $(X,x_0)$ be a pointed set. If $X$ is finite, we can endow $X$ with a cyclic group structure in which $x_0$ is the identity element. If $X$ is infinite, there is a bijection between $X$ and the set $P_{<\aleph_0}(X)$ of finite subsets of $X$, and we may assume that $x_0$ is mapped to $\varnothing$. Since $P_{<\aleph_0}(X)$ carries a group structure with identity element $\varnothing$ (it is the underlying set of the vector space $\IF_2^{\oplus X}$), $X$ also carries a group structure with identity element $x_0$.
 

databases/catdat/data/functors/forget_vector.yaml

@@ -24,9 +24,6 @@ satisfied_properties:
   - property: finitary
     proof: For every algebraic category the forgetful functor to the category of sets preserves filtered colimits.
 
-  - property: preserves epimorphisms
-    proof: This follows from the classifications of epimorphisms in <a href="/category/Vect">$\Vect$</a> and in <a href="/category/Set">$\Set$</a>.
-
   - property: preserves reflexive coequalizers
     proof: This follows from Theorem 2.5 at the <a href="https://ncatlab.org/nlab/show/reflexive+coequalizer" target="_blank">nLab</a>.
 

databases/catdat/data/functors/free_group.yaml

@@ -23,6 +23,7 @@ satisfied_properties:
 
   - property: preserves monomorphisms
     proof: 'This can be deduced from the description of the elements of a free group, but here is an abstract argument: Split monomorphisms are preserved by any functor. The only injective maps in $\Set$ that are not split are $\varnothing \hookrightarrow X$ (for non-empty $X$), and $F(\varnothing) \to F(X)$ is injective since $F(\varnothing)$ is the trivial group.'
+    check_redundancy: false
 
   - property: preserves coreflexive equalizers
     proof: 'More generally, if $f,g : X \rightrightarrows Y$ are two injective maps with equalizer $E \hookrightarrow X$, then $F(E) \to F(X)$ is the equalizer of $F(f),F(g) : F(X) \rightrightarrows F(Y)$. In fact, we already know that $F(E) \to F(X)$ is injective. Now let $w \in F(X)$ be an element, and write it as a reduced word $w = x_1^{k_1} \cdots x_n^{k_n}$, meaning $x_i \in X$, $x_i \neq x_{i+1}$, $k_i \in \IZ \setminus \{0\}$. Since $f$ is injective, also $f(w) = f(x_1)^{k_1} \cdots f(x_n)^{k_n}$ is a reduced word. The same is true for $g(w)$. Hence, $f(w)=g(w)$ implies $f(x_i)=g(x_i)$ for every $i$, i.e. $x_i \in E$. Therefore, $w \in F(E)$.'

databases/catdat/data/functors/group_units.yaml

@@ -45,5 +45,5 @@ unsatisfied_properties:
   - property: full
     proof: Let $M$ be a monoid and $G \subseteq M$ be its group of units. Then the identity $M^{\times} \to G^{\times} = G$ is in the image of the functor iff there is a homomorphism $M \to G$ that extends the identity on $G$, i.e. a retraction of $G \subseteq M$. If $M$ has an absorbing element, then its image in $G$ would be an absorbing element, forcing $G$ to be trivial. However, the monoid $(\IZ,\cdot,1)$, for example, has an absorbing element and a non-trivial group of units $\{\pm 1\}$.
 
-  - property: preserves epimorphisms
-    proof: The inclusion $\IN \hookrightarrow \IZ$ is an epimorphism of monoids. It is mapped to the trivial homomorphism $\{0\} \hookrightarrow \IZ$, which is not an epimorphism of groups.
+  - property: preserves regular epimorphisms
+    proof: 'Consider the monoids $M = \langle x : x^3 = x \rangle$ and $N = \langle y : y^2 = 1 \rangle$. Thus, $M$ has order $3$ and consists of $1,x,x^2$, and $N$ has order $2$ (and is even a group) with the elements $1,y$. We have a unique homomorphism $f : M \to N$ defined by $f(x)=y$, which is surjective. Since $M^{\times}$ is trivial and $N^{\times} \cong N$, the induced map $f^{\times} : M^{\times} \to N^{\times}$ is not surjective.'

databases/catdat/data/functors/pi_0.yaml

@@ -39,7 +39,7 @@ unsatisfied_properties:
   - property: essentially injective
     proof: We have $\pi_0(\{\ast\}) \cong \pi_0([0,1])$, but $\{\ast\} \not\cong [0,1]$.
 
-  - property: preserves monomorphisms
+  - property: preserves regular monomorphisms
     proof: The functor $\pi_0$ maps the embedding $\{0,1\} \hookrightarrow [0,1]$ to the (unique) map $\{\{0\},\{1\}\} \to \{[0,1]\}$, which is not injective.
 
   - property: cofinitary

databases/catdat/data/functors/pi_1.yaml

@@ -32,14 +32,11 @@ unsatisfied_properties:
   - property: essentially injective
     proof: We have $\pi_1(\{0\},0) \cong \pi_1([0,1],0)$ (both groups are trivial), but $(\{0\},0) \not\cong ([0,1],0)$.
 
-  - property: preserves monomorphisms
+  - property: preserves regular monomorphisms
     proof: The functor $\pi_1$ maps the embedding $(S^1,1) \hookrightarrow (\IC,1)$ to the trivial group homomorphism $\IZ \to \{1\}$, which is not injective.
 
-  - property: preserves epimorphisms
-    proof: The functor $\pi_1$ maps the epimorphism $(\IR,0) \to (S^1,1)$, $t \mapsto e^{2 \pi i t}$, to the trivial group homomorphism $\{1\} \to \IZ$, which is not surjective.
-
-  - property: preserves reflexive coequalizers
-    proof: 'The previous counterexample of an epimorphism $f : (\IR,0) \to (S^1,1)$ that is not preserved by $\pi_1$ is actually an open map and hence a regular epimorphism, and in <a href="/category/Top_*">$\Top_*$</a>, every regular epimorphism $f : X \to Y$ is the coequalizer of the reflexive pair $p_1,p_2 : X \times_Y X \rightrightarrows Y$.'
+  - property: preserves regular epimorphisms
+    proof: The functor $\pi_1$ maps the regular epimorphism $(\IR,0) \to (S^1,1)$, $t \mapsto e^{2 \pi i t}$, to the trivial group homomorphism $\{1\} \to \IZ$, which is not surjective.
 
   - property: preserves binary coproducts
     proof: See <a href="https://math.stackexchange.com/questions/3991443" target="_blank">MSE/3991443</a> or <a href="https://math.stackexchange.com/questions/2788471" target="_blank">MSE/2788471</a> for counterexamples. See <a href="https://math.stackexchange.com/questions/4625240" target="_blank">MSE/4625240</a> for conditions which binary products are preserved.

databases/catdat/data/functors/power_set_contravariant.yaml

@@ -16,9 +16,6 @@ satisfied_properties:
   - property: representable
     proof: This is because there are natural bijections $P(X) \cong \Hom(X,2)$, sending a subset to its characteristic function.
 
-  - property: preserves epimorphisms
-    proof: 'If $f : X \to Y$ is injective, then $f^* : P(Y) \to P(X)$ is surjective, since for all $A \subseteq X$ we have $A = f^*(f_*(A))$.'
-
   - property: conservative
     proof: >-
       Assume that $f : X \to Y$ is a map such that $f^* : P(Y) \to P(X)$ is bijective. For $y \in Y$ it follows that $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, which means that $y$ has an $f$-preimage. That is, $f$ is surjective.

databases/catdat/data/functors/power_set_covariant.yaml

@@ -21,6 +21,7 @@ satisfied_properties:
 
   - property: preserves monomorphisms
     proof: 'If $f : X \to Y$ is injective, then $f^* \circ f_* = \id_{P(X)}$, so that $f_*$ is injective.'
+    check_redundancy: false
 
   - property: conservative
     proof: 'Assume that $f : X \to Y$ is a map such that $f_* : P(X) \to P(Y)$ is an isomorphism. There is some $A \subseteq X$ with $Y = f_*(A)$, this proves that $f$ is surjective. It is also injective: If $x,y \in X$ satisfy $f(x) = f(y)$, then $f_*(\{x\}) = f_*(\{y\})$, and hence $\{x\} = \{y\}$, i.e. $x = y$.'

databases/catdat/data/functors/squaring_sets.yaml

@@ -19,9 +19,6 @@ satisfied_properties:
   - property: preserves initial objects
     proof: This is obvious.
 
-  - property: preserves epimorphisms
-    proof: This follows easily from the fact that epimorphisms in $\Set$ are surjective functions.
-
   - property: representable
     proof: We have $X^2 \cong \Hom(\{1,2\},X)$.
 

databases/catdat/scripts/expected-data/forget_vector.json

@@ -40,5 +40,7 @@
 	"right adjoint": true,
 	"preserves terminal objects": true,
 	"preserves reflexive coequalizers": true,
-	"preserves coreflexive equalizers": true
+	"preserves coreflexive equalizers": true,
+	"preserves regular monomorphisms": true,
+	"preserves regular epimorphisms": true
 }

databases/catdat/scripts/expected-data/id_Set.json

@@ -39,5 +39,7 @@
 	"full on isomorphisms": true,
 	"pseudomonic": true,
 	"dominant": true,
-	"isomorphism": true
+	"isomorphism": true,
+	"preserves regular monomorphisms": true,
+	"preserves regular epimorphisms": true
 }

databases/catdat/scripts/utils/implications.ts

@@ -143,7 +143,8 @@ export function get_contradiction_string(
 	const assumption_string = get_assumption_string(implication, properties_dict, true)
 	const conclusion_string = get_conclusion_string(implication, properties_dict, true)
 
-	const has_multiple_assumptions = implication.assumptions.size > 1
+	const has_multiple_assumptions =
+		implication.assumptions.size > 1 || !!implication.mapped_assumptions
 
 	const ref = `by <a href="/${type}-implication/${implication.id}">this result</a>`