Add extremal monomorphisms and extremal epimorphisms

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
+
+![Diagram showing the types of epimorphisms](/img/epis.webp)
+
+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.
+
+Fun fact: This describes a category in itself, the composition of $P : X \Rightarrow Y$ and $Q : Y \Rightarrow Z$ is $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)
+
+### TeX code
+
+```
+\begin{tikzcd}[column sep=-30pt, row sep=40pt,nodes={inner sep=10pt}]
+& \text{isomorphism} \ar[Rightarrow]{dr} \ar[Rightarrow]{dl}  & & \\
+\text{split monomorphism} \ar[Rightarrow]{dr} && \text{effective monomorphism} \ar[Rightarrow]{dl} & \\
+ & \text{regular monomorphism} \ar[Rightarrow]{rr} & & \text{strict monomorphism} \ar[Rightarrow]{ul}[swap]{\text{pushouts}} \ar[Rightarrow]{d} \\
+ & \text{extremal monomorphism} \ar[Rightarrow]{u}{\text{coregular\;}} \ar[Rightarrow]{d} & & \text{strong monomorphism} \ar[Rightarrow]{ll} \\
+ & \text{monomorphism} \ar[Rightarrow]{urr}[swap]{\text{epi-regular}} &&
+\end{tikzcd}$$
+
+$$\begin{tikzcd}[column sep=-30pt, row sep=40pt,nodes={inner sep=10pt}]
+& \text{isomorphism} \ar[Rightarrow]{dr} \ar[Rightarrow]{dl}  & & \\
+\text{split epimorphism} \ar[Rightarrow]{dr} && \text{effective epimorphism} \ar[Rightarrow]{dl} & \\
+ & \text{regular epimorphism} \ar[Rightarrow]{rr} & & \text{strict epimorphism} \ar[Rightarrow]{ul}[swap]{\text{pullbacks}} \ar[Rightarrow]{d} \\
+ & \text{extremal epimorphism} \ar[Rightarrow]{u}{\text{regular\;}} \ar[Rightarrow]{d} & & \text{strong epimorphism} \ar[Rightarrow]{ll} \\
+ & \text{epimorphism} \ar[Rightarrow]{urr}[swap]{\text{mono-regular}} &&
+\end{tikzcd}
+```

database/data/categories/forked_commutative_square.yaml

@@ -0,0 +1,79 @@
+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$.'
+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.'
+    # TODO: add proof reference
+
+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.'
+
+  - 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.'
+    # TODO: add proof reference
+
+  - 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

@@ -75,9 +75,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}

database/data/morphism-implications/mono-epi-iso.yaml

@@ -12,7 +12,18 @@
     - split monomorphism
   conclusions:
     - regular monomorphism
-  proof: 'Let $f : A \to B$ be a split monomorphism, and choose a morphism $g : B \to A$ with $g \circ f = \id_A$. Then it is easy to check that $f$ is an equalizer of $\id_B, f \circ g : B \rightrightarrows B$.'
+  proof: 'Let $m : A \to B$ be a split monomorphism, and choose a morphism $e : B \to A$ with $e \circ m = \id_A$. Then it is easy to check that $m$ is an equalizer of $\id_B$ and the idempotent morphism $m \circ e : B \to B$.'
+  is_equivalence: false
+
+- id: split_mono_epi_is_iso
+  # This implication follows strictly from the others, but we add it
+  # because the other proofs use it and also to prevent long chains.
+  assumptions:
+    - split monomorphism
+    - epimorphism
+  conclusions:
+    - isomorphism
+  proof: 'Assume that $m : A \to B$ is a split monomorphism, and choose a morphism $e : B \to A$ with $e \circ m = \id_A$. Then $m \circ e \circ m = m = {\id_B} \circ m$. Thus, if $m$ is also an epimorphism, we conclude $m \circ e = \id_B$, showing that $m$ is an isomorphism with inverse $e$.'
   is_equivalence: false
 
 - id: mono_is_iso
@@ -70,7 +81,7 @@
     - regular monomorphism
   conclusions:
     - strict monomorphism
