Various additions to functors

.cspell.json

@@ -100,6 +100,7 @@
 		"coquotients",
 		"coreflection",
 		"coreflective",
+		"coreflector",
 		"coreflexive",
 		"coreflexivity",
 		"coregular",

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

@@ -13,11 +13,20 @@
     source:
       - cogenerating set
       - complete
-      - locally small
+      - locally essentially small
       - well-powered
     target:
-      - locally small
+      - locally essentially small
   conclusions:
     - right adjoint
   proof: This is the Special Adjoint Functor Theorem. The proof can be found, for example, at the <a href="https://ncatlab.org/nlab/show/adjoint+functor+theorem" target="_blank">nLab</a>, or in <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. V, Theorem 8.2.
   is_equivalence: false
+
+- id: reflector_consequences
+  assumptions:
+    - reflector
+  conclusions:
+    - left adjoint
+    - 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

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

@@ -1,18 +1,29 @@
 - id: equivalence_criterion
   assumptions:
     - essentially surjective
-    - faithful
-    - full
+    - fully faithful
   conclusions:
     - equivalence
   proof: This is standard, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. IV, Theorem 4.1.
   is_equivalence: true
 
+- id: equivalence_invertible
+  assumptions:
+    - equivalence
+  conclusions:
+    - left-invertible
+    - right-invertible
+  proof: >-
+    If a functor $F$ has a right inverse $R$ and a left inverse $L$, then
+    $$L \cong L \circ F \circ R \cong R.$$
+    Hence, $R$ (and $L$) are (pseudo-)inverse to $F$.
+  is_equivalence: true
+
 - id: equivalence_consequences
   assumptions:
     - equivalence
   conclusions:
     - monadic
-    - left-invertible
+    - reflector
   proof: This is easy.
   is_equivalence: false

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

@@ -132,3 +132,51 @@
     - preserves monomorphisms
   proof: Any monomorphism in the domain is a regular monomorphism and is mapped to a regular monomorphism.
   is_equivalence: false
+
+- id: zero_preserving_condition
+  assumptions:
+    - preserves terminal objects
+  mapped_assumptions:
+    source:
+      - pointed
+    target:
+      - pointed
+  conclusions:
+    - preserves initial objects
+  proof: This is trivial.
+  is_equivalence: false
+
+- id: biproduct_preserving_condition
+  assumptions:
+    - preserves finite products
+  mapped_assumptions:
+    source:
+      - biproducts
+    target:
+      - biproducts
+  conclusions:
+    - preserves finite coproducts
+  proof: This is trivial.
+  is_equivalence: false
+
+- id: lift_implies_preservation
+  assumptions:
+    - lifts small limits
+  mapped_assumptions:
+    target:
+      - complete
+  conclusions:
+    - continuous
+  proof: 'Let $F : \C \to \D$ be the given functor and $X : \I \to \C$ be a small diagram. Since $\D$ is complete, the diagram $F \circ X$ has a limit cone. Since $F$ lifts small limits, there is a limit cone of $X$ which is mapped by $F$ to the limit cone of $F \circ X$. Hence, $F$ preserves this limit cone of $X$. Since any other limit cone of $X$ is isomorphic to it, the claim follows.'
+  is_equivalence: false
+
+- id: preservation_implies_lift
+  assumptions:
+    - continuous
+  mapped_assumptions:
+    source:
+      - complete
+  conclusions:
+    - lifts small limits
+  proof: 'Let $F : \C \to \D$ be the given functor and $X : \I \to \C$ be a small diagram such that $F \circ X$ has a limit cone. By assumption, $X$ has a limit cone, and $F$ maps it to a limit cone of $F \circ X$. But then the image must be isomorphic to the given limit cone.'
+  is_equivalence: false

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

@@ -1,3 +1,12 @@
+- id: fully-faithful-definition
+  assumptions:
+    - full
+    - faithful
+  conclusions:
+    - fully faithful
+  proof: This holds by definition.
+  is_equivalence: true
+
 - id: faithful-via-equalizers
   assumptions:
     - conservative
@@ -12,8 +21,7 @@
 
 - id: conservative_consequences
   assumptions:
-    - full
-    - faithful
+    - fully faithful
   conclusions:
     - 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$.
@@ -35,5 +43,13 @@
     - faithful
     - essentially injective
     - conservative
-  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.'
+  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 a 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
+
+- id: right-invertible_consequences
+  assumptions:
+    - right-invertible
+  conclusions:
+    - essentially surjective
+  proof: This is trivial.
   is_equivalence: false

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

@@ -20,3 +20,11 @@
     - monadic
   proof: This is the crude monadicity theorem. A proof can be found in <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, Thm. IV.4.2.
   is_equivalence: false
+
+- id: monadic_lift_limits
+  assumptions:
+    - monadic
+  conclusions:
+    - lifts small limits
+  proof: 'See <a href="https://ncatlab.org/nlab/show/Abstract+and+Concrete+Categories" target="_blank">Joy of Cats</a>, Prop. 20.12.'
+  is_equivalence: false

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

