diff --git a/content/Top-embeds-in-LRS.md b/content/Top-embeds-in-LRS.md
index be32010b..d560aaf7 100644
--- a/content/Top-embeds-in-LRS.md
+++ b/content/Top-embeds-in-LRS.md
@@ -11,7 +11,9 @@ For much of this development, we will be dealing with the case of $\LRS_k$ where
The forgetful functor $U : \LRS_k \to \Top$ has a right adjoint $K : \Top \to \LRS_k$ of equipping a topological space $X$ with the constant sheaf $\underline{k}$. Furthermore, the functor $K$ is fully faithful, thus making $\Top$ into a reflective subcategory of $\LRS_k$.
:::
-_Proof._ In this adjunction, the counit $UK \to \id$ is just the identity. To describe the unit $\id \to KU$, we need to define a morphism $(X, \O_X) \to (X, \underline{k})$ for any locally ringed space $(X, \O_X)$ over $k$. This morphism will be the identity on topological spaces, and the pullback operation $\underline{k} \to \O_X$ will be the unique morphism of sheaves induced by the given structure of $\O_X$ as a sheaf of $k$-algebras. It is now straightforward to check this indeed defines an adjunction; and since the counit is an isomorphism, that implies that $K$ is fully faithful. $\square$
+::: Proof
+In this adjunction, the counit $UK \to \id$ is just the identity. To describe the unit $\id \to KU$, we need to define a morphism $(X, \O_X) \to (X, \underline{k})$ for any locally ringed space $(X, \O_X)$ over $k$. This morphism will be the identity on topological spaces, and the pullback operation $\underline{k} \to \O_X$ will be the unique morphism of sheaves induced by the given structure of $\O_X$ as a sheaf of $k$-algebras. It is now straightforward to check this indeed defines an adjunction; and since the counit is an isomorphism, that implies that $K$ is fully faithful.
+:::
We now show that this reflective subcategory is in fact also a coreflective subcategory. Recall that for $f \in \O_X(U)$ we have its vanishing set $V(f) \coloneqq \{x\in U : f \in \m_{X,x}\} = \{x \in U : f(x) = 0\}$, where $f(x) \in \kappa(x)$ is the image of $f_x \in \O_{X,x}$ in the residue field.
@@ -19,7 +21,8 @@ We now show that this reflective subcategory is in fact also a coreflective subc
For each object $X$ of $\LRS_k$, let $X_0$ be the set of points $x \in X$ such that the induced morphism from $k$ to the residue field $\kappa(x)$ is an isomorphism. We give $X_0$ the following strengthening of the subspace topology: it will be the topology where a neighborhood subbasis at $x \in X_0$ is the collection of sets of the form $X_0 \cap V(f)$ where $f \in \O_X(U)$ for some neighborhood $U$ of $x$ in $X$, and $x \in V(f)$. Then $X \mapsto X_0$ defines a functor $S : \LRS_k \to \Top$ that is right adjoint to $K$.
:::
-_Proof._ First, to see that $S$ is a functor, suppose we have a morphism $f : (X, \O_X) \to (Y, \O_Y)$. Then for $x \in X_0$, we have a sequence $k \to \kappa(f(x)) \to \kappa(x)$ where the composition is an isomorphism. Thus, $\kappa(f(x)) \to \kappa(x)$ is a surjective morphism of fields, and therefore an isomorphism. It follows that $k \to \kappa(f(x))$ is also an isomorphism of fields, so $f(x) \in Y_0$. To see that the restriction map $X_0 \to Y_0$ is continuous, suppose $g \in \O_Y(V)$ is such that $f(x) \in V(g)$. Then $x \in V(f^\sharp g)$, and
+::: Proof
+First, to see that $S$ is a functor, suppose we have a morphism $f : (X, \O_X) \to (Y, \O_Y)$. Then for $x \in X_0$, we have a sequence $k \to \kappa(f(x)) \to \kappa(x)$ where the composition is an isomorphism. Thus, $\kappa(f(x)) \to \kappa(x)$ is a surjective morphism of fields, and therefore an isomorphism. It follows that $k \to \kappa(f(x))$ is also an isomorphism of fields, so $f(x) \in Y_0$. To see that the restriction map $X_0 \to Y_0$ is continuous, suppose $g \in \O_Y(V)$ is such that $f(x) \in V(g)$. Then $x \in V(f^\sharp g)$, and
$$X_0 \cap f^{-1}(Y_0 \cap V(g)) = X_0 \cap V(f^\sharp g)$$
where $f^\sharp g \in \O_X(f^{-1}(V))$. In other words, we have shown that the inverse image in $X_0$ of any subbasic neighborhood of $f(x)$ is a neighborhood of $x$.
@@ -27,7 +30,8 @@ Now if we apply the functor $S$ to a space of the form $(X, \underline{k})$, the
As for the counit $KS \to \id$, for any locally ringed space $(X, \O_X)$ over $k$ we need to define a morphism $(X_0, \underline{k}) \to (X, \O_X)$. The map of topological spaces will be the inclusion map $i : X_0 \hookrightarrow X$, which is continuous since in particular for $U$ an open neighborhood of $x \in X_0$ we have $X_0 \cap U = X_0 \cap V(0_U)$, where $0_U \in \O_X(U)$ is the zero element. The pullback map $\O_X \to i_* \underline{k}$ takes $f \in \O_X(U)$ to the function $X_0 \cap U \to k$ where $x \in X_0 \cap U$ maps to the inverse image of $f(x) \in \kappa(x)$ under the isomorphism $k \to \kappa(x)$. An alternative description of this pullback is that $x \in X_0 \cap U$ maps to the unique $a\in k$ such that $x \in V(f-a)$. Since $X_0 \cap V(f-a)$ is a neighborhood of $x$ in $X_0$ by definition, this shows that we get a locally constant function to $k$ as required.
-From here, it is straightforward to show that this does in fact define an adjunction. $\square$
+From here, it is straightforward to show that this does in fact define an adjunction.
+:::
_Remark._ In the special case where $k$ is a finite field, we have
$$\textstyle X_0 \cap V(f) = \bigcap_{a \in k^\times} (X_0 \cap D(f-a)),$$
@@ -37,7 +41,9 @@ which is already open in the subspace topology. Therefore, in this case, $X_0$ i
For any non-trivial commutative ring $R$, fix a quotient field $k$. Then the functor $K_R : \Top \to \LRS_R$ of equipping a topological space with the constant sheaf $\underline{k}$ is fully faithful; has a right adjoint; and preserves all inhabited limits.
:::
-_Proof._ The functor $K_R$ is the composition of $K : \Top \to \LRS_k$ and the forgetful functor $\LRS_k \to \LRS_R$. Since $\LRS_k$ is equivalent to the slice category of $\LRS_R$ over the subterminal object $\Spec k$, the forgetful functor is fully faithful; has right adjoint ${-} \times \Spec k$; and preserves all inhabited limits. Therefore, from the previously established results on $K$, the result follows. $\square$
+::: Proof
+The functor $K_R$ is the composition of $K : \Top \to \LRS_k$ and the forgetful functor $\LRS_k \to \LRS_R$. Since $\LRS_k$ is equivalent to the slice category of $\LRS_R$ over the subterminal object $\Spec k$, the forgetful functor is fully faithful; has right adjoint ${-} \times \Spec k$; and preserves all inhabited limits. Therefore, from the previously established results on $K$, the result follows.
+:::
::: Corollary 4
Let $R$ be any non-trivial commutative ring. Then:
@@ -48,4 +54,6 @@ Let $R$ be any non-trivial commutative ring. Then:
(e) $\LRS_R$ does not have effective cocongruences.
:::
-_Proof._ We already know that $\Top$ does not satisfy any of these properties. In order to conclude that $\LRS_R$ does not satisfy any of them either, we fix a quotient field of $R$ as above and consider the functor $K_R$. In each case, this is an easy application of a contrapositive of a result from [here](/content/subcategories) to the functor $K_R$. Namely, (a) follows from Lemma 5; (b) from Lemma 4; (c) from Lemma 7; (d) from the dual of Lemma 2 with the observation that $K_R$ preserves epimorphisms since it has a right adjoint; and (e) from the dual of Lemma 8. $\square$
+::: Proof
+We already know that $\Top$ does not satisfy any of these properties. In order to conclude that $\LRS_R$ does not satisfy any of them either, we fix a quotient field of $R$ as above and consider the functor $K_R$. In each case, this is an easy application of a contrapositive of a result from [here](/content/subcategories) to the functor $K_R$. Namely, (a) follows from Lemma 5; (b) from Lemma 4; (c) from Lemma 7; (d) from the dual of Lemma 2 with the observation that $K_R$ preserves epimorphisms since it has a right adjoint; and (e) from the dual of Lemma 8.
+:::
diff --git a/content/cocongruences_of_groups.md b/content/cocongruences_of_groups.md
index 62d8956a..b17046b1 100644
--- a/content/cocongruences_of_groups.md
+++ b/content/cocongruences_of_groups.md
@@ -27,7 +27,8 @@ is also a monomorphism.
The category $\Grp$ has good pushouts of monomorphisms.
:::
-_Proof._ Consider a diagram as above. We regard every monomorphism in it as an inclusion. Choose a system of representatives $S \subseteq B$ for the right $A$-cosets in $B$, meaning that the multiplication map $\cdot : A \times S \to B$ is bijective. Likewise, choose $T \subseteq C$ such that the multiplication map $\cdot : A \times T \to C$ is bijective. We may assume that $1 \in S$ and $1 \in T$.
+::: Proof
+Consider a diagram as above. We regard every monomorphism in it as an inclusion. Choose a system of representatives $S \subseteq B$ for the right $A$-cosets in $B$, meaning that the multiplication map $\cdot : A \times S \to B$ is bijective. Likewise, choose $T \subseteq C$ such that the multiplication map $\cdot : A \times T \to C$ is bijective. We may assume that $1 \in S$ and $1 \in T$.
It is well known (see, for example, Serre's book _Trees_, Ch. I, ยง1, Thm. 1) that every element of the amalgamated free product $B \sqcup_A C$ has a unique representation of the form
$$w = a \cdot x_1 \cdots x_n,$$
@@ -41,13 +42,15 @@ is injective. Indeed, if $b_1,b_2 \in B$ satisfy $A' b_1 = A' b_2$, then $b_1 b_
Therefore, we may extend $S$ to a system of representatives $S' \subseteq B'$ for the right $A'$-cosets in $B'$. Likewise, we may extend $T$ to a system of representatives $T' \subseteq C'$ for the right $A'$-cosets in $C'$.
-With respect to these systems, an element $w \in B \sqcup_A C$ written in normal form as above remains in normal form after being mapped to $B' \sqcup_{A'} C'$. This shows that the induced map is injective. $\square$
+With respect to these systems, an element $w \in B \sqcup_A C$ written in normal form as above remains in normal form after being mapped to $B' \sqcup_{A'} C'$. This shows that the induced map is injective.
+:::
::: Proposition 2
Let $\C$ be a balanced category with good pushouts of monomorphisms and equalizers of monomorphisms. Then every cocongruence in $\C$ is effective.
:::
-_Proof._ Let $X \in \C$ be an object, and let $i_1,i_2 : X \rightrightarrows Y$ be a cocongruence. Since it is coreflexive, there exists a morphism $r : Y \to X$ satisfying
+::: Proof
+Let $X \in \C$ be an object, and let $i_1,i_2 : X \rightrightarrows Y$ be a cocongruence. Since it is coreflexive, there exists a morphism $r : Y \to X$ satisfying
$$r \circ i_1 = \id_X, \quad r \circ i_2 = \id_X.$$
@@ -96,7 +99,8 @@ Since $\C$ has good pushouts of monomorphisms, it suffices to verify that both s
$$a = r \circ i_1 \circ a = r \circ i_2 \circ b = b.$$
-Thus, $a$ is simply a morphism equalizing $i_1$ and $i_2$, so it factors uniquely through $e$. $\square$
+Thus, $a$ is simply a morphism equalizing $i_1$ and $i_2$, so it factors uniquely through $e$.
+:::
::: Corollary 3
Every cocongruence in the category $\Grp$ is effective.
diff --git a/content/cogenerators_in_product_categories.md b/content/cogenerators_in_product_categories.md
index 26f8fc5c..307dfd35 100644
--- a/content/cogenerators_in_product_categories.md
+++ b/content/cogenerators_in_product_categories.md
@@ -9,5 +9,6 @@ description: How to construct a cogenerator in a product category
For a family of categories $(\C_i)_{i \in I}$, each having a cogenerator $Q_i$ which is weakly terminal, the object $(Q_i)_{i \in I}$ is a cogenerator in the product category $\prod_{i \in I} \C_i$.
:::
-_Proof._
-Let $(f_i: A_i \to B_i)_{i \in I}$ and $(g_i: A_i \to B_i)_{i \in I}$ be two parallel morphisms in the product category which are coequalized by any morphism $(B_i \to Q_i)_{i \in I}$. Let $i_0 \in I$. We claim that $f_{i_0},g_{i_0} : A_{i_0} \rightrightarrows B_{i_0}$ are coequalized by all morphisms $B_{i_0} \to Q_{i_0}$, and hence are equal: Indeed, for all $i \neq i_0$ we may choose some morphism $B_i \to Q_i$ since $Q_i$ is weakly terminal. Thus, the morphism $B_{i_0} \to Q_{i_0}$ extends to a morphism $(B_i \to Q_i)_{i \in I}$ in the product category. By assumption, it coequalizes $(f_i)_{i \in I}$ and $(g_i)_{i \in I}$. By looking at the $i_0$-component, we are done. $\square$
+::: Proof
+Let $(f_i: A_i \to B_i)_{i \in I}$ and $(g_i: A_i \to B_i)_{i \in I}$ be two parallel morphisms in the product category which are coequalized by any morphism $(B_i \to Q_i)_{i \in I}$. Let $i_0 \in I$. We claim that $f_{i_0},g_{i_0} : A_{i_0} \rightrightarrows B_{i_0}$ are coequalized by all morphisms $B_{i_0} \to Q_{i_0}$, and hence are equal: Indeed, for all $i \neq i_0$ we may choose some morphism $B_i \to Q_i$ since $Q_i$ is weakly terminal. Thus, the morphism $B_{i_0} \to Q_{i_0}$ extends to a morphism $(B_i \to Q_i)_{i \in I}$ in the product category. By assumption, it coequalizes $(f_i)_{i \in I}$ and $(g_i)_{i \in I}$. By looking at the $i_0$-component, we are done.
+:::
diff --git a/content/comphaus_copresentable.md b/content/comphaus_copresentable.md
index 3c2e38f2..3e2bf1ce 100644
--- a/content/comphaus_copresentable.md
+++ b/content/comphaus_copresentable.md
@@ -15,31 +15,33 @@ We first prove a couple preliminary results.
Let $\I$ be a cofiltered category, and let $X : \I \to \CompHaus$ be a cofiltered diagram in which $X_i$ is non-empty for each $i\in \I$. Then $\lim_{i\in \I} X_i$ is also non-empty.
:::
-_Proof._
+::: Proof
Consider the product space $\prod_{i\in \I} X_i$. Now for each morphism $f : i \to j$ in $\I$, define the subset
$$\textstyle E_f \coloneqq \bigl\{ x \in \prod_{i \in \I} X_i \mid X_f(x_i) = x_j \bigr\}.$$
Then each $E_f$ is a closed subset.
Next, we prove that the collection $\{ E_f : f \in \Mor(\I) \}$ has the finite intersection property, i.e. that $\bigcap_{f\in F} E_f$ is non-empty for every finite set $F \subseteq \Mor(\I)$. For $f\in F$ we write $f : i_f \to j_f$. Then the diagram with objects $J \coloneqq \{ i_f \mid f \in F \} \cup \{ j_f \mid f \in F \}$ and morphisms $\{ f \mid f \in F \}$ has a cone with vertex $k \in \I$ and morphisms $g_i : k \to i$ for each $i \in J$. Now choose $y \in X_k$, and define $x \in \prod_{i \in \I} X_i$ such that $x_i = X_{g_i}(y)$ if $i \in J$, with arbitrary choices of $x_i \in X_i$ for all other $i$. We then see that $x \in \bigcap_{f\in F} E_f$, which finishes the proof of the claim.
-Since $\prod_{i \in \I} X_i$ is compact, that implies that the intersection of all $E_f$ is non-empty. But that intersection is precisely $\lim_{i \in \I} X_i$. $\square$
+Since $\prod_{i \in \I} X_i$ is compact, that implies that the intersection of all $E_f$ is non-empty. But that intersection is precisely $\lim_{i \in \I} X_i$.
+:::
::: Lemma 2
Suppose we have a cofiltered limit $X = \lim_{i\in \I} X_i$ in $\Top$. Note the topology on $X$ is the weak topology for the projections $p_i : X \to X_i$. Then the canonical subbasis of this topology on $X$ is closed under finite intersections. Thus, it agrees with the canonical basis of the topology on $X$.
:::
-_Proof._
+::: Proof
Suppose we have a finite collection of subbasic open sets of the form $U_n = p_{i_n}^{-1}(V_n)$, $n \in \{ 1, \ldots, N \}$, where each $V_n$ is an open subset of $X_{i_n}$. Take a cone $(j, f_n : j \to i_n)$ of the objects $i_1, \ldots, i_N$. We then have
$$\bigcap_{n=1}^N U_n = p_j^{-1} \left( \bigcap_{n=1}^N X_{f_n}^{-1}(V_n) \right),$$
-where the right hand side is again in the canonical subbasis. $\square$
+where the right hand side is again in the canonical subbasis.
+:::
::: Proposition 3
The functor $\Hom({-}, [0, 1]) : \CompHaus^{\op} \to \Set$ is monadic. (Originally proved in [Dus69](#references))
:::
-_Proof._
+::: Proof
We use the crude monadicity theorem (see e.g. [SGL92](#references), Thm. IV.4.2). First, the functor has a left adjoint $S \mapsto [0, 1]^S$ with the evident isomorphism
$$\Hom_{\CompHaus}\bigl(X, [0, 1]^S\bigr) \cong \Hom_{\Set}\bigl(S, \Hom_{\CompHaus}(X, [0, 1])\bigr).$$
@@ -54,7 +56,8 @@ with $r : B \to A$. We may assume that $i$ is a subspace inclusion map. We may u
$$\Hom(B, [0,1]) ~\overset{f^*}{\underset{g^*}{\rightrightarrows}}~ \Hom(A, [0, 1]) \xrightarrow{i^*} \Hom(E, [0, 1])$$
-is a coequalizer diagram. We first define $s : \Hom(E,[0,1]) \to \Hom(A,[0,1])$ by choosing a Tietze extension of each continuous function $E \to [0,1]$. Now, for each $\varphi \in \Hom(A,[0,1])$, we can define a continuous function on $\im(f) \cup \im(g) \subseteq B$ to be $\varphi \circ r$ on $\im(f)$, and $s(i^*(\varphi))\circ r$ on $\im(g)$. Note that on the overlap $\im(f)\cap \im(g) = f(E) = g(E)$, the first expression gives $f(e) \mapsto \varphi(e)$, and the second expression gives $g(e) \mapsto s(i^*(\varphi))(e) = \varphi(e)$, so we have indeed given a well-defined function on $\im(f)\cup\im(g)$. Choosing a Tietze extension of this function to a function $B\to [0,1]$ for each $\varphi$, we get a map $t : \Hom(A,[0,1]) \to \Hom(B,[0,1])$. By construction, we have $i^* s = \id$, $f^* t = \id$, and $g^* t = s i^*$, so we have shown that the diagram above is a split coequalizer. $\square$
+is a coequalizer diagram. We first define $s : \Hom(E,[0,1]) \to \Hom(A,[0,1])$ by choosing a Tietze extension of each continuous function $E \to [0,1]$. Now, for each $\varphi \in \Hom(A,[0,1])$, we can define a continuous function on $\im(f) \cup \im(g) \subseteq B$ to be $\varphi \circ r$ on $\im(f)$, and $s(i^*(\varphi))\circ r$ on $\im(g)$. Note that on the overlap $\im(f)\cap \im(g) = f(E) = g(E)$, the first expression gives $f(e) \mapsto \varphi(e)$, and the second expression gives $g(e) \mapsto s(i^*(\varphi))(e) = \varphi(e)$, so we have indeed given a well-defined function on $\im(f)\cup\im(g)$. Choosing a Tietze extension of this function to a function $B\to [0,1]$ for each $\varphi$, we get a map $t : \Hom(A,[0,1]) \to \Hom(B,[0,1])$. By construction, we have $i^* s = \id$, $f^* t = \id$, and $g^* t = s i^*$, so we have shown that the diagram above is a split coequalizer.
+:::
This shows that $\CompHaus^{\op}$ is equivalent to the category of algebras over the monad
$$S \mapsto \Hom_{\CompHaus}\bigl([0, 1]^S, [0, 1]\bigr).$$
@@ -64,7 +67,7 @@ We may view such algebras as being models of the one-sorted infinitary algebraic
The object $[0,1]$ of $\CompHaus$ is $\aleph_1$-copresentable. (Originally proved in [GU71](#references), 6.5(c))
:::
-_Proof._
+::: Proof
Suppose we have an $\aleph_1$-cofiltered limit $X = \lim_{i\in \I} X_i$ with projections $p_i : X \to X_i$, and a continuous function $\varphi : X \to [0,1]$. For the time being, fix $n\in \IN_{>0}$. Then for any $x\in X$, there exists an interval neighborhood $N_x$ of $\varphi(x)$ of diameter at most $1/n$ — for example, we can take $N_x \coloneqq (\varphi(x) - 1/(2n), \varphi(x) + 1/(2n)) \cap [0,1]$. We can also take a basic open neighborhood whose image is contained in $N_x$; by lemma 2, we can write that basic open neighborhood in the form $p_i^{-1}(V)$ where $V$ is an open subset of $X_i$.
By compactness of $X$, we may take finitely many such basic open neighborhoods of the form $p_i^{-1}(V)$ which cover $X$. Again using the assumption that $\I$ is cofiltered, we may assume that $i$ is the same for each neighborhood. In particular, we see that whenever we have $x, y\in X$ with $p_i(x) = p_i(y)$, then $|\varphi(x) - \varphi(y)| < 1/n$.
@@ -79,13 +82,14 @@ Now each $D_n \setminus \im(X_f)$ is open and we have just shown such sets cover
This shows the canonical map
$$\textstyle \colim_{i\in \I^{\op}} \Hom(X_i, [0,1]) \to \Hom\bigl(\lim_{i\in I} X_i, [0,1]\bigr)$$
-is injective. $\square$
+is injective.
+:::
::: Corollary 5
The category $\CompHaus$ is locally $\aleph_1$-copresentable.
:::
-_Proof._
+::: Proof
It suffices to show that the monad
$$S \mapsto \Hom_{\CompHaus}\bigl([0, 1]^S, [0, 1]\bigr)$$
is $\aleph_1$-accessible. This functor is the composition of
@@ -94,7 +98,8 @@ followed by
$$\Hom_{\CompHaus}({-}, [0,1]) : \CompHaus^{\op} \to \Set.$$
The first automatically preserves $\aleph_1$-filtered colimits (and in fact all colimits) since it has a right adjoint. The second one preserves $\aleph_1$-filtered colimits by the previous lemma.
-Alternately, applying the general framework of Lawvere theories shows that $\CompHaus^{\op}$ is equivalent to the category of functors $\T \to \Set$ preserving countable products, where $\T$ is the full subcategory of $\CompHaus$ of all spaces $[0,1]^A$ where $A$ is countable. Note that $\T$ is essentially small. We thus reproduce a result from [Isb82](#references) which also provides a nice description of a small set of generators of the operations of the $\aleph_0$-ary algebraic theory. A more recent treatment in [MR17](#references) refines this by providing a nice axiomatization of the relations of that theory. $\square$
+Alternately, applying the general framework of Lawvere theories shows that $\CompHaus^{\op}$ is equivalent to the category of functors $\T \to \Set$ preserving countable products, where $\T$ is the full subcategory of $\CompHaus$ of all spaces $[0,1]^A$ where $A$ is countable. Note that $\T$ is essentially small. We thus reproduce a result from [Isb82](#references) which also provides a nice description of a small set of generators of the operations of the $\aleph_0$-ary algebraic theory. A more recent treatment in [MR17](#references) refines this by providing a nice axiomatization of the relations of that theory.
+:::
### References
diff --git a/content/congruences_in_rel.md b/content/congruences_in_rel.md
index de11ea43..278027e9 100644
--- a/content/congruences_in_rel.md
+++ b/content/congruences_in_rel.md
@@ -95,4 +95,6 @@ $$
:::
-_Proof._ Suppose we have generalized elements $x_1, x_2 : U \to X$ with $e x_1 = e x_2$. Then $f t x_1 = x_1$ and $g t x_1 = s e x_1$, so the pair $x_1, s e x_1$ factors through $E$. Similarly, the pair $x_2, s e x_2$ factors through $E$. However, by the assumption, we also have $s e x_1 = s e x_2$. Therefore, since $E$ is a congruence, we conclude $x_1, x_2$ factors through $E$. $\square$
+::: Proof
+Suppose we have generalized elements $x_1, x_2 : U \to X$ with $e x_1 = e x_2$. Then $f t x_1 = x_1$ and $g t x_1 = s e x_1$, so the pair $x_1, s e x_1$ factors through $E$. Similarly, the pair $x_2, s e x_2$ factors through $E$. However, by the assumption, we also have $s e x_1 = s e x_2$. Therefore, since $E$ is a congruence, we conclude $x_1, x_2$ factors through $E$.
+:::
diff --git a/content/constant_morphisms.md b/content/constant_morphisms.md
index 8962a069..25b18545 100644
--- a/content/constant_morphisms.md
+++ b/content/constant_morphisms.md
@@ -9,30 +9,40 @@ description: We prove some results that help determine whether a morphism in a c
A [constant morphism](/morphism-property/constant) in $\Set$ is the same as a constant map in the usual sense.
:::
-_Proof._ Let $X,Y$ be two sets and let $f : X \to Y$ be a map. If $f$ is a constant morphism, then, in particular, for all morphisms $x_1,x_2 : 1 \to X$, we have $f \circ x_1 = f \circ x_2$. Therefore, $f(x_1) = f(x_2)$ for all $x_1,x_2 \in X$, so $f$ is a constant map. Conversely, if $f$ is a constant map and $x_1,x_2 : T \rightrightarrows X$ are two maps, then $f \circ x_1 = f \circ x_2$, since for all $t \in T$ we have $f(x_1(t)) = f(x_2(t))$. $\square$
+::: Proof
+Let $X,Y$ be two sets and let $f : X \to Y$ be a map. If $f$ is a constant morphism, then, in particular, for all morphisms $x_1,x_2 : 1 \to X$, we have $f \circ x_1 = f \circ x_2$. Therefore, $f(x_1) = f(x_2)$ for all $x_1,x_2 \in X$, so $f$ is a constant map. Conversely, if $f$ is a constant map and $x_1,x_2 : T \rightrightarrows X$ are two maps, then $f \circ x_1 = f \circ x_2$, since for all $t \in T$ we have $f(x_1(t)) = f(x_2(t))$.
+:::
::: Lemma 2
Let $\C$ be a locally small category. Any representable functor $U : \C \to \Set$ maps constant morphisms to constant maps.
:::
-_Proof._ We may assume that $U = \Hom(G,-)$ for some $G \in \C$. If $f : X \to Y$ is a constant morphism in $\C$, then the induced map $f_* : \Hom(G,X) \to \Hom(G,Y)$ is constant by the definition of a constant morphism. $\square$
+::: Proof
+We may assume that $U = \Hom(G,-)$ for some $G \in \C$. If $f : X \to Y$ is a constant morphism in $\C$, then the induced map $f_* : \Hom(G,X) \to \Hom(G,Y)$ is constant by the definition of a constant morphism.
+:::
::: Lemma 3
Any right adjoint functor preserves constant morphisms.
:::
-_Proof._ Let $G : \C \to \D$ be a functor that is right adjoint to $F : \D \to \C$. Let $f : X \to Y$ be a constant morphism in $\C$. To show that $G(f) : G(X) \to G(Y)$ is constant, let $y_1,y_2 : T \rightrightarrows G(X)$ be two morphisms. Under the adjunction, these correspond to morphisms $x_1,x_2 : F(T) \rightrightarrows X$. Since $f$ is constant, we have $f \circ x_1 = f \circ x_2$ as morphisms $F(T) \rightrightarrows Y$. Hence, $G(f) \circ y_1 = G(f) \circ y_2$ as morphisms $T \rightrightarrows G(Y)$. $\square$
+::: Proof
+Let $G : \C \to \D$ be a functor that is right adjoint to $F : \D \to \C$. Let $f : X \to Y$ be a constant morphism in $\C$. To show that $G(f) : G(X) \to G(Y)$ is constant, let $y_1,y_2 : T \rightrightarrows G(X)$ be two morphisms. Under the adjunction, these correspond to morphisms $x_1,x_2 : F(T) \rightrightarrows X$. Since $f$ is constant, we have $f \circ x_1 = f \circ x_2$ as morphisms $F(T) \rightrightarrows Y$. Hence, $G(f) \circ y_1 = G(f) \circ y_2$ as morphisms $T \rightrightarrows G(Y)$.
+:::
::: Lemma 4
If $X$ is a subterminal object, then any morphism $X \to Y$ is constant. If $Y$ is a terminal object, then any morphism $X \to Y$ is constant.
:::
-_Proof._ This is immediate from the definitions. $\square$
+::: Proof
+This is immediate from the definitions.
+:::
::: Lemma 5
If $f : X \to Y$ is a monomorphism that is constant, then $X$ is subterminal.
:::
-_Proof._ If $x_1,x_2 : T \rightrightarrows X$ are morphisms, then $f \circ x_1 = f \circ x_2$ since $f$ is constant. Since $f$ is also a monomorphism, we infer that $x_1 = x_2$. $\square$
+::: Proof
+If $x_1,x_2 : T \rightrightarrows X$ are morphisms, then $f \circ x_1 = f \circ x_2$ since $f$ is constant. Since $f$ is also a monomorphism, we infer that $x_1 = x_2$.
+:::
Of course, all results on constant morphisms dualize to results on coconstant morphisms (except for Lemma 2). For example, Lemma 5 implies that if an epimorphism $f : X \to Y$ is coconstant, then $Y$ is "co-subterminal", i.e. every two morphisms $Y \rightrightarrows T$ are equal.
diff --git a/content/coslice-effective-congruences.md b/content/coslice-effective-congruences.md
index 7e60a5df..888e2f28 100644
--- a/content/coslice-effective-congruences.md
+++ b/content/coslice-effective-congruences.md
@@ -9,7 +9,7 @@ description: An extensive category has effective congruences when some of its co
Let $\C$ be an extensive category, and $A$ an object of $\C$. If the coslice category $A \backslash \C$ has effective congruences, then so does $\C$.
:::
-_Proof._
+::: Proof
Let $f, g : E \rightrightarrows X$ be a congruence in $\C$. We then construct a congruence on $A+X$ in $A \backslash \C$. On an intuitive level, this will be the congruence generated by $a \sim a$ for $a\in A$ and $x \sim y$ for $(x, y) \in E$. More precisely, we will show the two maps
$$\id_A + f,\, \id_A + g : A+E \rightrightarrows A+X$$
@@ -20,4 +20,5 @@ Now if this congruence is the kernel pair of $h : A+X \to Z$ in $A \backslash \C
$$\id_A + x_1,\, \id_A + x_2 : A+T \rightrightarrows A+X$$
-in $A \backslash \C$ with $h \circ (\id_A + x_1) = h \circ (\id_A + x_2)$. Therefore, $\id_A + x_1, \id_A + x_2$ factors through $A+E$ in $A \backslash \C$, so $x_1, x_2$ factors through $A+E$ in $\C$; and using disjoint coproducts, we may conclude $x_1, x_2$ factors through $E$. $\square$
+in $A \backslash \C$ with $h \circ (\id_A + x_1) = h \circ (\id_A + x_2)$. Therefore, $\id_A + x_1, \id_A + x_2$ factors through $A+E$ in $A \backslash \C$, so $x_1, x_2$ factors through $A+E$ in $\C$; and using disjoint coproducts, we may conclude $x_1, x_2$ factors through $E$.
+:::
diff --git a/content/effective-congruence-quotients.md b/content/effective-congruence-quotients.md
index bacc2cb1..83171747 100644
--- a/content/effective-congruence-quotients.md
+++ b/content/effective-congruence-quotients.md
@@ -10,11 +10,12 @@ Let $f, g : E \rightrightarrows X$ be an effective congruence. If $f, g$ have a
$$\begin{CD} E @> f >> X \\ @V g VV @VV p V \\ X @>> p > X/E. \end{CD}$$
:::
-_Proof._
+::: Proof
Suppose we have $h : X \to Z$ so that we have a cartesian square
$$\begin{CD} E @> f >> X \\ @V g VV @VV h V \\ X @>> h > Z. \end{CD}$$
Then by the universal property of the coequalizer, there is a unique morphism
$$\bar h : X/E \to Z$$
such that $h = \bar h \circ p$. Now suppose we have generalized elements $x_1, x_2 : T \rightrightarrows X$ such that $p \circ x_1 = p \circ x_2$. Then
$$h \circ x_1 = \bar h \circ p \circ x_1 = \bar h \circ p \circ x_2 = h \circ x_2,$$
-so the pair $x_1, x_2$ factors through $f, g : E \rightrightarrows X$. The uniqueness of the factorization follows from the assumption that $E$ is a congruence, so $f, g$ are jointly monomorphic. $\square$
+so the pair $x_1, x_2$ factors through $f, g : E \rightrightarrows X$. The uniqueness of the factorization follows from the assumption that $E$ is a congruence, so $f, g$ are jointly monomorphic.
+:::
diff --git a/content/functors_on_discrete_categories.md b/content/functors_on_discrete_categories.md
index 1b900169..72b80ccb 100644
--- a/content/functors_on_discrete_categories.md
+++ b/content/functors_on_discrete_categories.md
@@ -13,15 +13,19 @@ First, we consider the trivial case $\S = 1$.
Consider the trivial category $1 = \{0\}$ with a unique object $0$. Let $F : 1 \to \C$ be a functor corresponding to an object $F(0) \in \C$. Then $F$ is continuous if and only if $F(0)$ is a terminal object in $\C$.
:::
-_Proof._ If $F$ is continuous, it preserves terminal objects. Since $0 \in 1$ is terminal, it follows that $F(0) \in \C$ is terminal. Conversely, suppose that $F(0) \in \C$ is terminal. Then $F$ is continuous: for every index category $\I$, there is a unique diagram $D : \I \to 1$, namely $D(i) = 0$ and $D(i \to j) = \id_0$. Its limit is $0$, with the universal cone $(\id_0 : 0 \to D(i))_{i \in \I}$. We need to show that $(\id_{F(0)} : F(0) \to F(0))_{i \in \I}$ is a universal cone in $\C$. This is easy to see using that $F(0)$ is terminal. $\square$
+::: Proof
+If $F$ is continuous, it preserves terminal objects. Since $0 \in 1$ is terminal, it follows that $F(0) \in \C$ is terminal. Conversely, suppose that $F(0) \in \C$ is terminal. Then $F$ is continuous: for every index category $\I$, there is a unique diagram $D : \I \to 1$, namely $D(i) = 0$ and $D(i \to j) = \id_0$. Its limit is $0$, with the universal cone $(\id_0 : 0 \to D(i))_{i \in \I}$. We need to show that $(\id_{F(0)} : F(0) \to F(0))_{i \in \I}$ is a universal cone in $\C$. This is easy to see using that $F(0)$ is terminal.
+:::
::: Lemma 2
Let $\S$ be a non-trivial inhabited discrete category. Then a functor $F : \S \to \C$ is continuous if and only if, for every $s \in \S$, the object $F(s) \in \C$ is [subterminal](https://ncatlab.org/nlab/show/subterminal+object), i.e. every two morphisms with codomain $F(s)$ are equal.
:::
-_Proof._ Assume first that $F$ is continuous. An object $X$ is subterminal if and only if $X \times X$ exists and the diagonal $X \to X \times X$ is an isomorphism. Thus, every functor preserving binary products preserves subterminal objects. Since every object in a discrete category is subterminal, it follows that each $F(s) \in \C$ is subterminal.
+::: Proof
+Assume first that $F$ is continuous. An object $X$ is subterminal if and only if $X \times X$ exists and the diagonal $X \to X \times X$ is an isomorphism. Thus, every functor preserving binary products preserves subterminal objects. Since every object in a discrete category is subterminal, it follows that each $F(s) \in \C$ is subterminal.
-Conversely, assume that each $F(s) \in \C$ is subterminal. To show that $F$ is continuous, let $D : \I \to \S$ be a (small) diagram admitting a universal cone $(s \to D(i))_{i \in \I}$. Then $D(i) = s$ for all $i \in \I$, and each morphism $s \to D(i)$ is the identity. Since $\S$ has no terminal object (otherwise, $\S$ would be trivial), $\I$ is inhabited. We need to show that $(\id_{F(s)} : F(s) \to F(s))_{i \in \I}$ is a universal cone in $\C$. This follows immediately from $F(s)$ being subterminal: for a family of morphisms $X \to F(s)$ indexed by $\I$, all morphisms must be equal, and there is one such morphism since $\I$ is inhabited. $\square$
+Conversely, assume that each $F(s) \in \C$ is subterminal. To show that $F$ is continuous, let $D : \I \to \S$ be a (small) diagram admitting a universal cone $(s \to D(i))_{i \in \I}$. Then $D(i) = s$ for all $i \in \I$, and each morphism $s \to D(i)$ is the identity. Since $\S$ has no terminal object (otherwise, $\S$ would be trivial), $\I$ is inhabited. We need to show that $(\id_{F(s)} : F(s) \to F(s))_{i \in \I}$ is a universal cone in $\C$. This follows immediately from $F(s)$ being subterminal: for a family of morphisms $X \to F(s)$ indexed by $\I$, all morphisms must be equal, and there is one such morphism since $\I$ is inhabited.
+:::
Remark that in a thin category, every object is subterminal. Of course, Lemma 2 can also be dualized: A functor on a non-trivial inhabited discrete category is cocontinuous if and only if each object in its image is "co-subterminal". Here, an object $X$ is co-subterminal if any two morphisms with domain $X$ are equal (see [MSE/1092122](https://math.stackexchange.com/questions/1092122) for a discussion of the terminology).
@@ -31,14 +35,18 @@ Next, let us determine which of the continuous functors are right adjoints.
Let $\S$ be a discrete category. Then a functor $F : \S \to \C$ is a right adjoint if and only if there is a decomposition $\C = \coprod_{s \in \S} \C_s$ into full subcategories such that $F(s) \in \C_s$ is a terminal object for every $s \in \S$.
:::
-_Proof._ A functor $G : \C \to \S$ corresponds to a decomposition $\C = \coprod_{s \in \S} \C_s$ via
+::: Proof
+A functor $G : \C \to \S$ corresponds to a decomposition $\C = \coprod_{s \in \S} \C_s$ via
$$G(X) = s \iff X \in \C_s.$$
It is left adjoint to $F$ if and only if there are natural bijections
$$\Hom(G(X),s) \cong \Hom(X,F(s))$$
-for $X \in \C$ and $s \in \S$. For $X \in \C_s$, this means that there is a unique morphism $X \to F(s)$. For $X \in \C_t$ with $t \neq s$, it means that there is no morphism $X \to F(s)$. In other words, $F(s) \in \C_s$. Naturality in $s$ is automatic since $\S$ is discrete. Naturality in $X$, say for $X \in \C_s$, is also automatic. $\square$
+for $X \in \C$ and $s \in \S$. For $X \in \C_s$, this means that there is a unique morphism $X \to F(s)$. For $X \in \C_t$ with $t \neq s$, it means that there is no morphism $X \to F(s)$. In other words, $F(s) \in \C_s$. Naturality in $s$ is automatic since $\S$ is discrete. Naturality in $X$, say for $X \in \C_s$, is also automatic.
+:::
::: Corollary 4
Let $\S$ be a discrete category, and let $\C$ be a connected category. If there is a right adjoint functor $\S \to \C$, then $\S$ is trivial.
:::
-_Proof._ By Lemma 3, such a right adjoint yields a decomposition $\C = \coprod_{s \in \S} \C_s$ into full subcategories, each having a terminal object. In particular, each $\C_s$ is inhabited. Since $\C$ is connected, it follows that $\S$ has exactly one object. $\square$
+::: Proof
+By Lemma 3, such a right adjoint yields a decomposition $\C = \coprod_{s \in \S} \C_s$ into full subcategories, each having a terminal object. In particular, each $\C_s$ is inhabited. Since $\C$ is connected, it follows that $\S$ has exactly one object.
+:::
diff --git a/content/generator_construction.md b/content/generator_construction.md
index b11cc2cb..eceb44a0 100644
--- a/content/generator_construction.md
+++ b/content/generator_construction.md
@@ -9,8 +9,10 @@ description: How to construct a generator from a generating set
In a category let $S$ be a generating set which is [strongly connected](/category-property/strongly_connected), i.e. between any two objects $G,G' \in S$ there is a morphism $G \to G'$. If the coproduct $U \coloneqq \coprod_{G \in S} G$ exists, then it is a generator. Moreover, if $S$ is an extremal generating set, then $U$ is an extremal generator.
:::
-_Proof._ We remark that the assumption on $S$ implies that each coprojection $i_G : G \to U$ has a left inverse. Now let $f,g : A \rightrightarrows B$ be two morphisms with $f \circ \bar a = g \circ \bar a$ for all $\bar a : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by our preliminary remark. Thus, $f \circ a = g \circ a$ holds for all morphisms $a : G \to A$ with $G \in S$. Since $S$ is a generating set, this implies $f = g$.
+::: Proof
+We remark that the assumption on $S$ implies that each coprojection $i_G : G \to U$ has a left inverse. Now let $f,g : A \rightrightarrows B$ be two morphisms with $f \circ \bar a = g \circ \bar a$ for all $\bar a : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by our preliminary remark. Thus, $f \circ a = g \circ a$ holds for all morphisms $a : G \to A$ with $G \in S$. Since $S$ is a generating set, this implies $f = g$.
Similarly, for the case where $S$ is an extremal generating set, suppose we have a morphism $f : A \to B$ such that $f \circ {-} : \Hom(U, A) \to \Hom(U, B)$ is a bijection. In particular, because it is injective and $U$ is a generator, we can conclude that $f$ is a monomorphism, so $f \circ {-} : \Hom(G, A) \to \Hom(G, B)$ is injective for each $G \in S$. Now suppose $b \in \Hom(G, B)$ for $G \in S$. Then $b$ extends to a morphism $\bar b : U \to B$. By assumption, there exists $\bar a : U \to A$ such that $f \circ \bar a = \bar b$. Composing with the coprojection $i_G : G \to U$, we see
$$f \circ \bar a \circ i_G = \bar b \circ i_G = b.$$
-This shows that $f \circ {-} : \Hom(G, A) \to \Hom(G, B)$ is also surjective for each $G \in S$. Since $S$ is an extremal generating set, this implies $f$ is an isomorphism. $\square$
+This shows that $f \circ {-} : \Hom(G, A) \to \Hom(G, B)$ is also surjective for each $G \in S$. Since $S$ is an extremal generating set, this implies $f$ is an isomorphism.
+:::
diff --git a/content/inclusion-functors.md b/content/inclusion-functors.md
index 8cd2c071..82a51647 100644
--- a/content/inclusion-functors.md
+++ b/content/inclusion-functors.md
@@ -9,8 +9,10 @@ description: We gather results about inclusion functors
Let $\D$ be category that has an extremal cogenerator $Q$. Let $\C \subseteq \D$ be a full subcategory that contains $Q$. Then the inclusion functor $U : \C \hookrightarrow \D$ preserves all colimits that exist in $\C$ and in $\D$. In particular, if $\D$ is cocomplete, $U$ is cocontinuous.
:::
-_Proof._ Let $D : \I \to \C$ be a diagram such that $D$ has a colimit $(u_i : D(i) \to X)$ in $\C$ and $U \circ D$ has a colimit $(v_i : D(i) \to Y)$ in $\D$. There is a unique morphism $f : Y \to X$ such that $f \circ v_i = u_i$ for every $i \in \I$. Moreover, for every object $T \in \C$ the map of sets
+::: Proof
+Let $D : \I \to \C$ be a diagram such that $D$ has a colimit $(u_i : D(i) \to X)$ in $\C$ and $U \circ D$ has a colimit $(v_i : D(i) \to Y)$ in $\D$. There is a unique morphism $f : Y \to X$ such that $f \circ v_i = u_i$ for every $i \in \I$. Moreover, for every object $T \in \C$ the map of sets
$$f^* : \Hom(X,T) \to \Hom(Y,T)$$
-is a bijection; both sides identify with cones $D \to T$. Now apply this to $T \coloneqq Q$ to conclude that $f$ is an isomorphism. $\square$
+is a bijection; both sides identify with cones $D \to T$. Now apply this to $T \coloneqq Q$ to conclude that $f$ is an isomorphism.
+:::
diff --git a/content/missing_cogenerating_sets.md b/content/missing_cogenerating_sets.md
index 1a90b950..bf71c2b3 100644
--- a/content/missing_cogenerating_sets.md
+++ b/content/missing_cogenerating_sets.md
@@ -14,5 +14,6 @@ Let $\C$ be a category with a faithful functor $U: \C \to \Set$. Assume there ex
Then $\C$ does not have a cogenerating set.
:::
-_Proof._
-Assume that there is a cogenerating set $S$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than all the $U(Y)$ with $Y \in S$ (w.r.t. cardinalities) and which has a non-identity endomorphism $\sigma : X \to X$. Since $S$ cogenerates, there is a morphism $f : X \to Y$ with $Y \in S$ and $f \sigma \neq f$. For this, $Y$ must be non-terminal. By (1) the map $U(f) : U(X) \to U(Y)$ is injective. This is a contradiction. $\square$
+::: Proof
+Assume that there is a cogenerating set $S$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than all the $U(Y)$ with $Y \in S$ (w.r.t. cardinalities) and which has a non-identity endomorphism $\sigma : X \to X$. Since $S$ cogenerates, there is a morphism $f : X \to Y$ with $Y \in S$ and $f \sigma \neq f$. For this, $Y$ must be non-terminal. By (1) the map $U(f) : U(X) \to U(Y)$ is injective. This is a contradiction.
+:::
diff --git a/content/missing_cogenerator.md b/content/missing_cogenerator.md
index 1d071fc4..6e191595 100644
--- a/content/missing_cogenerator.md
+++ b/content/missing_cogenerator.md
@@ -15,5 +15,6 @@ Let $\C$ be a pointed category with a faithful functor $U: \C \to \Set$. Assume
Then $\C$ does not have a cogenerator.
:::
-_Proof._
-Assume that there is a cogenerator $Y$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than $U(Y)$ (w.r.t. cardinalities). Since $0,\id_X : X \rightrightarrows X$ are distinct, there is a morphism $f : X \to Y$ with $f \neq 0$. But then $U(f) : U(X) \to U(Y)$ is injective by assumption (1), which contradicts our choice of $X$. $\square$
+::: Proof
+Assume that there is a cogenerator $Y$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than $U(Y)$ (w.r.t. cardinalities). Since $0,\id_X : X \rightrightarrows X$ are distinct, there is a morphism $f : X \to Y$ with $f \neq 0$. But then $U(f) : U(X) \to U(Y)$ is injective by assumption (1), which contradicts our choice of $X$.
+:::
diff --git a/content/natural_numbers_objects.md b/content/natural_numbers_objects.md
index b3bd73d6..54feb572 100644
--- a/content/natural_numbers_objects.md
+++ b/content/natural_numbers_objects.md
@@ -21,7 +21,8 @@ N \times X @>>{g}> X
\end{CD}
$$
-_Proof._ Define the morphism $b : 1 \to N \times X$ by $b \coloneqq (z,a)$ and the morphism $h : N \times X \to N \times X$ by $h(n,x) \coloneqq (n,g(n,x))$. By the universal property of $(N,z,s)$, there is a unique morphism $\Psi : N \to N \times X$ such that:
+::: Proof
+Define the morphism $b : 1 \to N \times X$ by $b \coloneqq (z,a)$ and the morphism $h : N \times X \to N \times X$ by $h(n,x) \coloneqq (n,g(n,x))$. By the universal property of $(N,z,s)$, there is a unique morphism $\Psi : N \to N \times X$ such that:
- $\Psi(z) = b$
- $\Psi(s(n)) = h(\Psi(n))$
@@ -33,7 +34,8 @@ Write $\Psi(n) = (\Psi_0(n),\Psi_1(n))$, where $\Psi_0 : N \to N$ and $\Psi_1 :
- $\Psi_1(z) = a$
- $\Psi_1(s(n)) = g(\Psi_0(n),\Psi_1(n))$
-The uniqueness in the universal property of $(N,z,s)$ implies $\Psi_0 = \id_N$. Therefore, $\Phi \coloneqq \Psi_1$ is the unique morphism $\Phi : N \to X$ satisfying $\Phi(z)=a$ and $\Phi(s(n)) = g(n,\Phi(n))$. $\square$
+The uniqueness in the universal property of $(N,z,s)$ implies $\Psi_0 = \id_N$. Therefore, $\Phi \coloneqq \Psi_1$ is the unique morphism $\Phi : N \to X$ satisfying $\Phi(z)=a$ and $\Phi(s(n)) = g(n,\Phi(n))$.
+:::
The next result appears in [Johnstone](https://ncatlab.org/nlab/show/Sketches+of+an+Elephant), Part A, Lemma 2.5.5. Our proof is slightly more concise because we have extracted Lemma 1.
@@ -43,7 +45,9 @@ $$1 \xrightarrow{z} N \xleftarrow{s} N$$
is a coproduct cocone. Thus, $N \cong 1 \sqcup N$.
:::
-_Proof._ Let $a : 1 \to X$ and $b : N \to X$ be morphisms. We need to show that there is a unique morphism $c : N \to X$ satisfying $c(z) = a$ and $c(s(n)) = b(n)$. This follows by applying Lemma 1 to the morphism $g : N \times X \to X$ defined by $g(n,x) \coloneqq b(n)$. $\square$
+::: Proof
+Let $a : 1 \to X$ and $b : N \to X$ be morphisms. We need to show that there is a unique morphism $c : N \to X$ satisfying $c(z) = a$ and $c(s(n)) = b(n)$. This follows by applying Lemma 1 to the morphism $g : N \times X \to X$ defined by $g(n,x) \coloneqq b(n)$.
+:::
Next, we will check when the terminal object $1$ itself is a natural numbers object. In that case, $z : 1 \to 1$ and $s : 1 \to 1$ are necessarily equal to $\id_1$.
@@ -51,7 +55,9 @@ Next, we will check when the terminal object $1$ itself is a natural numbers obj
Let $1$ be a terminal object in a category. Then $(1,\id_1,\id_1)$ is a natural numbers object if and only if for every endomorphism $g : X \to X$ and every morphism $a : 1 \to X$ we have $g \circ a = a$. If the category has finite products, $(1,\id_1,\id_1)$ is a parametrized natural numbers object if and only if $g = \id_X$ for every endomorphism $g : X \to X$, i.e. the category is [one-way](/category-property/one-way).
:::
-_Proof._ The first statement is immediate from the definition of a natural numbers object. For the second, $(1,\id_1,\id_1)$ is a parametrized natural numbers object if and only if, for all morphisms $f : A \to X$ and all endomorphisms $g : X \to X$, there is a unique morphism $\Phi : A \to X$ such that $\Phi \circ \id_A = f$ and $\Phi \circ \id_A = g \circ \Phi$. These equations simplify to $\Phi = f$ and $f = g \circ f$. Since this must hold for every $f : A \to X$, we must have $g = \id_X$ (by the Yoneda Lemma or by a direct argument). $\square$
+::: Proof
+The first statement is immediate from the definition of a natural numbers object. For the second, $(1,\id_1,\id_1)$ is a parametrized natural numbers object if and only if, for all morphisms $f : A \to X$ and all endomorphisms $g : X \to X$, there is a unique morphism $\Phi : A \to X$ such that $\Phi \circ \id_A = f$ and $\Phi \circ \id_A = g \circ \Phi$. These equations simplify to $\Phi = f$ and $f = g \circ f$. Since this must hold for every $f : A \to X$, we must have $g = \id_X$ (by the Yoneda Lemma or by a direct argument).
+:::
Next, we prove a partial converse to the [result](/category-implication/parametrized_nno_criterion) that countably distributive categories have a parametrized natural numbers object.
@@ -61,7 +67,8 @@ $$\alpha : \IN \otimes A \to A \times (\IN \otimes 1)$$
is an isomorphism.
:::
-_Proof._ We will use element notation extensively. In particular, for every element $a \in A$ and $n \in \IN$, there is an element $n \otimes a \in \IN \otimes A$, formally defined by the $n$th coproduct inclusion. The morphism $\alpha$ is defined by
+::: Proof
+We will use element notation extensively. In particular, for every element $a \in A$ and $n \in \IN$, there is an element $n \otimes a \in \IN \otimes A$, formally defined by the $n$th coproduct inclusion. The morphism $\alpha$ is defined by
$$\alpha(n \otimes a) = (a,n \otimes 1).$$
In any category with a terminal object and countable copowers, we can construct the non-parametrized NNO $\IN \otimes 1$ with the element $0 \otimes 1 \in \IN \otimes 1$ and the map
@@ -96,7 +103,8 @@ namely $\id_{A \times N}$. Thus, it suffices to verify that $\alpha \circ \Phi :
$$\alpha(\Phi(a,z)) = \alpha(0 \otimes a) = (a, 0 \otimes 1) = (a,z),$$
and hence $\alpha \circ \Phi \circ (\id_A,z) = (\id_A,z)$. Moreover,
$$\alpha \circ \Phi \circ (\id_A \times s) = \alpha \circ g \circ \Phi = (\id_A \times s) \circ \alpha \circ \Phi.$$
-This finishes the proof. $\square$
+This finishes the proof.
+:::
_Remark._ Actually, the mentioned [result](/category-implication/parametrized_nno_criterion) and Lemma 4 can be combined into an equivalent characterization as follows: In a category with finite products and countable copowers, the NNO (which exists, see [here](/category-implication/nno_criterion)) is a parametrized NNO if and only if for all objects $A$ the canonical morphism
$$\textstyle \coprod_{n \in \IN} A = \coprod_{n \in \IN} (A \times 1) \to A \times \coprod_{n \in \IN} 1$$
diff --git a/content/preadditive_structure_unique.md b/content/preadditive_structure_unique.md
index 52a91c61..c478d9b9 100644
--- a/content/preadditive_structure_unique.md
+++ b/content/preadditive_structure_unique.md
@@ -13,7 +13,7 @@ $$f+g : A \to B$$
is the composite of $(f,g) : A \to B \times B$, the inverse $\alpha^{-1} : B \oplus B \to B \times B$, and the codiagonal $\nabla : B \oplus B \to B$.
:::
-_Proof._
+::: Proof
The morphism $\alpha : X \oplus Y \to X \times Y$ is defined by the equations
$$p_1 \circ \alpha \circ i_1 = \id_X, \quad p_2 \circ \alpha \circ i_2 = \id_Y,$$
$$p_2 \circ \alpha \circ i_1 = 0,\quad p_1 \circ \alpha \circ i_2 = 0.$$
@@ -32,4 +32,4 @@ $$
\end{align*}
$$
-$\square$
+:::
diff --git a/content/pushouts-of-monos-via-congruence-quotients.md b/content/pushouts-of-monos-via-congruence-quotients.md
index e21107b6..ac88890b 100644
--- a/content/pushouts-of-monos-via-congruence-quotients.md
+++ b/content/pushouts-of-monos-via-congruence-quotients.md
@@ -9,5 +9,6 @@ description: An extensive category with quotients of congruences has pushouts of
Let $\C$ be an extensive category with quotients of congruences. Then $\C$ has pushouts of monomorphisms.
:::
-_Proof._
-Let $f : S \hookrightarrow X$, $g : S \hookrightarrow Y$ be monomorphisms. We construct a congruence on $X+Y$ via the maps $p_1, p_2 : X + Y + S + S \rightrightarrows X+Y$ which act as the identity on $X+Y$, $i_1 \circ f, i_2 \circ g$ on the first copy of $S$, and $i_2 \circ g, i_1 \circ f$ on the second copy of $S$, respectively. To show that $p_1, p_2$ are jointly monomorphic, and again in proving transitivity of the congruence, we use extensivity to split the domain of the generalized elements of $X+Y+S+S$ so that without loss of generality we may assume each factors through one of the coproduct inclusions. Now a quotient of the congruence must be a pushout of $f$ and $g$. $\square$
+::: Proof
+Let $f : S \hookrightarrow X$, $g : S \hookrightarrow Y$ be monomorphisms. We construct a congruence on $X+Y$ via the maps $p_1, p_2 : X + Y + S + S \rightrightarrows X+Y$ which act as the identity on $X+Y$, $i_1 \circ f, i_2 \circ g$ on the first copy of $S$, and $i_2 \circ g, i_1 \circ f$ on the second copy of $S$, respectively. To show that $p_1, p_2$ are jointly monomorphic, and again in proving transitivity of the congruence, we use extensivity to split the domain of the generalized elements of $X+Y+S+S$ so that without loss of generality we may assume each factors through one of the coproduct inclusions. Now a quotient of the congruence must be a pushout of $f$ and $g$.
+:::
diff --git a/content/sifted-colimits-in-groupoids.md b/content/sifted-colimits-in-groupoids.md
index cc6c2530..8c58850d 100644
--- a/content/sifted-colimits-in-groupoids.md
+++ b/content/sifted-colimits-in-groupoids.md
@@ -15,7 +15,7 @@ Let $\C$ be a category. Let $D : \I \to \C$ be a sifted diagram which is constan
In particular, every groupoid has sifted colimits.
-_Proof._
+::: Proof
For every $i \in \I$, define a morphism $u_i : D(i) \to D(i_0)$ as follows. Choose a cospan
$$i \xrightarrow{a} k \xleftarrow{b} i_0,$$
@@ -52,13 +52,14 @@ We check that $v_i = h u_i$ for every $i \in \I$. Choose a cospan $i \xrightarro
$$h u_i = v_{i_0} D(b)^{-1} D(a) = v_k D(a) = v_i.$$
-Moreover, $h$ is uniquely determined: if $v_i = h u_i$ for all $i \in \I$, then for $i = i_0$ we obtain $v_{i_0} = h$. $\square$
+Moreover, $h$ is uniquely determined: if $v_i = h u_i$ for all $i \in \I$, then for $i = i_0$ we obtain $v_{i_0} = h$.
+:::
::: Corollary 2
Let $\C$ be a category with the property that every sifted diagram is eventually constant (for example, a groupoid). Then every object $X \in \C$ is strongly finitely presentable, i.e. the functor $\Hom(X,-) : \C \to \Set$ preserves sifted colimits.
:::
-_Proof._
+::: Proof
Let $D : \I \to \C$ be a diagram and choose $i_0 \in \I$ such that $D$ is constant after $i_0$. We obtain a commutative diagram:
$$
@@ -69,19 +70,22 @@ $$
\end{CD}
$$
-The top horizontal map is the identity. By Lemma 1 applied to $D$, the right vertical map is an isomorphism. By Lemma 2 applied to the diagram $\Hom(X,D(-))$ in $\Set$, the left vertical map is an isomorphism. Hence the bottom horizontal map is an isomorphism. $\square$
+The top horizontal map is the identity. By Lemma 1 applied to $D$, the right vertical map is an isomorphism. By Lemma 2 applied to the diagram $\Hom(X,D(-))$ in $\Set$, the left vertical map is an isomorphism. Hence the bottom horizontal map is an isomorphism.
+:::
::: Corollary 3
Let $\C$ be an essentially small category in which every sifted diagram is eventually constant. Then $\C$ is a [generalized variety](/category-property/generalized_variety).
:::
-_Proof._
-This follows directly from Lemma 1 and Corollary 2. $\square$
+::: Proof
+This follows directly from Lemma 1 and Corollary 2.
+:::
::: Corollary 4
Let $\C$ be an essentially small category in which every sifted diagram is eventually constant.
Then $\C$ is [finitely accessible](/category-property/finitely_accessible).
:::
-_Proof._
-Since sifted colimits exist, filtered colimits also exist. Moreover, every object is strongly finitely presentable and therefore also finitely presentable. $\square$
+::: Proof
+Since sifted colimits exist, filtered colimits also exist. Moreover, every object is strongly finitely presentable and therefore also finitely presentable.
+:::
diff --git a/content/special_sequential_colimits.md b/content/special_sequential_colimits.md
index f5df294e..a33338ce 100644
--- a/content/special_sequential_colimits.md
+++ b/content/special_sequential_colimits.md
@@ -9,7 +9,7 @@ description: A generalization of the proof that the category of finite groups ha
Let $\C$ be a category with finite powers, including a terminal object $1$. Let $a : 1 \to X$ be a morphism. Assume that the sequence of morphisms $(X^n,a) : X^n \to X^{n+1}$ for $n \geq 0$ admits a colimit $(i_n : X^n \to C)$. Then for every $m \geq 0$ there is a split epimorphism $C \to X^m$. In particular, if $U : \C \to \Set$ is a functor preserving finite powers and $\card(U(X)) \geq 2$, then $U(C)$ is infinite.
:::
-_Proof._
+::: Proof
Let $m \geq 0$ be fixed. For $n \geq 0$ we define a morphism $u_n : X^n \to X^m$ as follows: It is the projection on the first $m$ factors for $m \leq n$, and $(X^n,a^{m-n})$ for $m \geq n$ (for $m=n$ these agree). With generalized elements this says:
$$u_n(x_1,\dotsc,x_n) = \begin{cases} (x_1,\dotsc,x_m) & m \leq n \\ (x_1,\dotsc,x_n,a,\dotsc,a) & m \geq n \end{cases}$$
We claim that $u_n = u_{n+1} \circ (X^n,a)$, i.e.
@@ -17,4 +17,5 @@ $$u_n(x_1,\dotsc,x_n) = u_{n+1}(x_1,\dotsc,x_n,a).$$
If $m \leq n$ (hence, $m \leq n+1$), both sides are equal to $(x_1,\dotsc,x_m)$. If $m > n$, i.e. $m \geq n+1$, both sides are equal to $(x_1,\dotsc,x_n,a,\dotsc,a)$. This proves the claim.
Hence, there is a unique morphism $\varphi : C \to X^m$ such that $\varphi \circ i_n = u_n$ for all $n \geq 0$. Since $u_m$ is the identity, $\varphi$ is a split epimorphism.
-If $U$ is a functor with the mentioned properties, $U(\varphi)$ is also a split epimorphism from $U(C)$ to $U(X^m) \cong U(X)^m$, and $U(X)^m$ has $\geq 2^m$ elements. This holds for all $m$, so that $U(C)$ is infinite. $\square$
+If $U$ is a functor with the mentioned properties, $U(\varphi)$ is also a split epimorphism from $U(C)$ to $U(X^m) \cong U(X)^m$, and $U(X)^m$ has $\geq 2^m$ elements. This holds for all $m$, so that $U(C)$ is infinite.
+:::
diff --git a/content/subcategories.md b/content/subcategories.md
index c2f22f32..d30770e4 100644
--- a/content/subcategories.md
+++ b/content/subcategories.md
@@ -11,10 +11,11 @@ This page collects several useful results of the following form: if $U : \C \to
Let $\D$ be a category with a (regular) subobject classifier $\Omega$. Assume that $U : \C \to \D$ is a fully faithful functor such that (1) $U$ is coreflective, i.e. there is a functor $R : \D \to \C$ right adjoint to $U$, and (2) every (regular) monomorphism $Y \to U(X)$ in $\D$ is the image of a (regular) monomorphism $X' \to X$ in $\C$. Then $R(\Omega)$ is a (regular) subobject classifier in $\C$.
:::
-_Proof._
+::: Proof
If $X \in \C$, then
$$\Hom(X,R(\Omega)) \cong \Hom(U(X),\Omega) \cong \Sub(U(X)) \cong \Sub(X).$$
-The same proof works for regular subobjects. $\square$
+The same proof works for regular subobjects.
+:::
::: Lemma 2
Let $\C$ be a category with filtered colimits. Assume that $U : \C \to \D$ is a faithful functor that preserves monomorphisms and filtered colimits. If monomorphisms in $\D$ are stable under filtered colimits, then the same is true in $\C$.
@@ -22,18 +23,19 @@ Let $\C$ be a category with filtered colimits. Assume that $U : \C \to \D$ is a
For the record, here is the dual statement: let $\C$ be a category with cofiltered limits. Assume that $U : \C \to \D$ is a faithful functor that preserves epimorphisms and cofiltered limits. If epimorphisms in $\D$ are stable under cofiltered limits, then the same is true in $\C$.
-_Proof._
+::: Proof
If $(f_i : X_i \to Y_i)$ is a filtered diagram of monomorphisms in $\C$, it induces a filtered diagram $(U(f_i) : U(X_i) \to U(Y_i))$ of monomorphisms in $\D$. Hence, its colimit
$\colim_i U(f_i) : \colim_i U(X_i) \to \colim_i U(Y_i)$
is a monomorphism in $\D$. This morphism is isomorphic to
$U(\colim_i f_i) : U(\colim_i X_i) \to U(\colim_i Y_i)$.
-Since $U(\colim_i f_i)$ is a monomorphism in $\D$ and $U$ is faithful, it follows that $\colim_i f_i$ is a monomorphism in $\C$. $\square$
+Since $U(\colim_i f_i)$ is a monomorphism in $\D$ and $U$ is faithful, it follows that $\colim_i f_i$ is a monomorphism in $\C$.
+:::
::: Lemma 3
Let $U : \C \to \D$ be a fully faithful functor with a left adjoint $L : \D \to \C$ (i.e. $\C$ is equivalent to a reflective subcategory of $\D$). Assume that $\D$ has exact filtered colimits, that $\C$ has finite limits, and that $L$ preserves finite limits. Then $\C$ also has exact filtered colimits.
:::
-_Proof._
+::: Proof
It is well known (and easy to prove) that the colimit of a diagram $(X_j)$ in $\C$ is given by $L(\colim_j U(X_j))$, provided that the colimit in $\D$ exists. In particular, $\C$ has filtered colimits. By assumption, it also has finite limits, and $U$ preserves them since it is a right adjoint. Now let $X : \I \times \J \to \C$ be a diagram, where $\I$ is finite and $\J$ is filtered. We compute:
$$
@@ -46,21 +48,23 @@ $$
\end{align*}
$$
-$\square$
+:::
::: Lemma 4
Let $U : \C \to \D$ be a fully faithful functor. Assume that $\C$ has finite products and filtered colimits, and that $U$ preserves binary products and filtered colimits. If $\D$ has cartesian filtered colimits, then so does $\C$.
:::
-_Proof._
-Let $X$ be an object of $\C$ and $Y : \I \to \C$ a filtered diagram. Then we have the canonical comparison map $c : \colim_{i\in\I} (X \times Y_i) \to X \times \colim_{i\in\I} Y_i$. By the assumptions, $Uc$ is equivalent to the comparison map $\colim_{i\in\I} (UX \times UY_i) \to UX \times \colim_{i\in\I} UY_i$, which is an isomorphism. Since $U$ is fully faithful and therefore conservative, we conclude that $c$ is an isomorphism. $\square$
+::: Proof
+Let $X$ be an object of $\C$ and $Y : \I \to \C$ a filtered diagram. Then we have the canonical comparison map $c : \colim_{i\in\I} (X \times Y_i) \to X \times \colim_{i\in\I} Y_i$. By the assumptions, $Uc$ is equivalent to the comparison map $\colim_{i\in\I} (UX \times UY_i) \to UX \times \colim_{i\in\I} UY_i$, which is an isomorphism. Since $U$ is fully faithful and therefore conservative, we conclude that $c$ is an isomorphism.
+:::
::: Lemma 5
Let $U : \C \to \D$ be a fully faithful functor with a right adjoint $R : \D \to \C$ (i.e. $\C$ is equivalent to a coreflective subcategory of $\D$). Assume that $\C$ has binary products, and that $U$ preserves these binary products. If $\D$ is cartesian closed, then so is $\C$, with exponentials in $\C$ given by
$$[X, Y]_{\C} \cong R([UX, UY]_{\D}).$$
:::
-_Proof._ For any objects $X, Y, Z$ of $\C$ we have natural isomorphisms
+::: Proof
+For any objects $X, Y, Z$ of $\C$ we have natural isomorphisms
$$
\begin{align*}
@@ -70,40 +74,47 @@ $$
\end{align*}
$$
-$\square$
+:::
::: Corollary 6
If $\C$ is a cartesian closed category and $P$ is a [subterminal object](https://ncatlab.org/nlab/show/subterminal+object) of $\C$, then the slice category $\C / P$ is also cartesian closed, with exponentials in $\C / P$ given by
$$[X, Y]_{\C / P} \cong [X, Y]_{\C} \times P.$$
:::
-_Proof._ The forgetful functor $\C / P \to \C$ is fully faithful; it has right adjoint ${-} \times P$; and it preserves binary products (in fact all inhabited limits). Hence, Lemma 5 applies. $\square$
+::: Proof
+The forgetful functor $\C / P \to \C$ is fully faithful; it has right adjoint ${-} \times P$; and it preserves binary products (in fact all inhabited limits). Hence, Lemma 5 applies.
+:::
::: Lemma 7
Let $U : \C \to \D$ be a fully faithful functor. Assume that $\C$ has finite limits and coequalizers, and that $U$ preserves pullbacks and coequalizers. If $\D$ is regular, then so is $\C$.
:::
-_Proof._ Since $\C$ has finite limits and coequalizers, the only nontrivial part of proving $\C$ is regular is to check that regular epimorphisms are stable under pullbacks in $\C$. Since $U$ preserves pullbacks and regular epimorphisms, it suffices to show that $U$ reflects regular epimorphisms. Thus, suppose $f : X \to Y$ is a morphism in $\C$ with $Uf$ a regular epimorphism. Then in $\C$ we have the diagram
+::: Proof
+Since $\C$ has finite limits and coequalizers, the only nontrivial part of proving $\C$ is regular is to check that regular epimorphisms are stable under pullbacks in $\C$. Since $U$ preserves pullbacks and regular epimorphisms, it suffices to show that $U$ reflects regular epimorphisms. Thus, suppose $f : X \to Y$ is a morphism in $\C$ with $Uf$ a regular epimorphism. Then in $\C$ we have the diagram
$$X \times_Y X \rightrightarrows X \to \im(f) \xrightarrow{i} Y$$
where $X \times_Y X$ is the kernel pair of $f$, and $\im(f)$ is the coequalizer. By the assumptions, the image under $U$ is equivalent to the diagram in $\D$:
$$UX \times_{UY} UX \rightrightarrows UX \to \im(Uf) \xrightarrow{Ui} UY$$
-where $UX \times_{UY} UX$ is the kernel pair of $Uf$, and $\im(Uf)$ is the coequalizer. Since $Uf$ is a regular epimorphism, we must have $Ui$ is an isomorphism. Since $U$ is fully faithful and therefore conservative, we get $i$ is an isomorphism as well, so $f$ is a regular epimorphism. $\square$
+where $UX \times_{UY} UX$ is the kernel pair of $Uf$, and $\im(Uf)$ is the coequalizer. Since $Uf$ is a regular epimorphism, we must have $Ui$ is an isomorphism. Since $U$ is fully faithful and therefore conservative, we get $i$ is an isomorphism as well, so $f$ is a regular epimorphism.
+:::
::: Lemma 8
Let $U : \C \to \D$ be a fully faithful functor. Assume that $\C$ has finite limits and coequalizers, and that $U$ preserves inhabited finite limits and coequalizers. If $\D$ has effective congruences, then so does $\C$.
:::
-_Proof._ Suppose we have a congruence $E \hookrightarrow X\times X$ in $\C$. We can then form the quotient $X \to X/E$ as a coequalizer, along with the kernel pair $X \times_{X/E} X$ and the comparison map $i$ in the diagram below:
+::: Proof
+Suppose we have a congruence $E \hookrightarrow X\times X$ in $\C$. We can then form the quotient $X \to X/E$ as a coequalizer, along with the kernel pair $X \times_{X/E} X$ and the comparison map $i$ in the diagram below:
$$E \xrightarrow{i} X \times_{X/E} X \rightrightarrows X \to X/E.$$
By the assumptions, the image under $U$ is equivalent to the diagram in $\D$:
$$UE \xrightarrow{Ui} UX \times_{U(X/E)} UX \rightrightarrows UX \to U(X/E).$$
-Here, $UE \rightrightarrows UX$ is a congruence: the map $UE \to UX \times UX$ is a monomorphism since $U$ preserves pullbacks and therefore preserves monomorphisms; the reflexivity and symmetry morphisms for $E$ are easily seen to transform under $U$ to reflexivity and symmetry morphisms for $UE$; and similarly, since $U$ preserves pullbacks, the transitivity morphism for $E$ transforms under $U$ to a transitivity morphism for $UE$. This congruence $UE$ of $\D$ is effective, so we must have $Ui$ is an isomorphism. Since $U$ is fully faithful and therefore conservative, we get $i$ is an isomorphism as well, so $E$ is effective. $\square$
+Here, $UE \rightrightarrows UX$ is a congruence: the map $UE \to UX \times UX$ is a monomorphism since $U$ preserves pullbacks and therefore preserves monomorphisms; the reflexivity and symmetry morphisms for $E$ are easily seen to transform under $U$ to reflexivity and symmetry morphisms for $UE$; and similarly, since $U$ preserves pullbacks, the transitivity morphism for $E$ transforms under $U$ to a transitivity morphism for $UE$. This congruence $UE$ of $\D$ is effective, so we must have $Ui$ is an isomorphism. Since $U$ is fully faithful and therefore conservative, we get $i$ is an isomorphism as well, so $E$ is effective.
+:::
::: Lemma 9
Let $L$ be a functor which is left adjoint to a faithful functor $U$. Then $L$ preserves generating sets. (Thus in particular, any reflective subcategory of a category with a generating set also has a generating set; and similarly for a single generator.)
:::
-_Proof._ If $S$ is a generating set,
+::: Proof
+If $S$ is a generating set,
$$
\begin{align*}
@@ -112,16 +123,21 @@ $$
\end{align*}
$$
-is a composition of faithful functors, hence faithful. $\square$
+is a composition of faithful functors, hence faithful.
+:::
::: Lemma 10
Any fully faithful functor reflects extremal generating sets (and therefore, by duality, it also reflects extremal cogenerating sets). In other words, if $U : \C \to \D$ is a fully faithful functor, and $S$ is a set of objects such that $U(S)$ is an extremal generating set of $\D$, then $S$ is an extremal generating set of $\C$.
:::
-_Proof:_ Under the given assumptions, we can factor $\C \to (\Set^+)^S$, $X \mapsto (\Hom_\C(G, X))_{G\in S}$, as being isomorphic to the composition of $U : \C \to D$ followed by $Y \mapsto (\Hom_\D(UG, Y))_{G\in S}$, using the assumption on $U$ to identify $\Hom_\D(UG, UX)$ with $\Hom_C(G, X)$ naturally in $X$. In this composition, the first is fully faithful and therefore also conservative; and the second is assumed to be faithful and conservative. Therefore, the composition is also faithful and conservative. $\square$
+::: Proof
+Under the given assumptions, we can factor $\C \to (\Set^+)^S$, $X \mapsto (\Hom_\C(G, X))_{G\in S}$, as being isomorphic to the composition of $U : \C \to D$ followed by $Y \mapsto (\Hom_\D(UG, Y))_{G\in S}$, using the assumption on $U$ to identify $\Hom_\D(UG, UX)$ with $\Hom_C(G, X)$ naturally in $X$. In this composition, the first is fully faithful and therefore also conservative; and the second is assumed to be faithful and conservative. Therefore, the composition is also faithful and conservative.
+:::
::: Lemma 11
Let $U : \C \to \D$ be a faithful conservative functor (for example, a fully faithful functor). Assume that $\D$ is extensive, that $\C$ has finite coproducts and pullbacks along coproduct inclusions, and that $U$ preserves both. Then $\C$ is extensive. A similar statement holds for infinitary extensive (and countably extensive) categories, in which case we assume that $\C$ has all coproducts (resp. all countable coproducts) and that $U$ preserves these.
:::
-_Proof._ This is straight forward. We need to prove that finite coproducts are disjoint and stable under pullbacks in $\C$. If $A,B \in \C$, the coproduct inclusion $A \to A + B$ is a monomorphism: Since $U$ is faithful, it suffices to prove that its image under $U$ is a monomorphism. Since $U$ preserves finite coproducts, the image identifies with the coproduct inclusion $U(A) \to U(A) + U(B)$, which is a monomorphism since $\D$ is extensive. Moreover, the unique morphism $0 \to A \times_{A + B} B$ is an isomorphism: Since $U$ is conservative, it suffices to prove that its image under $U$ is an isomorphism. Since $U$ preserves finite coproducts and pullbacks along coproduct inclusions, the image identifies with the unique morphism $0 \to U(A) \times_{U(A) + U(B)} U(B)$, which is an isomorphism since $\D$ is extensive. This proves that finite coproducts are disjoint in $\C$. To prove that they are stable under pullbacks, let $T \to A + B$ be any morphism in $\C$, and consider the pullbacks $T_A \coloneqq T \times_{A + B} A$ and $T_B \coloneqq T \times_{A + B} B$. We need to show that the canonical morphism $T_A + T_B \to T$ is an isomorphism. Since $U$ is conservative, it suffices to prove that its image under $U$ is an isomorphism. Since $U$ preserves finite coproducts and pullbacks along coproduct inclusions, the image identifies with the canonical morphism $U(T)_{U(A)} + U(T)_{U(B)} \to U(T)$ induced by the morphism $U(T) \to U(A) + U(B)$ in $\D$, which is an isomorphism since $\D$ is extensive. $\square$
+::: Proof
+This is straight forward. We need to prove that finite coproducts are disjoint and stable under pullbacks in $\C$. If $A,B \in \C$, the coproduct inclusion $A \to A + B$ is a monomorphism: Since $U$ is faithful, it suffices to prove that its image under $U$ is a monomorphism. Since $U$ preserves finite coproducts, the image identifies with the coproduct inclusion $U(A) \to U(A) + U(B)$, which is a monomorphism since $\D$ is extensive. Moreover, the unique morphism $0 \to A \times_{A + B} B$ is an isomorphism: Since $U$ is conservative, it suffices to prove that its image under $U$ is an isomorphism. Since $U$ preserves finite coproducts and pullbacks along coproduct inclusions, the image identifies with the unique morphism $0 \to U(A) \times_{U(A) + U(B)} U(B)$, which is an isomorphism since $\D$ is extensive. This proves that finite coproducts are disjoint in $\C$. To prove that they are stable under pullbacks, let $T \to A + B$ be any morphism in $\C$, and consider the pullbacks $T_A \coloneqq T \times_{A + B} A$ and $T_B \coloneqq T \times_{A + B} B$. We need to show that the canonical morphism $T_A + T_B \to T$ is an isomorphism. Since $U$ is conservative, it suffices to prove that its image under $U$ is an isomorphism. Since $U$ preserves finite coproducts and pullbacks along coproduct inclusions, the image identifies with the canonical morphism $U(T)_{U(A)} + U(T)_{U(B)} \to U(T)$ induced by the morphism $U(T) \to U(A) + U(B)$ in $\D$, which is an isomorphism since $\D$ is extensive.
+:::
diff --git a/content/thin_algebraic_categories.md b/content/thin_algebraic_categories.md
index b57fb19c..e101ee9f 100644
--- a/content/thin_algebraic_categories.md
+++ b/content/thin_algebraic_categories.md
@@ -15,7 +15,8 @@ Evaluate later if we want to remove it.
Let $\C$ be a [thin](/category-property/thin) and [one-sorted finitary algebraic](/category-property/one-sorted_finitary_algebraic) category. Then $\C \simeq 1$ or $\C \simeq I$, where $I$ is the walking morphism.
:::
-_Proof._
-Let $F : \Set \to \C$ denote the free algebra functor. Every object $A \in \C$ admits a regular epimorphism $F(X) \twoheadrightarrow A$ for some set $X$. But since $\C$ is thin, every regular epimorphism must be an isomorphism. Thus, $A \cong F(X)$. Also, $F(X)$ is a coproduct of copies of $F(1)$, which means it is either the initial object $0$ or $F(1)$ itself (since $\C$ is thin). If $F(1) \cong 0$, then every object is isomorphic to the initial object $0$, and hence $\C$ is trivial. If not, then $\C$ has exactly two objects up to isomorphism, $0$ and $F(1)$, there is a morphism $0 \to F(1)$, but no morphism $F(1) \to 0$. Since $\C$ is thin, we conclude $\C \simeq I$. $\square$
+::: Proof
+Let $F : \Set \to \C$ denote the free algebra functor. Every object $A \in \C$ admits a regular epimorphism $F(X) \twoheadrightarrow A$ for some set $X$. But since $\C$ is thin, every regular epimorphism must be an isomorphism. Thus, $A \cong F(X)$. Also, $F(X)$ is a coproduct of copies of $F(1)$, which means it is either the initial object $0$ or $F(1)$ itself (since $\C$ is thin). If $F(1) \cong 0$, then every object is isomorphic to the initial object $0$, and hence $\C$ is trivial. If not, then $\C$ has exactly two objects up to isomorphism, $0$ and $F(1)$, there is a morphism $0 \to F(1)$, but no morphism $F(1) \to 0$. Since $\C$ is thin, we conclude $\C \simeq I$.
+:::
Remark: Another proof is possible by using the Lemma [here](/content/thin_extremal_generator).
diff --git a/content/thin_extremal_generator.md b/content/thin_extremal_generator.md
index 547184f1..dc97dcf4 100644
--- a/content/thin_extremal_generator.md
+++ b/content/thin_extremal_generator.md
@@ -9,14 +9,18 @@ description: A result restricting which thin categories can have an extremal gen
Suppose $G$ is an object of a thin category. Then $G$ is an extremal generator if and only if for every object $X$, either $X \cong G$ or every morphism with codomain $X$ is an isomorphism.
:::
-_Proof._ ($\Rightarrow$) Since the category is thin, $\Hom(G, X)$ is either a singleton or empty. In the first case, let $f \in \Hom(G, X)$. Then $f \circ {-} : \Hom(G, G) \to \Hom(G, X)$ is automatically a bijection since $\Hom(G, G) = \{ \id_G \}$ is also a singleton, implying that $f$ is an isomorphism.
+::: Proof
+($\Rightarrow$) Since the category is thin, $\Hom(G, X)$ is either a singleton or empty. In the first case, let $f \in \Hom(G, X)$. Then $f \circ {-} : \Hom(G, G) \to \Hom(G, X)$ is automatically a bijection since $\Hom(G, G) = \{ \id_G \}$ is also a singleton, implying that $f$ is an isomorphism.
In the second case, suppose we have a morphism $g : Y \to X$. Then $g \circ {-} : \Hom(G, Y) \to \Hom(G, X)$ is a function with empty codomain, so it is automatically a bijection, implying that $g$ is an isomorphism.
-($\Leftarrow$) Since the category is thin, any object is automatically a generator. Now suppose we have a morphism $f : X \to Y$ such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. Then by assumption, either $Y \cong G$ or every morphism with codomain $Y$ is an isomorphism. In the first case, $\Hom(G, Y)$ is non-empty, so $\Hom(G, X)$ is also non-empty. We also have $\Hom(Y, G)$ is non-empty. Therefore, $\Hom(Y, X)$ is non-empty, and the (necessarily unique) morphism $Y \to X$ is automatically an inverse to $f$. In the second case, $f$ is already a morphism with codomain $Y$ so it is an isomorphism. $\square$
+($\Leftarrow$) Since the category is thin, any object is automatically a generator. Now suppose we have a morphism $f : X \to Y$ such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. Then by assumption, either $Y \cong G$ or every morphism with codomain $Y$ is an isomorphism. In the first case, $\Hom(G, Y)$ is non-empty, so $\Hom(G, X)$ is also non-empty. We also have $\Hom(Y, G)$ is non-empty. Therefore, $\Hom(Y, X)$ is non-empty, and the (necessarily unique) morphism $Y \to X$ is automatically an inverse to $f$. In the second case, $f$ is already a morphism with codomain $Y$ so it is an isomorphism.
+:::
::: Corollary
For a poset $P$, the corresponding thin category has an extremal generator if and only if $P$ is non-empty and it has at most one non-minimal element. In particular, if this is the case, then either the poset is discrete, in which case any element gives an extremal generator; or otherwise, there is exactly one non-minimal element which is the unique extremal generator.
:::
-_Proof._ In a thin category coming from a poset, the condition in the previous lemma that every morphism with codomain $X$ is an isomorphism is equivalent to the corresponding element of the poset being minimal. $\square$
+::: Proof
+In a thin category coming from a poset, the condition in the previous lemma that every morphism with codomain $X$ is an isomorphism is equivalent to the corresponding element of the poset being minimal.
+:::
diff --git a/content/topos-with-generator.md b/content/topos-with-generator.md
index da2be294..c13a3c14 100644
--- a/content/topos-with-generator.md
+++ b/content/topos-with-generator.md
@@ -9,12 +9,16 @@ description: An elementary topos with a generator has at most two subterminal ob
Suppose a category is coregular, and it has disjoint finite coproducts, a terminal object, and a generator. Then every regular subterminal object (i.e. an object $X$ such that the unique morphism $X \to 1$ is a regular monomorphism) is either initial or terminal.
:::
-_Proof._ Suppose $G$ is a generator, and let $P$ be a regular subterminal object. If the two inclusion morphisms $P \rightrightarrows P + P$ are equal, then by disjointness of finite coproducts, $P$ must be initial. Otherwise, in order for $G$ to distinguish these two morphisms, there must be a morphism $G \to P$, which implies that the unique morphism $G \to 1$ factors through $P$.
+::: Proof
+Suppose $G$ is a generator, and let $P$ be a regular subterminal object. If the two inclusion morphisms $P \rightrightarrows P + P$ are equal, then by disjointness of finite coproducts, $P$ must be initial. Otherwise, in order for $G$ to distinguish these two morphisms, there must be a morphism $G \to P$, which implies that the unique morphism $G \to 1$ factors through $P$.
-Now, if we consider the two morphisms $i_1, i_2 : 1 \rightrightarrows 1 +_P 1$, we see that for every morphism $f : G \to 1$ (of which there is exactly one), we have $i_1 \circ f = i_2 \circ f$. Since $G$ is a generator, that implies $i_1 = i_2$. On the other hand, by coregularity, we see that the equalizer of $i_1, i_2 : 1 \rightrightarrows 1 +_P 1$ is $P$. Therefore, we conclude that $P \simeq 1$. $\square$
+Now, if we consider the two morphisms $i_1, i_2 : 1 \rightrightarrows 1 +_P 1$, we see that for every morphism $f : G \to 1$ (of which there is exactly one), we have $i_1 \circ f = i_2 \circ f$. Since $G$ is a generator, that implies $i_1 = i_2$. On the other hand, by coregularity, we see that the equalizer of $i_1, i_2 : 1 \rightrightarrows 1 +_P 1$ is $P$. Therefore, we conclude that $P \simeq 1$.
+:::
::: Corollary
In an elementary topos with a generator, every subterminal object is either initial or terminal.
:::
-_Proof._ An elementary topos satisfies all the conditions of the lemma; and it is also mono-regular so that every subterminal object is automatically regular subterminal. $\square$
+::: Proof
+An elementary topos satisfies all the conditions of the lemma; and it is also mono-regular so that every subterminal object is automatically regular subterminal.
+:::
diff --git a/src/lib/server/markdown.ts b/src/lib/server/markdown.ts
index 0d508a52..67011cfd 100644
--- a/src/lib/server/markdown.ts
+++ b/src/lib/server/markdown.ts
@@ -75,6 +75,59 @@ md.block.ruler.before(
}
)
+// add proof environments
+md.block.ruler.before(
+ 'fence',
+ 'proof_environment',
+ (state, start_line, end_line, silent) => {
+ const start = state.bMarks[start_line] + state.tShift[start_line]
+ const max = state.eMarks[start_line]
+ const line = state.src.slice(start, max).trim()
+
+ if (!/^:::\s*Proof$/i.test(line)) return false
+
+ let next_line = start_line + 1
+
+ while (next_line < end_line) {
+ const nStart = state.bMarks[next_line] + state.tShift[next_line]
+ const nEnd = state.eMarks[next_line]
+ const text = state.src.slice(nStart, nEnd).trim()
+
+ if (text === ':::') break
+ next_line++
+ }
+
+ if (silent) return true
+
+ const open = state.push('html_block', '', 0)
+ open.content = ``
+
+ const token_start = state.tokens.length
+
+ state.md.block.tokenize(state, start_line + 1, next_line)
+
+ const proof_tokens = state.tokens.slice(token_start)
+
+ const first_inline = proof_tokens.find((token) => token.type === 'inline')
+
+ const last_inline = [...proof_tokens].findLast((token) => token.type === 'inline')
+
+ if (first_inline) {
+ first_inline.content = `Proof. ${first_inline.content}`
+ }
+
+ if (last_inline) {
+ last_inline.content += ` ${render_formula('\\square')}`
+ }
+
+ const close = state.push('html_block', '', 0)
+ close.content = `
`
+
+ state.line = next_line + 1
+ return true
+ }
+)
+
/**
* Replaces the math formulas in a markdown text with placeholders and
* returns a dictionary with the rendered formulas.
diff --git a/src/routes/content/[id]/+page.svelte b/src/routes/content/[id]/+page.svelte
index 7296ce4a..5e761a02 100644
--- a/src/routes/content/[id]/+page.svelte
+++ b/src/routes/content/[id]/+page.svelte
@@ -91,12 +91,20 @@
}
}
- :global(span.qed) {
- float: right;
- }
+ :global(.proof) {
+ :global(.proof-title) {
+ font-style: italic;
+ }
- :global(p:has(span.qed:only-child)) {
- height: 1lh;
+ :global(.qed) {
+ float: right;
+ margin-left: 0.5rem;
+ }
+
+ :global(.qed-clear) {
+ display: block;
+ clear: both;
+ }
}
:global(pre) {