Constant morphisms

.cspell.json

@@ -69,6 +69,7 @@
 		"cocones",
 		"cocongruence",
 		"cocongruences",
+		"coconstant",
 		"cocontinuous",
 		"codiagonal",
 		"codirected",

content/constant_morphisms.md

@@ -0,0 +1,38 @@
+---
+title: Results on constant morphisms
+description: We prove some results that help determine whether a morphism in a category is constant.
+---
+
+## Results on constant morphisms
+
+::: Lemma 1
+A [constant morphism](/morphism-property/constant) in $\Set$ is the same as a constant map in the usual sense.
+:::
+
+_Proof._ Let $X,Y$ be two sets and let $f : X \to Y$ be a map. If $f$ is a constant morphism, then, in particular, for all morphisms $x_1,x_2 : 1 \to X$, we have $f \circ x_1 = f \circ x_2$. Therefore, $f(x_1) = f(x_2)$ for all $x_1,x_2 \in X$, so $f$ is a constant map. Conversely, if $f$ is a constant map and $x_1,x_2 : T \rightrightarrows X$ are two maps, then $f \circ x_1 = f \circ x_2$, since for all $t \in T$ we have $f(x_1(t)) = f(x_2(t))$. <span class="qed">$\square$</span>
+
+::: Lemma 2
+Let $\C$ be a locally small category. Any representable functor $U : \C \to \Set$ maps constant morphisms to constant maps.
+:::
+
+_Proof._ We may assume that $U = \Hom(G,-)$ for some $G \in \C$. If $f : X \to Y$ is a constant morphism in $\C$, then the induced map $f_* : \Hom(G,X) \to \Hom(G,Y)$ is constant by the definition of a constant morphism. <span class="qed">$\square$</span>
+
+::: Lemma 3
+Any right adjoint functor preserves constant morphisms.
+:::
+
+_Proof._ Let $G : \C \to \D$ be a functor that is right adjoint to $F : \D \to \C$. Let $f : X \to Y$ be a constant morphism in $\C$. To show that $G(f) : G(X) \to G(Y)$ is constant, let $y_1,y_2 : T \rightrightarrows G(X)$ be two morphisms. Under the adjunction, these correspond to morphisms $x_1,x_2 : F(T) \rightrightarrows X$. Since $f$ is constant, we have $f \circ x_1 = f \circ x_2$ as morphisms $F(T) \rightrightarrows Y$. Hence, $G(f) \circ y_1 = G(f) \circ y_2$ as morphisms $T \rightrightarrows G(Y)$. <span class="qed">$\square$</span>
+
+::: Lemma 4
+If $X$ is a subterminal object, then any morphism $X \to Y$ is constant. If $Y$ is a terminal object, then any morphism $X \to Y$ is constant.
+:::
+
+_Proof._ This is immediate from the definitions. <span class="qed">$\square$</span>
+
+::: Lemma 5
+If $f : X \to Y$ is a monomorphism that is constant, then $X$ is subterminal.
+:::
+
+_Proof._ If $x_1,x_2 : T \rightrightarrows X$ are morphisms, then $f \circ x_1 = f \circ x_2$ since $f$ is constant. Since $f$ is also a monomorphism, we infer that $x_1 = x_2$. <span class="qed">$\square$</span>
+
+Of course, all results on constant morphisms dualize to results on coconstant morphisms (except for Lemma 2). For example, Lemma 5 implies that if an epimorphism $f : X \to Y$ is coconstant, then $Y$ is "co-subterminal", i.e. every two morphisms $Y \rightrightarrows T$ are equal.

database/data/config.yaml

@@ -47,6 +47,7 @@ morphism_property_tags:
   - types of monomorphisms
   - types of epimorphisms
   - invertibility
+  - misc
 
 symmetric_monoidal_category_property_tags:
   - tensor-colimit interaction

database/data/morphism-implications/misc.yaml

