diff --git a/.cspell.json b/.cspell.json index 302147ec..d060b9b6 100644 --- a/.cspell.json +++ b/.cspell.json @@ -21,6 +21,7 @@ "words": [ "abelian", "abelianization", + "abelianizations", "abelianize", "Adamek", "adic", @@ -122,6 +123,7 @@ "dualizable", "Dualization", "Duskin", + "Easton", "Eilenberg", "endofunctors", "Engelking", @@ -145,6 +147,7 @@ "groupoid", "groupoids", "Haus", + "Hertweck", "Heyting", "homotopy", "HuĊĦek", diff --git a/databases/catdat/data/functor-implications/equivalences.yaml b/databases/catdat/data/functor-implications/equivalences.yaml index 27b770b0..d504ef34 100644 --- a/databases/catdat/data/functor-implications/equivalences.yaml +++ b/databases/catdat/data/functor-implications/equivalences.yaml @@ -17,5 +17,6 @@ target_assumptions: [] conclusions: - monadic + - left-invertible proof: This is easy. is_equivalence: false diff --git a/databases/catdat/data/functor-implications/misc.yaml b/databases/catdat/data/functor-implications/misc.yaml index 3b714006..068a10ea 100644 --- a/databases/catdat/data/functor-implications/misc.yaml +++ b/databases/catdat/data/functor-implications/misc.yaml @@ -20,3 +20,26 @@ - conservative proof: If $F(f)$ is an isomorphism, its inverse has the form $F(g)$ since $F$ is full. Since $F$ is faithful, it follows that $f$ is inverse to $g$. is_equivalence: false + +- id: reflects_isomorphism_criterion + assumptions: + - full + - conservative + conclusions: + - essentially injective + source_assumptions: [] + target_assumptions: [] + proof: 'The functor even lifts isomorphisms: If $F(A) \to F(B)$ is an isomorphism, then it is induced by a morphism $A \to B$ since $F$ is full. Moreover, $A \to B$ is an isomorphism since its $F$-image is an isomorphism and $F$ is conservative.' + is_equivalence: false + +- id: left-invertible_consequences + assumptions: + - left-invertible + conclusions: + - faithful + - essentially injective + - conservative + source_assumptions: [] + target_assumptions: [] + proof: 'Let $G : \D \to \C$ be a left-inverse to $F : \C \to \D$, meaning that $G \circ F \cong \id_{\C}$. Then $F(A) \cong F(B)$ implies $A \cong G(F(A)) \cong G(F(B)) \cong B$ for all $A,B \in \C$. Thus, $F$ essentially injective. Moreover, since $G \circ F$ is faithful, the composed map $\Hom(A,B) \to \Hom(F(A),F(B)) \to \Hom(G(F(A)),G(F(B))$ is injective, so that also $\Hom(A,B) \to \Hom(F(A),F(B))$ is injective. This shows that $F$ is faithful. Finally, if $f : A \to B$ is am morphism such that $F(f)$ is an isomorphism, then $G(F(f))$ is an isomorphism. Since $G(F(f)) \cong f$ in $\Mor(\C)$, we conclude that $f$ is an isomorphism. Therefore, $F$ is conservative.' + is_equivalence: false diff --git a/databases/catdat/data/functor-properties/conservative.yaml b/databases/catdat/data/functor-properties/conservative.yaml index b1755d7f..a8d69ee7 100644 --- a/databases/catdat/data/functor-properties/conservative.yaml +++ b/databases/catdat/data/functor-properties/conservative.yaml @@ -6,3 +6,4 @@ invariant_under_equivalences: true dual_property: conservative related_properties: - equivalence + - essentially injective diff --git a/databases/catdat/data/functor-properties/equivalence.yaml b/databases/catdat/data/functor-properties/equivalence.yaml index 273909a7..4d3f4d2b 100644 --- a/databases/catdat/data/functor-properties/equivalence.yaml +++ b/databases/catdat/data/functor-properties/equivalence.yaml @@ -10,3 +10,4 @@ related_properties: - essentially surjective - continuous - cocontinuous + - left-invertible diff --git a/databases/catdat/data/functor-properties/essentially injective.yaml b/databases/catdat/data/functor-properties/essentially injective.yaml new file mode 100644 index 00000000..1510d5c2 --- /dev/null +++ b/databases/catdat/data/functor-properties/essentially injective.yaml @@ -0,0 +1,14 @@ +id: essentially injective +relation: 'is' +description: >- + A functor $F : \C \to \D$ is essentially injective if the implication + $$F(A) \cong F(B) \implies A \cong B$$ + holds for all objects $A,B \in \C$. This is a condition solely on the objects themselves. It is not required that every isomorphism between $F(A)$ and $F(B)$ lifts to an isomorphism between $A$ and $B$. An equivalent condition is that $F$ induces an injective map on isomorphism classes. +nlab_link: https://ncatlab.org/nlab/show/essentially+injective+functor +invariant_under_equivalences: true +dual_property: essentially injective +related_properties: + - conservative + - faithful + - full + - essentially surjective diff --git a/databases/catdat/data/functor-properties/essentially surjective.yaml b/databases/catdat/data/functor-properties/essentially surjective.yaml index 4758d739..73a4f99c 100644 --- a/databases/catdat/data/functor-properties/essentially surjective.yaml +++ b/databases/catdat/data/functor-properties/essentially surjective.yaml @@ -6,3 +6,4 @@ invariant_under_equivalences: true dual_property: essentially surjective related_properties: - equivalence + - essentially injective diff --git a/databases/catdat/data/functor-properties/faithful.yaml b/databases/catdat/data/functor-properties/faithful.yaml index 8939812f..2dc054aa 100644 --- a/databases/catdat/data/functor-properties/faithful.yaml +++ b/databases/catdat/data/functor-properties/faithful.yaml @@ -1,9 +1,11 @@ id: faithful relation: is -description: 'A functor is faithful when it is injective on Hom-sets: If $F(f)=F(g)$, then $f=g$.' +description: 'A functor is faithful when it is injective on Hom-sets: If $F(f)=F(g)$ for two morphisms $f,g : A \rightrightarrows B$, then $f=g$.' nlab_link: https://ncatlab.org/nlab/show/faithful+functor invariant_under_equivalences: true dual_property: faithful related_properties: - equivalence - full + - essentially injective + - left-invertible diff --git a/databases/catdat/data/functor-properties/full.yaml b/databases/catdat/data/functor-properties/full.yaml index 1d5547fe..c7747d34 100644 --- a/databases/catdat/data/functor-properties/full.yaml +++ b/databases/catdat/data/functor-properties/full.yaml @@ -7,3 +7,4 @@ dual_property: full related_properties: - equivalence - faithful + - essentially injective diff --git a/databases/catdat/data/functor-properties/left-invertible.yaml b/databases/catdat/data/functor-properties/left-invertible.yaml new file mode 100644 index 00000000..081bb50d --- /dev/null +++ b/databases/catdat/data/functor-properties/left-invertible.yaml @@ -0,0 +1,10 @@ +id: left-invertible +relation: is +description: 'A left inverse of a functor $F : \C \to \D$ is a functor $G : \D \to \C$ satisfying $G \circ F \cong \id_{\C}$. We do not require $G \circ F = \id_{\C}$ here, which is often too strict. A functor is called left-invertible when it has a left inverse.' +nlab_link: https://ncatlab.org/nlab/show/inverse+functor +invariant_under_equivalences: true +dual_property: left-invertible +related_properties: + - equivalence + - faithful + - essentially injective diff --git a/databases/catdat/data/functors/abelianization.yaml b/databases/catdat/data/functors/abelianization.yaml index ab54c2b0..d6b54547 100644 --- a/databases/catdat/data/functors/abelianization.yaml +++ b/databases/catdat/data/functors/abelianization.yaml @@ -23,6 +23,9 @@ satisfied_properties: proof: See MO/386144. unsatisfied_properties: + - property: essentially injective + proof: The abelianizations of $S_3$ and $C_2$ are both isomorphic to $C_2$. + - property: faithful proof: Both the inclusion $A_3 \hookrightarrow S_3$ and the trivial homomorphism $A_3 \to S_3$ are mapped to the trivial homomorphism $A_3 \to 1$. diff --git a/databases/catdat/data/functors/continuous-functions.yaml b/databases/catdat/data/functors/continuous-functions.yaml index 3be7f3f9..1f348c56 100644 --- a/databases/catdat/data/functors/continuous-functions.yaml +++ b/databases/catdat/data/functors/continuous-functions.yaml @@ -19,11 +19,14 @@ satisfied_properties: proof: The initial object in $\Top^{\op}$ is the singleton space, which is mapped to $\IR$, the initial commutative $\IR$-algebra. unsatisfied_properties: + - property: essentially injective + proof: 'If $X,Y$ are non-empty indiscrete spaces, then $C(X) \cong \IR \cong C(Y)$ since every continuous function on $X$ resp. $Y$ is constant.' + - property: essentially surjective proof: The algebra $C(X)$ is reduced, whereas there exist non-reduced algebras such as $\IR[T]/\langle T^2 \rangle$. - - 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: faithful + proof: 'If $X,Y$ are non-empty indiscrete spaces, there is only one homomorphism of $\IR$-algebras $C(Y) \to C(X)$ (since both are isomorphic to $\IR$), but there can be many maps $X \to Y$.' - property: full proof: >- @@ -33,8 +36,8 @@ unsatisfied_properties: $$u(\beta) \coloneqq \begin{cases} 0 & \beta \leq \alpha \\ 1 & \beta > \alpha \end{cases}$$ satisfies $\varphi(u) = u(\alpha + 1) \neq u(\alpha)$. - - property: faithful - proof: 'If $X,Y$ are non-empty indiscrete spaces, there is only one homomorphism of $\IR$-algebras $C(Y) \to C(X)$ (since both are isomorphic to $\IR$), but there can be many maps $X \to Y$.' + - 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.' diff --git a/databases/catdat/data/functors/coproduct_sets.yaml b/databases/catdat/data/functors/coproduct_sets.yaml index 85b54ac0..e51c2c75 100644 --- a/databases/catdat/data/functors/coproduct_sets.yaml +++ b/databases/catdat/data/functors/coproduct_sets.yaml @@ -34,3 +34,6 @@ satisfied_properties: unsatisfied_properties: - property: preserves terminal objects proof: This is obvious. + + - property: essentially injective + proof: Both $(1,0)$ and $(0,1)$ are mapped to $1$. diff --git a/databases/catdat/data/functors/countable_copower_sets.yaml b/databases/catdat/data/functors/countable_copower_sets.yaml index 5e88a627..2c234fe7 100644 --- a/databases/catdat/data/functors/countable_copower_sets.yaml +++ b/databases/catdat/data/functors/countable_copower_sets.yaml @@ -28,11 +28,11 @@ satisfied_properties: proof: We have $\Hom(\IN \times X,Y) \cong \Hom(X,Y^{\IN})$. unsatisfied_properties: - - property: full - proof: If $X$ is non-empty, the map $\IN \times X \to \IN \times X$, $(n,x) \mapsto (n+1,x)$ is not induced by a map $X \to X$. - - property: preserves terminal objects proof: We have $\IN \times 1 \cong \IN \not\cong 1$. - property: essentially surjective proof: A non-empty finite set is not contained in the essential image. + + - property: essentially injective + proof: For any two non-empty finite sets $X,Y$ there is a bijection $\IN \times X \cong \IN \cong \IN \times Y$, so this does not imply $X \cong Y$. diff --git a/databases/catdat/data/functors/diagonal_sets.yaml b/databases/catdat/data/functors/diagonal_sets.yaml index a5d27176..f35bc6ae 100644 --- a/databases/catdat/data/functors/diagonal_sets.yaml +++ b/databases/catdat/data/functors/diagonal_sets.yaml @@ -14,7 +14,7 @@ related_functors: - id_Set satisfied_properties: - - property: conservative + - property: left-invertible proof: This follows from $p_1 \circ \Delta = \id_\Set$. - property: left adjoint diff --git a/databases/catdat/data/functors/discrete_topology.yaml b/databases/catdat/data/functors/discrete_topology.yaml index ac1af518..c58f9b30 100644 --- a/databases/catdat/data/functors/discrete_topology.yaml +++ b/databases/catdat/data/functors/discrete_topology.yaml @@ -16,10 +16,10 @@ satisfied_properties: - property: left adjoint proof: 'This functor is left adjoint to the forgetful functor $U_{\Top} : \Top \to \Set$.' - - property: full - proof: This is trivial. + - property: left-invertible + proof: The forgetful functor provides a left inverse. - - property: faithful + - property: full proof: This is trivial. - property: preserves finite products diff --git a/databases/catdat/data/functors/doubling_sets.yaml b/databases/catdat/data/functors/doubling_sets.yaml index b9a44356..b98cc2ea 100644 --- a/databases/catdat/data/functors/doubling_sets.yaml +++ b/databases/catdat/data/functors/doubling_sets.yaml @@ -27,6 +27,9 @@ satisfied_properties: - property: cofinitary proof: The doubling functor can also be written as $X \mapsto \{1,2\} \times X$, from which the claim follows. + - property: essentially injective + proof: Let $X,Y$ be two sets with $X + X \cong Y + Y$. If $X$ is finite, then $X + X$ and hence $Y + Y$ is finite, so that also $Y$ is finite. For the cardinalities we deduce $2 \card(X) = 2 \card(Y)$ and hence $\card(X) = \card(Y)$. This yields $X \cong Y$. If $X$ is infinite, then $Y$ is infinite, and $X \cong X + X \cong Y + Y \cong Y$. + unsatisfied_properties: - property: full proof: If $X$ is non-empty, the swap $2X \to 2X$ is not induced by a map $X \to X$. @@ -36,3 +39,15 @@ unsatisfied_properties: - property: essentially surjective proof: The singleton set is not contained in the essential image. + + - property: left-invertible + proof: >- + Assume that there is a functor $F : \Set \to \Set$ with natural isomorphisms + $$\alpha_X : X \to F(X+X).$$ + By the Yoneda Lemma, there is some $u \in F(1+1)$ such that $\alpha_X$ is given by + $$\alpha_X(x) = F((x;x) : 1+1 \to X + X)(u)$$ + for $x \in X$. For the involution $\tau_X : X + X \to X + X$ we have $(x;x) = \tau_X \circ (x;x)$. Since $\alpha_X$ is surjective, it follows that $F(\tau_X) : F(X+X) \to F(X+X)$ is the identity. The inclusions $\iota_1,\iota_2 : X \to X + X$ satisfy $\tau_X \circ \iota_1 = \iota_2$, so that $F(\iota_1) = F(\iota_2)$. + + Now let $f : X \to X$ be any endomorphism. It induces a map $\tilde{f} : X + X \to X$ defined by $\tilde{f} \circ \iota_1 = \id_X$ and $\tilde{f} \circ \iota_2 = f$. Thus, $F(\iota_1) = F(\iota_2)$ implies + $$F(f) = F(\tilde{f} \circ \iota_2) = F(\tilde{f} \circ \iota_1) = F(\id_X) = \id_{F(X)}.$$ + In particular, for every endomorphism $f : X \to X$, the induced endomorphism $F(f+f) : F(X+X) \to F(X+X)$ is the identity. By using naturality of $\alpha_X$, it follows that $f$ is the identity, which is absurd. diff --git a/databases/catdat/data/functors/enveloping_group.yaml b/databases/catdat/data/functors/enveloping_group.yaml index 45812add..f11b97ae 100644 --- a/databases/catdat/data/functors/enveloping_group.yaml +++ b/databases/catdat/data/functors/enveloping_group.yaml @@ -35,6 +35,9 @@ satisfied_properties: It is straightforward to check that it is inverse to $\alpha$ by arguing with the generators in both groups. unsatisfied_properties: + - property: essentially injective + proof: The enveloping group of any monoid with an absorbing element is trivial. + - property: faithful proof: 'Take any non-trivial monoid $M$ with an absorbing element, such as $(\IN,\cdot,1)$. Its enveloping group is trivial. Hence, $\id_M,1 : M \rightrightarrows M$ provide a counterexample.' diff --git a/databases/catdat/data/functors/forget_abelian.yaml b/databases/catdat/data/functors/forget_abelian.yaml index 362b2563..92a87387 100644 --- a/databases/catdat/data/functors/forget_abelian.yaml +++ b/databases/catdat/data/functors/forget_abelian.yaml @@ -19,11 +19,11 @@ satisfied_properties: - property: full proof: This is trivial. - - property: faithful - proof: This is trivial. - - property: right adjoint - proof: The abelianization functor is left adjoint to this forgetful functor. + proof: The abelianization functor $\Grp \to \Ab$, $G \mapsto G^{\ab}$ provides a left adjoint. + + - property: left-invertible + proof: The abelianization functor $\Grp \to \Ab$, $G \mapsto G^{\ab}$ provides a left inverse. - property: preserves initial objects proof: The trivial group is initial in both $\Ab$ and $\Grp$. diff --git a/databases/catdat/data/functors/forget_addition.yaml b/databases/catdat/data/functors/forget_addition.yaml index aef28f05..d0843fcb 100644 --- a/databases/catdat/data/functors/forget_addition.yaml +++ b/databases/catdat/data/functors/forget_addition.yaml @@ -34,8 +34,8 @@ unsatisfied_properties: - property: preserves initial objects proof: The initial object in $\Ring$ is $\IZ$, but the initial object in $\Mon$ is the trivial monoid. - - property: full - proof: The map $\IZ \to \IZ$, $z \mapsto 1$ is compatible with multiplication, but not with addition. + - property: essentially injective + proof: See MSE/4054295 for a collection of counterexamples. - property: essentially surjective proof: 'A necessary condition for a monoid to be the multiplicative monoid of a ring is that it has an absorbing element. Thus, for example, $(\IN,+,0)$ is not contained in the essential image. Remark: even a monoid with an absorbing element does not necessarily come from a ring; see MSE/3075364.' diff --git a/databases/catdat/data/functors/forget_group.yaml b/databases/catdat/data/functors/forget_group.yaml index a7f2c470..312a9cf5 100644 --- a/databases/catdat/data/functors/forget_group.yaml +++ b/databases/catdat/data/functors/forget_group.yaml @@ -33,7 +33,7 @@ satisfied_properties: proof: This follows from Theorem 2.5 at the nLab. unsatisfied_properties: - - property: full + - property: essentially injective proof: This is trivial. - property: essentially surjective diff --git a/databases/catdat/data/functors/forget_inverses.yaml b/databases/catdat/data/functors/forget_inverses.yaml index 468c8f1c..b96f8acf 100644 --- a/databases/catdat/data/functors/forget_inverses.yaml +++ b/databases/catdat/data/functors/forget_inverses.yaml @@ -15,9 +15,6 @@ related_functors: - forget_abelian satisfied_properties: - - property: faithful - proof: This is trivial. - - property: full proof: It is a standard fact from group theory that a multiplicative map already preserves inverses. @@ -27,6 +24,9 @@ satisfied_properties: - property: left adjoint proof: 'This functor is left adjoint to the functor $(-)^{\times} : \Mon \to \Grp$ that sends a monoid $M$ to its group of units $M^{\times} \coloneqq \{(a,b) \in M^2 : ab = ba = 1 \}$. In fact, if $M$ is a monoid and $G$ is a group, there is a bijection $\Hom(U_{\Grp,\Mon}(G),M) \to \Hom(G,M^{\times})$ given by mapping $\varphi$ to $g \mapsto (\varphi(g),\varphi(g^{-1}))$.' + - property: left-invertible + proof: 'The group of units functor $(-)^{\times} : \Mon \to \Grp$ provides a left inverse.' + unsatisfied_properties: - property: essentially surjective proof: This is trivial. diff --git a/databases/catdat/data/functors/forget_ring.yaml b/databases/catdat/data/functors/forget_ring.yaml index 3b545a91..f7fd9103 100644 --- a/databases/catdat/data/functors/forget_ring.yaml +++ b/databases/catdat/data/functors/forget_ring.yaml @@ -29,7 +29,7 @@ satisfied_properties: proof: This follows from Theorem 2.5 at the nLab. unsatisfied_properties: - - property: full + - property: essentially injective proof: This is trivial. - property: essentially surjective diff --git a/databases/catdat/data/functors/forget_topology.yaml b/databases/catdat/data/functors/forget_topology.yaml index 54f56a48..f129178b 100644 --- a/databases/catdat/data/functors/forget_topology.yaml +++ b/databases/catdat/data/functors/forget_topology.yaml @@ -27,5 +27,8 @@ satisfied_properties: proof: 'The indiscrete topology defines a functor $I : \Set \to \Top$ which is right adjoint to $U_{\Top}$.' unsatisfied_properties: + - property: essentially injective + proof: This is trivial. + - property: conservative proof: If $X$ is a set, the map $D(X) \to I(X)$, $x \mapsto x$ is bijective and continuous (where $D(-)$ denotes the discrete topological space and $I()$ the indiscrete topological space), but not an isomorphism (unless $X$ has at most one element). diff --git a/databases/catdat/data/functors/forget_vector.yaml b/databases/catdat/data/functors/forget_vector.yaml index e90d4f75..71c325e3 100644 --- a/databases/catdat/data/functors/forget_vector.yaml +++ b/databases/catdat/data/functors/forget_vector.yaml @@ -31,7 +31,7 @@ satisfied_properties: proof: This follows from Theorem 2.5 at the nLab. unsatisfied_properties: - - property: full + - property: essentially injective proof: This is trivial. - property: essentially surjective diff --git a/databases/catdat/data/functors/free_group.yaml b/databases/catdat/data/functors/free_group.yaml index 85ad3b15..e3fa8dc7 100644 --- a/databases/catdat/data/functors/free_group.yaml +++ b/databases/catdat/data/functors/free_group.yaml @@ -27,6 +27,9 @@ satisfied_properties: - 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)$.' + - property: essentially injective + proof: See MSE/35229. + unsatisfied_properties: - property: full proof: The homomorphism $F(\{x\}) \to F(\{x\})$, $x \mapsto x^k$ for $k \in \IZ$ provides a counterexample when $k \neq 1$. @@ -46,3 +49,10 @@ unsatisfied_properties: The canonical map $F(L) \to \lim_n F(X_n)$ is not surjective: For $n \geq 0$ define $w_n \in F(X_n)$ by $$w_n \coloneqq x_1 y^{-1} \cdots x_n y^{-1}.$$ Since $X_{n+1} \to X_n$ maps $w_{n+1} \mapsto w_n$, these elements yield a unique element $w \in \lim_n F(X_n)$. Notice that the word length of $w_n$ is unbounded in $n$. However, every element in $F(L)$ is contained already in $F(\{y,x_1,\dotsc,x_m\})$ for some $m$ and hence maps to an element with bounded word length. Hence, $w$ is not contained in the image. + + - property: left-invertible + proof: 'Assume that there is a functor $H : \Grp \to \Set$ with $H \circ F \cong \id_\Set$. In particular, $H(1)= \varnothing$. Since for every $G \in \Grp$ there is a homomorphism $G \to 1$, there is a map $H(G) \to H(1) = \varnothing$, which forces $H(G) = \varnothing$. If we apply this to $G = F(X)$ for some non-empty set $X$, we obtain a contradiction.' + # TODO: when category_conclusions are integrated, replace this proof with + # this more general implication: + # if F : C -> D is a left-invertible functor, D has a zero object, + # and C has a strict initial object, then C is trivial. diff --git a/databases/catdat/data/functors/group_units.yaml b/databases/catdat/data/functors/group_units.yaml index 04c83b07..c223cba4 100644 --- a/databases/catdat/data/functors/group_units.yaml +++ b/databases/catdat/data/functors/group_units.yaml @@ -39,6 +39,9 @@ satisfied_properties: which shows that $1 = y_1 x_n$ in $M_k$. Combined with $x_n y_1 = 1$, this shows that $x_n$ is a unit as well. unsatisfied_properties: + - property: essentially injective + proof: If $M$ is the free monoid on one generator (i.e. $\IN$ w.r.t. addition), then $M^{\times}$ is trivial, just as the group of units of the trivial monoid, but $M$ is not trivial. + - property: faithful proof: If $M$ is the free monoid on one generator (i.e. $\IN$ w.r.t. addition), then $M^{\times}$ is trivial, but $M$ is not. Hence, the identity $M \to M$ and the trivial homomorphism $M \to M$ have the same image under the functor, but they are not equal. diff --git a/databases/catdat/data/functors/modulo-p.yaml b/databases/catdat/data/functors/modulo-p.yaml index 075d049c..e7ad4039 100644 --- a/databases/catdat/data/functors/modulo-p.yaml +++ b/databases/catdat/data/functors/modulo-p.yaml @@ -27,8 +27,11 @@ unsatisfied_properties: - property: essentially surjective proof: The essential image consists precisely of the elementary abelian $p$-groups, equivalently, the vector spaces over $\IF_p$. For example, $\IZ$ is not contained in it. + - property: essentially injective + proof: 'We have $\IQ / p \IQ \cong 0 \cong 0 / p 0$, but $\IQ \not\cong 0$.' + - property: faithful - proof: 'We have $\IQ / p \IQ = 0$, but $\IQ \not\cong 0$. Thus, faithfulness is failing for $0, \id_{\IQ} : \IQ \rightrightarrows \IQ$.' + proof: 'We have $\IQ / p \IQ \cong 0$, but $\IQ \not\cong 0$. Thus, faithfulness is failing for $0, \id_{\IQ} : \IQ \rightrightarrows \IQ$.' - property: full proof: 'Let $\IZ_{(p)}$ denote the additive group of $p$-local numbers, i.e. the localization of $\IZ$ at the prime ideal $\langle p \rangle$. The map from $\Hom(\IZ_{(p)},\IZ)$ to $\Hom(\IZ_{(p)} / p \IZ_{(p)} ,\IZ / p)$ is not surjective: The abelian group $\HomInternal(\IZ_{(p)},\IZ)$ is trivial: For a prime $q \neq p$ every element of $\IZ_{(p)}$ is $q^\infty$-divisible, but $0$ is the only $q^\infty$-divisible integer. However, $\IZ_{(p)} / p \IZ_{(p)} \cong \IZ/p$ shows that $\HomInternal(\IZ_{(p)} / p \IZ_{(p)} ,\IZ / p)$ is isomorphic to $\IZ/p$.' diff --git a/databases/catdat/data/functors/monoid_ring.yaml b/databases/catdat/data/functors/monoid_ring.yaml index 7ecaea63..74b57894 100644 --- a/databases/catdat/data/functors/monoid_ring.yaml +++ b/databases/catdat/data/functors/monoid_ring.yaml @@ -29,6 +29,12 @@ satisfied_properties: unsatisfied_properties: - property: full proof: Take $M = \langle X \rangle$ and $N = \{1\}$, the free monoids of ranks $1$ and $0$, respectively. Their monoid rings are $\IZ[X]$ (the polynomial ring) and $\IZ$. The only ring homomorphism $\IZ[X] \to \IZ$ in the image of the functor is $X \mapsto 1$. But there are many more, such as $X \mapsto 0$. + check_redundancy: false + + - property: essentially injective + proof: See MSE/5139806. + # use this proof when group rings are added. + # proof: There are finite non-isomorphic groups whose group rings are isomorphic. The first example has been constructed by M. Hertweck, A Counterexample to the Isomorphism Problem for Integral Group Rings. - property: essentially surjective proof: Every monoid ring is torsion-free (in fact, the underlying additive group is free abelian), so the ring $\IZ/2$ is not contained in the essential image. diff --git a/databases/catdat/data/functors/p-torsion.yaml b/databases/catdat/data/functors/p-torsion.yaml index 8e8d869b..a719682b 100644 --- a/databases/catdat/data/functors/p-torsion.yaml +++ b/databases/catdat/data/functors/p-torsion.yaml @@ -34,14 +34,17 @@ satisfied_properties: Surjectivity: Assume we have a $p$-torsion element in $\colim_i A_i$. It has a preimage in some $A_i$. When we multiply it with $p$, it becomes zero in the colimit. This means that there exists some $i \to j$ such that this multiple becomes zero in $A_j$. Therefore, the image in $A_j$ is a $p$-torsion element. It provides the desired preimage. unsatisfied_properties: + - property: essentially injective + proof: 'We have $T_p(\IZ) = 0 = T_p(0)$, but $\IZ \not\cong 0$.' + + - property: essentially surjective + proof: The essential image consists precisely of the elementary abelian $p$-groups, equivalently, the vector spaces over $\IF_p$. For example, $\IZ$ is not contained in it. + - property: faithful proof: 'We have $T_p(\IZ) = 0$, but $\IZ \not\cong 0$. Thus, faithfulness is failing for $0, \id_{\IZ} : \IZ \rightrightarrows \IZ$.' - property: full proof: 'The canonical map from $\Hom(\IZ/p^2,\IZ/p)$ to $\Hom(T_p(\IZ/p^2),T_p(\IZ/p)) = \Hom(p \IZ/p^2, \IZ/p)$ is not surjective: The homomorphism $[p] \mapsto [1]$ is not contained in its image.' - - property: essentially surjective - proof: The essential image consists precisely of the elementary abelian $p$-groups, equivalently, the vector spaces over $\IF_p$. For example, $\IZ$ is not contained in it. - - property: preserves epimorphisms proof: The surjective homomorphism $\IZ \to \IZ/p$ is mapped to the homomorphism $0 \to \IZ/p$, which is not surjective. diff --git a/databases/catdat/data/functors/power_set_contravariant.yaml b/databases/catdat/data/functors/power_set_contravariant.yaml index 207c7a04..6903a5b4 100644 --- a/databases/catdat/data/functors/power_set_contravariant.yaml +++ b/databases/catdat/data/functors/power_set_contravariant.yaml @@ -67,3 +67,11 @@ unsatisfied_properties: - property: finitary proof: Consider the sequence of truncation maps $\cdots \twoheadrightarrow \{0,1\}^2 \twoheadrightarrow \{0,1\}^1$. Its limit in $\Set$ (i.e. colimit in $\Set^{\op}$) is $\{0,1\}^{\IN}$, which is uncountable, so that $P(\{0,1\}^{\IN})$ is also uncountable. But the colimit of the induced diagram $P(\{0,1\}^1) \hookrightarrow P(\{0,1\}^2) \hookrightarrow \cdots$ is countable since each set $P(\{0,1\}^n)$ is finite. + + - property: left-invertible + proof: 'Assume for a contradiction that there is a functor $F : \Set \to \Set^{\op}$ with (natural) isomorphisms $X \cong F(P(X))$. For any non-empty set $X$ there is a map $1 \to X$, which yields a map $F(X) \to F(1)$. Since $F(1) \cong F(P(0)) \cong 0$ is empty, it follows that also $F(X)$ is empty. Since this holds for every non-empty set, it also follows that $X \cong F(P(X)) \cong 0$, which is a contradiction.' + +undecidable_properties: + - property: essentially injective + proof: >- + The property $P(X) \cong P(Y) \implies X \cong Y$ is undecidable in ZFC. It holds when the generalized continuum hypothesis is true, but it can fail otherwise. A more precise result is given by Easton's Theorem. See also MO/17152. diff --git a/databases/catdat/data/functors/power_set_covariant.yaml b/databases/catdat/data/functors/power_set_covariant.yaml index 5b7c6bda..69da9178 100644 --- a/databases/catdat/data/functors/power_set_covariant.yaml +++ b/databases/catdat/data/functors/power_set_covariant.yaml @@ -62,3 +62,18 @@ unsatisfied_properties: - property: cofinitary proof: 'The canonical map $P(\lim_i X_i) \to \lim_i P(X_i)$ is typically not injective already for cardinality reasons: Consider for example the sequential diagram $X_n \coloneqq \{0,1\}^n$ with the truncation maps $X_{n+1} \to X_n$. The limit is $\{0,1\}^{\IN}$ with cardinality $c \coloneqq 2^{\aleph_0}$, so that its power set has cardinality $2^c$. However, the limit of the power sets $P(X_n)$ is a subset of a countable product of finite sets, hence has cardinality $\leq c$, which is strictly smaller than $2^c$.' + + - property: left-invertible + proof: >- + Assume that there is a functor $F : \Set \to \Set$ with natural isomorphisms + $$\alpha_X : X \to F(P(X)).$$ + By the Yoneda Lemma, there is some element $u \in F(P(1))$ (where $1$ is the singleton set as usual) such that $\alpha_X$ is given by + $$\alpha_X(x) = F(P(x : 1 \to X))(u).$$ + The map $P(x) : P(1) \to P(X)$ is given by $\varnothing \mapsto \varnothing$ and $1 \mapsto \{x\}$. It factors through the map $e : X + 1 \to P(X)$ which maps $a \in X$ to $\{a\}$ and the unique element of $1$ to $\varnothing$. Since $\alpha_X$ is surjective, it follows that also $F(e) : F(X + 1) \to F(P(X))$ is surjective. Since $e$ is a split monomorphism, also $F(e)$ is a split monomorphism. Hence, $F(e)$ must be an isomorphism. But then $F(X+1) \cong F(P(X)) \cong X$ for all sets $X$. If $X$ is a finite non-empty set, we conclude $\card(F(X)) = \card(X) - 1$. But then + $$\card(X) = \card(F(P(X))) = \card(P(X)) - 1 = 2^{\card(X)} - 1$$ + yields a contradiction when $\card(X) > 1$. + +undecidable_properties: + - property: essentially injective + proof: >- + The property $P(X) \cong P(Y) \implies X \cong Y$ is undecidable in ZFC. It holds when the generalized continuum hypothesis is true, but it can fail otherwise. A more precise result is given by Easton's Theorem. See also MO/17152. diff --git a/databases/catdat/data/functors/product_sets.yaml b/databases/catdat/data/functors/product_sets.yaml index 021f049b..0e7e1958 100644 --- a/databases/catdat/data/functors/product_sets.yaml +++ b/databases/catdat/data/functors/product_sets.yaml @@ -42,5 +42,8 @@ unsatisfied_properties: - property: faithful proof: 'If $f,g : A \rightrightarrows B$ are two maps, we always have $f \times \id_{\varnothing} = g \times \id_{\varnothing} : A \times \varnothing \rightrightarrows B \times \varnothing$.' + - property: essentially injective + proof: Both $(1,0)$ and $(0,1)$ are mapped to $0$. + - property: preserves coequalizers proof: 'Since the diagonal functor $\Delta : \Set \to \Set \times \Set$ preserves coequalizers (in fact, all colimits), it would follow that the composition $\Set \to \Set$, $X \mapsto X^2$ preserves coequalizers. But this is the squaring functor, from we already know that it does not preserve coequalizers.' diff --git a/databases/catdat/data/functors/sequences_sets.yaml b/databases/catdat/data/functors/sequences_sets.yaml index aafadd38..8c80b156 100644 --- a/databases/catdat/data/functors/sequences_sets.yaml +++ b/databases/catdat/data/functors/sequences_sets.yaml @@ -29,12 +29,12 @@ satisfied_properties: proof: We have $X^{\IN} \cong \Hom(\IN,X)$. unsatisfied_properties: - - property: full - proof: There are many counterexamples. For example, take the map $\{0,1\}^\IN \to \{0,1\}^\IN$ that switches the first two entries. It is not induced by a map $\{0,1\} \to \{0,1\}$. - - property: essentially surjective proof: A finite set with at least $2$ elements is not contained in the essential image. + - property: essentially injective + proof: There is an isomorphism $2^{\IN} \cong 2^{2 \cdot \IN} \cong 4^{\IN}$. There are also counterexamples for infinite sets, such as $\IN^{\IN} \cong 2^{\IN} \cong \IR \cong \IR^{\IN}$. + - property: finitary proof: >- If $X$ is any set, it is the colimit of its finite subsets (ordered by inclusion), and the canonical map diff --git a/databases/catdat/data/functors/squaring_sets.yaml b/databases/catdat/data/functors/squaring_sets.yaml index db900403..1d4c2bac 100644 --- a/databases/catdat/data/functors/squaring_sets.yaml +++ b/databases/catdat/data/functors/squaring_sets.yaml @@ -40,12 +40,24 @@ satisfied_properties: # TODO: refactor this once we add "preserves sifted colimits" proof: See Prop. 2.4 at the nLab. + - property: essentially injective + proof: Let $X,Y$ be two sets with $X^2 \cong Y^2$. If $X$ is finite, then $X^2$ and hence $Y^2$ is finite, so that also $Y$ is finite. For the cardinalities we deduce $\card(X)^2 = \card(Y)^2$ and hence $\card(X) = \card(Y)$. This yields $X \cong Y$. If $X$ is infinite, then $Y$ is infinite, and $X \cong X^2 \cong Y^2 \cong Y$. + unsatisfied_properties: - property: full proof: If $X$ has more than one element, the swap $X^2 \to X^2$, $(x,y) \mapsto (y,x)$ is not induced by a map $X \to X$. + - property: essentially surjective + proof: We have $2 \neq a^2$ for all $a \in \IN$. + - property: preserves coequalizers proof: 'Consider the two maps $x,y : \{\ast\} \rightrightarrows \{x,y\}$. Their coequalizer is the unique map $\{x,y\} \to \{\ast\}$. The coequalizer of the induced maps $\{\ast\}^2 \rightrightarrows \{x,y\}^2$ is the quotient of $\{x,y\}^2$ by the equivalence relation generated by $(x,x) \sim (y,y)$. It has three elements and is therefore not isomorphic to $\{\ast\} \cong \{\ast\}^2$.' - - property: essentially surjective - proof: We have $2 \neq a^2$ for all $a \in \IN$. + - property: left-invertible + proof: >- + Assume that there is a functor $F : \Set \to \Set$ with natural isomorphisms + $$\alpha_X : X \to F(X^2).$$ + By the Yoneda Lemma, there is some $u \in F(1)$ such that $\alpha_X$ is given by + $$\alpha_X(x) = F((x,x) : 1 \to X^2)(u)$$ + for $x \in X$. Since $(x,x)$ factors through the diagonal $\Delta_X : X \to X^2$, and $\alpha_X$ is surjective, it follows that $F(\Delta_X) : F(X) \to F(X^2)$ is surjective. It is also injective since $\Delta_X$ is a split monomorphism. Hence, $F(\Delta_X)$ is an isomorphism. + Thus, $X \cong F(X^2) \cong F(X)$. But then also $X \cong F(X^2) \cong X^2$, and we obtain a contradiction. diff --git a/databases/catdat/data/functors/torsion.yaml b/databases/catdat/data/functors/torsion.yaml index 76a48dd3..289a7e4d 100644 --- a/databases/catdat/data/functors/torsion.yaml +++ b/databases/catdat/data/functors/torsion.yaml @@ -35,15 +35,18 @@ satisfied_properties: Surjectivity: Assume we have a torsion element in $\colim_i A_i$. It has a preimage in some $A_i$. When we multiply it with some integer $\geq 1$, it becomes zero in the colimit. This means that there exists some $i \to j$ such that this multiple becomes zero in $A_j$. Therefore, the image in $A_j$ is a torsion element. It provides the desired preimage. unsatisfied_properties: + - property: essentially injective + proof: We have $T(\IZ) = 0 = T(0)$, but $\IZ \not\cong 0$. + + - property: essentially surjective + proof: The essential image consists precisely of the abelian torsion groups. For example, $\IZ$ is not contained in it. + - property: faithful proof: 'We have $T(\IZ) = 0$, but $\IZ \not\cong 0$. Thus, faithfulness is failing for $0, \id_{\IZ} : \IZ \rightrightarrows \IZ$.' - property: full proof: 'Let $p$ be a prime. The canonical map from $\Hom(\IZ/p^2,\IZ/p)$ to $\Hom(T(\IZ/p^2),T(\IZ/p)) = \Hom(p \IZ/p^2, \IZ/p)$ is not surjective: The homomorphism $[p] \mapsto [1]$ is not contained in its image.' - - property: essentially surjective - proof: The essential image consists precisely of the abelian torsion groups. For example, $\IZ$ is not contained in it. - - property: preserves epimorphisms proof: Let $p$ be a prime. The surjective homomorphism $\IZ \to \IZ/p$ is mapped to the homomorphism $0 \to \IZ/p$, which is not surjective. diff --git a/databases/catdat/scripts/expected-data/forget_vector.json b/databases/catdat/scripts/expected-data/forget_vector.json index 85816527..e45b70b6 100644 --- a/databases/catdat/scripts/expected-data/forget_vector.json +++ b/databases/catdat/scripts/expected-data/forget_vector.json @@ -11,6 +11,8 @@ "preserves initial objects": false, "left adjoint": false, "right exact": false, + "essentially injective": false, + "left-invertible": false, "cofinitary": true, "conservative": true, diff --git a/databases/catdat/scripts/expected-data/id_Set.json b/databases/catdat/scripts/expected-data/id_Set.json index 024592de..486c2879 100644 --- a/databases/catdat/scripts/expected-data/id_Set.json +++ b/databases/catdat/scripts/expected-data/id_Set.json @@ -27,5 +27,7 @@ "right exact": true, "preserves terminal objects": true, "preserves reflexive coequalizers": true, - "preserves coreflexive equalizers": true + "preserves coreflexive equalizers": true, + "essentially injective": true, + "left-invertible": true }