Various additions to functors

.cspell.json

@@ -100,6 +100,7 @@
 		"coquotients",
 		"coreflection",
 		"coreflective",
+		"coreflector",
 		"coreflexive",
 		"coreflexivity",
 		"coregular",
@@ -236,6 +237,7 @@
 		"proset",
 		"prosets",
 		"protomodular",
+		"pseudomonic",
 		"pushforward",
 		"pushout",
 		"pushouts",

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

@@ -16,13 +16,14 @@
   proof: This is trivial.
   is_equivalence: false
 
-- id: finite_products_consequences
+- id: preserve_finite_products_criterion
   assumptions:
     - preserves finite products
   conclusions:
     - preserves terminal objects
-  proof: This is trivial.
-  is_equivalence: false
+    - preserves binary products
+  proof: This follows immediately from <a href="/category-implication/finite_products_characterization">this result</a> about finite products in categories.
+  is_equivalence: true
 
 - id: continuous_criterion
   assumptions:
@@ -33,7 +34,7 @@
       - products
   conclusions:
     - continuous
-  proof: This follows from the construction of limits via equalizers and products, see  <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. V, Theorem 2.2.
+  proof: This follows from the construction of limits via equalizers and products, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. V, Theorem 2.2.
   is_equivalence: false
 
 - id: continuous_criterion_filtered
@@ -113,7 +114,7 @@
 - id: criterion_coreflexive_equalizers
   assumptions:
     - preserves coreflexive equalizers
-    - preserves finite products # TODO: only need binary products
+    - preserves binary products
   mapped_assumptions:
     source:
       - binary products
@@ -132,3 +133,29 @@
     - 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

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
@@ -10,30 +19,62 @@
   proof: 'Let $f,g : X \rightrightarrows Y$ be two morphisms in the source category, and choose an equalizer $E \hookrightarrow X$. By assumption, $F(E) \to F(X)$ is the equalizer of $F(f),F(g) : F(X) \rightrightarrows F(Y)$. Thus, if $F(f) = F(g)$, then $F(E) \to F(X)$ is an isomorphism. Since $F$ is conservative, $E \to X$ is an isomorphism, which means $f = g$.'
   is_equivalence: false
 
-- id: conservative_consequences
+- id: conservative_criterion
   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$.
   is_equivalence: false
 
-- id: reflects_isomorphism_criterion
+- id: left-invertible_consequences
+  assumptions:
+    - left-invertible
+  conclusions:
+    - 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 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
+
+- id: full-on-isomorphisms_criterion
   assumptions:
     - full
     - conservative
+  conclusions:
+    - full on isomorphisms
+  proof: This is obvious.
+  is_equivalence: false
+
+- id: full-on-isomorphisms_consequences
+  assumptions:
+    - full on isomorphisms
   conclusions:
     - essentially injective
-  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.'
+  proof: This is trivial.
   is_equivalence: false
 
-- id: left-invertible_consequences
+- id: pseudomonic_definition
   assumptions:
-    - left-invertible
+    - pseudomonic
   conclusions:
     - 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.'
+    - full on isomorphisms
+  proof: This holds by definition.
+  is_equivalence: true
+
+- id: essentially-surjective_implies_dominant
+  assumptions:
+    - essentially surjective
+  conclusions:
+    - dominant
+  proof: This is trivial.
   is_equivalence: false

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

@@ -5,5 +5,6 @@ nlab_link: https://ncatlab.org/nlab/show/conservative+functor
 invariant_under_equivalences: true
 dual_property: conservative
 related_properties:
-  - equivalence
+  - fully faithful
   - essentially injective
+  - full on isomorphisms

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/dominant.yaml

@@ -0,0 +1,8 @@
+id: dominant
+relation: is
+description: 'A functor $F : \C \to \D$ is <i>dominant</i> when every object $Y \in \D$ there is an object $X \in \C$ such that $Y$ is a retract of $F(X)$. That is, there is a split monomorphism $Y \hookrightarrow F(X)$.'
+nlab_link: https://ncatlab.org/nlab/show/dominant+functor
+invariant_under_equivalences: true
+dual_property: dominant
+related_properties:
+  - essentially surjective

databases/catdat/data/functor-properties/essentially injective.yaml

