Add extremal monomorphisms and extremal epimorphisms

content/foundations.md

@@ -25,7 +25,7 @@ For example, there is a collection $[\mathrm{Set},\mathrm{Set}]$ that consists o
 
 Just imagine three copies of ZFC embedded into each other, each representing a "level of size". Grothendieck universes are merely an implementation detail, which we can _and will_ drop from now on. Sets are on level 1, collections on level 2, and hypercollections on level 3. Concrete mathematical objects such as numbers or functions can be thought of as living on level 0 (even though they are usually modeled as sets in ZFC).
 
-![visualization of three levels of size](/img/three-levels-of-size.webp)
+<img class="small" alt="visualization of three levels of size" src="/img/three-levels-of-size.webp" />
 
 The levels are not defined by cardinality alone. For example, $\{\mathrm{Set}\}$ is a collection with just one element, but it is not a set (since otherwise $\mathrm{Set}$ would be a set). In particular, not every finite collection is a set. However, every finite collection is isomorphic to a set.
 

content/relationships-epis-monos.md

@@ -0,0 +1,42 @@
+---
+title: Relationships between epimorphisms and monomorphisms
+description: A graphical overview of the relationships between the various types of epimorphisms and monomorphisms
+---
+
+## Relationships between epimorphisms and monomorphisms
+
+There are several [properties of morphisms](/morphism-properties), including various types of epimorphisms and monomorphisms. The [implications](/morphism-implications) establish various relationships between these types. Here we present a graphical overview of these relationships.
+
+### The various types of epimorphisms
+
+In the diagram, an arrow $X \Longrightarrow Y$ means that every morphism with property $X$ also has property $Y$. If it is labelled with a category property $P$, the implication does not hold in general, but it holds in categories satisfying $P$. For example, in a category with pullbacks, every strict epimorphism is effective.
+
+![Diagram showing the types of epimorphisms](/img/epis.webp)
+
+<!--
+\begin{tikzcd}[column sep=35pt, row sep=50pt, nodes={inner sep=10pt}]
+& \text{isomorphism} \ar[Rightarrow]{dr} \ar[Rightarrow]{d} \ar[Rightarrow]{dl}[swap]{\text{zero morphisms\;}} & \\
+\text{normal epimorphism} \ar[Rightarrow, shift left=1.25ex]{dr} &\text{split epimorphism} \ar[Rightarrow]{d} &  \text{effective epimorphism} \ar[Rightarrow]{dl} \\
+& \text{regular epimorphism} \ar[Rightarrow,shift left=1.25ex]{ul}{\text{preadditive\;}} \ar[Rightarrow]{r} & \text{strict epimorphism} \ar[Rightarrow]{u}[swap]{\text{\;pullbacks}} \ar[Rightarrow]{d} \\
+& \text{extremal epimorphism} \ar[Rightarrow]{u}{\text{regular\;}} \ar[Rightarrow,shift left=1.5ex]{d} \ar[Rightarrow, shift left=1ex]{r}{\text{pullbacks}} & \text{strong epimorphism} \ar[Rightarrow,shift left=1ex]{l} \\
+& \text{epimorphism} \ar[Rightarrow]{ur}[swap]{\text{mono-regular}} \ar[Rightarrow, shift left=1.5ex]{u}{\text{balanced\;}} \ar[Rightarrow, bend left=45, shift left=8ex]{uu}{\text{epi-regular\;}} &
+\end{tikzcd}
+-->
+
+Fun fact: This describes a category in itself: We define the composition of $P : X \Rightarrow Y$ and $Q : Y \Rightarrow Z$ as $P \wedge Q : X \Rightarrow Z$.
+
+### The various types of monomorphisms
+
+This diagram is just the dual of the previous diagram. The same notation applies.
+
+![Diagram showing the types of monomorphisms](/img/monos.webp)
+
+<!--
+\begin{tikzcd}[column sep=35pt, row sep=50pt, nodes={inner sep=10pt}]
+& \text{isomorphism} \ar[Rightarrow]{dr} \ar[Rightarrow]{d} \ar[Rightarrow]{dl}[swap]{\text{zero morphisms\;}} & \\
+\text{normal monomorphism} \ar[Rightarrow, shift left=1.25ex]{dr} &\text{split monomorphism} \ar[Rightarrow]{d} &  \text{effective monomorphism} \ar[Rightarrow]{dl} \\
+& \text{regular monomorphism} \ar[Rightarrow,shift left=1.25ex]{ul}{\text{preadditive\;}} \ar[Rightarrow]{r} & \text{strict monomorphism} \ar[Rightarrow]{u}[swap]{\text{\;pushouts}} \ar[Rightarrow]{d} \\
+& \text{extremal monomorphism} \ar[Rightarrow]{u}{\text{coregular\;}} \ar[Rightarrow,shift left=1.5ex]{d} \ar[Rightarrow, shift left=1ex]{r}{\text{pushouts}} & \text{strong monomorphism} \ar[Rightarrow,shift left=1ex]{l} \\
+& \text{monomorphism} \ar[Rightarrow]{ur}[swap]{\text{epi-regular}} \ar[Rightarrow, shift left=1.5ex]{u}{\text{balanced\;}} \ar[Rightarrow, bend left=45, shift left=8ex]{uu}{\text{mono-regular\;}} &
+\end{tikzcd}
+-->