-  proof: 'Let $m : A \to B$ be the equalizer of $g,h : B \rightrightarrows C$. In particular, $m$ is a monomorphism. Let $t : T \to B$ be a monomorphism which equalizes all pairs that are equalized by $m$. In particular, $t$ equalizes $g,h$, i.e. $g \circ t = h \circ t$. By definition of an equalizer, this means that $t$ factors through $m$.'
+  proof: 'Let $m : A \to B$ be the equalizer of $f,g : B \rightrightarrows C$. In particular, $m$ is a monomorphism. Let $t : T \to B$ be a morphism that equalizes all pairs that are equalized by $m$. In particular, $t$ equalizes $f,g$, i.e. $f \circ t = g \circ t$. By definition of an equalizer, this means that $t$ factors through $m$.'
   is_equivalence: false
 
 - id: effective_mono_implies_regular_mono
@@ -91,9 +102,9 @@
     - effective monomorphism
   proof: >-
     Let $m : A \to B$ be a strict monomorphism in a category with pushouts. In particular, the pushout $B \sqcup_A B$ exists (and actually, we only need this pushout) with coprojections $i_1,i_2 : B \rightrightarrows B \sqcup_A B$ satisfying $i_1 \circ m = i_2 \circ m$.
-    To show that $m$ is the equalizer of $i_1,i_2$, let $t : T \to B$ be a morphism with $i_1 \circ t = i_2 \circ t$. If $g,h : B \rightrightarrows C$ is any parallel pair with $g \circ m = h \circ m$, it induces a morphism $(g;h) : B \sqcup_A B \to C$ with $(g;h) \circ i_1 = g$ and $(g;h) \circ i_2 = h$.
+    To show that $m$ is the equalizer of $i_1,i_2$, let $t : T \to B$ be a morphism with $i_1 \circ t = i_2 \circ t$. If $f,g : B \rightrightarrows C$ is any parallel pair with $f \circ m = g \circ m$, it induces a morphism $(f;g) : B \sqcup_A B \to C$ with $(f;g) \circ i_1 = f$ and $(f;g) \circ i_2 = g$.
     By composing these equations with $t$, we get
-    $$g \circ t = (g;h) \circ i_1 \circ t = (g;h) \circ i_2 \circ t = h \circ t.$$
+    $$f \circ t = (f;g) \circ i_1 \circ t = (f;g) \circ i_2 \circ t = g \circ t.$$
     Thus, $t$ equalizes every parallel pair that is equalized by $m$. Since $m$ is a strict monomorphism, $t$ factors through $m$.
   is_equivalence: false
 
@@ -124,7 +135,7 @@
       - preadditive
   conclusions:
     - normal monomorphism
-  proof: 'The equalizer of $g,h : B \rightrightarrows C$ is the kernel of $g-h : B \to C$.'
+  proof: 'The equalizer of $f,g : B \rightrightarrows C$ is the kernel of $f-g : B \to C$.'
   is_equivalence: false
 
 - id: strong_mono_is_mono
@@ -146,39 +157,83 @@
     where $e$ is an epimorphism and $m$ is a strict monomorphism. We need to show that $D \to B$ factors through $m$. It suffices to show that it equalizes all pairs $B \rightrightarrows T$ that are equalized by $m$. Since $e$ is an epimorphism, it suffices to check this for the composite $C \to D \to B$. This is equal to $C \to A \to B$, which factors through $m$ and hence equalizes the pair.
   is_equivalence: false
 
-- id: strong_monos_are_regular_in_coregular_category
+- id: extremal_mono_is_mono
+  assumptions:
+    - extremal monomorphism
+  conclusions:
+    - monomorphism
+  proof: This holds by definition.
+  is_equivalence: false
+
+- id: strong_mono_is_extremal
   assumptions:
     - strong monomorphism
+  conclusions:
+    - extremal monomorphism
+  proof: >-
+    Assume that $m : A \to B$ is a strong monomorphism that factors as $m = g \circ e$, where $e : A \to C$ is an epimorphism and $g : C \to B$ is any morphism. Then the commutative diagram
+    $$\begin{CD} A @>e>> C \\ @V{\id_A}VV @VV{g}V \\ A @>>m> B \end{CD}$$
+    can be filled with a morphism $h : C \to A$. In particular, $h \circ e = \id_A$. Thus, $e$ is an epimorphism and a split monomorphism, <a href="/morphism-implication/split_mono_epi_is_iso">hence</a> an isomorphism.
+  is_equivalence: false
+
+- id: extremal_mono_epi_is_iso
+  assumptions:
+    - extremal monomorphism
+    - epimorphism
+  conclusions:
+    - isomorphism
+  proof: This is obvious.
+  is_equivalence: false
+
+- id: extremal_monos_are_regular_in_coregular_category
+  assumptions:
+    - extremal monomorphism
   mapped_assumptions:
     category:
       - coregular
   conclusions:
     - regular monomorphism
   proof: >-
