From 70aa147febe2ade0f00eaa02a3704eb0a7321ab2 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 13 Aug 2026 11:37:16 +0200 Subject: [PATCH 1/3] show morphism references on content pages --- src/lib/server/fetchers/content.ts | 12 +++++++++++- src/routes/content/[id]/+page.svelte | 8 +++++++- 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/src/lib/server/fetchers/content.ts b/src/lib/server/fetchers/content.ts index ae820491..c70f0754 100644 --- a/src/lib/server/fetchers/content.ts +++ b/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 } } diff --git a/src/routes/content/[id]/+page.svelte b/src/routes/content/[id]/+page.svelte index 6fdb0219..d397ef18 100644 --- a/src/routes/content/[id]/+page.svelte +++ b/src/routes/content/[id]/+page.svelte @@ -15,7 +15,7 @@ -{#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}

Context

{#if data.categories.length > 0} @@ -49,6 +49,12 @@ {/if} + + {#if data.morphisms.length > 0} +

This page is referenced by the following morphisms.

+ + + {/if} {/if} From 4450eb622410a3db2f8199bf3740ff23768c49e6 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 13 Aug 2026 13:51:36 +0200 Subject: [PATCH 2/3] add constant and coconstant morphisms --- .cspell.json | 1 + content/constant_morphisms.md | 48 +++++++++++++++++++ database/data/config.yaml | 1 + database/data/morphism-implications/misc.yaml | 9 ++++ .../data/morphism-properties/coconstant.yaml | 10 ++++ .../data/morphism-properties/constant.yaml | 10 ++++ database/data/morphisms/A3-S3-embedding.yaml | 8 +++- .../morphisms/baer-specker-relations.yaml | 6 +++ database/data/morphisms/empty-map.yaml | 6 +++ .../extremal-not-strong-example.yaml | 6 +++ database/data/morphisms/fork-handle.yaml | 6 +++ database/data/morphisms/id_G.yaml | 9 +++- database/data/morphisms/id_X.yaml | 9 +++- .../morphisms/inclusion_positive_number.yaml | 6 +++ .../morphisms/integer-rational-embedding.yaml | 6 +++ database/data/morphisms/multiply-2.yaml | 6 +++ database/data/morphisms/reduction-mod-p.yaml | 6 +++ database/data/morphisms/terminal-map.yaml | 6 +++ .../data/morphisms/universal-split-epi.yaml | 6 +++ .../walking-idempotent-presentation.yaml | 6 +++ database/scripts/test.ts | 1 - 21 files changed, 166 insertions(+), 6 deletions(-) create mode 100644 content/constant_morphisms.md create mode 100644 database/data/morphism-implications/misc.yaml create mode 100644 database/data/morphism-properties/coconstant.yaml create mode 100644 database/data/morphism-properties/constant.yaml diff --git a/.cspell.json b/.cspell.json index 13ab69fc..f8e7b4fc 100644 --- a/.cspell.json +++ b/.cspell.json @@ -69,6 +69,7 @@ "cocones", "cocongruence", "cocongruences", + "coconstant", "cocontinuous", "codiagonal", "codirected", diff --git a/content/constant_morphisms.md b/content/constant_morphisms.md new file mode 100644 index 00000000..6e4d42f2 --- /dev/null +++ b/content/constant_morphisms.md @@ -0,0 +1,48 @@ +--- +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))$. $\square$ + +::: 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. $\square$ + +::: 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)$. $\square$ + +::: 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. $\square$ + +::: 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$. $\square$ + +::: Lemma 6 +In a category with [zero morphisms](/category-property/zero_morphisms), the constant morphisms coincide with the zero morphisms. +::: + +_Proof._ A zero morphism $0_{X,Y} : X \to Y$ is constant because, for all $x_1,x_2 : T \rightrightarrows X$, we have +$$0_{X,Y} \circ x_1 = 0_{T,Y} = 0_{X,Y} \circ x_2.$$ +Conversely, if $f : X \to Y$ is constant, then +$$f = f \circ \id_X = f \circ 0_{X,X} = 0_{X,Y}.$$ +$\square$ + +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. Also, Lemma 6 implies that in a category with zero morphisms, the coconstant morphisms coincide with the zero morphisms as well. diff --git a/database/data/config.yaml b/database/data/config.yaml index 36b07641..391bea0d 100644 --- a/database/data/config.yaml +++ b/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 diff --git a/database/data/morphism-implications/misc.yaml b/database/data/morphism-implications/misc.yaml new file mode 100644 index 00000000..554925cd --- /dev/null +++ b/database/data/morphism-implications/misc.yaml @@ -0,0 +1,9 @@ +- id: thin_implies_constant + assumptions: [] + mapped_assumptions: + category: + - thin + conclusions: + - constant + proof: This is trivial. + is_equivalence: false diff --git a/database/data/morphism-properties/coconstant.yaml b/database/data/morphism-properties/coconstant.yaml new file mode 100644 index 00000000..509ea1c2 --- /dev/null +++ b/database/data/morphism-properties/coconstant.yaml @@ -0,0 +1,10 @@ +id: coconstant +relation: is +description: 'A morphism $f : A \to B$ is called coconstant 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 diff --git a/database/data/morphism-properties/constant.yaml b/database/data/morphism-properties/constant.yaml new file mode 100644 index 00000000..8c1b7260 --- /dev/null +++ b/database/data/morphism-properties/constant.yaml @@ -0,0 +1,10 @@ +id: constant +relation: is +description: 'A morphism $f : A \to B$ is called constant 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 diff --git a/database/data/morphisms/A3-S3-embedding.yaml b/database/data/morphisms/A3-S3-embedding.yaml index d59e348a..9a245ed6 100644 --- a/database/data/morphisms/A3-S3-embedding.yaml +++ b/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,9 @@ 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: constant + proof: This follows from Lemma 6 here. + + - property: coconstant + proof: This follows from Lemma 6 here. diff --git a/database/data/morphisms/baer-specker-relations.yaml b/database/data/morphisms/baer-specker-relations.yaml index 557e207d..331be0ae 100644 --- a/database/data/morphisms/baer-specker-relations.yaml +++ b/database/data/morphisms/baer-specker-relations.yaml @@ -17,3 +17,9 @@ satisfied_properties: unsatisfied_properties: - property: regular monomorphism proof: 'We know that a monomorphism $f : A \to B$ in $\FreeAb$ 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: constant + proof: This follows from Lemma 6 here. + + - property: coconstant + proof: This follows from Lemma 6 here. diff --git a/database/data/morphisms/empty-map.yaml b/database/data/morphisms/empty-map.yaml index e54a0b23..fcbcfa14 100644 --- a/database/data/morphisms/empty-map.yaml +++ b/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 here 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 here. + unsatisfied_properties: - property: split monomorphism proof: There is no map $X \to \varnothing$. diff --git a/database/data/morphisms/extremal-not-strong-example.yaml b/database/data/morphisms/extremal-not-strong-example.yaml index 1c050c12..dbc90f8c 100644 --- a/database/data/morphisms/extremal-not-strong-example.yaml +++ b/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 here. + + - 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: >- diff --git a/database/data/morphisms/fork-handle.yaml b/database/data/morphisms/fork-handle.yaml index e903821d..6a6c9694 100644 --- a/database/data/morphisms/fork-handle.yaml +++ b/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 here. + + - property: coconstant + proof: This is because $0$ is initial; see also the dual of Lemma 4 here. + unsatisfied_properties: - property: split monomorphism proof: There is no morphism $1 \to 0$. diff --git a/database/data/morphisms/id_G.yaml b/database/data/morphisms/id_G.yaml index 0ac62165..bb11c4fa 100644 --- a/database/data/morphisms/id_G.yaml +++ b/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,9 @@ satisfied_properties: - property: isomorphism proof: This is obvious. -unsatisfied_properties: [] +unsatisfied_properties: + - property: constant + proof: This follows from Lemma 6 here. + + - property: coconstant + proof: This follows from Lemma 6 here. diff --git a/database/data/morphisms/id_X.yaml b/database/data/morphisms/id_X.yaml index 4ff2c137..ca6b1f16 100644 --- a/database/data/morphisms/id_X.yaml +++ b/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 here 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 here. diff --git a/database/data/morphisms/inclusion_positive_number.yaml b/database/data/morphisms/inclusion_positive_number.yaml index 04c5b8fc..404313e9 100644 --- a/database/data/morphisms/inclusion_positive_number.yaml +++ b/database/data/morphisms/inclusion_positive_number.yaml @@ -18,3 +18,9 @@ satisfied_properties: unsatisfied_properties: - property: strong monomorphism proof: See MSE/5146052. + + - property: constant + proof: The underlying map of sets is not constant, so that the claim follows from Lemma 2 here. + + - 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$.' diff --git a/database/data/morphisms/integer-rational-embedding.yaml b/database/data/morphisms/integer-rational-embedding.yaml index c361e49d..57e9527c 100644 --- a/database/data/morphisms/integer-rational-embedding.yaml +++ b/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 here. + 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 here. diff --git a/database/data/morphisms/multiply-2.yaml b/database/data/morphisms/multiply-2.yaml index a38b08e4..7f253a3c 100644 --- a/database/data/morphisms/multiply-2.yaml +++ b/database/data/morphisms/multiply-2.yaml @@ -20,3 +20,9 @@ satisfied_properties: unsatisfied_properties: - property: isomorphism proof: The map is not bijective. + + - property: constant + proof: This follows from Lemma 6 here. + + - property: coconstant + proof: This follows from Lemma 6 here. diff --git a/database/data/morphisms/reduction-mod-p.yaml b/database/data/morphisms/reduction-mod-p.yaml index d6f8faaf..f4e894f6 100644 --- a/database/data/morphisms/reduction-mod-p.yaml +++ b/database/data/morphisms/reduction-mod-p.yaml @@ -17,3 +17,9 @@ satisfied_properties: unsatisfied_properties: - property: split epimorphism proof: Every homomorphism $\IZ/p \to \IZ$ is trivial since $\IZ$ has no torsion. + + - property: constant + proof: This follows from Lemma 6 here. + + - property: coconstant + proof: This follows from Lemma 6 here. diff --git a/database/data/morphisms/terminal-map.yaml b/database/data/morphisms/terminal-map.yaml index c1442c12..f6f19410 100644 --- a/database/data/morphisms/terminal-map.yaml +++ b/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 here. + 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 here, $1$ would be co-subterminal, which is absurd.' diff --git a/database/data/morphisms/universal-split-epi.yaml b/database/data/morphisms/universal-split-epi.yaml index 5f02df9f..8802cbe2 100644 --- a/database/data/morphisms/universal-split-epi.yaml +++ b/database/data/morphisms/universal-split-epi.yaml @@ -14,6 +14,12 @@ 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: constant + proof: This follows from Lemma 6 here. + + - property: coconstant + proof: This follows from Lemma 6 here. + 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. diff --git a/database/data/morphisms/walking-idempotent-presentation.yaml b/database/data/morphisms/walking-idempotent-presentation.yaml index b7ab11e7..06921a48 100644 --- a/database/data/morphisms/walking-idempotent-presentation.yaml +++ b/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 here 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$.' diff --git a/database/scripts/test.ts b/database/scripts/test.ts index b55f6789..76e6b5b0 100644 --- a/database/scripts/test.ts +++ b/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 ---') From 1fc1f5864d0c07db9672ca5be3d114acc0ab90d6 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 13 Aug 2026 14:17:29 +0200 Subject: [PATCH 3/3] add zero morphisms as a morphism property --- content/constant_morphisms.md | 12 +-------- database/data/morphism-implications/misc.yaml | 25 +++++++++++++++++++ .../morphism-properties/zero morphism.yaml | 12 +++++++++ database/data/morphisms/A3-S3-embedding.yaml | 7 ++---- .../morphisms/baer-specker-relations.yaml | 7 ++---- database/data/morphisms/id_G.yaml | 5 +--- database/data/morphisms/multiply-2.yaml | 7 ++---- database/data/morphisms/reduction-mod-p.yaml | 7 ++---- .../data/morphisms/universal-split-epi.yaml | 7 ++---- 9 files changed, 49 insertions(+), 40 deletions(-) create mode 100644 database/data/morphism-properties/zero morphism.yaml diff --git a/content/constant_morphisms.md b/content/constant_morphisms.md index 6e4d42f2..8962a069 100644 --- a/content/constant_morphisms.md +++ b/content/constant_morphisms.md @@ -35,14 +35,4 @@ 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$. $\square$ -::: Lemma 6 -In a category with [zero morphisms](/category-property/zero_morphisms), the constant morphisms coincide with the zero morphisms. -::: - -_Proof._ A zero morphism $0_{X,Y} : X \to Y$ is constant because, for all $x_1,x_2 : T \rightrightarrows X$, we have -$$0_{X,Y} \circ x_1 = 0_{T,Y} = 0_{X,Y} \circ x_2.$$ -Conversely, if $f : X \to Y$ is constant, then -$$f = f \circ \id_X = f \circ 0_{X,X} = 0_{X,Y}.$$ -$\square$ - -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. Also, Lemma 6 implies that in a category with zero morphisms, the coconstant morphisms coincide with the zero morphisms as well. +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. diff --git a/database/data/morphism-implications/misc.yaml b/database/data/morphism-implications/misc.yaml index 554925cd..b5e4e52e 100644 --- a/database/data/morphism-implications/misc.yaml +++ b/database/data/morphism-implications/misc.yaml @@ -7,3 +7,28 @@ - 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 diff --git a/database/data/morphism-properties/zero morphism.yaml b/database/data/morphism-properties/zero morphism.yaml new file mode 100644 index 00000000..70bf5399 --- /dev/null +++ b/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 zero morphism if it is constant and coconstant. In a category with zero morphisms, 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 here).' +nlab_link: https://ncatlab.org/nlab/show/zero+morphism +invariant_under_equivalences: true +dual: zero morphism +related: + - constant + - coconstant + +tags: + - misc diff --git a/database/data/morphisms/A3-S3-embedding.yaml b/database/data/morphisms/A3-S3-embedding.yaml index 9a245ed6..9e4fae35 100644 --- a/database/data/morphisms/A3-S3-embedding.yaml +++ b/database/data/morphisms/A3-S3-embedding.yaml @@ -18,8 +18,5 @@ 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: constant - proof: This follows from Lemma 6 here. - - - property: coconstant - proof: This follows from Lemma 6 here. + - property: zero morphism + proof: The embedding is not the trivial homomorphism. diff --git a/database/data/morphisms/baer-specker-relations.yaml b/database/data/morphisms/baer-specker-relations.yaml index 331be0ae..e4e1f34a 100644 --- a/database/data/morphisms/baer-specker-relations.yaml +++ b/database/data/morphisms/baer-specker-relations.yaml @@ -18,8 +18,5 @@ unsatisfied_properties: - property: regular monomorphism proof: 'We know that a monomorphism $f : A \to B$ in $\FreeAb$ 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: constant - proof: This follows from Lemma 6 here. - - - property: coconstant - proof: This follows from Lemma 6 here. + - property: zero morphism + proof: The homomorphism is not the trivial homomorphism. diff --git a/database/data/morphisms/id_G.yaml b/database/data/morphisms/id_G.yaml index bb11c4fa..b3524a0e 100644 --- a/database/data/morphisms/id_G.yaml +++ b/database/data/morphisms/id_G.yaml @@ -17,7 +17,4 @@ satisfied_properties: unsatisfied_properties: - property: constant - proof: This follows from Lemma 6 here. - - - property: coconstant - proof: This follows from Lemma 6 here. + proof: The homomorphism is not the trivial homomorphism since $G$ is non-trivial. diff --git a/database/data/morphisms/multiply-2.yaml b/database/data/morphisms/multiply-2.yaml index 7f253a3c..63cbd54c 100644 --- a/database/data/morphisms/multiply-2.yaml +++ b/database/data/morphisms/multiply-2.yaml @@ -21,8 +21,5 @@ unsatisfied_properties: - property: isomorphism proof: The map is not bijective. - - property: constant - proof: This follows from Lemma 6 here. - - - property: coconstant - proof: This follows from Lemma 6 here. + - property: zero morphism + proof: The homomorphism is not the trivial homomorphism. diff --git a/database/data/morphisms/reduction-mod-p.yaml b/database/data/morphisms/reduction-mod-p.yaml index f4e894f6..3465ca57 100644 --- a/database/data/morphisms/reduction-mod-p.yaml +++ b/database/data/morphisms/reduction-mod-p.yaml @@ -18,8 +18,5 @@ unsatisfied_properties: - property: split epimorphism proof: Every homomorphism $\IZ/p \to \IZ$ is trivial since $\IZ$ has no torsion. - - property: constant - proof: This follows from Lemma 6 here. - - - property: coconstant - proof: This follows from Lemma 6 here. + - property: zero morphism + proof: The homomorphism is not the trivial homomorphism. diff --git a/database/data/morphisms/universal-split-epi.yaml b/database/data/morphisms/universal-split-epi.yaml index 8802cbe2..80cb8416 100644 --- a/database/data/morphisms/universal-split-epi.yaml +++ b/database/data/morphisms/universal-split-epi.yaml @@ -14,11 +14,8 @@ 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: constant - proof: This follows from Lemma 6 here. - - - property: coconstant - proof: This follows from Lemma 6 here. + - property: zero morphism + proof: It factors through the zero object and is therefore the trivial homomorphism. unsatisfied_properties: - property: effective epimorphism