@@ -0,0 +1,34 @@
+- id: thin_implies_constant
+  assumptions: []
+  mapped_assumptions:
+    category:
+      - thin
+  conclusions:
+    - constant
+  proof: This is trivial.
+  is_equivalence: false
+
+- id: zero_morphism_definition
+  assumptions:
+    - constant
+    - coconstant
+  conclusions:
+    - zero morphism
+  proof: This holds by definition.
+  is_equivalence: true
+
+- id: zero_morphism_criterion
+  assumptions:
+    - constant
+  mapped_assumptions:
+    category:
+      - zero morphisms
+  conclusions:
+    - zero morphism
+  proof: >-
+    Let $f : A \to B$ be a constant morphism in a category with zero morphisms. Then it is the zero morphism $0_{A,B}$ because 
+    $$f = f \circ \id_A = f \circ 0_{A,A} = 0_{A,B}.$$
+    Furthermore, $0_{A,B}$ is coconstant because for all $g,h : B \rightrightarrows C$ we have
+    $$g \circ 0_{A,B} = 0_{A,C} = h \circ 0_{A,B}.$$
+    (A similar argument shows that $0_{A,B}$ is also constant.)
+  is_equivalence: false

database/data/morphism-properties/coconstant.yaml

@@ -0,0 +1,10 @@
+id: coconstant
+relation: is
+description: 'A morphism $f : A \to B$ is called <i>coconstant</i> if for all morphisms $b_1,b_2 : B \rightrightarrows T$ we have $b_1 \circ f = b_2 \circ f$.'
+nlab_link: https://ncatlab.org/nlab/show/coconstant+morphism
+invariant_under_equivalences: true
+dual: constant
+related: []
+
+tags:
+  - misc

database/data/morphism-properties/constant.yaml

@@ -0,0 +1,10 @@
+id: constant
+relation: is
+description: 'A morphism $f : A \to B$ is called <i>constant</i> if for all morphisms $a_1,a_2 : T \rightrightarrows A$ we have $f \circ a_1 = f \circ a_2$. This is a categorical generalization of the concept of a constant function.'
+nlab_link: https://ncatlab.org/nlab/show/constant+morphism
+invariant_under_equivalences: true
+dual: coconstant
+related: []
+
+tags:
+  - misc

database/data/morphism-properties/zero morphism.yaml

@@ -0,0 +1,12 @@
+id: zero morphism
+relation: is a
+description: 'A morphism in an arbitrary category is a <i>zero morphism</i> if it is constant and coconstant. In a <a href="/category-property/zero_morphisms">category with zero morphisms</a>, for every pair of objects $A,B$, there is a unique morphism $A \to B$ with this property, the distinguished zero morphism $0_{A,B} : A \to B$ (see <a href="/morphism-implication/zero_morphism_criterion">here</a>).'
+nlab_link: https://ncatlab.org/nlab/show/zero+morphism
+invariant_under_equivalences: true
+dual: zero morphism
+related:
+  - constant
+  - coconstant
+
+tags:
+  - misc

database/data/morphisms/A3-S3-embedding.yaml

@@ -2,7 +2,7 @@ id: A3-S3-embedding
 name: embedding of A3 into S3
 notation: $i$
 category: Grp
-description: 'This is the inclusion $A_3 = \langle (1 \, 2 \, 3 ) \rangle \hookrightarrow S_3$. It serves as an example of a normal monomorphism which is not split.'
+description: 'This is the embedding of groups $A_3 = \langle (1 \, 2 \, 3 ) \rangle \hookrightarrow S_3$. It serves as an example of a normal monomorphism which is not split.'
 nlab_link: https://ncatlab.org/nlab/show/alternating+group
 
 tags:
@@ -17,3 +17,6 @@ satisfied_properties:
 unsatisfied_properties:
   - property: split monomorphism
     proof: Every homomorphism $S_3 \to A_3$ is trivial because $S_3$ is generated by transpositions and $A_3$ has no element of order $2$.
+
+  - property: zero morphism
+    proof: The embedding is not the trivial homomorphism.

database/data/morphisms/baer-specker-relations.yaml