-    Let $m : A \to B$ be a strong monomorphism in a coregular category. We may factor it as $m = i \circ e$, where $i : C \to B$ is a regular monomorphism and $e : A \to C$ is an epimorphism. The orthogonality condition applied to the diagram
-    $$\begin{CD} A @>e>> C \\ @V{\id_A}VV @VV{i}V \\ A @>>m> B \end{CD}$$
-    shows that $e$ is a split monomorphism, hence an isomorphism. But then $m = i \circ e$ is a regular monomorphism as well.
+    Let $m : A \to B$ be an extremal monomorphism in a coregular category. By coregularity, we may factor it as $m = i \circ e$, where $i : C \to B$ is a regular monomorphism and $e : A \to C$ is an epimorphism. Since $m$ is an extremal monomorphism, $e$ is an isomorphism. Therefore, $m \cong i$ is a regular monomorphism.
+
+    The proof shows that the assumption of coregularity can be relaxed to the existence of (Epi, RegMono)-factorizations.
   is_equivalence: false
 
-- id: strong_monos_are_no_epis
+- id: extremal_mono_strong_criterion
   assumptions:
-    - strong monomorphism
-    - epimorphism
+    - extremal monomorphism
+  mapped_assumptions:
+    category:
+      - pushouts
   conclusions:
-    - isomorphism
+    - strong monomorphism
   proof: >-
-    Assume that $m : A \to B$ is a strong monomorphism which is also an epimorphism. Then we apply the orthogonality condition to
-    $$\begin{CD} A @>m>> B \\ @V{\id_A}VV @VV{\id_B}V \\ A @>>m> B \end{CD}$$
-    to conclude that $m$ is a split epimorphism, and hence an isomorphism.
+    Let $m : A \to B$ be an extremal monomorphism and consider a diagram
+    $$\begin{CD} C @>{e}>> D \\ @V{f}VV @VV{g}V \\ A @>>{m}> B \end{CD}$$
+    in which $e : C \to D$ is an epimorphism. Choose a pushout
+    $$\begin{CD} C @>{e}>> D \\ @V{f}VV @VV{u}V \\ A @>>{v}> P. \end{CD}$$
+    Here, $v$ is an epimorphism since $e$ is an epimorphism. Moreover, by the universal property of the pushout, there is a unique morphism $h : P \to B$ such that $h \circ v = m$ and $h \circ u = g$. Since $m$ is an extremal monomorphism, $v$ is an isomorphism. Then $v^{-1} \circ u : D \to A$ is the required filling of the first diagram, since
+    $$v^{-1} \circ u \circ e = v^{-1} \circ v \circ f = f.$$
+  is_equivalence: false
+
+- id: extremal_mono_balanced
+  assumptions:
+    - monomorphism
+  mapped_assumptions:
+    category:
+      - balanced
+  conclusions:
+    - extremal monomorphism
+  proof: Assume $m$ is a monomorphism that factors as $m = g \circ e$, where $e$ is an epimorphism. But then $e$ is also a monomorphism, and since the category is balanced, $e$ must be an isomorphism.
   is_equivalence: false
 
-- id: strong_monos_collapse
+- id: every_mono_strong_criterion
   assumptions:
     - monomorphism
   mapped_assumptions:
     category:
-      - quotient-trivial
+      - epi-regular
   conclusions:
     - strong monomorphism
-  proof: This is because any morphism is right orthogonal to any isomorphism.
+  proof: Any monomorphism is right orthogonal to any regular epimorphism because regular epimorphisms are strong (by combining <a href="/morphism-implication/regular_mono_is_strict">this result</a> and <a href="/morphism-implication/strict_mono_is_strong">this result</a>).
   is_equivalence: false