@@ -10,3 +10,4 @@ related_properties:
   - left adjoint
   - preserves coequalizers
   - finitary
+  - lifts small colimits

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

@@ -10,3 +10,4 @@ related_properties:
   - right adjoint
   - preserves equalizers
   - cofinitary
+  - lifts small limits

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

@@ -0,0 +1,9 @@
+id: coreflector
+relation: is a
+description: 'A functor $F : \C \to \D$ is a <i>coreflector</i> if it is right adjoint to a functor $G : \D \to \C$ which is fully faithful. Hence, $G$ is equivalent to the inclusion of a full coreflective subcategory. The condition that $G$ is fully faithful can also be expressed by the condition that the counit $\eta : \id_{\D} \to F \circ G$ is an isomorphism (Prop. 3.4 at the <a href="https://ncatlab.org/nlab/show/adjoint+functor#FullyFaithfulAndInvertibleAdjoints" target="_blank">nLab</a>).'
+nlab_link: https://ncatlab.org/nlab/show/coreflective+subcategory
+invariant_under_equivalences: true
+dual_property: reflector
+related_properties:
+  - right adjoint
+  - right-invertible

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

@@ -7,5 +7,6 @@ dual_property: faithful
 related_properties:
   - equivalence
   - full
+  - fully faithful
   - essentially injective
   - left-invertible

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

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

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

@@ -0,0 +1,10 @@
+id: fully faithful
+relation: is
+description: 'A functor is <i>fully faithful</i> when it is full and faithful. This means that for all objects $A,B$ in its domain the map $\Hom(A,B) \to \Hom(F(A),F(B))$, $f \mapsto F(f)$ is a bijection.'
+nlab_link: https://ncatlab.org/nlab/show/full+and+faithful+functor
+invariant_under_equivalences: true
+dual_property: fully faithful
+related_properties:
+  - full
+  - faithful
+  - equivalence

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

@@ -7,3 +7,4 @@ dual_property: right adjoint
 related_properties:
   - cocontinuous
   - comonadic
+  - reflector

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

@@ -1,10 +1,11 @@
 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.'
+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. This notion is self-dual in the sense that $F : \C \to \D$ is left-invertible iff $F^{\op} : \C^{\op} \to \D^{\op}$ is left-invertible.'
 nlab_link: https://ncatlab.org/nlab/show/inverse+functor
 invariant_under_equivalences: true
 dual_property: left-invertible
 related_properties:
   - equivalence
   - faithful
   - essentially injective
+  - right-invertible

databases/catdat/data/functor-properties/lifts small colimits.yaml

@@ -0,0 +1,8 @@
+id: lifts small colimits
+relation: ''
+description: 'A functor $F : \C \to \D$ <i>lifts small colimits</i> when for every small diagram $X : \I \to \C$ and every every colimit cocone of $F \circ X$ there is a colimit cocone of $X$ that is mapped by $F$ to the given colimit cocone of $F \circ X$.'
+nlab_link: https://ncatlab.org/nlab/show/lifted+limit
+invariant_under_equivalences: true
+dual_property: lifts small limits
+related_properties:
+  - cocontinuous

databases/catdat/data/functor-properties/lifts small limits.yaml

@@ -0,0 +1,8 @@
+id: lifts small limits
+relation: ''
+description: 'A functor $F : \C \to \D$ <i>lifts small limits</i> when for every small diagram $X : \I \to \C$ and every every limit cone of $F \circ X$ there is a limit cone of $X$ that is mapped by $F$ to the given limit cone of $F \circ X$.'
+nlab_link: https://ncatlab.org/nlab/show/lifted+limit
+invariant_under_equivalences: true
+dual_property: lifts small colimits
+related_properties:
+  - continuous

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

@@ -0,0 +1,9 @@
+id: reflector
+relation: is a
+description: 'A functor $F : \C \to \D$ is a <i>reflector</i> if it is left adjoint to a functor $G : \D \to \C$ which is fully faithful. Hence, $G$ is equivalent to the inclusion of a full reflective subcategory. The condition that $G$ is fully faithful can also be expressed by the condition that 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>).'
+nlab_link: https://ncatlab.org/nlab/show/reflective+subcategory
+invariant_under_equivalences: true
+dual_property: coreflector
+related_properties:
+  - left adjoint
+  - right-invertible

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

@@ -3,6 +3,5 @@ relation: is
 description: 'A functor $F : \C \to \D$ is <i>representable</i> if $\C$ is locally small, $\D = \Set$, and there is an object $A \in \C$ with $F \cong \Hom(A,-)$.'
 nlab_link: https://ncatlab.org/nlab/show/representable+functor
 invariant_under_equivalences: true
-dual_property: null
 related_properties:
   - continuous

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