@@ -17,3 +17,6 @@ satisfied_properties:
 unsatisfied_properties:
   - property: regular monomorphism
     proof: 'We know that a monomorphism $f : A \to B$ in <a href="/category/FreeAb">$\FreeAb$</a> is regular if and only if the quotient (taken in $\Ab$) $B/f(A)$ is free abelian. But $F/K \cong \IZ^\IN$ is the Baer-Specker group, which is not free abelian.'
+
+  - property: zero morphism
+    proof: The homomorphism is not the trivial homomorphism.

database/data/morphisms/empty-map.yaml

@@ -14,6 +14,12 @@ satisfied_properties:
   - property: monomorphism
     proof: It is vacuously injective.
 
+  - property: constant
+    proof: The map is clearly constant, and by Lemma 1 <a href="/content/constant_morphisms">here</a> this means that the morphism in $\Set$ is constant.
+
+  - property: coconstant
+    proof: This is because $\varnothing$ is initial; see also the dual of Lemma 4 <a href="/content/constant_morphisms">here</a>.
+
 unsatisfied_properties:
   - property: split monomorphism
     proof: There is no map $X \to \varnothing$.

database/data/morphisms/extremal-not-strong-example.yaml

@@ -14,6 +14,12 @@ satisfied_properties:
   - property: extremal monomorphism
     proof: It is a monomorphism because, in fact, every morphism in the forked commutative square is a monomorphism. The only factorizations of $m$ are $m \circ \id_C$ and ${\id_D} \circ m$, and $m$ is not an epimorphism (because $u \circ m = v \circ m$ but $u \neq v$).
 
+  - property: constant
+    proof: This is easy to check. The conceptual reason is that $C$ is subterminal and Lemma 4 <a href="/content/constant_morphisms">here</a>.
+
+  - property: coconstant
+    proof: 'The only pair we need to check is $u,v : D \rightrightarrows E$, but we have $u \circ m = v \circ m$ by construction.'
+
 unsatisfied_properties:
   - property: strong monomorphism
     proof: >-

database/data/morphisms/fork-handle.yaml

@@ -14,6 +14,12 @@ satisfied_properties:
   - property: regular monomorphism
     proof: 'In fact, $i$ is the equalizer of the other two morphisms $f,g : 1 \rightrightarrows 2$.'
 
+  - property: constant
+    proof: This is easy to check. The conceptual reason is that $0$ is subterminal and Lemma 4 <a href="/content/constant_morphisms">here</a>.
+
+  - property: coconstant
+    proof: This is because $0$ is initial; see also the dual of Lemma 4 <a href="/content/constant_morphisms">here</a>.
+
 unsatisfied_properties:
   - property: split monomorphism
     proof: There is no morphism $1 \to 0$.

database/data/morphisms/id_G.yaml

@@ -2,7 +2,7 @@ id: id_G
 name: identity map of a group
 notation: $\id_G$
 category: Grp
-description: 'Every object of a category has an identity morphism. In this case, we take a group $G$ and consider its identity morphism $\id_G : G \to G$ in $\Grp$.'
+description: 'Every object of a category has an identity morphism. In this case, we take a non-trivial group $G$ and consider its identity morphism $\id_G : G \to G$ in $\Grp$.'
 nlab_link: https://ncatlab.org/nlab/show/identity+morphism
 
 tags:
@@ -15,4 +15,6 @@ satisfied_properties:
   - property: isomorphism
     proof: This is obvious.
 
-unsatisfied_properties: []
+unsatisfied_properties:
+  - property: constant
+    proof: The homomorphism is not the trivial homomorphism since $G$ is non-trivial.

database/data/morphisms/id_X.yaml

@@ -2,7 +2,7 @@ id: id_X
 name: identity map of a set
 notation: $\id_X$
 category: Set
-description: 'Every object of a category has an identity morphism. In this case, we take a set $X$ and consider its identity morphism $\id_X : X \to X$ in $\Set$.'
+description: 'Every object of a category has an identity morphism. In this case, we take a set $X$ and consider its identity morphism $\id_X : X \to X$ in $\Set$. To decide all of its properties, we assume that $X$ has at least two elements.'
 nlab_link: https://ncatlab.org/nlab/show/identity+morphism
 
 tags:
