Add strong epimorphisms and strong monomorphisms

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

@@ -57,15 +57,6 @@
   proof: This is the definition of a mono-regular category.
   is_equivalence: false
 
-- id: strict_epi_and_mono_is_iso
-  assumptions:
-    - strict epimorphism
-    - monomorphism
-  conclusions:
-    - isomorphism
-  proof: 'Assume that $p : A \to B$ is a strict epimorphism and a monomorphism. Then $p$ is the joint coequalizer of all pairs $g,h : C \rightrightarrows A$ with $p \circ g = p \circ h$, which simplifies to $g = h$. Thus, any morphism $A \to T$ automatically coequalizes these pairs and therefore factors uniquely through $p$. This shows that $p$ is an isomorphism.'
-  is_equivalence: false
-
 - id: strict_mono_is_mono
   assumptions:
     - strict monomorphism
@@ -135,3 +126,59 @@
     - normal monomorphism
   proof: 'The equalizer of $g,h : B \rightrightarrows C$ is the kernel of $g-h : B \to C$.'
   is_equivalence: false
+
+- id: strong_mono_is_mono
+  assumptions:
+    - strong monomorphism
+  conclusions:
+    - monomorphism
+  proof: This holds by definition.
+  is_equivalence: false
+
+- id: strict_mono_is_strong
+  assumptions:
+    - strict monomorphism
+  conclusions:
+    - strong monomorphism
+  proof: >-
+    Consider a commutative diagram
+    $$\begin{CD} C @>e>> D \\ @VVV @VVV \\ A @>>m> B \end{CD}$$
+    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
+  assumptions:
+    - strong 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.
+  is_equivalence: false
+
+- id: strong_monos_are_no_epis
+  assumptions:
+    - strong monomorphism
+    - epimorphism
+  conclusions:
+    - isomorphism
+  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.
+  is_equivalence: false
+
+- id: strong_monos_collapse
+  assumptions:
+    - monomorphism
+  mapped_assumptions:
+    category:
+      - quotient-trivial
+  conclusions:
+    - strong monomorphism
+  proof: This is because any morphism is right orthogonal to any isomorphism.
+  is_equivalence: false

database/data/morphism-properties/strong epimorphism.yaml

@@ -0,0 +1,17 @@
+id: strong epimorphism
+relation: is a
+description: >-
+  A morphism $e : A \to B$ is a <i>strong epimorphism</i> if it is a epimorphism that is left orthogonal to any monomorphism. That is, for every commutative diagram
+  $$\begin{CD} A @>e>> B \\ @VVV @VVV \\ C @>>m> D \end{CD}$$
+  in which $m : C \to D$ is a monomorphism, there is a unique morphism $B \to C$ such that both triangles commute. Uniqueness is actually for free, and it suffices to demand commutativity of one triangle, as the other one follows.
+  $$\begin{CD} A @>e>> B \\ @VVV \swarrow @VVV \\ C @>>m> D \end{CD}$$
+  If the category has equalizers, the orthogonality condition already implies that $e$ is an epimorphism, but in general, we need to demand this.
+nlab_link: https://ncatlab.org/nlab/show/strong+epimorphism
+invariant_under_equivalences: true
+dual: strong monomorphism
+related:
+  - strict epimorphism
+  - epimorphism
+
+tags:
+  - types of epimorphisms

database/data/morphism-properties/strong monomorphism.yaml

@@ -0,0 +1,17 @@
+id: strong monomorphism
+relation: is a
+description: >-
+  A morphism $m : A \to B$ is a <i>strong monomorphism</i> if it is a monomorphism that is right orthogonal to any epimorphism. That is, for every commutative diagram
+  $$\begin{CD} C @>e>> D \\ @VVV @VVV \\ A @>>m> B \end{CD}$$
+  in which $e : C \to D$ is an epimorphism, there is a unique morphism $D \to A$ such that both triangles commute. Uniqueness is actually for free, and it suffices to demand commutativity of one triangle, as the other one follows.
+  $$\begin{CD} C @>e>> D \\ @VVV \swarrow @VVV \\ A @>>m> B \end{CD}$$
+  If the category has coequalizers, the orthogonality condition already implies that $m$ is a monomorphism, but in general, we need to demand this.
+nlab_link: https://ncatlab.org/nlab/show/strong+monomorphism
+invariant_under_equivalences: true
+dual: strong epimorphism
+related:
+  - strict monomorphism
+  - monomorphism
+
+tags:
+  - types of monomorphisms

database/data/morphisms/universal-morphism.yaml

@@ -0,0 +1,22 @@
+id: universal-morphism
+name: universal morphism
+notation: $!$
+category: walking_morphism
+description: 'This is the morphism $! : 0 \to 1$ in the <a href="/category/walking_morphism">walking morphism</a> $I$, see there for details.'
+nlab_link: null
+
+tags:
+  - category theory
+
+related: []
+
+satisfied_properties:
+  - property: monomorphism
+    proof: There is only one morphism with codomain $0$, namely $\id_0$.
+
+  - property: epimorphism
+    proof: There is only one morphism with domain $1$, namely $\id_1$.
+
+unsatisfied_properties:
+  - property: split monomorphism
+    proof: There is no morphism $1 \to 0$.

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

@@ -0,0 +1,30 @@
+id: walking-idempotent-presentation
+name: presentation of the walking idempotent
+notation: $F$
+category: Cat
+description: 'Let $I$ denote the <a href="/category/walking_morphism">walking morphism</a> and $\Idem$ denote the <a href="/category/walking_idempotent">walking idempotent</a>. In this entry, we consider the functor $F : I \to \Idem$ that sends the universal morphism $! : 0 \to 1$ to the universal idempotent $e : 0 \to 0$ and view $F$ as a morphism in $\Cat$. It provides an example of a strong epimorphism which is not strict.'
+nlab_link: null
+
+tags:
+  - category theory
+
+related: []
+
+satisfied_properties:
+  - property: strong epimorphism
+    proof: >-
+      First of all, $F$ is an epimorphism since it is surjective on objects and full. Now consider a commutative diagram of functors
+      $$\begin{CD}
+      I @>F>> \Idem \\ @V{U}VV @VV{V}V \\ \C @>>{M}> \D
+      \end{CD}$$
+      in which $M$ is a monomorphism, i.e. injective on objects and faithful. The functor $V$ corresponds to an idempotent endomorphism $v : Y \to Y$ in $\D$. The functor $U$ corresponds to a morphism $u : X \to X'$ in $\C$. Commutativity of the diagram means that $M(X) = M(X')$ and $M(u) = v$.
+      Since $M$ is injective on objects, we conclude $X = X'$. Since $M$ is faithful and $v$ is idempotent, we see that $u$ is idempotent. Thus, $u$ corresponds to a functor $\tilde{U} : \Idem \to \C$ with $M \circ \tilde{U} = U$.
+
+unsatisfied_properties:
+  - property: strict epimorphism
+    proof: >-
+      Let $B(\IN)$ denote the <a href="/category/BN">delooping of the additive monoid of natural numbers</a> whose single object is denoted $*$. Consider the functor $E : I \to B(\IN)$ defined by $E(!) = 1$. We claim that it coequalizes all pairs of functors that are coequalized by $F$.
+      Let $G,H : \C \rightrightarrows I$ be two functors with $FG = FH$, we need to prove $EG = EH$.
+      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$.