Add various examples of functors to witness property combinations

content/functors_on_discrete_categories.md

@@ -0,0 +1,45 @@
+---
+title: Functors on discrete categories
+description: We describe which functors on discrete categories are continuous or cocontinuous.
+author: Martin Brandenburg
+---
+
+## Functors on discrete categories
+
+Let $\S$ be a discrete category. Thus, a functor $F : \S \to \C$ is the same as a family of objects $F(s) \in \C$ indexed by the objects $s \in \S$. Here, we want to determine under which conditions $F$ is continuous (or cocontinuous). The case $\S = \varnothing$ is rather boring, which is why we assume from now on that $\S \neq \varnothing$, i.e. that $\S$ is inhabited.
+
+First, we consider the trivial case $\S = 1$.
+
+::: Lemma 1
+Consider the trivial category $1 = \{0\}$ with a unique object $0$. Let $F : 1 \to \C$ be a functor corresponding to an object $F(0) \in \C$. Then $F$ is continuous if and only if $F(0)$ is a terminal object in $\C$.
+:::
+
+_Proof._ If $F$ is continuous, it preserves terminal objects. Since $0 \in 1$ is terminal, it follows that $F(0) \in \C$ is terminal. Conversely, suppose that $F(0) \in \C$ is terminal. Then $F$ is continuous: for every index category $\I$, there is a unique diagram $D : \I \to 1$, namely $D(i) = 0$ and $D(i \to j) = \id_0$. Its limit is $0$, with the universal cone $(\id_0 : 0 \to D(i))_{i \in \I}$. We need to show that $(\id_{F(0)} : F(0) \to F(0))_{i \in \I}$ is a universal cone in $\C$. This is easy to see using that $F(0)$ is terminal. <span class="qed">$\square$</span>
+
+::: Lemma 2
+Let $\S$ be a non-trivial inhabited discrete category. Then a functor $F : \S \to \C$ is continuous if and only if, for every $s \in \S$, the object $F(s) \in \C$ is [subterminal](https://ncatlab.org/nlab/show/subterminal+object), i.e. every two morphisms with codomain $F(s)$ are equal.
+:::
+
+_Proof._ Assume first that $F$ is continuous. An object $X$ is subterminal if and only if $X \times X$ exists and the diagonal $X \to X \times X$ is an isomorphism. Thus, every functor preserving binary products preserves subterminal objects. Since every object in a discrete category is subterminal, it follows that each $F(s) \in \C$ is subterminal.
+
+Conversely, assume that each $F(s) \in \C$ is subterminal. To show that $F$ is continuous, let $D : \I \to \S$ be a (small) diagram admitting a universal cone $(s \to D(i))_{i \in \I}$. Then $D(i) = s$ for all $i \in \I$, and each morphism $s \to D(i)$ is the identity. Since $\S$ has no terminal object (otherwise, $\S$ would be trivial), $\I$ is inhabited. We need to show that $(\id_{F(s)} : F(s) \to F(s))_{i \in \I}$ is a universal cone in $\C$. This follows immediately from $F(s)$ being subterminal: for a family of morphisms $X \to F(s)$ indexed by $\I$, all morphisms must be equal, and there is one such morphism since $\I$ is inhabited. <span class="qed">$\square$</span>
+
+Remark that in a thin category, every object is subterminal. Of course, Lemma 2 can also be dualized: A functor on a non-trivial inhabited discrete category is cocontinuous if and only if each object in its image is "co-subterminal". Here, an object $X$ is co-subterminal if any two morphisms with domain $X$ are equal (see [MSE/1092122](https://math.stackexchange.com/questions/1092122) for a discussion of the terminology).
+
+Next, let us determine which of the continuous functors are right adjoints.
+
+::: Lemma 3
+Let $\S$ be a discrete category. Then a functor $F : \S \to \C$ is a right adjoint if and only if there is a decomposition $\C = \coprod_{s \in \S} \C_s$ into full subcategories such that $F(s) \in \C_s$ is a terminal object for every $s \in \S$.
+:::
+
+_Proof._ A functor $G : \C \to \S$ corresponds to a decomposition $\C = \coprod_{s \in \S} \C_s$ via
+$$G(X) = s \iff X \in \C_s.$$
+It is left adjoint to $F$ if and only if there are natural bijections
+$$\Hom(G(X),s) \cong \Hom(X,F(s))$$
+for $X \in \C$ and $s \in \S$. For $X \in \C_s$, this means that there is a unique morphism $X \to F(s)$. For $X \in \C_t$ with $t \neq s$, it means that there is no morphism $X \to F(s)$. In other words, $F(s) \in \C_s$. Naturality in $s$ is automatic since $\S$ is discrete. Naturality in $X$, say for $X \in \C_s$, is also automatic. <span class="qed">$\square$</span>
+
+::: Corollary 4
+Let $\S$ be a discrete category, and let $\C$ be a connected category. If there is a right adjoint functor $\S \to \C$, then $\S$ is trivial.
+:::
+
+_Proof._ By Lemma 3, such a right adjoint yields a decomposition $\C = \coprod_{s \in \S} \C_s$ into full subcategories, each having a terminal object. In particular, each $\C_s$ is inhabited. Since $\C$ is connected, it follows that $\S$ has exactly one object. <span class="qed">$\square$</span>

database/data/functor-implications/adjoints.yaml

@@ -30,3 +30,27 @@
     - right-invertible
   proof: 'If $F : \C \to \D$ is a reflector, it is left adjoint to a fully faithful functor $G : \D \to \C$. Thus, the counit $\varepsilon : F \circ G \to \id_{\D}$ is an isomorphism (Prop. 3.4 at the <a href="https://ncatlab.org/nlab/show/adjoint+functor#FullyFaithfulAndInvertibleAdjoints" target="_blank">nLab</a>). This shows that $G$ is a right inverse of $F$.'
   is_equivalence: false
+
+- id: representable_right_adjoint
+  assumptions:
+    - representable
+  mapped_assumptions:
+    domain:
+      - locally essentially small
+      - coproducts
+  conclusions:
+    - right adjoint
+  proof: 'If $\C$ is a locally small category with coproducts and $X \in \C$ is any object, then the copower functor $\Set \to \C$, $T \mapsto T \otimes X$ is left adjoint to $\Hom(X,-) : \C \to \Set$.'
+  is_equivalence: false
+
+- id: initial_object_as_left_adjoint
+  assumptions: []
+  mapped_assumptions:
+    domain:
+      - initial object
+    codomain:
+      - trivial
+  conclusions:
+    - coreflector
+  proof: 'Let $F : \C \to 1$ be the unique functor into the trivial category, and assume that $\C$ has an initial object $X$. Then the constant functor $X : 1 \to \C$ is fully faithful and left adjoint to $F$ because $\Hom(X(*),Y) \cong * \cong \Hom(*,F(Y))$.'
+  is_equivalence: false

database/data/functor-implications/limits preservation.yaml

@@ -203,3 +203,23 @@
     - regular
   proof: This holds by definition of a regular functor.
   is_equivalence: true
+
+- id: trivial_functors_continuous
+  assumptions: []
+  mapped_assumptions:
+    codomain:
+      - trivial
+  conclusions:
+    - continuous
+  proof: 'We need to show that for every category $\C$ the unique functor $!_{\C} : \C \to 1$ into the trivial category is continuous. This easy to verify directly because in the trivial category every limit is, well, trivial. More generally, for every category $\C$ and every set $S$ the diagonal functor $\Delta : \C \to \C^S$ is continuous. Here we apply this to $S = \varnothing$ so that $\C^S$ is the trivial category.'
+  is_equivalence: false
+
+- id: automatically_preserve_equalizers
+  assumptions: []
+  mapped_assumptions:
+    domain:
+      - regular-subobject-trivial
+  conclusions:
+    - preserves equalizers
+  proof: This is trivial.
+  is_equivalence: false

database/data/functor-implications/misc.yaml

@@ -78,3 +78,72 @@
     - dominant
   proof: This is trivial.
   is_equivalence: false
+
+- id: surjective_functor_to_core_connected_category
+  assumptions: []
+  mapped_assumptions:
+    domain:
+      - inhabited
+    codomain:
+      - core-connected
+  conclusions:
+    - essentially surjective
+  proof: 'Let $F : \C \to \D$ be a functor from an inhabited category to a core-connected category. Choose any object $X \in \C$. For every $Y \in \D$ we have $Y \cong F(X)$. Thus, $F$ is essentially surjective.'
+  is_equivalence: false
+
+- id: right_invertible_functor_to_trivial_category
+  assumptions: []
+  mapped_assumptions:
+    domain:
+      - inhabited
+    codomain:
+      - trivial
+  conclusions:
+    - right-invertible
+  proof: 'Let $\C$ be an inhabited category and let $F : \C \to 1$ be the unique functor to the trivial category. Choose any object $X \in \C$. Then the constant functor $X : 1 \to \C$ satisfies $F \circ X = \id_1$.'
+  is_equivalence: false
+
+- id: full_functor_to_trivial_category
+  # TODO: add the converse once we have category_conclusions
+  assumptions: []
+  mapped_assumptions:
+    domain:
+      - strongly connected
+    codomain:
+      - trivial
+  conclusions:
+    - full
+  proof: 'Let $\C$ be a strongly connected category. Then the unique functor $F : \C \to 1$ to the trivial category is full: for all $X,Y \in \C$ the map $\Hom(X,Y) \to \Hom(F(X),F(Y))$ is surjective since its domain is non-empty and its codomain is a singleton set.'
+  is_equivalence: false
+
+- id: functor_conservative_on_groupoids
+  assumptions: []
+  mapped_assumptions:
+    domain:
+      - groupoid
+  conclusions:
+    - conservative
+  proof: This is trivial.
+  is_equivalence: false
+
+- id: automatic_ess_injective_functors
+  assumptions: []
+  mapped_assumptions:
+    domain:
+      - core-connected
+  conclusions:
+    - essentially injective
+  proof: This is trivial.
+  is_equivalence: false
+
+- id: automatic_full_on_isos_functors
+  assumptions: []
+  mapped_assumptions:
+    domain:
+      - core-connected
+    codomain:
+      - trivial
+  conclusions:
+    - full on isomorphisms
+  proof: This is trivial.
+  is_equivalence: false

database/data/functors/simple_group_probing.yaml

@@ -0,0 +1,58 @@
+id: simple_group_probing
+name: simple-group probing functor
+notation: $F$
+domain: Grp
+codomain: Set
+description: >-
+  This functor maps a group $G$ to the collection
+  $$F(G) := \textstyle\prod_{\kappa} \Hom(L_\kappa,G),$$
+  where $\kappa$ ranges over all infinite cardinals and $L_\kappa$ is an infinite simple group of cardinality $\kappa$; we choose $L_\kappa := \Alt_{\fin}(\kappa)$ to make things concrete. For each $G$, the collection $F(G)$ is isomorphic to a set, since for $\kappa > \card(G)$ every homomorphism $L_\kappa \to G$ is trivial. Thus, a more precise definition would be
+  $$F(G) := \textstyle\prod_{\kappa \leq \card(G)} \Hom(L_\kappa,G),$$
+  but the first definition makes it more apparent that $F$ is a functor.
+  This is the canonical example of a continuous functor $\Grp \to \Set$ that is not representable, and not a right adjoint.
+nlab_link: null
+left_adjoint: null
+
+tags:
+  - algebra
+
+related: []
+
+satisfied_properties:
+  - property: continuous
+    proof: It is a product of representable functors.
+
+unsatisfied_properties:
+  - property: right adjoint
+    # TODO: refactor this once functor implications may have category equality assumptions
+    proof: 'If $F : \Grp \to \Set$ is right adjoint to $G : \Set \to \Grp$, then $F$ is representable with representing object $U := G(1)$. Let $u \in F(U)$ be a universal element, consisting of homomorphisms $u_\kappa : L_\kappa \to U$. Choose an infinite cardinal $\kappa > \card(U)$. Then $u_\kappa$ must be trivial. The set $F(L_\kappa) = \prod_{\lambda \leq \kappa} \Hom(L_\lambda,L_\kappa)$ contains the element $x$ whose $\kappa$-component is $\id_{L_\kappa}$ and all other components are trivial. Since $u \in F(U)$ is universal, there is a unique homomorphism $f : U \to L_\kappa$ such that $F(f)(u) = x$ in $F(L_\kappa)$. The $\kappa$-component of this equality is $f \circ u_\kappa = \id_{L_\kappa}$. Thus, $u_\kappa$ is injective, contradicting our previous observation that $u_\kappa$ is trivial and the fact that $L_\kappa$ is non-trivial.'
+
+  # TODO: refactor this once functor implications may have category conclusions
+  # here: if a functor preserves terminal objects, and the domain is pointed,
+  # then the codomain is pointed as well.
+  - property: preserves initial objects
+    proof: The functor maps the trivial group to the singleton set, which is not initial.
+
+  - property: preserves binary coproducts
+    proof: The canonical map $F(1) \sqcup F(1) \to F(1 \sqcup 1) = F(1)$ is not injective, since $F(1)$ has one element, whereas $F(1) \sqcup F(1)$ has two elements.
+
+  - property: essentially injective
+    proof: Every finite group is mapped to a singleton set.
+
+  - property: faithful
+    proof: If $G$ is a non-trivial finite group, the trivial homomorphism $G \to G$ and the identity of $G$ are mapped to the same map, because $F(G)$ is a singleton set.
+
+  - property: dominant
+    proof: There is no group $G$ with a split monomorphism $\varnothing \to F(G)$, since $F(G)$ is not empty. In fact, using trivial homomorphisms $L_\kappa \to G$, we may regard $F(G)$ as a pointed set.
+
+  - property: preserves epimorphisms
+    proof: >-
+      We first prove that if $G$ is a torsion-free group, then the pointed set $F(G)$ is trivial, i.e. a singleton set. In fact, our explicit choice $L_\kappa = \Alt_{\fin}(\kappa)$ implies that $L_\kappa$ is a filtered colimit of finite groups and is therefore a torsion group, which implies that every homomorphism $L_\kappa \to G$ is trivial.
+
+      Now choose a free group $G$ that admits an epimorphism $G \to L_{\alpha_0}$. The induced map $F(G) \to F(L_{\alpha_0})$ is not an epimorphism, since otherwise $F(L_{\alpha_0})$ would be trivial, but $(\id_{L_{\alpha_0}},1,1,\dotsc)$ is a non-trivial element.
+
+  - property: full
+    proof: 'We already mentioned that $F(G)$ can be regarded as a pointed set. Every homomorphism $G \to H$ induces a pointed map $F(G) \to F(H)$. (Thus, the functor should really be regarded as a functor to $\Set_*$, but in this entry, the codomain is $\Set$, which makes life easier.) Thus, it suffices to find a group $G$ with a non-pointed map $F(G) \to F(G)$, which of course exists as soon as $F(G)$ is non-trivial. But we already saw that each $F(L_\kappa)$ is non-trivial.'
+
+  - property: finitary
+    proof: By our explicit choice of $L_{\aleph_0}$, it is a filtered colimit of finite groups $(\Alt(n))_{n \in \IN}$. But $F(L_{\aleph_0})$ is not the filtered colimit of the sets $F(\Alt(n))$, since these are singleton sets.

database/data/functors/span_endpoints_inclusion.yaml

@@ -0,0 +1,36 @@
+id: span_endpoints_inclusion
+name: span endpoints inclusion
+notation: $E$
+domain: '2'
+codomain: walking_span
+description: This is the functor that embeds the discrete category $\{1,2\}$ into the walking span $\{1 \leftarrow 0 \rightarrow 2\}$. Among other things, it provides an example of a fully faithful functor which is not left-invertible.
+nlab_link: null
+left_adjoint: null
+
+tags:
+  - category theory
+
+related: []
+
+satisfied_properties:
+  - property: fully faithful
+    proof: This is trivial.
+
+  - property: continuous
+    proof: This follows from Lemma 2 <a href="/content/functors_on_discrete_categories">here</a>.
+
+  - property: cocontinuous
+    proof: This follows from the dual of Lemma 2 <a href="/content/functors_on_discrete_categories">here</a>.
+
+unsatisfied_properties:
+  - property: dominant
+    proof: The object $0 \in \Span$ does not admit a split monomorphism to either $1$ or $2$.
+
+  - property: left-invertible
+    proof: 'Assume that there is a functor $F : \Span \to \{1,2\}$ with $F(E(X)) \cong X$ for $X \in \{1,2\}$. Thus, $F(1) = 1$ and $F(2) = 2$. There are two possible choices for $F(0)$. Without loss of generality, assume that $F(0) = 1$. Then the morphism $0 \to 2$ in the walking span induces a morphism $1 = F(0) \to F(2) = 2$ in the discrete category, but no such morphism exists.'
+
+  - property: right adjoint
+    proof: This follows from Corollary 4 <a href="/content/functors_on_discrete_categories">here</a>.
+
+  - property: left adjoint
+    proof: This follows from the dual of Corollary 4 <a href="/content/functors_on_discrete_categories">here</a>.

database/data/functors/trivial_BG.yaml

@@ -0,0 +1,22 @@
+id: trivial_BG
+name: trivial functor from the delooping
+notation: $!_{BG}$
+domain: BG_f
+codomain: '1'
+description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the delooping of a non-trivial finite group $G$. It is a basic example of a conservative functor which is not faithful.'
+nlab_link: null
+left_adjoint: null
+
+tags:
+  - algebra
+
+related:
+  - trivial_groups
+  - trivial_sets
+  - trivial_Idem
+
+satisfied_properties: []
+
+unsatisfied_properties:
+  - property: faithful
+    proof: This is trivial.

database/data/functors/trivial_Idem.yaml

@@ -0,0 +1,30 @@
+id: trivial_Idem
+name: trivial functor from the walking idempotent
+notation: $!_{\Idem}$
+domain: walking_idempotent
+codomain: '1'
+description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the walking idempotent. It is a basic example of an essentially injective functor which is not conservative.'
+nlab_link: null
+left_adjoint: null
+
+tags:
+  - category theory
+
+related:
+  - trivial_groups
+  - trivial_sets
+  - trivial_BG
+
+satisfied_properties: []
+
+unsatisfied_properties:
+  - property: conservative
+    proof: The universal idempotent is mapped to an isomorphism, but is not an isomorphism.
+
+  - property: left adjoint
+    # TODO: refactor this once functor implications support category conclusions
+    proof: A functor $1 \to \C$ which is right adjoint to $\Idem \to 1$ provides a terminal object in <a href="/category/walking_idempotent">$\Idem$</a>, which does not exist.
+
+  - property: right adjoint
+    # TODO: refactor this once functor implications support category conclusions
+    proof: A functor $1 \to \C$ which is left adjoint to $\Idem \to 1$ provides an initial object in <a href="/category/walking_idempotent">$\Idem$</a>, which does not exist.

database/data/functors/trivial_groups.yaml

@@ -1,9 +1,9 @@
 id: trivial_groups
 name: trivial functor from the category of groups
-notation: $!$
+notation: $!_\Grp$
 domain: Grp
 codomain: '1'
-description: 'Every category $\C$ has a unique functor $! : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of groups. It is a basic example of a full functor which is not faithful.'
+description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of groups. It is a basic example of a full functor which is not faithful.'
 nlab_link: null
 left_adjoint: null
 
@@ -12,16 +12,10 @@ tags:
 
 related:
   - trivial_sets
+  - trivial_BG
+  - trivial_Idem
 
-satisfied_properties:
-  - property: coreflector
-    proof: 'The constant functor $1 \to \Grp$ with value the trivial group is a left adjoint of $! : \Grp \to 1$ and fully faithful; this is because the trivial group is an initial object of $\Grp$.'
-
-  - property: reflector
-    proof: 'The constant functor $1 \to \Grp$ with value the trivial group is a right adjoint of $! : \Grp \to 1$ and fully faithful; this is because the trivial group is a terminal object of $\Grp$.'
-
-  - property: full
-    proof: This follows easily from the fact that <a href="/category/Grp">$\Grp$</a> is strongly connected.
+satisfied_properties: []
 
 unsatisfied_properties:
   - property: essentially injective

database/data/functors/trivial_sets.yaml

@@ -1,9 +1,9 @@
 id: trivial_sets
 name: trivial functor from the category of sets
-notation: $!$
+notation: $!_\Set$
 domain: Set
 codomain: '1'
-description: 'Every category $\C$ has a unique functor $! : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of sets.'
+description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of sets.'
 nlab_link: null
 left_adjoint: null
 
@@ -12,13 +12,10 @@ tags:
 
 related:
   - trivial_groups
+  - trivial_BG
+  - trivial_Idem
 
-satisfied_properties:
-  - property: coreflector
-    proof: 'The constant functor $1 \to \Set$ with value $\varnothing$ is a left adjoint of $! : \Set \to 1$ and fully faithful; this is because $\varnothing$ is an initial object of $\Set$.'
-
-  - property: reflector
-    proof: 'The constant functor $1 \to \Set$ with value $\{\ast\}$ is a right adjoint of $! : \Set \to 1$ and fully faithful; this is because $\{\ast\}$ is a terminal object of $\Set$.'
+satisfied_properties: []
 
 unsatisfied_properties:
   - property: faithful

database/data/functors/walking_isomorphism_object_inclusion.yaml

@@ -15,9 +15,11 @@ related: []
 satisfied_properties:
   - property: fully faithful
     proof: This is trivial.
+    check_redundancy: false
 
   - property: essentially surjective
     proof: The object $0$ is in the image, and the other object $1$ is isomorphic to $0$.
+    check_redundancy: false
 
 unsatisfied_properties:
   - property: isomorphism