@@ -3,12 +3,13 @@ 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.
+  holds for all objects $A,B \in \C$. This is a condition solely on the objects themselves, i.e. it is <i>not</i> required that every isomorphism between $F(A)$ and $F(B)$ is induced by an isomorphism between $A$ and $B$ (cf. <a href="/functor-property/full_on_isomorphisms">full on isomorphisms</a>). 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
+  - fully faithful
+  - full on isomorphisms
   - essentially surjective
+  - pseudomonic

databases/catdat/data/functor-properties/essentially surjective.yaml

@@ -1,9 +1,10 @@
 id: essentially surjective
 relation: is
-description: 'A functor $F : \C \to \D$ is <i>essentially surjective</i> when every object $Y \in \D$ is isomorphic to $F(X)$ for some $X \in \C$.'
+description: 'A functor $F : \C \to \D$ is <i>essentially surjective</i> (on objects) when every object $Y \in \D$ is isomorphic to $F(X)$ for some object $X \in \C$.'
 nlab_link: https://ncatlab.org/nlab/show/essentially+surjective+functor
 invariant_under_equivalences: true
 dual_property: essentially surjective
 related_properties:
   - equivalence
   - essentially injective
+  - dominant

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

@@ -5,7 +5,8 @@ nlab_link: https://ncatlab.org/nlab/show/faithful+functor
 invariant_under_equivalences: true
 dual_property: faithful
 related_properties:
-  - equivalence
   - full
+  - fully faithful
   - essentially injective
   - left-invertible
+  - pseudomonic

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

@@ -0,0 +1,10 @@
+id: full on isomorphisms
+relation: 'is'
+description: 'A functor $F : \C \to \D$ is <i>full on isomorphisms</i> when, for every pair of objects $A,B \in \C$, every isomorphism $F(A) \to F(B)$ is induced by an isomorphism $A \to B$.'
+nlab_link: null
+invariant_under_equivalences: true
+dual_property: full on isomorphisms
+related_properties:
+  - full
+  - conservative
+  - essentially injective

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

@@ -7,4 +7,6 @@ dual_property: full
 related_properties:
   - equivalence
   - faithful
+  - fully faithful
   - essentially injective
+  - full on isomorphisms

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

@@ -0,0 +1,11 @@
+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
+  - pseudomonic

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/preserves binary coproducts.yaml

@@ -0,0 +1,10 @@
+id: preserves binary coproducts
+relation: ''
+description: A functor $F$ <i>preserves binary coproducts</i> when for every pair of objects $A,B$ in the source whose coproduct $A \sqcup B$ exists, also the coproduct $F(A) \sqcup F(B)$ exists in the target and such that the canonical morphism $F(A) \sqcup F(B) \to F(A \sqcup B)$ is an isomorphism.
+nlab_link: https://ncatlab.org/nlab/show/preserved+colimit
+invariant_under_equivalences: true
+dual_property: preserves binary products
+related_properties:
+  - preserves finite products
+  - preserves products
+  - continuous

databases/catdat/data/functor-properties/preserves binary products.yaml

@@ -0,0 +1,10 @@
+id: preserves binary products
+relation: ''
+description: A functor $F$ <i>preserves binary products</i> when for every pair of objects $A,B$ in the source whose product $A \times B$ exists, also the product $F(A) \times F(B)$ exists in the target and such that the canonical morphism $F(A \times B) \to F(A) \times F(B)$ is an isomorphism.
+nlab_link: https://ncatlab.org/nlab/show/preserved+limit
+invariant_under_equivalences: true
+dual_property: preserves binary coproducts
+related_properties:
+  - preserves finite products
+  - preserves products
+  - continuous

databases/catdat/data/functor-properties/preserves finite coproducts.yaml

@@ -6,5 +6,6 @@ invariant_under_equivalences: true
 dual_property: preserves finite products
 related_properties:
   - preserves coproducts
+  - preserves binary coproducts
   - preserves initial objects
   - cocontinuous

databases/catdat/data/functor-properties/preserves finite products.yaml

@@ -6,5 +6,6 @@ invariant_under_equivalences: true
 dual_property: preserves finite coproducts
 related_properties:
   - preserves products
+  - preserves binary products
   - preserves terminal objects
   - continuous

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

@@ -0,0 +1,10 @@
+id: pseudomonic
+relation: 'is'
+description: A functor is <i>pseudomonic</i> when it is faithful and full on isomorphisms.
+nlab_link: https://ncatlab.org/nlab/show/pseudomonic+functor
+invariant_under_equivalences: true
+dual_property: pseudomonic
+related_properties:
+  - essentially injective
+  - full on isomorphisms
+  - faithful

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