diff --git a/database/data/morphism-implications/mono-epi-iso.yaml b/database/data/morphism-implications/mono-epi-iso.yaml index 6c762cd9..ec2e03a3 100644 --- a/database/data/morphism-implications/mono-epi-iso.yaml +++ b/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 diff --git a/database/data/morphism-properties/strong epimorphism.yaml b/database/data/morphism-properties/strong epimorphism.yaml new file mode 100644 index 00000000..94b80d57 --- /dev/null +++ b/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 strong epimorphism 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 diff --git a/database/data/morphism-properties/strong monomorphism.yaml b/database/data/morphism-properties/strong monomorphism.yaml new file mode 100644 index 00000000..d12800f1 --- /dev/null +++ b/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 strong monomorphism 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 diff --git a/database/data/morphisms/universal-morphism.yaml b/database/data/morphisms/universal-morphism.yaml new file mode 100644 index 00000000..2a8ca413 --- /dev/null +++ b/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 walking morphism $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$. diff --git a/database/data/morphisms/walking-idempotent-presentation.yaml b/database/data/morphisms/walking-idempotent-presentation.yaml new file mode 100644 index 00000000..b7ab11e7 --- /dev/null +++ b/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 walking morphism and $\Idem$ denote the walking idempotent. 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 delooping of the additive monoid of natural numbers 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$.