@@ -15,4 +15,9 @@ satisfied_properties:
   - property: isomorphism
     proof: This is obvious.
 
-unsatisfied_properties: []
+unsatisfied_properties:
+  - property: constant
+    proof: The map is not constant since $X$ has at least two elements, and by Lemma 1 <a href="/content/constant_morphisms">here</a> this means that the morphism in $\Set$ is not constant.
+
+  - property: coconstant
+    proof: This is clear since there are two different maps $X \rightrightarrows X$. Conceptually, we can say that $X$ is not co-subterminal and apply the dual of Lemma 5 <a href="/content/constant_morphisms">here</a>.

database/data/morphisms/inclusion_positive_number.yaml

@@ -18,3 +18,9 @@ satisfied_properties:
 unsatisfied_properties:
   - property: strong monomorphism
     proof: See <a href="https://math.stackexchange.com/a/5146482" target="_blank">MSE/5146052</a>.
+
+  - property: constant
+    proof: The underlying map of sets is not constant, so that the claim follows from Lemma 2 <a href="/content/constant_morphisms">here</a>.
+
+  - property: coconstant
+    proof: 'Consider for example the two smooth maps $f,g : \IR \rightrightarrows \IR$ defined by $f(x)=x$ and $g(x)=-x$. Then $f \circ i \neq g \circ i$.'

database/data/morphisms/integer-rational-embedding.yaml

@@ -17,6 +17,12 @@ satisfied_properties:
   - property: epimorphism
     proof: Every localization $R \to S^{-1} R$ has this property by the universal property of localizations.
 
+  - property: coconstant
+    proof: This is because the $\IZ$ is initial; see also the dual of Lemma 4 <a href="/content/constant_morphisms">here</a>.
+
 unsatisfied_properties:
   - property: isomorphism
     proof: Clearly, this map is not surjective.
+
+  - property: constant
+    proof: The underlying map of sets is not constant, so that the claim follows from Lemma 2 <a href="/content/constant_morphisms">here</a>.

database/data/morphisms/multiply-2.yaml

@@ -20,3 +20,6 @@ satisfied_properties:
 unsatisfied_properties:
   - property: isomorphism
     proof: The map is not bijective.
+
+  - property: zero morphism
+    proof: The homomorphism is not the trivial homomorphism.

database/data/morphisms/reduction-mod-p.yaml

@@ -17,3 +17,6 @@ satisfied_properties:
 unsatisfied_properties:
   - property: split epimorphism
     proof: Every homomorphism $\IZ/p \to \IZ$ is trivial since $\IZ$ has no torsion.
+
+  - property: zero morphism
+    proof: The homomorphism is not the trivial homomorphism.

database/data/morphisms/terminal-map.yaml

@@ -14,6 +14,12 @@ satisfied_properties:
   - property: split epimorphism
     proof: 'Take any element $x \in X$. The corresponding map $x : 1 \to X$ is a section of $! : X \to 1$.'
 
+  - property: constant
+    proof: This is clear because $1$ is terminal; see also Lemma 4 <a href="/content/constant_morphisms">here</a>.
+
 unsatisfied_properties:
   - property: monomorphism
     proof: Since $X$ has two different elements by assumption, which trivially have the same image, the map is not injective.
+
+  - property: coconstant
+    proof: 'A direct proof is possible, but we can also argue as follows: Since the map is an epimorphism, if it were coconstant, by the dual of Lemma 5 <a href="/content/constant_morphisms">here</a>, $1$ would be co-subterminal, which is absurd.'

database/data/morphisms/universal-split-epi.yaml

@@ -14,6 +14,9 @@ satisfied_properties:
   - property: split epimorphism
     proof: 'We have $p \circ i = \id_0$ for the other morphism $i : 0 \to 1$ in the category.'
 