database/data/categories/forked_commutative_square.yaml

@@ -0,0 +1,82 @@
+id: forked_commutative_square
+name: forked commutative square
+notation: $\ForkSquare$
+objects: $A,B,C,D,E$
+morphisms: 'The morphisms are generated by $e : A \to B$, $f : A \to C$, $g : B \to D$, $m : C \to D$ and $u,v : D \rightrightarrows E$, subject to the relations $g \circ e = m \circ f$, $u \circ g = v \circ g$, and $u \circ m = v \circ m$. In total, there are $15$ morphisms.'
+description: >-
+  This finite category is generated by the graph
+  $$\begin{array}{ccccc}
+  A & \xrightarrow{\hspace{1em} e \hspace{1em}} & B & & \\
+  \text{\scriptsize $f$}\bigg\downarrow\;\, && \;\,\bigg\downarrow\text{\scriptsize $g$} && \\
+  C & \xrightarrow{\hspace{1em} m \hspace{1em}} & D &
+  \begin{array}{c}
+  \xrightarrow{\hspace{1em} u \hspace{1em}}\\
+  \xrightarrow{\hspace{1em} v \hspace{1em}}
+  \end{array} & E
+  \end{array}$$
+  and the evident relations: the square commutes, and the parallel pair $u,v$ is equalized by both $g$ and $m$. We have added this category to the database solely as an example of an extremal monomorphism (namely $m$) that is not a strong monomorphism. There is probably no common name for this category, but "forked commutative square" seems like a good fit.
+nlab_link: null
+tags:
+  - category theory
+
+related:
+  - walking_fork
+  - walking_commutative_square
+
+satisfied_properties:
+  - property: small
+    proof: This is obvious.
+
+  - property: finite
+    proof: This is obvious.
+
+  - property: skeletal
+    proof: The five objects are clearly pairwise non-isomorphic.
+
+  - property: one-way
+    proof: This is obvious.
+
+  - property: strict initial object
+    proof: Clearly, $A$ is an initial object. Since $\id_A$ is the only morphism with codomain $A$, it is strict.
+
+  - property: generator
+    proof: 'The only parallel pair of distinct morphisms is $u,v : D \rightrightarrows E$. It follows that $D$ is a generator.'
+
+  - property: cogenerator
+    proof: 'The only parallel pair of distinct morphisms is $u,v : D \rightrightarrows E$. It follows that $E$ is a cogenerator.'
+
+  - property: left cancellative
+    proof: 'The only parallel pair of distinct morphisms is $u,v : D \rightrightarrows E$. Thus, it is sufficient to prove that every morphism with domain $E$ is a monomorphism. But there is only one such morphism, namely $\id_E$.'
+
+  - property: regular-subobject-trivial
+    proof: 'The only parallel pair of distinct morphisms is $u,v : D \rightrightarrows E$, so it suffices to prove that they do not have an equalizer. This is proven in the list of unsatisfied properties.'
+    references:
+      - forked_commutative_square_no_equalizers
+
+unsatisfied_properties:
+  - property: semi-strongly connected
+    proof: There is no morphism $B \to C$ and no morphism $C \to B$.
+
+  - property: equalizers
+    proof: 'The morphisms $u,v : D \rightrightarrows E$ do not have an equalizer: the four morphisms with codomain $D$ are $g$, $m$, $g \circ e = m \circ f$, and $\id_D$. But $\id_D$ does not equalize $u,v$. The other three morphisms equalize $u,v$, but they are not universal: $m$ is not universal since $g$ does not factor through it, $g$ is not universal since $m$ does not factor through it, and $g \circ e$ is not universal since $g$ does not factor through it.'
+    label: forked_commutative_square_no_equalizers
+
+  - property: pullbacks
+    proof: 'Any two parallel morphisms with codomain $D$ are equal. It follows that a pullback of the cospan $D \xrightarrow{u} E \xleftarrow{v} D$ would be an equalizer of $u,v : D \rightrightarrows E$, which we know does not exist.'
+    references:
+      - forked_commutative_square_no_equalizers
+
+  - property: extremal generator
+    proof: 'Since both $m$ and $g$ equalize $u,v$, it is easy to see that $D$ is the only generator. But it is not extremal since $e$ induces a bijection $e_* : \Hom(D,A) \to \Hom(D,B)$ (both sets are empty), without $e$ being an isomorphism.'
+
+  - property: extremal cogenerator
+    proof: 'We already saw that $E$ is a cogenerator, and it is also the only one because any cogenerator must admit a morphism from $E$ to be able to distinguish $u,v$. But $E$ is not extremal since $f$ induces a bijection $f^* : \Hom(C,E) \to \Hom(A,E)$ (both sets are singletons), without $f$ being an isomorphism.'
+
+special_objects:
+  initial object:
+    description: $A$
+
+special_morphisms:
+  epimorphisms:
+    description: all morphisms except for the three non-identity morphisms with codomain $D$, namely $g$, $m$, and the diagonal $g \circ e$
+    proof: 'Every one of the three non-identity morphisms with codomain $D$ equalizes $u,v$, and thus cannot be an epimorphism. Conversely, the identity morphisms are of course epimorphisms, and if a morphism does not have codomain $D$, then it is an epimorphism because the only parallel pair of distinct morphisms is $u,v : D \rightrightarrows E$.'

