Add functor properties: essentially injective / left-invertible

.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",

databases/catdat/data/functor-implications/equivalences.yaml

@@ -17,5 +17,6 @@
   target_assumptions: []
   conclusions:
     - monadic
+    - left-invertible
   proof: This is easy.
   is_equivalence: false

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

databases/catdat/data/functor-properties/conservative.yaml

@@ -6,3 +6,4 @@ invariant_under_equivalences: true
 dual_property: conservative
 related_properties:
   - equivalence
+  - essentially injective

databases/catdat/data/functor-properties/equivalence.yaml

@@ -10,3 +10,4 @@ related_properties:
   - essentially surjective
   - continuous
   - cocontinuous
+  - left-invertible

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 <i>essentially injective</i> 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 <i>not</i> 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

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

databases/catdat/data/functor-properties/faithful.yaml

@@ -1,9 +1,11 @@
 id: faithful
 relation: is
-description: 'A functor is <i>faithful</i> when it is injective on Hom-sets: If $F(f)=F(g)$, then $f=g$.'
+description: 'A functor is <i>faithful</i> 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

databases/catdat/data/functor-properties/full.yaml

@@ -7,3 +7,4 @@ dual_property: full
 related_properties:
   - equivalence
   - faithful
+  - essentially injective

databases/catdat/data/functor-properties/left-invertible.yaml

@@ -0,0 +1,10 @@
+id: left-invertible
+relation: is
+description: 'A <i>left inverse</i> 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 <i>left-invertible</i> 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

databases/catdat/data/functors/abelianization.yaml

@@ -23,6 +23,9 @@ satisfied_properties:
     proof: See <a href="https://mathoverflow.net/questions/386144">MO/386144</a>.
 
 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$.
 

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 <a href="https://en.wikipedia.org/wiki/Reduced_ring" target="_blank">reduced</a>, 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.'

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$.

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$.

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

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

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.

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.'
 

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$.

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 <a href="https://math.stackexchange.com/questions/4054295" target="_blank">MSE/4054295</a> 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 <a href="https://en.wikipedia.org/wiki/Absorbing_element" target="_blank">absorbing element</a>. 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 <a href="https://math.stackexchange.com/questions/3075364" target="_blank">MSE/3075364</a>.'

databases/catdat/data/functors/forget_group.yaml

@@ -33,7 +33,7 @@ satisfied_properties:
     proof: This follows from Theorem 2.5 at the <a href="https://ncatlab.org/nlab/show/reflexive+coequalizer" target="_blank">nLab</a>.
 
 unsatisfied_properties:
-  - property: full
+  - property: essentially injective
     proof: This is trivial.
 
   - property: essentially surjective

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.

databases/catdat/data/functors/forget_ring.yaml

@@ -29,7 +29,7 @@ satisfied_properties:
     proof: This follows from Theorem 2.5 at the <a href="https://ncatlab.org/nlab/show/reflexive+coequalizer" target="_blank">nLab</a>.
 
 unsatisfied_properties:
-  - property: full
+  - property: essentially injective
     proof: This is trivial.
 
   - property: essentially surjective

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).

databases/catdat/data/functors/forget_vector.yaml

@@ -31,7 +31,7 @@ satisfied_properties:
     proof: This follows from Theorem 2.5 at the <a href="https://ncatlab.org/nlab/show/reflexive+coequalizer" target="_blank">nLab</a>.
 
 unsatisfied_properties:
-  - property: full
+  - property: essentially injective
     proof: This is trivial.
 
   - property: essentially surjective

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 <a href="https://math.stackexchange.com/questions/35229" target="_blank">MSE/35229</a>.
+
 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.

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.
 

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$.'