@@ -0,0 +1,11 @@
+id: right-invertible
+relation: is
+description: 'A <i>right inverse</i> of a functor $F : \C \to \D$ is a functor $G : \D \to \C$ satisfying $F \circ G \cong \id_{\D}$. We do not require $F \circ G = \id_{\D}$ here, which is often too strict. A functor is called <i>right-invertible</i> when it has a right inverse. This notion is self-dual in the sense that $F : \C \to \D$ is right-invertible iff $F^{\op} : \C^{\op} \to \D^{\op}$ is right-invertible.'
+nlab_link: https://ncatlab.org/nlab/show/inverse+functor
+invariant_under_equivalences: true
+dual_property: right-invertible
+related_properties:
+  - equivalence
+  - essentially surjective
+  - left-invertible
+  - reflector

databases/catdat/data/functors/abelianization.yaml

@@ -13,11 +13,8 @@ tags:
 related_functors: []
 
 satisfied_properties:
-  - property: left adjoint
-    proof: This functor is left adjoint to the forgetful functor.
-
-  - property: essentially surjective
-    proof: For abelian groups $G$ we have $G \cong G^{\ab}$.
+  - property: reflector
+    proof: 'This functor is left adjoint to the forgetful functor $U_{\Ab,\Grp} : \Ab \hookrightarrow \Grp$, which is fully faithful.'
 
   - property: preserves finite products
     proof: See <a href="https://mathoverflow.net/questions/386144">MO/386144</a>.

databases/catdat/data/functors/coproduct_sets.yaml

@@ -3,7 +3,7 @@ name: binary coproduct functor on sets
 notation: $+$
 source: SetxSet
 target: Set
-description: This functor maps a pair of sets $(X,Y)$ to their coproduct $X + Y$.
+description: This functor maps a pair of sets $(X,Y)$ to their coproduct $X + Y$. It is an example of a right-invertible left adjoint functor which is not a reflector.
 nlab_link: null
 
 tags:
@@ -14,8 +14,8 @@ related_functors:
   - product_sets
 
 satisfied_properties:
-  - property: essentially surjective
-    proof: We have $X \cong X + 0$.
+  - property: right-invertible
+    proof: The functor $\Set \to \Set \times \Set$, $X \mapsto (X,0)$ provides a right inverse since $X + 0 \cong X$.
 
   - property: preserves equalizers
     proof: This can be checked with a straight forward calculation.
@@ -37,3 +37,6 @@ unsatisfied_properties:
 
   - property: essentially injective
     proof: Both $(1,0)$ and $(0,1)$ are mapped to $1$.
+
+  - property: reflector
+    proof: 'Its right adjoint, the diagonal functor $\Delta : X \to X \times X$, is faithful, but not full.'

databases/catdat/data/functors/discrete_topology.yaml

@@ -10,7 +10,8 @@ tags:
   - topology
   - free
 
-related_functors: []
+related_functors:
+  - indiscrete_topology
 
 satisfied_properties:
   - property: left adjoint

databases/catdat/data/functors/enveloping_group.yaml

@@ -14,11 +14,8 @@ related_functors:
   - free_group
 
 satisfied_properties:
-  - property: left adjoint
-    proof: 'By definition, this functor is left adjoint to the forgetful functor $U_{\Grp,\Mon} : \Grp \to \Mon$.'
-
-  - property: essentially surjective
-    proof: 'In fact, the counit of the adjunction $F \circ U_{\Grp,\Mon} \to \id_{\Grp}$ is an isomorphism since the right adjoint $U_{\Grp,\Mon}$ is fully faithful (Prop. 3.4 at the <a href="https://ncatlab.org/nlab/show/adjoint+functor#FullyFaithfulAndInvertibleAdjoints" target="_blank">nLab</a>).'
+  - property: reflector
+    proof: 'By definition, this functor is left adjoint to the forgetful functor $U_{\Grp,\Mon} : \Grp \hookrightarrow \Mon$, which is fully faithful.'
 
   - property: preserves finite products
     proof: >-

databases/catdat/data/functors/forget_abelian.yaml

@@ -25,9 +25,6 @@ satisfied_properties:
   - 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$.
-
   - property: preserves coequalizers
     proof: 'This follows from the concrete construction of coequalizers, but it can also be proven as follows: Assume that $f,g : A \rightrightarrows B$ have coequalizer $p : B \to C$ in $\Ab$. If $G$ is any group and $h : B \to G$ is a homomorphism with $hf = hg$, consider the image factorization $h = i h''$ of $h$. We have $h'' f = h'' g$, and the image $\im(h)$ is abelian. Hence, there is a unique homomorphism $k : C \to \im(h)$ with $kp = h''$. Hence, $ik : C \to G$ satisfies $ikp = h$. Uniqueness follows since we already know that the forgetful functor is preserves epimorphisms.'
 

databases/catdat/data/functors/forget_group.yaml

@@ -15,6 +15,7 @@ related_functors:
   - forget_vector
   - forget_ring
   - forget_abelian
+  - forget_group_pointed
 
 satisfied_properties:
   - property: representable