database/data/categories/walking_commutative_square.yaml

@@ -14,6 +14,7 @@ tags:
 related:
   - walking_fork
   - walking_morphism
+  - forked_commutative_square
 
 satisfied_properties:
   - property: small
@@ -51,7 +52,4 @@ special_objects:
   products:
     description: $b \times c = a$, $x \times x = x$, $a \times x = a$, $d \times x = x$
 
-special_morphisms:
-  isomorphisms:
-    description: the four identities
-    proof: This is trivial.
+special_morphisms: {}

database/data/categories/walking_composable_pair.yaml

@@ -48,7 +48,4 @@ special_objects:
   products:
     description: infimum taken in $\{0 < 1 < 2\}$
 
-special_morphisms:
-  isomorphisms:
-    description: the three identities
-    proof: This is trivial.
+special_morphisms: {}

database/data/categories/walking_coreflexive_pair.yaml

@@ -85,9 +85,6 @@ special_objects:
     description: $[1]$
 
 special_morphisms:
-  isomorphisms:
-    description: the two identities
-    proof: This is obvious.
   monomorphisms:
     description: the identities and $i$, $j$
     proof: Since $pi = \id$, but $ip \neq \id$, we conclude that $i$ is a monomorphism, but $p$ is not. Likewise, $j$ is a monomorphism. Since $p$ is not a monomorphism, $ip$ and $jp$ are also no monomorphisms.

database/data/categories/walking_fork.yaml

@@ -15,6 +15,7 @@ related:
   - walking_commutative_square
   - walking_composable_pair
   - walking_pair
+  - forked_commutative_square
 
 satisfied_properties:
   - property: small
@@ -68,9 +69,6 @@ special_objects:
     description: $0$
 
 special_morphisms:
-  isomorphisms:
-    description: the three identities
-    proof: This is trivial.
   epimorphisms:
     description: the identities and $f,g$
     proof: This is easily checked.

database/data/categories/walking_morphism.yaml

@@ -53,7 +53,4 @@ special_objects:
   products:
     description: $0 \times x = 0$, $1 \times x = x$
 
-special_morphisms:
-  isomorphisms:
-    description: the two identities
-    proof: This is trivial.
+special_morphisms: {}

database/data/categories/walking_pair.yaml

@@ -15,6 +15,7 @@ related:
   - walking_coreflexive_pair
   - walking_fork
   - walking_morphism
+  - forked_commutative_square
 
 satisfied_properties:
   - property: small
@@ -50,7 +51,4 @@ unsatisfied_properties:
 
 special_objects: {}
 
-special_morphisms:
-  isomorphisms:
-    description: the two identities
-    proof: This is trivial.
+special_morphisms: {}

database/data/categories/walking_span.yaml

@@ -50,7 +50,4 @@ special_objects:
   products:
     description: '[binary case] $1 \times 2 = 0$, $x \times x = x$, $0 \times x = 0$'
 
-special_morphisms:
-  isomorphisms:
-    description: the three identities
-    proof: This is trivial.
+special_morphisms: {}

database/data/categories/walking_splitting.yaml

@@ -64,12 +64,9 @@ special_objects:
     description: $0$
 
 special_morphisms:
-  isomorphisms:
-    description: the two identities
-    proof: This is obvious.
   monomorphisms:
     description: the identities and $i$
     proof: The morphism $i$ is even a split monomorphism. The morphism $p$ is not a monomorphism since $p \circ \id_1 = p \circ ip$. The morphism $ip$ is not a monomorphism since it would imply that $p$ is a monomorphism.
   epimorphisms:
     description: the identities and $p$
-    proof: The morphism $p$ is even a split monomorphism. The morphism $i$ is not an epimorphism since $\id_1 \circ i = ip \circ i$. The morphism $ip$ is not a epimorphism since it would imply that $i$ is an epimorphism.
+    proof: The morphism $p$ is even a split monomorphism. The morphism $i$ is not an epimorphism since $\id_1 \circ i = ip \circ i$. The morphism $ip$ is not an epimorphism since it would imply that $i$ is an epimorphism.

database/data/macros.yaml

@@ -123,6 +123,7 @@
 \Cone: \mathbf{Cone}
 \SemiGrp: \mathbf{SemiGrp}
 \Square: \mathbf{Square}
+\ForkSquare: \mathbf{ForkSquare}
 \Comp: \mathbf{Comp}
 \Fork: \mathbf{Fork}
 \Isom: \mathbf{Isom}