+  - property: zero morphism
+    proof: It factors through the zero object and is therefore the trivial homomorphism.
+
 unsatisfied_properties:
   - property: effective epimorphism
     proof: If $p$ were effective, the pullback $1 \times_0 1$ would exist, which is the product $1 \times 1$ since $0$ is terminal. Each hom-set in the walking splitting has $\leq 2$ elements, but $\Hom(1, 1 \times 1) \cong \Hom(1,1)^2$ would have four elements.

database/data/morphisms/walking-idempotent-presentation.yaml

@@ -28,3 +28,9 @@ unsatisfied_properties:
       On objects this is trivial since $B(\IN)$ has a single object.
       Now let $f$ be any morphism in $\C$. There are two cases for the morphism $F(G(f)) = F(H(f))$ in $\Idem$. If it is $\id_0$, then $G(f)$ and $H(f)$ must be one of $\id_0, \id_1$ in $I$. In both cases, since $E$ maps both $\id_0$ and $\id_1$ to $\id_*$, we conclude $E(G(f)) = E(H(f))$. Otherwise, $F(G(f)) = F(H(f))$ is $e$, but then $G(f) = H(f) = {!}$, so that $E(G(f)) = E(H(f))$.
       This proves our claim. If $F$ was a strict epimorphism, this would mean in particular that $E$ factors through $F$, i.e. that the morphism $1$ is $B(\IN)$ is idempotent, which yields the contradiction $1 + 1 = 1$.
+
+  - property: constant
+    proof: 'The functor $\Mor : \Cat \to \Set$ is representable (by the walking morphism $I$), so that by Lemma 2 <a href="/content/constant_morphisms">here</a> it maps constant morphisms to constant maps. But the map $\Mor(F) : \Mor(I) \to \Mor(\Idem)$ is not constant since both $\id_0$ and $e$ are contained in its image.'
+
+  - property: coconstant
+    proof: 'Consider any category $\C$ with two different objects $X,Y$. Then we have functors $X,Y : \Idem \rightrightarrows \C$ mapping $e$ to $\id_X$ resp. $\id_Y$. But we have $X \circ F \neq Y \circ F$.'

database/scripts/test.ts

@@ -56,7 +56,6 @@ function execute_tests() {
 
 		devlog('\n--- Test morphisms ---')
 
-		test_positivity('id_G', 'morphism')
 		test_decided_structures(decided_morphisms, 'morphism')
 
 		devlog('\n--- Test symmetric monoidal categories ---')

src/lib/server/fetchers/content.ts

@@ -24,6 +24,16 @@ export function fetch_content_references(content_id: string) {
 		)
 		.all(content_id)
 
+	const morphisms = db
+		.prepare<[string], StructureShort>(
+			`SELECT DISTINCT s.id, s.name
+	        FROM property_assignments pa
+	        INNER JOIN structures s ON s.id = pa.structure_id
+	        WHERE pa.type = 'morphism'
+	        AND pa.proof LIKE '%/content/' || ? || '%'`
+		)
+		.all(content_id)
+
 	const category_properties = db
 		.prepare<[string], PropertyShort>(
 			`SELECT id, relation FROM properties
@@ -40,5 +50,5 @@ export function fetch_content_references(content_id: string) {
 		)
 		.all(content_id)
 
-	return { categories, category_properties, category_implications, functors }
+	return { categories, category_properties, category_implications, functors, morphisms }
 }

src/routes/content/[id]/+page.svelte

@@ -15,7 +15,7 @@
 
 <!-- TODO: make this more systematic -->
 
-{#if data.categories.length > 0 || data.category_properties.length > 0 || data.category_implications.length > 0 || data.functors.length > 0}
+{#if data.categories.length > 0 || data.category_properties.length > 0 || data.category_implications.length > 0 || data.functors.length > 0 || data.morphisms.length > 0}
 	<h3>Context</h3>
 
 	{#if data.categories.length > 0}
@@ -49,6 +49,12 @@
 
 		<StructureList structures={data.functors} type="functor" />
 	{/if}
+
+	{#if data.morphisms.length > 0}
+		<p class="hint">This page is referenced by the following morphisms.</p>
+
+		<StructureList structures={data.morphisms} type="morphism" />
+	{/if}
 {/if}
 
 <SuggestionForm />