diff --git a/content/foundations.md b/content/foundations.md index eb8d2ac34..9eda43438 100644 --- a/content/foundations.md +++ b/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) +visualization of three levels of size 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. diff --git a/content/relationships-epis-monos.md b/content/relationships-epis-monos.md new file mode 100644 index 000000000..20d296fcd --- /dev/null +++ b/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) + + + +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) + + diff --git a/database/data/categories/forked_commutative_square.yaml b/database/data/categories/forked_commutative_square.yaml new file mode 100644 index 000000000..782317776 --- /dev/null +++ b/database/data/categories/forked_commutative_square.yaml @@ -0,0 +1,149 @@ +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 + + - property: cosifted limits + proof: >- + Let $F : \I \to \ForkSquare$ be a diagram, where $\I$ is a small cosifted category. We need to show that the functor + $$\textstyle L : \ForkSquare^{\op} \to \Set, \, X \mapsto \lim_{i \in \I} \Hom(X,F(i))$$ + is representable. + + + Since $A$ is initial and $\I$ is connected, we have $L(A)=1$ (the singleton set). + + + Case 1: $F$ hits $A$. Then $L(X)= \varnothing$ for every $X \neq A$, since it maps to $\Hom(X,A) = \varnothing$. Moreover, we have $L(A)=1$. Therefore, $L \cong \Hom(-,A)$. + + + Case 2: $F$ hits $B$, but does not hit $A$. We claim that $F$ then does not hit $C$. In fact, if $F(i)=B$ and $F(j)=C$, since $\I$ is cosifted, there is a cospan + $$i \leftarrow k \rightarrow j,$$ + which induces a cospan + $$B \leftarrow F(k) \rightarrow C.$$ + But then $F(k)=A$ is forced, contradicting our assumption that $F$ does not hit $A$. Therefore, $F$ takes values in $\{B,D,E\}$. Since $B$ has a unique morphism to each of these objects and $\I$ is connected, we see that $L(B)=1$. Moreover, we have $L(C)=\varnothing$ since it maps to $\Hom(C,B)=\varnothing$, and for the same reason we have $L(D)=\varnothing$ and $L(E)=\varnothing$. From these values, it is clear that $L \cong \Hom(-,B)$. (There is a bijection for each object, and naturality is automatic since we are only dealing with sets with at most one element.) + + + Case 3: $F$ hits $C$, but does not hit $A$. This is symmetric to Case 2 and leads to $L \cong \Hom(-,C)$. In fact, there is an automorphism of $\ForkSquare$ that swaps $B$ and $C$. + + + Case 4: $F$ only hits $E$. Then $F$ is the constant functor with value $E$, since $\End(E)=\{\id_E\}$. Since $\I$ is connected, it follows that $L \cong \Hom(-,E)$. + + + Case 5: $F$ takes values in $\{D,E\}$ and hits $D$. In this case, we will show that $L \cong \Hom(-,D)$. Choose $i_0 \in \I$ with + $$F(i_0)=D.$$ + Since there is no morphism $E \to D = F(i_0)$, we have $L(E) = \varnothing$. We already know $L(A)=1$. Since $B$ has a unique morphism to each value of $F$ and $\I$ is connected, we see that $L(B)=1$. For the same reason, we have $L(C)=1$. Therefore, it remains to show that $L(D)=1$. + + + We first show that $L(D)$ has at most one element. Assume that $x,y \in L(D)$. For every $i \in \I$ we have morphisms $x_i,y_i : D \to F(i)$. Since $D$ has only one endomorphism, namely the identity, we must have $x_{i_0} = \id_D = y_{i_0}$. Since $\I$ is connected, it therefore remains to show that + $$x_i = y_i \iff x_j = y_j$$ + for morphisms $\alpha : i \to j$. Because of the relations + $$x_j = F(\alpha) \circ x_i, \quad y_j = F(\alpha) \circ y_i,$$ + the direction $\implies$ is clear. Now assume that $x_j = y_j$ holds. If $F(\alpha)$ is the identity, we have $x_i = y_i$. Otherwise, since $F$ takes only values in $\{D,E\}$, we must have $F(\alpha) \in \{u,v\}$ and hence $F(i)=D$ and $F(j)=E$. But then both $x_i$ and $y_i$ are endomorphisms of $D$ and therefore both equal to $\id_D$. + + + Finally, we will construct an element of $L(D)$ (and this is where we will use the full strength of the assumption that $\I$ is cosifted). For any $i \in \I$, choose a cospan + $$\begin{CD} i_0 @<{\beta}<< k @>{\alpha}>> i.\end{CD}$$ + It induces a cospan + $$\begin{CD} D @<{F(\beta)}<< F(k) @>{F(\alpha)}>> F(i).\end{CD}$$ + Since $F(k)$ is either $D$ or $E$, but has a morphism to $D$, it must be $D$, and $F(\beta)=\id_D$ is forced. Therefore, we may define + $$x_i := F(\alpha) : D \to F(i).$$ + We need to show that this morphism does not depend on the choice of the cospan. Since $\I$ is cosifted, the category of cospans over $(i_0,i)$ is connected. Thus, for another cospan + $$\begin{CD} i_0 @<{\beta'}<< k' @>{\alpha'}>> i.\end{CD}$$ + that induces another morphism $F(\alpha') : D \to F(i)$, we may assume that it receives a morphism from the given one: + $$\begin{CD} i_0 @<{\beta}<< k @>{\alpha}>> i \\ + @V{\id}VV @VV{\gamma}V @VV{\id}V \\ + i_0 @<<{\beta'}< k' @>>{\alpha'}> i + \end{CD}$$ + The induced diagram in $\ForkSquare$ is very simple, since $D$ has only one endomorphism, the identity: + $$\begin{CD} D @<{\id}<< D @>{F(\alpha)}>> F(i) \\ + @V{\id}VV @VV{\id}V @VV{\id}V \\ + D @<<{\id}< D @>>{F(\alpha')}> F(i) + \end{CD}$$ + Therefore, $F(\alpha) = F(\alpha')$. Therefore, $x_i : D \to F(i)$ is well-defined. + + + The morphisms $x_i : D \to F(i)$ are compatible with respect to morphisms $\gamma : i \to j$: If we use the cospan + $$\begin{CD} i_0 @<{\beta}<< k @>{\alpha}>> i\end{CD}$$ + to compute $x_i$, we use the cospan + $$\begin{CD} i_0 @<{\beta}<< k @>{\alpha}>> i @>{\gamma}>> j\end{CD}$$ + to compute $x_j$. Thus, + $$x_j = F(\gamma \circ \alpha) = F(\gamma) \circ F(\alpha) = F(\gamma) \circ x_i.$$ + Therefore, $x = (x_i)_{i \in \I}$ is a well-defined element of $L(D)$, and the proof is finished. + +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$.' diff --git a/database/data/categories/walking_commutative_square.yaml b/database/data/categories/walking_commutative_square.yaml index 9af901084..39504d5c0 100644 --- a/database/data/categories/walking_commutative_square.yaml +++ b/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: {} diff --git a/database/data/categories/walking_composable_pair.yaml b/database/data/categories/walking_composable_pair.yaml index 026b79355..6fe5a57b0 100644 --- a/database/data/categories/walking_composable_pair.yaml +++ b/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: {} diff --git a/database/data/categories/walking_coreflexive_pair.yaml b/database/data/categories/walking_coreflexive_pair.yaml index 777f7be30..2d3352482 100644 --- a/database/data/categories/walking_coreflexive_pair.yaml +++ b/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. diff --git a/database/data/categories/walking_fork.yaml b/database/data/categories/walking_fork.yaml index f5d44606b..fd3401c22 100644 --- a/database/data/categories/walking_fork.yaml +++ b/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. diff --git a/database/data/categories/walking_morphism.yaml b/database/data/categories/walking_morphism.yaml index 05c5fdd68..1eb68c2ee 100644 --- a/database/data/categories/walking_morphism.yaml +++ b/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: {} diff --git a/database/data/categories/walking_pair.yaml b/database/data/categories/walking_pair.yaml index 7df4c3065..2f09cf634 100644 --- a/database/data/categories/walking_pair.yaml +++ b/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: {} diff --git a/database/data/categories/walking_span.yaml b/database/data/categories/walking_span.yaml index 265ec3184..424548f4f 100644 --- a/database/data/categories/walking_span.yaml +++ b/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: {} diff --git a/database/data/categories/walking_splitting.yaml b/database/data/categories/walking_splitting.yaml index eaca453e3..5b26c59eb 100644 --- a/database/data/categories/walking_splitting.yaml +++ b/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. diff --git a/database/data/macros.yaml b/database/data/macros.yaml index 4d7178e67..652f1e185 100644 --- a/database/data/macros.yaml +++ b/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} diff --git a/database/data/morphism-implications/mono-epi-iso.yaml b/database/data/morphism-implications/mono-epi-iso.yaml index ec2e03a39..fdd418f3f 100644 --- a/database/data/morphism-implications/mono-epi-iso.yaml +++ b/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 @@ -38,14 +49,6 @@ proof: This holds by definition of a balanced category. is_equivalence: false -- id: regular_mono_is_mono - assumptions: - - regular monomorphism - conclusions: - - monomorphism - proof: This is an immediate consequence of the definition of an equalizer. - is_equivalence: false - - id: mono-regular_def assumptions: - monomorphism @@ -57,20 +60,12 @@ proof: This is the definition of a mono-regular category. is_equivalence: false -- id: strict_mono_is_mono - assumptions: - - strict monomorphism - conclusions: - - monomorphism - proof: This is trivial. - is_equivalence: false - - id: regular_mono_is_strict assumptions: - 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 +86,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,15 +119,7 @@ - preadditive conclusions: - 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. + proof: 'The equalizer of $f,g : B \rightrightarrows C$ is the kernel of $f-g : B \to C$.' is_equivalence: false - id: strict_mono_is_strong @@ -146,39 +133,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, hence 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 this result and this result). is_equivalence: false diff --git a/database/data/morphism-properties/effective epimorphism.yaml b/database/data/morphism-properties/effective epimorphism.yaml index 2726981ff..8a9095c04 100644 --- a/database/data/morphism-properties/effective epimorphism.yaml +++ b/database/data/morphism-properties/effective epimorphism.yaml @@ -1,9 +1,9 @@ id: effective epimorphism relation: is an description: >- - A morphism $p : A \to B$ is an effective epimorphism if the pullback $A \times_B A$ exists and $p$ is the coequalizer of the two projections $p_1,p_2 : A \times_B A \rightrightarrows A$. + A morphism $e : A \to B$ is an effective epimorphism if the pullback $A \times_B A$ exists and $e$ is the coequalizer of the two projections $p_1,p_2 : A \times_B A \rightrightarrows A$. - By the implications below, effective epimorphisms are closely related to strict and regular epimorphisms. Every effective epimorphism is regular and hence strict, and in a category with pullbacks, every strict epimorphism is effective. Thus, in categories with pullbacks, all three mentioned classes of epimorphisms coincide. + By the implications below, effective epimorphisms are closely related to strict and regular epimorphisms. Every effective epimorphism is regular and hence strict, and in a category with pullbacks, every strict epimorphism is effective. Thus, in categories with pullbacks, all three mentioned classes of epimorphisms coincide. See also this overview. nlab_link: https://ncatlab.org/nlab/show/effective+epimorphism invariant_under_equivalences: true dual: effective monomorphism diff --git a/database/data/morphism-properties/effective monomorphism.yaml b/database/data/morphism-properties/effective monomorphism.yaml index 29c7449f1..370bc44c6 100644 --- a/database/data/morphism-properties/effective monomorphism.yaml +++ b/database/data/morphism-properties/effective monomorphism.yaml @@ -3,7 +3,7 @@ relation: is an description: >- A morphism $m : A \to B$ is an effective monomorphism if the pushout $B \sqcup_A B$ exists and $m$ is the equalizer of the two coprojections $i_1,i_2 : B \rightrightarrows B \sqcup_A B$. - By the implications below, effective monomorphisms are closely related to strict and regular monomorphisms. Every effective monomorphism is regular and hence strict, and in a category with pushouts, every strict monomorphism is effective. Thus, in categories with pushouts, all three mentioned classes of monomorphisms coincide. + By the implications below, effective monomorphisms are closely related to strict and regular monomorphisms. Every effective monomorphism is regular and hence strict, and in a category with pushouts, every strict monomorphism is effective. Thus, in categories with pushouts, all three mentioned classes of monomorphisms coincide. See also this overview. nlab_link: https://ncatlab.org/nlab/show/effective+monomorphism invariant_under_equivalences: true dual: effective epimorphism diff --git a/database/data/morphism-properties/epimorphism.yaml b/database/data/morphism-properties/epimorphism.yaml index a03edcc3e..e9fb934bd 100644 --- a/database/data/morphism-properties/epimorphism.yaml +++ b/database/data/morphism-properties/epimorphism.yaml @@ -1,6 +1,6 @@ id: epimorphism relation: is an -description: 'A morphism $f : A \to B$ is an epimorphism if it is right-cancellative, i.e. if $g \circ f = h \circ f$ for two morphisms $g,h : B \rightrightarrows T$, then $g = h$. In many concrete categories appearing in practice, these are are a bit harder to understand than monomorphisms; in particular, epimorphisms usually are not to be confused with surjective structure-preserving maps.' +description: 'A morphism $e : A \to B$ is an epimorphism if it is right-cancellative, i.e. if $f \circ e = g \circ e$ for two morphisms $f,g : B \rightrightarrows T$, then $f = g$. In many concrete categories appearing in practice, these are are a bit harder to understand than monomorphisms; in particular, epimorphisms usually are not to be confused with surjective structure-preserving maps. Stronger types of epimorphisms (such as regular epimorphisms) are often much better understood.' nlab_link: https://ncatlab.org/nlab/show/epimorphism invariant_under_equivalences: true dual: monomorphism diff --git a/database/data/morphism-properties/extremal epimorphism.yaml b/database/data/morphism-properties/extremal epimorphism.yaml new file mode 100644 index 000000000..a49b054ad --- /dev/null +++ b/database/data/morphism-properties/extremal epimorphism.yaml @@ -0,0 +1,16 @@ +id: extremal epimorphism +relation: is an +description: >- + A morphism $e : A \to B$ is an extremal epimorphism if it is an epimorphism and whenever $e = m \circ g$ is a factorization in which $m$ is a monomorphism, then $m$ is an isomorphism. The condition that $e$ is an epimorphism follows from the factorization property when the category has equalizers, but in general, we need to explicitly demand it. + + By the implications below, extremal epimorphisms are closely related to strong epimorphisms: every strong epimorphism is extremal, and the converse holds when pullbacks exist. See also this overview. +nlab_link: https://ncatlab.org/nlab/show/extremal+epimorphism +invariant_under_equivalences: true +dual: extremal monomorphism +related: + - epimorphism + - strong epimorphism + - regular epimorphism + +tags: + - types of epimorphisms diff --git a/database/data/morphism-properties/extremal monomorphism.yaml b/database/data/morphism-properties/extremal monomorphism.yaml new file mode 100644 index 000000000..027b7f1f5 --- /dev/null +++ b/database/data/morphism-properties/extremal monomorphism.yaml @@ -0,0 +1,16 @@ +id: extremal monomorphism +relation: is an +description: >- + A morphism $m : A \to B$ is an extremal monomorphism if it is a monomorphism and whenever $m = g \circ e$ is a factorization in which $e$ is an epimorphism, then $e$ is an isomorphism. The condition that $m$ is a monomorphism follows from the factorization property when the category has coequalizers, but in general, we need to explicitly demand it. + + By the implications below, extremal monomorphisms are closely related to strong monomorphisms: every strong monomorphism is extremal, and the converse holds when pushouts exist. See also this overview. +nlab_link: https://ncatlab.org/nlab/show/extremal+monomorphism +invariant_under_equivalences: true +dual: extremal epimorphism +related: + - monomorphism + - strong monomorphism + - regular monomorphism + +tags: + - types of monomorphisms diff --git a/database/data/morphism-properties/isomorphism.yaml b/database/data/morphism-properties/isomorphism.yaml index ec0bb6472..58cad2477 100644 --- a/database/data/morphism-properties/isomorphism.yaml +++ b/database/data/morphism-properties/isomorphism.yaml @@ -7,6 +7,8 @@ dual: isomorphism related: - monomorphism - epimorphism + - split monomorphism + - split epimorphism tags: - invertibility diff --git a/database/data/morphism-properties/monomorphism.yaml b/database/data/morphism-properties/monomorphism.yaml index d93403028..7eb1cd30c 100644 --- a/database/data/morphism-properties/monomorphism.yaml +++ b/database/data/morphism-properties/monomorphism.yaml @@ -1,6 +1,6 @@ id: monomorphism relation: is a -description: 'A morphism $f : A \to B$ is a monomorphism if it is left-cancellative, i.e. if $f \circ g = f \circ h$ for two morphisms $g,h : T \rightrightarrows A$, then $g = h$. In many concrete categories appearing in practice, these are injective structure-preserving maps.' +description: 'A morphism $m : A \to B$ is a monomorphism if it is left-cancellative, i.e. if $m \circ f = m \circ g$ for two morphisms $f,g : T \rightrightarrows A$, then $f = g$. In many concrete categories appearing in practice, these are injective structure-preserving maps.' nlab_link: https://ncatlab.org/nlab/show/monomorphism invariant_under_equivalences: true dual: epimorphism diff --git a/database/data/morphism-properties/normal epimorphism.yaml b/database/data/morphism-properties/normal epimorphism.yaml index 4c0127434..7af486b9c 100644 --- a/database/data/morphism-properties/normal epimorphism.yaml +++ b/database/data/morphism-properties/normal epimorphism.yaml @@ -1,6 +1,6 @@ id: normal epimorphism relation: is a -description: 'A morphism $f : A \to B$ in a category with zero morphisms is a normal epimorphism if it is the cokernel of a morphism $g : C \to A$, i.e. the coequalizer of $g$ and the zero morphism $0 : C \to A$.' +description: 'A morphism $e : A \to B$ in a category with zero morphisms is a normal epimorphism if it is the cokernel of a morphism $f : C \to A$, i.e. the coequalizer of $f$ and the zero morphism $0_{C,A} : C \to A$.' nlab_link: https://ncatlab.org/nlab/show/normal+epimorphism invariant_under_equivalences: true dual: normal monomorphism diff --git a/database/data/morphism-properties/normal monomorphism.yaml b/database/data/morphism-properties/normal monomorphism.yaml index 77d421ff8..ee55c46e5 100644 --- a/database/data/morphism-properties/normal monomorphism.yaml +++ b/database/data/morphism-properties/normal monomorphism.yaml @@ -1,6 +1,6 @@ id: normal monomorphism relation: is a -description: 'A morphism $f : A \to B$ in a category with zero morphisms is a normal monomorphism if it is the kernel of a morphism $g : B \to C$, i.e. the equalizer of $g$ and the zero morphism $0 : B \to C$.' +description: 'A morphism $m : A \to B$ in a category with zero morphisms is a normal monomorphism if it is the kernel of a morphism $f : B \to C$, i.e. the equalizer of $f$ and the zero morphism $0_{B,C} : B \to C$.' nlab_link: https://ncatlab.org/nlab/show/normal+monomorphism invariant_under_equivalences: true dual: normal epimorphism diff --git a/database/data/morphism-properties/regular epimorphism.yaml b/database/data/morphism-properties/regular epimorphism.yaml index 46069ac4b..8b133b85e 100644 --- a/database/data/morphism-properties/regular epimorphism.yaml +++ b/database/data/morphism-properties/regular epimorphism.yaml @@ -1,6 +1,6 @@ id: regular epimorphism relation: is a -description: 'A morphism $f : A \to B$ is a regular epimorphism if it is the coequalizer of a pair of morphisms $g,h : C \rightrightarrows A$. In many categories appearing in practice, this is the same as a quotient.' +description: 'A morphism $e : A \to B$ is a regular epimorphism if it is the coequalizer of a pair of morphisms $f,g : C \rightrightarrows A$. In many categories appearing in practice, this is the same as a quotient. This property is strongly related to other types of epimorphisms by the implications below; see also this overview.' nlab_link: https://ncatlab.org/nlab/show/regular+epimorphism invariant_under_equivalences: true dual: regular monomorphism @@ -9,6 +9,7 @@ related: - effective epimorphism - strict epimorphism - normal epimorphism + - extremal epimorphism tags: - types of epimorphisms diff --git a/database/data/morphism-properties/regular monomorphism.yaml b/database/data/morphism-properties/regular monomorphism.yaml index 4d7834bc0..9ec53f569 100644 --- a/database/data/morphism-properties/regular monomorphism.yaml +++ b/database/data/morphism-properties/regular monomorphism.yaml @@ -1,6 +1,6 @@ id: regular monomorphism relation: is a -description: 'A morphism $f : A \to B$ is a regular monomorphism if it is the equalizer of a pair of morphisms $g,h : B \rightrightarrows C$. In many categories appearing in practice, this is the same as an embedding.' +description: 'A morphism $m : A \to B$ is a regular monomorphism if it is the equalizer of a pair of morphisms $f,g : B \rightrightarrows C$. In many categories appearing in practice, this is the same as an embedding. This property is strongly related to other types of monomorphisms by the implications below; see also this overview.' nlab_link: https://ncatlab.org/nlab/show/regular+monomorphism invariant_under_equivalences: true dual: regular epimorphism @@ -9,6 +9,7 @@ related: - effective monomorphism - strict monomorphism - normal monomorphism + - extremal monomorphism tags: - types of monomorphisms diff --git a/database/data/morphism-properties/split epimorphism.yaml b/database/data/morphism-properties/split epimorphism.yaml index 8f25c30af..71867c708 100644 --- a/database/data/morphism-properties/split epimorphism.yaml +++ b/database/data/morphism-properties/split epimorphism.yaml @@ -1,11 +1,12 @@ id: split epimorphism relation: is a -description: 'A morphism $f : A \to B$ is a split epimorphism if there is a morphism $g : B \to A$ with $f \circ g = \id_B$.' +description: 'A morphism $e : A \to B$ is a split epimorphism if there is a morphism $m : B \to A$ with $e \circ m = \id_B$.' nlab_link: https://ncatlab.org/nlab/show/split+epimorphism invariant_under_equivalences: true dual: split monomorphism related: - epimorphism + - isomorphism tags: - types of epimorphisms diff --git a/database/data/morphism-properties/split monomorphism.yaml b/database/data/morphism-properties/split monomorphism.yaml index 5c63ebd9b..914ef0ff8 100644 --- a/database/data/morphism-properties/split monomorphism.yaml +++ b/database/data/morphism-properties/split monomorphism.yaml @@ -1,11 +1,12 @@ id: split monomorphism relation: is a -description: 'A morphism $f : A \to B$ is a split monomorphism if there is a morphism $g : B \to A$ with $g \circ f = \id_A$.' +description: 'A morphism $m : A \to B$ is a split monomorphism if there is a morphism $e : B \to A$ with $e \circ m = \id_A$.' nlab_link: https://ncatlab.org/nlab/show/split+monomorphism invariant_under_equivalences: true dual: split epimorphism related: - monomorphism + - isomorphism tags: - types of monomorphisms diff --git a/database/data/morphism-properties/strict epimorphism.yaml b/database/data/morphism-properties/strict epimorphism.yaml index 25162d5ca..d8010a8b0 100644 --- a/database/data/morphism-properties/strict epimorphism.yaml +++ b/database/data/morphism-properties/strict epimorphism.yaml @@ -1,9 +1,9 @@ id: strict epimorphism relation: is a description: >- - A morphism $p : A \to B$ is a strict epimorphism if it is the joint coequalizer of all pairs of morphisms $g,h : C \rightrightarrows A$ that it coequalizes. That is, $p$ is an epimorphism, and a morphism $t : A \to T$ factors through $p$ if we have $t \circ g = t \circ h$ for all morphisms $g,h : C \rightrightarrows A$ that satisfy $p \circ g = p \circ h$. That is, the minimal requirement for a morphism to factor through $p$ is actually sufficient. + A morphism $e : A \to B$ is a strict epimorphism if it is the joint coequalizer of all pairs of morphisms $f,g : C \rightrightarrows A$ that it coequalizes. That is, $e$ is an epimorphism, and a morphism $t : A \to T$ factors through $e$ if we have $t \circ f = t \circ g$ for all morphisms $f,g : C \rightrightarrows A$ that satisfy $e \circ f = e \circ g$. That is, the minimal requirement for a morphism to factor through $e$ is actually sufficient. - By the implications below, strict epimorphisms are closely related to effective and regular epimorphisms. Every effective epimorphism is regular and hence strict, and in a category with pullbacks, every strict epimorphism is effective. Thus, in categories with pullbacks, all three mentioned classes of epimorphisms coincide. + By the implications below, strict epimorphisms are closely related to effective and regular epimorphisms. Every effective epimorphism is regular and hence strict, and in a category with pullbacks, every strict epimorphism is effective. Thus, in categories with pullbacks, all three mentioned classes of epimorphisms coincide. See also this overview. nlab_link: https://ncatlab.org/nlab/show/strict+epimorphism invariant_under_equivalences: true dual: strict monomorphism diff --git a/database/data/morphism-properties/strict monomorphism.yaml b/database/data/morphism-properties/strict monomorphism.yaml index df2623ecc..7ed0f4ba8 100644 --- a/database/data/morphism-properties/strict monomorphism.yaml +++ b/database/data/morphism-properties/strict monomorphism.yaml @@ -1,9 +1,9 @@ id: strict monomorphism relation: is a description: >- - A morphism $m : A \to B$ is a strict monomorphism if it is the joint equalizer of all pairs of morphisms $g,h : B \rightrightarrows C$ that it equalizes. That is, $m$ is a monomorphism, and a morphism $t : T \to B$ factors through $m$ if we have $g \circ t = h \circ t$ for all morphisms $g,h : B \rightrightarrows C$ that satisfy $g \circ m = h \circ m$. That is, the minimal requirement for a morphism to factor through $m$ is actually sufficient. + A morphism $m : A \to B$ is a strict monomorphism if it is the joint equalizer of all pairs of morphisms $f,g : B \rightrightarrows C$ that it equalizes. That is, $m$ is a monomorphism, and a morphism $t : T \to B$ factors through $m$ if we have $f \circ t = g \circ t$ for all morphisms $f,g : B \rightrightarrows C$ that satisfy $f \circ m = g \circ m$. That is, the minimal requirement for a morphism to factor through $m$ is actually sufficient. - By the implications below, strict monomorphisms are closely related to effective and regular monomorphisms. Every effective monomorphism is regular and hence strict, and in a category with pushouts, every strict monomorphism is effective. Thus, in categories with pushouts, all three mentioned classes of monomorphisms coincide. + By the implications below, strict monomorphisms are closely related to effective and regular monomorphisms. Every effective monomorphism is regular and hence strict, and in a category with pushouts, every strict monomorphism is effective. Thus, in categories with pushouts, all three mentioned classes of monomorphisms coincide. See also this overview. nlab_link: https://ncatlab.org/nlab/show/strict+monomorphism invariant_under_equivalences: true dual: strict epimorphism diff --git a/database/data/morphism-properties/strong epimorphism.yaml b/database/data/morphism-properties/strong epimorphism.yaml index 94b80d571..b3b1cb437 100644 --- a/database/data/morphism-properties/strong epimorphism.yaml +++ b/database/data/morphism-properties/strong epimorphism.yaml @@ -1,16 +1,21 @@ 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 + A morphism $e : A \to B$ is a strong epimorphism if it is an 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. + in which $m : C \to D$ is a monomorphism, there is a unique morphism $B \to C$ such that both triangles commute. $$\begin{CD} A @>e>> B \\ @VVV \swarrow @VVV \\ C @>>m> D \end{CD}$$ + Uniqueness is actually for free, and it suffices to demand commutativity of one triangle, as the other one follows. + If the category has equalizers, the orthogonality condition already implies that $e$ is an epimorphism, but in general, we need to demand this. + + By the implications below, strong epimorphisms are closely related to extremal epimorphisms: every strong epimorphism is extremal, and the converse holds when pullbacks exist. See also this overview. nlab_link: https://ncatlab.org/nlab/show/strong+epimorphism invariant_under_equivalences: true dual: strong monomorphism related: - strict epimorphism + - extremal epimorphism - epimorphism tags: diff --git a/database/data/morphism-properties/strong monomorphism.yaml b/database/data/morphism-properties/strong monomorphism.yaml index d12800f10..2b244eb40 100644 --- a/database/data/morphism-properties/strong monomorphism.yaml +++ b/database/data/morphism-properties/strong monomorphism.yaml @@ -3,14 +3,19 @@ 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. + in which $e : C \to D$ is an epimorphism, there is a unique morphism $D \to A$ such that both triangles commute. $$\begin{CD} C @>e>> D \\ @VVV \swarrow @VVV \\ A @>>m> B \end{CD}$$ + Uniqueness is actually for free, and it suffices to demand commutativity of one triangle, as the other one follows. + If the category has coequalizers, the orthogonality condition already implies that $m$ is a monomorphism, but in general, we need to demand this. + + By the implications below, strong monomorphisms are closely related to extremal monomorphisms: every strong monomorphism is extremal, and the converse holds when pushouts exist. See also this overview. nlab_link: https://ncatlab.org/nlab/show/strong+monomorphism invariant_under_equivalences: true dual: strong epimorphism related: - strict monomorphism + - extremal monomorphism - monomorphism tags: diff --git a/database/data/morphisms/extremal-not-strong-example.yaml b/database/data/morphisms/extremal-not-strong-example.yaml new file mode 100644 index 000000000..1c050c123 --- /dev/null +++ b/database/data/morphisms/extremal-not-strong-example.yaml @@ -0,0 +1,22 @@ +id: extremal-not-strong-example +name: example of a non-strong extremal monomorphism +notation: $m$ +category: forked_commutative_square +description: 'This is the morphism $m : C \to D$ from the forked commutative square, see details there. It provides an example of an extremal monomorphism which is not strong, and this is the only reason we have added this morphism and its category to the database.' +nlab_link: null + +tags: + - category theory + +related: [] + +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$). + +unsatisfied_properties: + - property: strong monomorphism + proof: >- + The category contains a commutative diagram + $$\begin{CD} A @>e>> B \\ @V{f}VV @VV{g}V \\ C @>>m> D \end{CD}$$ + in which $e$ is an epimorphism, but there is no morphism $B \to C$ at all. diff --git a/database/data/special-morphism-rules.yaml b/database/data/special-morphism-rules.yaml index 0c72983f6..b65d572a7 100644 --- a/database/data/special-morphism-rules.yaml +++ b/database/data/special-morphism-rules.yaml @@ -3,6 +3,11 @@ description: every morphism proof: The category is a groupoid. +- property: gaunt + type: isomorphisms + description: only the identities + proof: The category is gaunt. + - property: thin type: monomorphisms description: every morphism @@ -57,3 +62,13 @@ type: regular epimorphisms description: same as epimorphisms proof: The category is epi-regular. + +- property: regular-subobject-trivial + type: regular monomorphisms + description: same as isomorphisms + proof: The category is regular-subobject-trivial. + +- property: regular-quotient-trivial + type: regular epimorphisms + description: same as isomorphisms + proof: The category is regular-quotient-trivial. diff --git a/src/routes/[type]-implications/+page.svelte b/src/routes/[type]-implications/+page.svelte index c3ba82ca5..46c8dbcaf 100644 --- a/src/routes/[type]-implications/+page.svelte +++ b/src/routes/[type]-implications/+page.svelte @@ -47,6 +47,12 @@ each morphism whenever applicable. Moreover, implications are automatically dualized when the corresponding dual properties exist.

