diff --git a/databases/catdat/data/functor-implications/limits preservation.yaml b/databases/catdat/data/functor-implications/limits preservation.yaml index d282cf79..eb8aa8ea 100644 --- a/databases/catdat/data/functor-implications/limits preservation.yaml +++ b/databases/catdat/data/functor-implications/limits preservation.yaml @@ -115,11 +115,12 @@ proof: This is standard, see Mac Lane, 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 nLab, $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 diff --git a/databases/catdat/data/functor-properties/preserves epimorphisms.yaml b/databases/catdat/data/functor-properties/preserves epimorphisms.yaml index ae8cc453..de32af58 100644 --- a/databases/catdat/data/functor-properties/preserves epimorphisms.yaml +++ b/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 diff --git a/databases/catdat/data/functor-properties/preserves monomorphisms.yaml b/databases/catdat/data/functor-properties/preserves monomorphisms.yaml index 177ead44..f4e6f6e4 100644 --- a/databases/catdat/data/functor-properties/preserves monomorphisms.yaml +++ b/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 diff --git a/databases/catdat/data/functor-properties/preserves regular epimorphisms.yaml b/databases/catdat/data/functor-properties/preserves regular epimorphisms.yaml new file mode 100644 index 00000000..bfc7b265 --- /dev/null +++ b/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$ preserves regular epimorphisms 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 diff --git a/databases/catdat/data/functor-properties/preserves regular monomorphisms.yaml b/databases/catdat/data/functor-properties/preserves regular monomorphisms.yaml new file mode 100644 index 00000000..8bdec318 --- /dev/null +++ b/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$ preserves regular monomorphisms 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 diff --git a/databases/catdat/data/functors/binary_product_sets.yaml b/databases/catdat/data/functors/binary_product_sets.yaml index 2cccb01f..f8fc6c8b 100644 --- a/databases/catdat/data/functors/binary_product_sets.yaml +++ b/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))$. diff --git a/databases/catdat/data/functors/continuous-functions.yaml b/databases/catdat/data/functors/continuous-functions.yaml index 2deb28e8..38164a88 100644 --- a/databases/catdat/data/functors/continuous-functions.yaml +++ b/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: >- diff --git a/databases/catdat/data/functors/enveloping_group.yaml b/databases/catdat/data/functors/enveloping_group.yaml index 05451be8..9e40ab45 100644 --- a/databases/catdat/data/functors/enveloping_group.yaml +++ b/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: >- diff --git a/databases/catdat/data/functors/forget_group.yaml b/databases/catdat/data/functors/forget_group.yaml index 421591c3..eee9daf3 100644 --- a/databases/catdat/data/functors/forget_group.yaml +++ b/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 $\Grp$ and in $\Set$. - - property: preserves reflexive coequalizers proof: This follows from Theorem 2.5 at the nLab. diff --git a/databases/catdat/data/functors/forget_group_pointed.yaml b/databases/catdat/data/functors/forget_group_pointed.yaml index 1ef1628f..6beedf93 100644 --- a/databases/catdat/data/functors/forget_group_pointed.yaml +++ b/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 nLab.' - - property: preserves epimorphisms - proof: This follows from the classifications of epimorphisms in $\Grp$ and in $\Set_*$. - - 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$. diff --git a/databases/catdat/data/functors/forget_vector.yaml b/databases/catdat/data/functors/forget_vector.yaml index 1529c997..74d62b1e 100644 --- a/databases/catdat/data/functors/forget_vector.yaml +++ b/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 $\Vect$ and in $\Set$. - - property: preserves reflexive coequalizers proof: This follows from Theorem 2.5 at the nLab. diff --git a/databases/catdat/data/functors/free_group.yaml b/databases/catdat/data/functors/free_group.yaml index c5abe7bb..caa41cef 100644 --- a/databases/catdat/data/functors/free_group.yaml +++ b/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)$.' diff --git a/databases/catdat/data/functors/group_units.yaml b/databases/catdat/data/functors/group_units.yaml index 8a7d05ae..7ecd7a6c 100644 --- a/databases/catdat/data/functors/group_units.yaml +++ b/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.' diff --git a/databases/catdat/data/functors/pi_0.yaml b/databases/catdat/data/functors/pi_0.yaml index 96e33cc8..2954f5c3 100644 --- a/databases/catdat/data/functors/pi_0.yaml +++ b/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 diff --git a/databases/catdat/data/functors/pi_1.yaml b/databases/catdat/data/functors/pi_1.yaml index be68e2b6..6ff61a9d 100644 --- a/databases/catdat/data/functors/pi_1.yaml +++ b/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 $\Top_*$, 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 MSE/3991443 or MSE/2788471 for counterexamples. See MSE/4625240 for conditions which binary products are preserved. diff --git a/databases/catdat/data/functors/power_set_contravariant.yaml b/databases/catdat/data/functors/power_set_contravariant.yaml index 86882ad2..2a164740 100644 --- a/databases/catdat/data/functors/power_set_contravariant.yaml +++ b/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. diff --git a/databases/catdat/data/functors/power_set_covariant.yaml b/databases/catdat/data/functors/power_set_covariant.yaml index 02d6cfbe..26e464b7 100644 --- a/databases/catdat/data/functors/power_set_covariant.yaml +++ b/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$.' diff --git a/databases/catdat/data/functors/squaring_sets.yaml b/databases/catdat/data/functors/squaring_sets.yaml index ede7392b..25d0906e 100644 --- a/databases/catdat/data/functors/squaring_sets.yaml +++ b/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)$. diff --git a/databases/catdat/scripts/expected-data/forget_vector.json b/databases/catdat/scripts/expected-data/forget_vector.json index 863f1eb4..bf3952fe 100644 --- a/databases/catdat/scripts/expected-data/forget_vector.json +++ b/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 } diff --git a/databases/catdat/scripts/expected-data/id_Set.json b/databases/catdat/scripts/expected-data/id_Set.json index 3a5032ff..bda5a5f9 100644 --- a/databases/catdat/scripts/expected-data/id_Set.json +++ b/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 } diff --git a/databases/catdat/scripts/utils/implications.ts b/databases/catdat/scripts/utils/implications.ts index 87d7f9e9..472270e4 100644 --- a/databases/catdat/scripts/utils/implications.ts +++ b/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 this result`