+ +

+ See this page for a graphical + overview of the relationships between the various types of epimorphisms and + monomorphisms. +

{/if}

diff --git a/src/routes/content/[id]/+page.svelte b/src/routes/content/[id]/+page.svelte index 8c722cbb6..6fdb0219c 100644 --- a/src/routes/content/[id]/+page.svelte +++ b/src/routes/content/[id]/+page.svelte @@ -58,9 +58,13 @@ line-height: 1.6; :global(img) { - width: min(100%, 30rem); + border-radius: 0.5rem; + border: 1px solid var(--secondary-outline-color); + } + + :global(img.small) { margin-inline: auto; - border-radius: 1rem; + width: min(100%, 30rem); } :global(svg.diagram) { @@ -96,5 +100,16 @@ :global(p:has(span.qed:only-child)) { height: 1lh; } + + :global(pre) { + padding: 1rem; + border-radius: 0.75rem; + font-size: 0.875rem; + background-color: var(--secondary-bg-color); + } + + :global(pre code) { + white-space: pre-wrap; + } } diff --git a/static/img/epis.webp b/static/img/epis.webp new file mode 100644 index 000000000..48573724f Binary files /dev/null and b/static/img/epis.webp differ diff --git a/static/img/monos.webp b/static/img/monos.webp new file mode 100644 index 000000000..1b1fece22 Binary files /dev/null and b/static/img/monos.webp differ