diff --git a/content/cocongruences_of_groups.md b/content/cocongruences_of_groups.md new file mode 100644 index 000000000..cf295ff38 --- /dev/null +++ b/content/cocongruences_of_groups.md @@ -0,0 +1,104 @@ +--- +title: Cocongruences on groups are effective +description: This result will be proved more generally for categories in which pushouts and monomorphisms interact in a suitable way. +author: Martin Brandenburg +--- + +## Cocongruences on groups are effective + +Our goal is to prove that every cocongruence in $\Grp$ is effective. We will establish a more general result for categories in which pushouts and monomorphisms interact in a suitable way. + +We shall say that a category $\C$ has _good pushouts of monomorphisms_ if it has pushouts of monomorphisms and if, for every diagram of monomorphisms + +$$ +\begin{CD} +B @>>> B' \\ +@AAA @AAA \\ +A @>>> A' \\ +@VVV @VVV \\ +C @>>> C' +\end{CD} +$$ + +in which each square is a pullback, the induced morphism +$$B \sqcup_A C \to B' \sqcup_{A'} C'$$ +is also a monomorphism. + +::: Proposition 1 +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$. + +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,$$ +where $a \in A$, each $x_i$ lies either in $S \setminus \{1\}$ or in $T \setminus \{1\}$, and these choices alternate. + +The map + +$$A \backslash B \to A' \backslash B', \, Ab \mapsto A'b$$ + +is injective. Indeed, if $b_1,b_2 \in B$ satisfy $A' b_1 = A' b_2$, then $b_1 b_2^{-1} \in A'$. Since $B \cap A' = A$, it follows that $b_1 b_2^{-1} \in A$, and hence $A b_1 = A b_2$. + +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$ + +::: 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 + +$$r \circ i_1 = \id_X, \quad r \circ i_2 = \id_X.$$ + +In particular, $i_1$ and $i_2$ are monomorphisms. Since the cocongruence is cotransitive, there exists a morphism + +$$c : Y \to Y \sqcup_{i_2,X,i_1} Y$$ + +satisfying + +$$c \circ i_1 = u_1 \circ i_1, \quad c \circ i_2 = u_2 \circ i_2,$$ + +where $u_1,u_2 : Y \rightrightarrows Y \sqcup_{i_2,X,i_1} Y$ are the pushout inclusions satisfying $u_1 i_2 = u_2 i_1$. We will not use the fact that the cocongruence is cosymmetric; this will follow automatically. Define the monomorphism + +$$E := \eq(i_1,i_2) \hookrightarrow X.$$ + +Since $i_1$ and $i_2$ agree on $E$, there exists a unique morphism + +$$\varphi : X \sqcup_E X \to Y$$ + +defined by $\varphi \circ j_1 = i_1$ and $\varphi \circ j_2 = i_2$, where $j_1,j_2 : X \rightrightarrows X \sqcup_E X$ are the two inclusions. + +We must show that $\varphi$ is an isomorphism. It is clearly an epimorphism, since $i_1$ and $i_2$ are jointly epimorphic by assumption. Since $\C$ is balanced, it therefore suffices to prove that $\varphi$ is a monomorphism. + +We will show that even the morphism + +$$\gamma := c \circ \varphi : X \sqcup_E X \to Y \sqcup_{i_2,X,i_1} Y$$ + +is a monomorphism. It is characterized by + +$$\gamma \circ j_1 = c \circ \varphi \circ j_1 = c \circ i_1 = u_1 \circ i_1,$$ +$$\gamma \circ j_2 = c \circ \varphi \circ j_2 = c \circ i_2 = u_2 \circ i_2.$$ + +In other words, $\gamma$ is induced by the diagram of monomorphisms + +$$ +\begin{CD} +X @>{i_1}>> Y \\ +@AAA @AA{i_2}A \\ +E @>>> X \\ +@VVV @VV{i_2}V \\ +X @>>{i_2}> Y +\end{CD} +$$ + +Since $\C$ has good pushouts of monomorphisms, it suffices to verify that both squares are pullbacks. Observe that the two squares are symmetric, so it is enough to consider one of them. To verify the universal property, let $a : T \to X$ and $b : T \to X$ be morphisms satisfying $i_1 \circ a = i_2 \circ b$. Applying $r : Y \to X$, we obtain + +$$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 \hookrightarrow X$. $\square$ + +::: Corollary 3 +Every cocongruence in the category $\Grp$ is effective. +::: diff --git a/content/comphaus_copresentable.md b/content/comphaus_copresentable.md new file mode 100644 index 000000000..332d6d9af --- /dev/null +++ b/content/comphaus_copresentable.md @@ -0,0 +1,114 @@ +--- +title: Local ℵ₁-copresentability of the category of compact Hausdorff spaces +description: We gather several relevant results about the category of compact Hausdorff spaces, and provide accessible proofs of these facts leading up to a proof that it is locally ℵ₁-copresentable. +author: Daniel Schepler +--- + +## Local ℵ₁-copresentability of the category of compact Hausdorff spaces + +Our purpose here is to gather several relevant results about $\CompHaus$, the [category of compact Hausdorff spaces](/category/CompHaus), and provide accessible (sic) proofs of these facts leading up to a proof that it is locally $\aleph_1$-copresentable. + +A good overview of some of these results is contained in the introduction of [HNN13](#references). + +We first prove a couple preliminary results. + +::: Lemma 1 +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 X_i$ is also non-empty. +::: + +_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 := \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 := \{ 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$ + +::: 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._ +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$ + +::: Proposition 3 +The functor $\Hom({-}, [0, 1]) : \CompHaus^{\op} \to \Set$ is monadic. (Originally proved in [Dus69](#references)) +::: + +_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}(X, [0, 1]^S) \simeq \Hom_{\Set}(S, \Hom_{\CompHaus}(X, [0, 1])).$$ + +To see the functor is conservative, suppose we have a continuous function $f : X \to Y$ such that $f^* : \Hom(Y, [0, 1]) \to \Hom(X, [0, 1])$ is a bijection. Then for any $x_1, x_2 \in X$ with $x_1 \ne x_2$, there exists $\varphi : X \to [0, 1]$ with $\varphi(x_1) = 0$ and $\varphi(x_2) = 1$ by Urysohn's lemma. Since $f^*$ is surjective, there exists $\psi : Y \to [0, 1]$ with $\varphi = \psi \circ f$; thus, we must have $f(x_1) \ne f(x_2)$. Likewise, we know the image of $f$ is closed. If this image is not all of $Y$, then by Urysohn's lemma there exists nonzero $\varphi : Y \to [0, 1]$ which is zero on the image. But then $\varphi \circ f = 0 \circ f$, contradicting the injectivity of $f^*$. Thus, $f$ is a bijective continuous function, and therefore a homeomorphism. + +Finally, suppose we have a coreflexive equalizer pair + +$$E \xhookrightarrow{i} A ~\overset{f}{\underset{g}{\rightrightarrows}}~ B$$ + +with $r : B \to A$. We may assume that $i$ is a subspace inclusion map. We may use $r$ to think of $B$ as a bundle of compact spaces over $A$, with two sections $f, g$. We then need to show that + +$$\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$ + +This shows that $\CompHaus^{\op}$ is equivalent to the category of algebras over the monad $S \mapsto \Hom_{\CompHaus}([0, 1]^S, [0, 1])$. We may view such algebras as being models of the infinitary algebraic theory of all continuous functions $[0,1]^S \to [0,1]$. In fact, we can show that any such function only depends on countably many coordinates in the domain, so that operations of this theory will be generated by the continuous functions $[0,1]^\omega \to [0,1]$. Indeed, we get the following somewhat stronger result: + +::: Proposition 4 +The object $[0,1]$ of $\CompHaus$ is $\aleph_1$-copresentable. (Originally proved in [GU71](#references), 6.5(c)) +::: + +_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 := (\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$. + +To summarize, we have shown that for each $n \in \IN_{>0}$, there exists $i \in \I$ and a finite cover $\{ V_\lambda \mid \lambda \in \Lambda \}$ of $\im(p_i)$ such that whenever $p_i(x), p_i(y) \in V_\lambda$ for some $\lambda$, we have $|\varphi(x) - \varphi(y)| < 1/n$. Now choose such a $i_n$ and associated finite cover of $\im(p_{i_n})$ for each $n$. Then use the fact that $\I$ is $\aleph_1$-cofiltered to take a cone $(j, f_n : j \to i_n)$ of the objects $i_n$. We then see that whenever we have $x, y\in X$ with $p_j(x) = p_j(y)$, then $\varphi(x) = \varphi(y)$. Thus, $\varphi$ induces a well-defined function on the image of $p_j$. This function is continuous, since by construction for any $n\in \IN_{>0}$ and $x \in X$, there is a neighborhood $V$ of $p_j(x)$ such that whenever $p_j(y)\in V$ as well, $|\varphi(y) - \varphi(x)| < 1/n$. By the Tietze extension theorem, this induced function can then be extended to a continuous function $\psi : X_j \to [0,1]$. Then $\varphi = \psi \circ p_j$. + +This shows the canonical map +$$\textstyle \colim_{i\in \I^{\op}} \Hom(X_i, [0,1]) \to \Hom(\lim_{i\in \I} X_i, [0,1])$$ +is surjective. + +Likewise, suppose we have $\alpha, \beta : X_i \rightrightarrows [0,1]$ such that $\alpha \circ p_i = \beta \circ p_i$. For each $n\in \IN_{>0}$, consider the set $D_n := \{ x \in X_i \mid |\alpha(x) - \beta(x)| \ge 1/n \}$. Note that $D_n$ is a closed subset of $X_i$, so it is compact. For any $x \in D_n$, we must have $x \notin \im(p_i)$. Using the contrapositive of lemma 1, we can conclude that there exists $f : j \to i$ such that $x \not\in \im(X_f)$. Indeed, suppose not: then the slice category $\I / i$ is cofiltered, with the limit over this slice category being the same as the limit over $\I$. Also, by the contrary assumption, we have that $x \in \im(X_f)$ for any $f : j \to i$, so $X_f^{-1}(\{ x \})$ is non-empty. Therefore, by lemma 1, the limit $p_i^{-1}(\{ x \})$ would be non-empty, contradicting the assumption. +Now each $D_n \setminus \im(X_f)$ is open and we have just shown such sets cover $D_n$; taking a finite subcover and then using the cofiltering assumption again, we conclude that there is a single $f_n : j_n \to i$ such that $\im(X_{f_n})$ is disjoint from $D_n$. Using the $\aleph_1$-cofiltering assumption to take a cone of the $f_n$, we get that there is $f : k \to i$ such that $\im(X_f)$ is disjoint from all $D_n$. This implies that $\alpha \circ X_f = \beta \circ X_f$. + +This shows the canonical map +$$\textstyle \colim_{i\in \I^{\op}} \Hom(X_i, [0,1]) \to \Hom(\lim_{i\in I} X_i, [0,1])$$ +is injective. $\square$ + +::: Corollary 5 +The category $\CompHaus$ is locally $\aleph_1$-copresentable. +::: + +_Proof._ +It suffices to show that the monad +$$S \mapsto \Hom_{\CompHaus}([0, 1]^S, [0, 1])$$ +is $\aleph_1$-accessible. This monad is the composition of +$$[0, 1]^{-} : \Set \to \CompHaus^{\op}$$ +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$ + +### References + +[Dus69]  J. Duskin, _Variations on Beck’s tripleability criterion_. Reports of the Midwest Category Seminar III, pages 74–129. Springer Berlin Heidelberg, 1969 + +[GU71]  P. Gabriel and F. Ulmer, _Lokal präsentierbare Kategorien_. Lecture Notes in Mathematics, 221, 1971. + +[Isb82]  J.R. Isbell, _Generating the algebraic theory of C(X)_, Algebra Universalis, 15 (2):153–155, 1982 + +[SGL92]  Saunders Mac Lane and Ieke Moerdijk. _Sheaves in Geometry and Logic: A First Introduction to Topos Theory._ Universitext. Springer-Verlag New York, Inc., 1992. + +[HNN13]  Dirk Hoffman, Renato Neves, and Pedro Nora. _Generating the algebraic theory of C(X): The case of partially ordered compact spaces._ Theory and Applications of Categories, 33 (12):276–295, 2018. + +[MR17]  Vincenzo Marra and Luca Reggio, _Stone duality above dimension zero: Axiomatising the algebraic theory of C(X)_, Advances in Mathematics, 307:253–287, 2017 + +[HR19]  M. Hušek and J. Rosický, _Factorization and local presentability in topological and uniform spaces_, Topology and its Applications, 259:251–266, 2019 + +[MR20]  Vincenzo Marra and Luca Reggio, _A characterisation of the category of compact Hausdorff spaces_, 2020, diff --git a/content/congruences_in_rel.md b/content/congruences_in_rel.md new file mode 100644 index 000000000..e5e1ac1e7 --- /dev/null +++ b/content/congruences_in_rel.md @@ -0,0 +1,99 @@ +--- +title: A classification of congruences in the category of sets and relations +description: The classification will prove in particular that the category of sets and relations has quotients of congruences and that congruences are effective. +author: Daniel Schepler +--- + +## A classification of congruences in the category of sets and relations + +We will give a classification of congruences in $\Rel$, the [category of sets and relations](/category/Rel). This classification will prove in particular that $\Rel$ has quotients of congruences and that congruences are effective. + +Let $i : E \hookrightarrow X \times X$ be a congruence in $\Rel$. Recall that products in $\Rel$ are actually given by disjoint unions at the level of underlying sets. Also, recall that a morphism $R : X \to Y$ in $\Rel$ is a monomorphism if and only if +$$R_* : P(X) \to P(Y),\, S \mapsto \bigl\{ y\in Y \mid \exists x\in S, (x, y) \in R \bigr\}$$ +is injective, and it is an isomorphism if and only if $R$ is the graph of a bijection $X \to Y$ in $\Set$. +In particular, we get +$$i_* : P(E) \to P(X + X) \simeq P(X) \times P(X)$$ +which must be injective. It must also preserve arbitrary unions and in particular be inclusion-preserving. From the assumption that $i$ is a congruence, since the functor $(P, {-}_*) : \Rel \to \Set$ is representable by the object 1, we see that $i_*$ must have image given by an equivalence relation $\sim$ on $P(X)$. Note also that since $i_*$ preserves arbitrary unions, we must have that $\sim$ respects arbitrary unions. + +Since the symmetry morphism $s : E \to E$ satisfies $s^2 = \id$, it must be the graph of an involution $s_0$ on $E$, where $s_0$ is a morphism in $\Set$. + +::: Claim 1 +Consider the reflexivity morphism $r : X \to E$. For each $x \in X$, $r_*(\{ x \})$ must be either a singleton or a pair. +::: + +To see this, $r_*(\{ x \})$ certainly cannot be empty, or we would have +$$i_*(r_*(\{ x \})) = (\varnothing, \varnothing) \ne (\{ x \}, \{ x \}).$$ +On the other hand, if we had at least three distinct elements $a,b,c \in r_*(\{ x \})$, then +$$i_*(\varnothing), i_*(\{ a \}), i_*(\{ a, b \}), i_*(\{ a, b, c \})$$ +would have to be a chain of four distinct subsets of $i_*(r_*(\{ x \})) = (\{ x \}, \{ x \})$, which is impossible. + +::: Claim 2 +For each $x \in X$, if $r_*(\{ x \}) = \{ e, f \}$ with $e \ne f$, then $s_0(e) = f$ and $s_0(f) = e$; and we have either that $i_*(\{e\}) = (\varnothing, \{ x \})$ and $i_*(\{f\}) = (\{ x \}, \varnothing)$, or vice versa. Otherwise, if $r_*(\{ x \}) = \{ e \}$, then $s_0(e) = e$; and $i_*(\{ e \}) = (\{ x \}, \{ x \})$. +::: + +To see this, if $r_*(\{ x \}) = \{ e, f \}$ with $e\ne f$, then we must have +$$\varnothing = i_*(\varnothing) \subsetneqq i_*(\{ e \}) \subsetneqq i_*(\{ e, f \}) = (\{ x \}, \{ x \}),$$ +which means that $i_*(\{ e \})$ is equal to either $(\{ x \}, \varnothing)$ or $(\varnothing, \{ x \})$. By the same token, $i_*(\{ f \})$ is also one of those choices, and $i_*(\{ e \}) \ne i_*(\{ f \})$. Since +$$i_*(\{ s_0(e) \}) = i_*(s_*(\{ e \})) = i_*(\{ f \})$$ +in either choice of order, by injectivity of $i_*$ we must have that $s_0(e) = f$. Similarly, $s_0(f) = e$. Otherwise, if $r_*(\{ x \}) = \{ e \}$ is a singleton, +$$i_*(\{ s_0(e) \}) = i_*(s_*(\{ e \})) = i_*(\{ e \}),$$ +so injectivity of $i_*$ gives $s_0(e) = e$. + +::: Claim 3 +For $x\in X$, suppose that $r_*(\{ x \}) = \{ e \}$. Then $\{ x \} \not\sim \varnothing$. +::: + +If we did have $\{ x \} \sim \varnothing$, then there would have to be some subset of $E$ which maps to $(\varnothing, \{ x \})$. Similarly to previous steps, injectivity of $i_*$ implies the subset is non-empty, and if the subset had two distinct elements $a,b$, then we would have +$$i_*(\varnothing) \subsetneqq i_*(\{a\}) \subsetneqq i_*(\{a,b\}) \subseteq (\varnothing, \{ x \}),$$ +giving a contradiction. Therefore, this subset of $E$ would have to be a singleton $\{ f_1 \}$. Similarly, $(\{ x \}, \varnothing)$ would have to be the image of a singleton $\{ f_2 \}$ with $f_1 \ne f_2$. But then $i_*(\{ f_1, f_2 \}) = (\{ x \}, \{ x \}) = i_*(\{ e \})$, contradicting the injectivity of $i_*$. + +::: Claim 4 +For any $e \in E$, $i_*(\{ e \})$ is of one of the forms $(\{ x \}, \varnothing)$, $(\varnothing, \{ x \})$, or $(\{ x \}, \{ x \})$. In the first two cases, $s_0(e) \ne e$ and $\{ x \} \sim \varnothing$; and in the third case, $s_0(e) = e$ and $\{ x \} \not\sim \varnothing$. +::: + +To show this, let $e\in E$, and suppose that $i_*(\{ e \}) = (S, T)$. Then $i_*(\{ s_0(e) \}) = (T, S)$, so +$$\textstyle i_*(\{ e, s_0(e) \}) = (S \cup T, S\cup T) = i_*\bigl(\bigcup_{x\in S\cup T} r_*(\{ x \})\bigr).$$ +It follows that +$$\textstyle\bigcup_{x\in S\cup T} r_*(\{ x \}) = \{ e, s_0(e) \}.$$ +Therefore, $e \in r_*(\{ x \})$ for some $x \in X$, and by claims 2 and 3, we get the desired conclusion. + +::: Claim 5 +For any $S, T \in P(X)$, $S \sim T$ if and only if $S\cap A = T\cap A$, where $A$ is the set of $x\in X$ such that $\{ x \} \not\sim \varnothing$. +::: + +For the forward direction, suppose $(S, T) = i_*(U)$ for $U \subseteq E$. Then +$$\textstyle (S, T) = \bigcup_{e\in U} i_*(\{ e \}).$$ +The set $i_*(\{ e \})$ satisfies the relation of having equal intersections with $A$ for each $e\in E$ in any case from claim 4; and this relation respects unions. For the reverse implication, whenever $x\notin A$, we have $\{ x \} \sim \varnothing$. Therefore, since +$$\textstyle S = (S \cap A) \cup \bigcup_{x\in S \setminus A} \{ x \},$$ +we must have +$$\textstyle S \sim (S \cap A) \cup \bigcup_{x\in S \setminus A} \varnothing = S \cap A.$$ +Similarly, $T \sim T \cap A$, so if $S\cap A = T\cap A$, then $S \sim T$. + +::: Claim 6 +Let $E'$ be the set pushout $X +_A X$ with inclusion maps $i_1, i_2 : X \to E'$. Define a morphism $E' \to X \times X$ in $\Rel$ given by the inverse relation of the graph $i_1 + i_2 : X + X \to E'$. Then the congruences $E$ and $E'$ are equivalent. +::: + +We can define a bijection $E \to E'$ as follows: let $e \in E$. If $i_*(\{ e \}) = (\{ x \}, \varnothing)$ with $x\notin A$, then send $e \mapsto i_1(x)$; if $i_*(\{ e \}) = (\varnothing, \{ x \})$ with $x\notin A$, then send $e \mapsto i_2(x)$; and if $i_*(\{ e \}) = (\{ x \}, \{ x \})$ with $x \in A$, then send $e \mapsto i_1(x) = i_2(x)$. Transferring the congruence to $E'$, we see that it is exactly of the given form. + +Now, without loss of generality we will assume from now on that the congruence is of exactly this form. + +With this classification, we can show that $A$ is a quotient for the congruence, with quotient morphism $\Delta_A \subseteq A \times A \subseteq X \times A$. In fact, we can define a morphism $\Delta_A^\circ : A \to X$ as the inverse relation to $\Delta_A$, and a morphism $X \to E$ as the graph of $i_1$. It is then straightforward to verify that these maps together make $A$ a split coequalizer of $p_1 \circ i$ and $p_2 \circ i$. + +We can also conclude that $E$ is the kernel pair of this quotient, by the general result below. + +::: Lemma +Suppose we have a congruence $f, g : E \rightrightarrows X$ with a contractible coequalizer +$$ E \, \overset{f}{\underset{g}{\rightrightarrows}} \, X \overset{e}{\rightarrow} Q $$ +with maps in the reverse direction $s : Q \to X$ and $t : X \to E$. Then $E$ is the kernel pair of this quotient, i.e. we have a cartesian square + +$$ +\begin{CD} +E @> f >> X \\ +@V g VV @V e VV \\ +X @> e >> A. +\end{CD} +$$ + +::: + +_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$ diff --git a/src/lib/content/foundations.md b/content/foundations.md similarity index 96% rename from src/lib/content/foundations.md rename to content/foundations.md index dcb5d70a6..dc5f2c176 100644 --- a/src/lib/content/foundations.md +++ b/content/foundations.md @@ -1,3 +1,9 @@ +--- +title: Foundations +description: How to make sense of categories in set theory +author: Martin Brandenburg +--- + ## Foundations In _CatDat_, we work with the following convenient set-theoretic foundation for category theory. @@ -22,7 +28,7 @@ Just imagine three copies of ZFC embedded into each other, each representing a " ![visualization of three levels of size](/img/three-levels-of-size.webp) -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. +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. In our framework, there is no way to group all hypercollections into a single mathematical object; for this, one would need a third Grothendieck universe $\mathrm{Set}^{++}$, but such a grouping is usually not required. diff --git a/content/walking_parallel_pair_sifted_colimit.md b/content/walking_parallel_pair_sifted_colimit.md new file mode 100644 index 000000000..a67b6d588 --- /dev/null +++ b/content/walking_parallel_pair_sifted_colimit.md @@ -0,0 +1,53 @@ +--- +title: The walking parallel pair has sifted colimits +description: A proof of this fact is presented. +author: Yuto Kawase +--- + +## The walking parallel pair has sifted colimits + +We will prove that the [walking parallel pair](/category/walking_pair) $\{u,v \colon 0 \rightrightarrows 1\}$ has [sifted colimits](/category-property/sifted_colimits). + +Let $D \colon \C \to \{u,v \colon 0 \rightrightarrows 1\}$ be a functor from a sifted category. If the object $1$ is not contained in the image under $D$, the object $0$ gives a colimit of $D$ because the sifted category $\C$ is connected. +In what follows, we suppose that there is an object $c_0 \in \C$ such that $D(c_0)=1$. + +We first claim that for every object $c \in \C$ such that $D(c)=0$, there is a morphism $f \colon c \to x$ with $D(x)=1$; moreover, which of $u$ and $v$ such a morphism is sent to by $D$ is independent of the choice of $f$. +The existence of $f$ is easy. +Indeed, since $\C$ is sifted, there is a cospan $c \rightarrow x \leftarrow c_0$, and $D(x)=1$ follows from $D(c_0)=1$. + +To show the independence of the value of $D(f)$, suppose that there are morphisms $f \colon c \to x$ and $g \colon c \to y$ such that $D(f)=u$ and $D(g)=v$. +Since $\C$ is sifted, there is a cospan consisting of $p\colon x \rightarrow z$ and $q \colon z \leftarrow y$. +Since $\C$ is sifted again, two cospans $(p \circ f, q \circ g)$ and $(\id_c, \id_c)$ are connected to each other, that is, there are a zigzag consisting of + +- $s_i \colon d_{i-1} \rightarrow e_i$, +- $t_i \colon e_i \leftarrow d_i$ $(1 \le i \le n)$, and +- parallel pairs $(l_i,r_i) \colon c \rightrightarrows d_i$ $(0 \le i \le n)$ + +such that + +- $d_0=z$, +- $l_0=p \circ f$, +- $r_0=q \circ g$, +- $d_n=c$, +- $l_n=r_n=\id_c$, +- $s_i \circ l_{i-1} = t_i \circ l_i$, and +- $s_i \circ r_{i-1} = t_i \circ r_i$ $(1 \le i \le n)$. + +@@@SVG:/img/diagram-sifted-colimit.svg@@@ + +Then, the equality $D(t_1) \circ D(l_1) = D(s_1) \circ D(l_0) = u$ implies that either $D(l_1)=u$ or $D(t_1)=u$ holds, while $D(t_1) \circ D(r_1) = D(s_1)\circ D(r_0) = v$ implies that either $D(r_1)=v$ or $D(t_1)=v$ holds. +However, the only possible combination is $D(l_1)=u$ together with $D(r_1)=v$, and by repeating this argument, we have $D(l_n)=u$ and $D(r_n)=v$, which is a contradiction. + +By the claim, each object $c \in \C$ can be classified exclusively into the following three cases: + +1. $D(c)=1$; +2. $D(c)=0$ and there is a morphism from itself sent to $u$ by $D$; +3. $D(c)=0$ and there is a morphism from itself sent to $v$ by $D$. + +Now, we have a cocone $(\alpha_c \colon D(c) \to 1)_{c \in \C}$ under $D$ by letting $\alpha_c \coloneqq \id_1$ if $c$ is classified into the first case, $\alpha_c \coloneqq u$ for the second case, and $\alpha_c \coloneqq v$ for the third case. +Moreover, this is a unique cocone under $D$: +If $\beta$ is another cocone, its vertex should be $1$ by the existence of $c_0$. +If $c \in \C$ is classified into the first case, $\beta_c$ should be the identity. +For the second case, taking a morphism $f \colon c \to x$ such that $D(f)=u$, we can obtain $\beta_c = \beta_x \circ D(f) = D(f) = u$. +Similarly, we have $\beta_c = v$ for the third case. +This concludes $\beta = \alpha$, and since there is no non-trivial endomorphism on the vertex $1$, $\alpha$ gives a colimit. diff --git a/databases/catdat/data/categories/CompHaus.yaml b/databases/catdat/data/categories/CompHaus.yaml index 0ee0c8e6b..eba3aa9b0 100644 --- a/databases/catdat/data/categories/CompHaus.yaml +++ b/databases/catdat/data/categories/CompHaus.yaml @@ -65,10 +65,10 @@ satisfied_properties: Now the identity morphism from $Y$, with the quotient topology of $f$, to $Y$ with its given topology is a bijective continuous function between compact Hausdorff spaces, so it is a homeomorphism. In other words, $f$ is a quotient map. Therefore, we see that if $g, h : E \rightrightarrows X$ is the kernel pair of $f$, and $U : \CompHaus \to \Top$ is the forgetful functor, then $U(f)$ is the coequalizer of $U(g)$ and $U(h)$. Since $U$ is fully faithful, that implies $f$ is the coequalizer of $g$ and $h$. - property: cofiltered-limit-stable epimorphisms - reason: 'Suppose we have a cofiltered diagram of epimorphisms $(f_i : X_i \to Y_i)$, and $y = (y_i) \in \lim_i Y_i$. Then by lemma 1 here, the limit of $f_i^{-1}(\{ y_i \})$ is non-empty. If $x$ is in this limit, that implies that $(\lim_i f_i)(x) = y$.' + reason: 'Suppose we have a cofiltered diagram of epimorphisms $(f_i : X_i \to Y_i)$, and $y = (y_i) \in \lim_i Y_i$. Then by lemma 1 here, the limit of $f_i^{-1}(\{ y_i \})$ is non-empty. If $x$ is in this limit, that implies that $(\lim_i f_i)(x) = y$.' - property: locally copresentable - reason: A proof can be found here. + reason: A proof can be found here. unsatisfied_properties: - property: skeletal diff --git a/databases/catdat/data/categories/Grp.yaml b/databases/catdat/data/categories/Grp.yaml index 211446d6e..4ed658ed7 100644 --- a/databases/catdat/data/categories/Grp.yaml +++ b/databases/catdat/data/categories/Grp.yaml @@ -37,7 +37,7 @@ satisfied_properties: reason: See Example 2.2.4 in Malcev, protomodular, homological and semi-abelian categories. - property: effective cocongruences - reason: A proof can be found here. + reason: A proof can be found here. unsatisfied_properties: - property: skeletal diff --git a/databases/catdat/data/categories/Rel.yaml b/databases/catdat/data/categories/Rel.yaml index f5dab65fe..67d4e8eed 100644 --- a/databases/catdat/data/categories/Rel.yaml +++ b/databases/catdat/data/categories/Rel.yaml @@ -46,10 +46,10 @@ satisfied_properties: reason: 'Let $R : A \to B$ be a relation. Define $K = \bigl\{a \in A : \neg \exists b \in B ((a,b) \in R) \bigr\}$. We have an inclusion map $I : K \to A$, which can also be regarded as relation, and $R \circ I = \empty$ is the empty relation, i.e. the zero morphism. It is easy to check the universal property.' - property: quotients of congruences - reason: A proof can be found here. + reason: A proof can be found here. - property: effective congruences - reason: A proof can be found here. + reason: A proof can be found here. unsatisfied_properties: - property: skeletal diff --git a/databases/catdat/data/categories/walking_pair.yaml b/databases/catdat/data/categories/walking_pair.yaml index d01cf5981..9b8c78031 100644 --- a/databases/catdat/data/categories/walking_pair.yaml +++ b/databases/catdat/data/categories/walking_pair.yaml @@ -41,7 +41,7 @@ satisfied_properties: reason: The two morphisms $0 \rightrightarrows 1$ are clearly monomorphisms. - property: sifted colimits - reason: A proof can be found here. + reason: A proof can be found here. unsatisfied_properties: - property: strongly connected diff --git a/databases/catdat/data/macros.yaml b/databases/catdat/data/macros.yaml index f5cf311d3..5a4f891d4 100644 --- a/databases/catdat/data/macros.yaml +++ b/databases/catdat/data/macros.yaml @@ -22,6 +22,7 @@ \J: \mathcal{J} \O: \mathcal{O} \S: \mathcal{S} +\T: \mathcal{T} # abbreviations \op: \mathrm{op} diff --git a/package.json b/package.json index d22f26cbe..a6fe16bfe 100644 --- a/package.json +++ b/package.json @@ -38,7 +38,10 @@ "better-sqlite3": "^12.9.0", "chokidar": "^5.0.0", "dotenv": "^17.3.1", + "gray-matter": "^4.0.3", "husky": "^9.1.7", + "katex": "^0.16.44", + "markdown-it": "^14.1.1", "prettier": "^3.8.1", "prettier-plugin-svelte": "^3.5.2", "svelte": "^5.55.7", @@ -57,8 +60,6 @@ "@octokit/app": "^16.1.2", "es6-crawler-detect": "^4.0.2", "ioredis": "^5.10.1", - "katex": "^0.16.44", - "markdown-it": "^14.1.1", "nodemailer": "^8.0.5", "sql-template-tag": "^5.2.1", "svelte-fa": "^4.0.4", diff --git a/pnpm-lock.yaml b/pnpm-lock.yaml index b50d0894c..d5d7783f4 100644 --- a/pnpm-lock.yaml +++ b/pnpm-lock.yaml @@ -29,12 +29,6 @@ importers: ioredis: specifier: ^5.10.1 version: 5.10.1 - katex: - specifier: ^0.16.44 - version: 0.16.45 - markdown-it: - specifier: ^14.1.1 - version: 14.1.1 nodemailer: specifier: ^8.0.5 version: 8.0.7 @@ -81,9 +75,18 @@ importers: dotenv: specifier: ^17.3.1 version: 17.4.2 + gray-matter: + specifier: ^4.0.3 + version: 4.0.3 husky: specifier: ^9.1.7 version: 9.1.7 + katex: + specifier: ^0.16.44 + version: 0.16.45 + markdown-it: + specifier: ^14.1.1 + version: 14.1.1 prettier: specifier: ^3.8.1 version: 3.8.3 @@ -796,6 +799,9 @@ packages: engines: {node: '>=0.4.0'} hasBin: true + argparse@1.0.10: + resolution: {integrity: sha512-o5Roy6tNG4SL/FOkCAN6RzjiakZS25RLYFrcMttJqbdd8BWrnA+fGz57iN5Pb06pvBGvl5gQ0B48dJlslXvoTg==} + argparse@2.0.1: resolution: {integrity: sha512-8+9WqebbFzpX9OR+Wa6O29asIogeRMzcGtAINdpMHHyAg10f05aSFVBbcEqGf/PXw1EjAZ+q2/bEBg3DvurK3Q==} @@ -916,6 +922,11 @@ packages: esm-env@1.2.2: resolution: {integrity: sha512-Epxrv+Nr/CaL4ZcFGPJIYLWFom+YeV1DqMLHJoEd9SYRxNbaFruBwfEX/kkHUJf55j2+TUbmDcmuilbP1TmXHA==} + esprima@4.0.1: + resolution: {integrity: sha512-eGuFFw7Upda+g4p+QHvnW0RyTX/SVeJBDM/gCtMARO0cLuT2HcEKnTPvhjV6aGeqrCB/sbNop0Kszm0jsaWU4A==} + engines: {node: '>=4'} + hasBin: true + esrap@2.2.5: resolution: {integrity: sha512-/yLB1538mag+dn0wsePTe8C0rDIjUOaJpMs2McodSzmM2msWcZsBSdRtg6HOBt0A/r82BN+Md3pgwSc/uWt2Ig==} peerDependencies: @@ -928,6 +939,10 @@ packages: resolution: {integrity: sha512-XYfuKMvj4O35f/pOXLObndIRvyQ+/+6AhODh+OKWj9S9498pHHn/IMszH+gt0fBCRWMNfk1ZSp5x3AifmnI2vg==} engines: {node: '>=6'} + extend-shallow@2.0.1: + resolution: {integrity: sha512-zCnTtlxNoAiDc3gqY2aYAWFx7XWWiasuF2K8Me5WbN8otHKTUKBwjPtNpRs/rbUZm7KxWAaNj7P1a/p52GbVug==} + engines: {node: '>=0.10.0'} + fast-content-type-parse@3.0.0: resolution: {integrity: sha512-ZvLdcY8P+N8mGQJahJV5G4U88CSvT1rP8ApL6uETe88MBXrBHAkZlSEySdUlyztF7ccb+Znos3TFqaepHxdhBg==} @@ -957,6 +972,10 @@ packages: github-from-package@0.0.0: resolution: {integrity: sha512-SyHy3T1v2NUXn29OsWdxmK6RwHD+vkj3v8en8AOBZ1wBQ/hCAQ5bAQTD02kW4W9tUp/3Qh6J8r9EvntiyCmOOw==} + gray-matter@4.0.3: + resolution: {integrity: sha512-5v6yZd4JK3eMI3FqqCouswVqwugaA9r4dNZB1wwcmrD02QkV5H0y7XBQW8QwQqEaZY1pM9aqORSORhJRdNK44Q==} + engines: {node: '>=6.0'} + husky@9.1.7: resolution: {integrity: sha512-5gs5ytaNjBrh5Ow3zrvdUUY+0VxIuWVL4i9irt6friV+BqdCfmV11CQTWMiBYWHbXhco+J1kHfTOUkePhCDvMA==} engines: {node: '>=18'} @@ -975,12 +994,20 @@ packages: resolution: {integrity: sha512-HuEDBTI70aYdx1v6U97SbNx9F1+svQKBDo30o0b9fw055LMepzpOOd0Ccg9Q6tbqmBSJaMuY0fB7yw9/vjBYCA==} engines: {node: '>=12.22.0'} + is-extendable@0.1.1: + resolution: {integrity: sha512-5BMULNob1vgFX6EjQw5izWDxrecWK9AM72rugNr0TFldMOi0fj6Jk+zeKIt0xGj4cEfQIJth4w3OKWOJ4f+AFw==} + engines: {node: '>=0.10.0'} + is-reference@3.0.3: resolution: {integrity: sha512-ixkJoqQvAP88E6wLydLGGqCJsrFUnqoH6HnaczB8XmDH1oaWU+xxdptvikTgaEhtZ53Ky6YXiBuUI2WXLMCwjw==} js-base64@3.7.8: resolution: {integrity: sha512-hNngCeKxIUQiEUN3GPJOkz4wF/YvdUdbNL9hsBcMQTkKzboD7T/q3OYOuuPZLUE6dBxSGpwhk5mwuDud7JVAow==} + js-yaml@3.14.2: + resolution: {integrity: sha512-PMSmkqxr106Xa156c2M265Z+FTrPl+oxd/rgOQy2tijQeK5TxQ43psO1ZCwhVOSdnn+RzkzlRz/eY4BgJBYVpg==} + hasBin: true + json-with-bigint@3.5.8: resolution: {integrity: sha512-eq/4KP6K34kwa7TcFdtvnftvHCD9KvHOGGICWwMFc4dOOKF5t4iYqnfLK8otCRCRv06FXOzGGyqE8h8ElMvvdw==} @@ -988,6 +1015,10 @@ packages: resolution: {integrity: sha512-pQpZbdBu7wCTmQUh7ufPmLr0pFoObnGUoL/yhtwJDgmmQpbkg/0HSVti25Fu4rmd1oCR6NGWe9vqTWuWv3GcNA==} hasBin: true + kind-of@6.0.3: + resolution: {integrity: sha512-dcS1ul+9tmeD95T+x28/ehLgd9mENa3LsvDTtzm3vyBEO7RPptvAD+t44WVXaUjTBRcrpFeFlC8WCruUR456hw==} + engines: {node: '>=0.10.0'} + kleur@4.1.5: resolution: {integrity: sha512-o+NO+8WrRiQEE4/7nwRJhN1HWpVmJm511pBHUxPLtp0BUISzlBplORYSmTclCnJvQq2tKu/sgl3xVpkc7ZWuQQ==} engines: {node: '>=6'} @@ -1213,6 +1244,10 @@ packages: safe-buffer@5.2.1: resolution: {integrity: sha512-rp3So07KcdmmKbGvgaNxQSJr7bGVSVk5S9Eq1F+ppbRo70+YeaDxkw5Dd8NPN+GD6bjnYm2VuPuCXmpuYvmCXQ==} + section-matter@1.0.0: + resolution: {integrity: sha512-vfD3pmTzGpufjScBh50YHKzEu2lxBWhVEHsNGoEXmCmn2hKGfeNLYMzCJpe8cD7gqX7TJluOVpBkAequ6dgMmA==} + engines: {node: '>=4'} + semver@7.7.4: resolution: {integrity: sha512-vFKC2IEtQnVhpT78h1Yp8wzwrf8CM+MzKMHGJZfBtzhZNycRFnXsHk6E5TxIkkMsgNS7mdX3AGB7x2QM2di4lA==} engines: {node: '>=10'} @@ -1235,6 +1270,9 @@ packages: resolution: {integrity: sha512-UXWMKhLOwVKb728IUtQPXxfYU+usdybtUrK/8uGE8CQMvrhOpwvzDBwj0QhSL7MQc7vIsISBG8VQ8+IDQxpfQA==} engines: {node: '>=0.10.0'} + sprintf-js@1.0.3: + resolution: {integrity: sha512-D9cPgkvLlV3t3IzL0D0YLvGA9Ahk4PcvVwUbN0dSGr1aP0Nrt4AEnTUbuGvquEC0mA64Gqt1fzirlRs5ibXx8g==} + sql-template-tag@5.2.1: resolution: {integrity: sha512-lFdvXCOqWhV40A7w4oQVDyuaNFb5yO+dhsHStZzOdtDJWCBWYv4+hhATK5nPpY5v/T1OMVcLMPeN4519qIyb9Q==} engines: {node: '>=14'} @@ -1245,6 +1283,10 @@ packages: string_decoder@1.3.0: resolution: {integrity: sha512-hkRX8U1WjJFd8LsDJ2yQ/wWWxaopEsABU1XfkM8A+j0+85JAGppt16cr1Whg6KIbb4okU6Mql6BOj+uup/wKeA==} + strip-bom-string@1.0.0: + resolution: {integrity: sha512-uCC2VHvQRYu+lMh4My/sFNmF2klFymLX1wHJeXnbEJERpV/ZsVuonzerjfrGpIGF7LBVa1O7i9kjiWvJiFck8g==} + engines: {node: '>=0.10.0'} + strip-json-comments@2.0.1: resolution: {integrity: sha512-4gB8na07fecVVkOI6Rs4e7T6NOTki5EmL7TUduTs6bu3EdnSycntVJ4re8kgZA+wx9IueI2Y11bfbgwtzuE0KQ==} engines: {node: '>=0.10.0'} @@ -1928,6 +1970,10 @@ snapshots: acorn@8.16.0: {} + argparse@1.0.10: + dependencies: + sprintf-js: 1.0.3 + argparse@2.0.1: {} aria-query@5.3.1: {} @@ -2066,12 +2112,18 @@ snapshots: esm-env@1.2.2: {} + esprima@4.0.1: {} + esrap@2.2.5: dependencies: '@jridgewell/sourcemap-codec': 1.5.5 expand-template@2.0.3: {} + extend-shallow@2.0.1: + dependencies: + is-extendable: 0.1.1 + fast-content-type-parse@3.0.0: {} fdir@6.5.0(picomatch@4.0.4): @@ -2091,6 +2143,13 @@ snapshots: github-from-package@0.0.0: {} + gray-matter@4.0.3: + dependencies: + js-yaml: 3.14.2 + kind-of: 6.0.3 + section-matter: 1.0.0 + strip-bom-string: 1.0.0 + husky@9.1.7: {} ieee754@1.2.1: {} @@ -2113,18 +2172,27 @@ snapshots: transitivePeerDependencies: - supports-color + is-extendable@0.1.1: {} + is-reference@3.0.3: dependencies: '@types/estree': 1.0.8 js-base64@3.7.8: {} + js-yaml@3.14.2: + dependencies: + argparse: 1.0.10 + esprima: 4.0.1 + json-with-bigint@3.5.8: {} katex@0.16.45: dependencies: commander: 8.3.0 + kind-of@6.0.3: {} + kleur@4.1.5: {} libsql@0.5.29: @@ -2337,6 +2405,11 @@ snapshots: safe-buffer@5.2.1: {} + section-matter@1.0.0: + dependencies: + extend-shallow: 2.0.1 + kind-of: 6.0.3 + semver@7.7.4: {} set-cookie-parser@3.1.0: {} @@ -2357,6 +2430,8 @@ snapshots: source-map-js@1.2.1: {} + sprintf-js@1.0.3: {} + sql-template-tag@5.2.1: {} standard-as-callback@2.1.0: {} @@ -2365,6 +2440,8 @@ snapshots: dependencies: safe-buffer: 5.2.1 + strip-bom-string@1.0.0: {} + strip-json-comments@2.0.1: {} svelte-check@4.4.8(picomatch@4.0.4)(svelte@5.55.7)(typescript@5.9.3): diff --git a/src/components/Footer.svelte b/src/components/Footer.svelte index 3dca753a0..c92d869d0 100644 --- a/src/components/Footer.svelte +++ b/src/components/Footer.svelte @@ -31,7 +31,7 @@
  • - Foundations + Foundations
  • diff --git a/src/components/NavMobile.svelte b/src/components/NavMobile.svelte index 13c244cbd..70a6368a7 100644 --- a/src/components/NavMobile.svelte +++ b/src/components/NavMobile.svelte @@ -119,7 +119,7 @@
  • - Foundations + Foundations
  • diff --git a/src/lib/server/rendering.ts b/src/lib/server/formulas.ts similarity index 68% rename from src/lib/server/rendering.ts rename to src/lib/server/formulas.ts index f35ddd137..fa5abc971 100644 --- a/src/lib/server/rendering.ts +++ b/src/lib/server/formulas.ts @@ -1,9 +1,10 @@ import katex from 'katex' import { is_object } from './utils' -import MarkdownIt from 'markdown-it' import { MACROS } from './macros' -function render_formula( +export const MATH_REGEX = /\$\$(.*?)\$\$|\$(.*?)\$/gs + +export function render_formula( formula: string, options: { displayMode: boolean } = { displayMode: false }, ): string { @@ -20,10 +21,8 @@ function render_formula( }) } -const math_regex = /\$\$(.*?)\$\$|\$(.*?)\$/gs - function render_formulas(txt: string): string { - return txt.replace(math_regex, (_, display_formula, inline_formula) => { + return txt.replace(MATH_REGEX, (_, display_formula, inline_formula) => { if (display_formula !== undefined) { return render_formula(display_formula, { displayMode: true }) } @@ -54,18 +53,3 @@ export function render_nested_formulas(obj: T): T { return obj } - -const md = new MarkdownIt() - -const content_dict = import.meta.glob('$lib/content/*.md', { - query: '?raw', - import: 'default', - eager: true, -}) as Record - -export function get_rendered_content(file: string) { - const key = `/src/lib/content/${file}.md` - const txt = content_dict[key] - const html = md.render(txt) - return render_formulas(html) -} diff --git a/src/lib/server/markdown.ts b/src/lib/server/markdown.ts new file mode 100644 index 000000000..05ab6a7e7 --- /dev/null +++ b/src/lib/server/markdown.ts @@ -0,0 +1,178 @@ +import MarkdownIt from 'markdown-it' +import matter from 'gray-matter' +import { MATH_REGEX, render_formula } from './formulas' +import path from 'node:path' +import fs from 'node:fs' + +const md = new MarkdownIt({ html: true }) + +// add id attribute to each heading +md.renderer.rules.heading_open = (tokens, idx, options, _, self) => { + const token = tokens[idx + 1] + const text = + token?.children + ?.filter((t) => t.type === 'text') + .map((t) => t.content) + .join('') ?? '' + const id = text.trim().replace(/\s+/g, '_').toLowerCase() + tokens[idx].attrSet('id', id) + return self.renderToken(tokens, idx, options) +} + +// open external links in new tab +md.renderer.rules.link_open = (tokens, idx, options, _, self) => { + const token = tokens[idx] + + const href_index = token.attrIndex('href') + if (href_index >= 0) { + const href = token.attrs?.[href_index]?.[1] + + if (href?.startsWith('https://') || href?.startsWith('http://')) { + token.attrSet('target', '_blank') + } + } + + return self.renderToken(tokens, idx, options) +} + +// add structure and classes to theorem environments +md.block.ruler.before( + 'fence', + 'theorem_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() + + const match = line.match(/^:::\s*(lemma|theorem|proposition|corollary|claim)/i) + if (!match) return false + + const title = line.slice(3).trim() + + 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 body_lines = state.getLines( + start_line + 1, + next_line, + state.blkIndent, + true, + ) + + const body_html = md.renderInline(body_lines.trim()) + + const token = state.push('html_block', '', 0) + token.content = + `
    ` + + `${title}.` + + `${body_html}` + + `
    ` + + 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. + */ +function preprocess_math(content: string) { + const formulas: Record = {} + + const with_placeholders = content.replace( + MATH_REGEX, + (_, display_formula, inline_formula) => { + const placeholder = `@@MATH-${Object.keys(formulas).length}@@` + + formulas[placeholder] = + display_formula === undefined + ? render_formula(inline_formula, { displayMode: false }) + : render_formula(display_formula, { displayMode: true }) + + return placeholder + }, + ) + + return { processed_content: with_placeholders, formulas } +} + +/** + * Replaces the placeholders with the rendered formulas. + */ +function postprocess_math(html: string, formulas: Record) { + for (const [placeholder, rendered] of Object.entries(formulas)) { + html = html.replaceAll(placeholder, rendered) + } + return html +} + +/** + * Replaces SVG placeholders with file contents + */ +function insert_svg(content: string) { + const regex = /@@@SVG:([^@]+)@@@/g + + return content.replace(regex, (_, src: string) => { + if (!src.startsWith('/')) return '' + + const svg_path = path.resolve(`static${src}`) + return fs.readFileSync(svg_path, 'utf8') + }) +} + +/** + * Renders markdown content and formulas of a given string + */ +function render_content>( + txt: string, +): { meta_data: T; html: string } { + const { data, content } = matter(txt) + + const { processed_content, formulas } = preprocess_math(content) + + const html = md.render(processed_content) + + const html_with_formulas = postprocess_math(html, formulas) + + const html_with_svg = insert_svg(html_with_formulas) + + return { meta_data: data as T, html: html_with_svg } +} + +/** + * Names of stored markdown files + */ +export const content_ids = fs + .readdirSync(path.resolve('content')) + .filter((file) => file.endsWith('.md')) + .map((file) => file.replace(/\.md$/, '')) + +type ContentMetaData = { + title: string + description: string + author?: string +} + +/** + * Returns the rendered content of a markdown file + */ +export function get_rendered_content(id: string) { + const file_path = path.resolve('content', `${id}.md`) + + if (!fs.existsSync(file_path)) return null + + const txt = fs.readFileSync(file_path, 'utf8') + + return render_content(txt) +} diff --git a/src/routes/app.css b/src/routes/app.css index d4c750bd9..78ad04589 100644 --- a/src/routes/app.css +++ b/src/routes/app.css @@ -16,6 +16,7 @@ body { --bg-color: #fff; --secondary-bg-color: #eee; + --theorem-bg-color: #eee; --text-color: #111; --secondary-text-color: #555; --outline-color: #666; @@ -34,6 +35,7 @@ body { body[data-theme='dark'] { --bg-color: #121216; --secondary-bg-color: #262626; + --theorem-bg-color: #000; --text-color: #fff; --secondary-text-color: #999; --outline-color: #aaa; diff --git a/src/routes/category-comparison/[...ids]/+page.server.ts b/src/routes/category-comparison/[...ids]/+page.server.ts index 2c002f9fa..a0fc5905b 100644 --- a/src/routes/category-comparison/[...ids]/+page.server.ts +++ b/src/routes/category-comparison/[...ids]/+page.server.ts @@ -1,6 +1,6 @@ import { error } from '@sveltejs/kit' import { query } from '$lib/server/db.catdat' -import { render_nested_formulas } from '$lib/server/rendering' +import { render_nested_formulas } from '$lib/server/formulas' import { MAX_CATEGORIES_COMPARE } from '../compare.config' export const prerender = false diff --git a/src/routes/category-implication/[id]/+page.server.ts b/src/routes/category-implication/[id]/+page.server.ts index 258333702..8d72521ae 100644 --- a/src/routes/category-implication/[id]/+page.server.ts +++ b/src/routes/category-implication/[id]/+page.server.ts @@ -1,6 +1,6 @@ import type { ImplicationDB, ImplicationDisplay } from '$lib/commons/types' import { query } from '$lib/server/db.catdat' -import { render_nested_formulas } from '$lib/server/rendering' +import { render_nested_formulas } from '$lib/server/formulas' import { display_implication } from '$lib/server/utils' import { error } from '@sveltejs/kit' import sql from 'sql-template-tag' diff --git a/src/routes/category-implications/+page.server.ts b/src/routes/category-implications/+page.server.ts index fca4f7cfa..9c1133491 100644 --- a/src/routes/category-implications/+page.server.ts +++ b/src/routes/category-implications/+page.server.ts @@ -1,4 +1,4 @@ -import { render_nested_formulas } from '$lib/server/rendering' +import { render_nested_formulas } from '$lib/server/formulas' import { query } from '$lib/server/db.catdat' import sql from 'sql-template-tag' import { error } from '@sveltejs/kit' diff --git a/src/routes/category-property/[id]/+page.server.ts b/src/routes/category-property/[id]/+page.server.ts index 2c0cd3047..6e81c7681 100644 --- a/src/routes/category-property/[id]/+page.server.ts +++ b/src/routes/category-property/[id]/+page.server.ts @@ -1,5 +1,5 @@ import { error } from '@sveltejs/kit' -import { render_nested_formulas } from '$lib/server/rendering' +import { render_nested_formulas } from '$lib/server/formulas' import { decode_property_ID } from '$lib/commons/property.url' import { batch } from '$lib/server/db.catdat' import sql from 'sql-template-tag' diff --git a/src/routes/category/[id]/+page.server.ts b/src/routes/category/[id]/+page.server.ts index 77bcbaca5..d7ef5cfbb 100644 --- a/src/routes/category/[id]/+page.server.ts +++ b/src/routes/category/[id]/+page.server.ts @@ -1,5 +1,5 @@ import { error } from '@sveltejs/kit' -import { render_nested_formulas } from '$lib/server/rendering' +import { render_nested_formulas } from '$lib/server/formulas' import { batch } from '$lib/server/db.catdat' import sql from 'sql-template-tag' import type { diff --git a/src/routes/content/[id]/+page.server.ts b/src/routes/content/[id]/+page.server.ts new file mode 100644 index 000000000..2403891e1 --- /dev/null +++ b/src/routes/content/[id]/+page.server.ts @@ -0,0 +1,14 @@ +import { content_ids, get_rendered_content } from '$lib/server/markdown' +import { error } from '@sveltejs/kit' +import type { EntryGenerator } from './$types' + +export const entries: EntryGenerator = () => { + return content_ids.map((id) => ({ id })) +} + +export const load = async (event) => { + const id = event.params.id + const content = get_rendered_content(id) + if (!content) error(404, 'Not Found') + return content +} diff --git a/src/routes/content/[id]/+page.svelte b/src/routes/content/[id]/+page.svelte new file mode 100644 index 000000000..5c547f2b1 --- /dev/null +++ b/src/routes/content/[id]/+page.svelte @@ -0,0 +1,49 @@ + + + + +
    + {@html data.html} +
    + +{#if data.meta_data.author} +

    Author: {data.meta_data.author}

    +{/if} + + diff --git a/src/routes/foundations/+page.server.ts b/src/routes/foundations/+page.server.ts deleted file mode 100644 index 7fef77fd2..000000000 --- a/src/routes/foundations/+page.server.ts +++ /dev/null @@ -1,6 +0,0 @@ -import { get_rendered_content } from '$lib/server/rendering' - -export const load = async () => { - const content = get_rendered_content('foundations') - return { content } -} diff --git a/src/routes/foundations/+page.svelte b/src/routes/foundations/+page.svelte deleted file mode 100644 index 4f8dd24cc..000000000 --- a/src/routes/foundations/+page.svelte +++ /dev/null @@ -1,19 +0,0 @@ - - - - -{@html data.content} - - diff --git a/src/routes/functor-implication/[id]/+page.server.ts b/src/routes/functor-implication/[id]/+page.server.ts index 4fffd7893..40346ac3f 100644 --- a/src/routes/functor-implication/[id]/+page.server.ts +++ b/src/routes/functor-implication/[id]/+page.server.ts @@ -1,4 +1,4 @@ -import { render_nested_formulas } from '$lib/server/rendering' +import { render_nested_formulas } from '$lib/server/formulas' import { query } from '$lib/server/db.catdat' import sql from 'sql-template-tag' import { error } from '@sveltejs/kit' diff --git a/src/routes/functor-implications/+page.server.ts b/src/routes/functor-implications/+page.server.ts index 9831c299b..5c5f151c1 100644 --- a/src/routes/functor-implications/+page.server.ts +++ b/src/routes/functor-implications/+page.server.ts @@ -1,4 +1,4 @@ -import { render_nested_formulas } from '$lib/server/rendering' +import { render_nested_formulas } from '$lib/server/formulas' import { query } from '$lib/server/db.catdat' import sql from 'sql-template-tag' import { error } from '@sveltejs/kit' diff --git a/src/routes/functor-property/[id]/+page.server.ts b/src/routes/functor-property/[id]/+page.server.ts index 7e2856568..ea73b94a5 100644 --- a/src/routes/functor-property/[id]/+page.server.ts +++ b/src/routes/functor-property/[id]/+page.server.ts @@ -6,7 +6,7 @@ import type { FunctorShort, } from '$lib/commons/types' import { batch } from '$lib/server/db.catdat' -import { render_nested_formulas } from '$lib/server/rendering' +import { render_nested_formulas } from '$lib/server/formulas' import { display_functor_implication, display_functor_property } from '$lib/server/utils' import { error } from '@sveltejs/kit' import sql from 'sql-template-tag' diff --git a/src/routes/functor/[id]/+page.server.ts b/src/routes/functor/[id]/+page.server.ts index e359a6124..50f75998e 100644 --- a/src/routes/functor/[id]/+page.server.ts +++ b/src/routes/functor/[id]/+page.server.ts @@ -5,7 +5,7 @@ import type { FunctorPropertyShort, } from '$lib/commons/types' import { batch } from '$lib/server/db.catdat' -import { render_nested_formulas } from '$lib/server/rendering' +import { render_nested_formulas } from '$lib/server/formulas' import { error } from '@sveltejs/kit' import sql from 'sql-template-tag' diff --git a/src/routes/lemma/[id]/+page.server.ts b/src/routes/lemma/[id]/+page.server.ts index 2d077771f..cf479501e 100644 --- a/src/routes/lemma/[id]/+page.server.ts +++ b/src/routes/lemma/[id]/+page.server.ts @@ -1,6 +1,6 @@ import type { CategoryShort, Lemma } from '$lib/commons/types' import { batch } from '$lib/server/db.catdat' -import { render_nested_formulas } from '$lib/server/rendering' +import { render_nested_formulas } from '$lib/server/formulas' import { error } from '@sveltejs/kit' import sql from 'sql-template-tag' diff --git a/static/img/diagram-sifted-colimit.svg b/static/img/diagram-sifted-colimit.svg new file mode 100644 index 000000000..d27dd4b77 --- /dev/null +++ b/static/img/diagram-sifted-colimit.svg @@ -0,0 +1,318 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/static/img/diagram-sifted-colimit.tex b/static/img/diagram-sifted-colimit.tex new file mode 100644 index 000000000..4107d04c5 --- /dev/null +++ b/static/img/diagram-sifted-colimit.tex @@ -0,0 +1,31 @@ +\documentclass{standalone} +\usepackage{amsmath, amssymb, amsfonts, mathtools} +\usepackage{tikz} +\usepackage{tikz-cd} + +\begin{document} + +\begin{tikzcd}[column sep = 1.6em] +& & & & c +\ar[dllll,bend right=25,shift right=1,"l_0 = p\circ f"',pos=0.8] +\ar[dllll,bend right=25,shift left=1,"r_0 = q\circ g",pos=0.8] +\ar[dll,bend right=10,shift right=1,"l_1"'] +\ar[dll,bend right=10,shift left=1,"r_1"] +\ar[d,shift right=1,"l_2"'] +\ar[d,shift left=1,"r_2"] +\ar[drrrr,bend left=25,dash, shift left=0.75] +\ar[drrrr,bend left=25,dash, shift right=0.75] +\ar[drr,bend left=10,shift right=1,"l_{n-1}"{below left=-2}] +\ar[drr,bend left=10,shift left=1,"r_{n-1}"] +& & & & \\ [50pt] +z = d_0 \quad +& & d_1 & & d_2 & \cdots & d_{n-1} & & \quad d_n = c \\ +& +e_1 \ar[ul,leftarrow,"s_1"] \ar[ur,leftarrow,"t_1"'] +& & +e_2 \ar[ul,leftarrow,"s_2"] \ar[ur,leftarrow,"t_2"'] +& & & & +e_n \ar[ul,leftarrow,"s_n"] \ar[ur,leftarrow,"t_n"'] +& +\end{tikzcd} +\end{document} \ No newline at end of file diff --git a/static/pdf/.gitignore b/static/pdf/.gitignore deleted file mode 100644 index 662623f71..000000000 --- a/static/pdf/.gitignore +++ /dev/null @@ -1,9 +0,0 @@ -# Files from Latex Workshop -*.aux -*.bbl -*.blg -*.fdb_latexmk -*.fls -*.log -*.synctex.gz -*.out \ No newline at end of file diff --git a/static/pdf/cocongruences_of_groups.pdf b/static/pdf/cocongruences_of_groups.pdf deleted file mode 100644 index f5bdf0b6b..000000000 Binary files a/static/pdf/cocongruences_of_groups.pdf and /dev/null differ diff --git a/static/pdf/cocongruences_of_groups.tex b/static/pdf/cocongruences_of_groups.tex deleted file mode 100644 index c6957f45b..000000000 --- a/static/pdf/cocongruences_of_groups.tex +++ /dev/null @@ -1,108 +0,0 @@ -\documentclass[a4paper,12pt,reqno]{amsart} -\usepackage[utf8]{inputenc} -\usepackage[top=25truemm,bottom=25truemm,left=20truemm,right=20truemm]{geometry} -\usepackage{parskip} -\usepackage{tikz-cd} - -\usepackage{amsmath, amssymb, amsfonts, amscd, amsthm, mathtools} -\usepackage{hyperref} - -\theoremstyle{plain} -\newtheorem{prop}{Proposition} -\newtheorem{cor}[prop]{Corollary} - -\theoremstyle{definition} -\newtheorem{defi}[prop]{Definition} - -\DeclareMathOperator{\id}{id} -\DeclareMathOperator{\eq}{eq} -\DeclareMathOperator{\Grp}{\mathbf{Grp}} - -\newcommand{\C}{\mathcal{C}} - -\title{Cocongruences on groups are effective} -\author{Martin Brandenburg} -\date{\today} - -\begin{document} -\maketitle - -Our goal is to prove that every cocongruence in the category $\Grp$ is effective. We will establish a more general result for categories in which pushouts and monomorphisms interact in a suitable way. - -\begin{defi} -We shall say that a category $\C$ has \emph{good pushouts of monomorphisms} if it has pushouts of monomorphisms and if, for every diagram of monomorphisms -\[\begin{tikzcd} -B \ar{r} & B' \\ -A \ar{r} \ar{u} \ar{d} & A' \ar{u} \ar{d} \\ -C \ar{r} & C' -\end{tikzcd}\] -in which each square is a pullback, the induced morphism -\[B \sqcup_A C \to B' \sqcup_{A'} C'\] -is also a monomorphism. -\end{defi} - -\begin{prop} -The category $\Grp$ has good pushouts of monomorphisms. -\end{prop} - -\begin{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 \emph{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,\] -where $a \in A$, each $x_i$ lies either in $S \setminus \{1\}$ or in $T \setminus \{1\}$, and these choices alternate. - -The map -\[A \backslash B \to A' \backslash B', \, Ab \mapsto A'b\] -is injective. Indeed, if $b_1,b_2 \in B$ satisfy $A' b_1 = A' b_2$, then $b_1 b_2^{-1} \in A'$. Since $B \cap A' = A$, it follows that $b_1 b_2^{-1} \in A$, and hence $A b_1 = A b_2$. - -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. -\end{proof} - -\begin{prop} -Let $\C$ be a balanced category with good pushouts of monomorphisms and equalizers of monomorphisms. Then every cocongruence in $\C$ is effective. -\end{prop} - -\begin{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.\] -In particular, $i_1$ and $i_2$ are monomorphisms. Since the cocongruence is cotransitive, there exists a morphism -\[c : Y \to Y \sqcup_{i_2,X,i_1} Y\] -satisfying -\[c \circ i_1 = u_1 \circ i_1, \quad c \circ i_2 = u_2 \circ i_2,\] -where $u_1,u_2 : Y \rightrightarrows Y \sqcup_{i_2,X,i_1} Y$ are the pushout inclusions satisfying $u_1 i_2 = u_2 i_1$. We will not use the fact that the cocongruence is cosymmetric; this will follow automatically. Define the monomorphism -\[E := \eq(i_1,i_2) \hookrightarrow X.\] - -Since $i_1$ and $i_2$ agree on $E$, there exists a unique morphism -\[\varphi : X \sqcup_E X \to Y\] -defined by $\varphi \circ j_1 = i_1$ and $\varphi \circ j_2 = i_2$, where $j_1,j_2 : X \rightrightarrows X \sqcup_E X$ are the two inclusions. - -We must show that $\varphi$ is an isomorphism. It is clearly an epimorphism, since $i_1$ and $i_2$ are jointly epimorphic by assumption. Since $\C$ is balanced, it therefore suffices to prove that $\varphi$ is a monomorphism. - -We will show that even the morphism -\[\gamma := c \circ \varphi : X \sqcup_E X \to Y \sqcup_{i_2,X,i_1} Y\] -is a monomorphism. It is characterized by -\[\gamma \circ j_1 = c \circ \varphi \circ j_1 = c \circ i_1 = u_1 \circ i_1,\] -\[\gamma \circ j_2 = c \circ \varphi \circ j_2 = c \circ i_2 = u_2 \circ i_2.\] - -In other words, $\gamma$ is induced by the diagram of monomorphisms -\[\begin{tikzcd} -X \ar{r}{i_1} & Y \\ -E \ar{r} \ar{u} \ar{d} & X \ar{u}[swap]{i_2} \ar{d}{i_1} \\ -X \ar{r}[swap]{i_2} & Y -\end{tikzcd}\] - -Since $\C$ has good pushouts of monomorphisms, it suffices to verify that both squares are pullbacks. Observe that the two squares are symmetric, so it is enough to consider one of them. To verify the universal property, let $a : T \to X$ and $b : T \to X$ be morphisms satisfying $i_1 \circ a = i_2 \circ b$. Applying $r : Y \to X$, we obtain -\[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 \hookrightarrow X$. -\end{proof} - -\begin{cor} -Every cocongruence in the category $\Grp$ is effective. -\end{cor} - - -\end{document} diff --git a/static/pdf/comphaus_copresentable.bib b/static/pdf/comphaus_copresentable.bib deleted file mode 100644 index c94f74256..000000000 --- a/static/pdf/comphaus_copresentable.bib +++ /dev/null @@ -1,78 +0,0 @@ -@misc{marra2020characterisationcategorycompacthausdorff, - title={A characterisation of the category of compact {H}ausdorff spaces}, - author={Vincenzo Marra and Luca Reggio}, - year={2020}, - eprint={1808.09738}, - archivePrefix={arXiv}, - primaryClass={math.CT}, - url={https://arxiv.org/abs/1808.09738}, -} -@article{HUSEK2019251, - title = {Factorization and local presentability in topological and uniform spaces}, - journal = {Topology and its Applications}, - volume = {259}, - pages = {251-266}, - year = {2019}, - note = {William Wistar Comfort (1933-2016): In Memoriam}, - issn = {0166-8641}, - doi = {https://doi.org/10.1016/j.topol.2019.02.033}, - url = {https://www.sciencedirect.com/science/article/pii/S0166864119300513}, - author = {M. Hušek and J. Rosický}, - keywords = {Realcompact space, Factorization, Locally presentable category}, - abstract = {Investigating dual local presentability of some topological and uniform classes, a new procedure is developed for factorization of maps defined on subspaces of products and a new characterization of local presentability is produced. The factorization is related to large cardinals and deals, mainly, with realcompact spaces. Instead of factorization of maps on colimits, local presentability is characterized by means of factorization on products.} -} -@article{Marra_2017, - title={Stone duality above dimension zero: Axiomatising the algebraic theory of {C(X)}}, - volume={307}, - ISSN={0001-8708}, - url={http://dx.doi.org/10.1016/j.aim.2016.11.012}, - DOI={10.1016/j.aim.2016.11.012}, - journal={Advances in Mathematics}, - publisher={Elsevier BV}, - author={Marra, Vincenzo and Reggio, Luca}, - year={2017}, - month=Feb, pages={253–287} } -@article{Isb82, - title = {Generating the algebraic theory of {C(X)}}, - journal = {Algebra Universalis}, - volume = {15 (2)}, - pages = {153-155}, - year = {1982}, - author = {Isbell, J.R.} -} -@inproceedings{Dus69, - title = {Variations on {B}eck's tripleability criterion}, - series = {Reports of the Midwest Category Seminar III}, - editor = {MacLane, S.}, - author = {Duskin, J.}, - pages = {74-129}, - year = {1969}, - publisher = {Springer Berlin Heidelberg} -} -@article{Hoff18, - title = {Generating the algebraic theory of {C(X)}: The case of partially ordered compact spaces}, - journal = {Theory and Applications of Categories}, - author = {Hoffman, Dirk and Neves, Renato and Nora, Pedro}, - pages = {276-295}, - year = {2018}, - volume = {33}, - number = {12}, - url = {http://www.tac.mta.ca/tac/volumes/33/12/33-12.pdf}} -@article{GU71, - title = {Lokal pr\"asentierbare {K}ategorien}, - author = {P. Gabriel and F. Ulmer}, - journal = {Lecture Notes in Mathematics}, - publisher = {Springer-Verlag, Berlin}, - volume = {221}, - year = {1971} -} -@book{SGL, - title={Sheaves in Geometry and Logic: A First Introduction to Topos Theory}, - author={Mac Lane, Saunders and Moerdijk, Ieke}, - year={1992}, - publisher={Springer-Verlag New York, Inc.}, - series={Universitext}, - isbn={978-0-387-97710-2}, - doi={10.1007/978-1-4612-0927-0}, - url={https://link.springer.com/book/10.1007/978-1-4612-0927-0} -} diff --git a/static/pdf/comphaus_copresentable.pdf b/static/pdf/comphaus_copresentable.pdf deleted file mode 100644 index 96c164894..000000000 Binary files a/static/pdf/comphaus_copresentable.pdf and /dev/null differ diff --git a/static/pdf/comphaus_copresentable.tex b/static/pdf/comphaus_copresentable.tex deleted file mode 100644 index ed589d725..000000000 --- a/static/pdf/comphaus_copresentable.tex +++ /dev/null @@ -1,118 +0,0 @@ -\documentclass[a4paper,12pt,reqno]{amsart} -\usepackage[utf8]{inputenc} -\usepackage[top=25truemm,bottom=25truemm,left=20truemm,right=20truemm]{geometry} - -\usepackage{amsmath, amssymb, amsfonts, amscd, amsthm, mathtools, hyperref, doi} -\usepackage[numbers]{natbib} -\newtheorem{proposition}{Proposition} -\newtheorem{lemma}[proposition]{Lemma} -\newtheorem{corollary}[proposition]{Corollary} - -\newcommand{\Hom}{\operatorname{Hom}} -\newcommand{\Mor}{\operatorname{Mor}} -\newcommand{\op}{\operatorname{op}} -\newcommand{\CompHaus}{\mathbf{CompHaus}} -\newcommand{\Set}{\mathbf{Set}} -\newcommand{\im}{\operatorname{im}} -\newcommand{\id}{\operatorname{id}} -\newcommand{\I}{\mathcal{I}} -\newcommand{\calT}{\mathcal{T}} -\newcommand{\INnz}{\mathbb{N}_{>0}} -\newcommand{\colim}{\operatorname{colim}} - -\title{Local $\aleph_1$-copresentability of the category of compact Hausdorff spaces} -\author{Daniel Schepler} -\date{\today} - -\begin{document} -\maketitle - -Our purpose here is to gather several relevant results about the category $\CompHaus$ of compact Hausdorff spaces, and provide accessible (sic) proofs of these facts leading up to a proof that it is locally $\aleph_1$-copresentable. - -A good overview of some of these results is contained in the introduction of \cite{Hoff18}. - -We first prove a couple preliminary results. - -\begin{lemma} - 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 X_i$ is also non-empty. - - \begin{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 := \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 := \{ 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$. - \end{proof} -\end{lemma} - -\begin{lemma} - Suppose we have a cofiltered limit $X = \lim_{i\in \I} X_i$ in $\mathbf{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$. - - \begin{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. - \end{proof} -\end{lemma} - -\begin{proposition} - The functor $\Hom({-}, [0, 1]) : \CompHaus^{\op} \to \Set$ is monadic. (Originally proved in \cite{Dus69}) - - \begin{proof} - We use the crude monadicity theorem (see e.g.~\cite{SGL}, Thm.~IV.4.2). First, the functor has a left adjoint $S \mapsto [0, 1]^S$ with the evident isomorphism - $$\Hom_{\CompHaus}(X, [0, 1]^S) \simeq \Hom_{\Set}(S, \Hom_{\CompHaus}(X, [0, 1])). $$ - - To see the functor is conservative, suppose we have a continuous function $f : X \to Y$ such that $f^* : \Hom(Y, [0, 1]) \to \Hom(X, [0, 1])$ is a bijection. Then for any $x_1, x_2 \in X$ with $x_1 \ne x_2$, there exists $\varphi : X \to [0, 1]$ with $\varphi(x_1) = 0$ and $\varphi(x_2) = 1$ by Urysohn's lemma. Since $f^*$ is surjective, there exists $\psi : Y \to [0, 1]$ with $\varphi = \psi \circ f$; thus, we must have $f(x_1) \ne f(x_2)$. Likewise, we know the image of $f$ is closed. If this image is not all of $Y$, then by Urysohn's lemma there exists nonzero $\varphi : Y \to [0, 1]$ which is zero on the image. But then $\varphi \circ f = 0 \circ f$, contradicting the injectivity of $f^*$. Thus, $f$ is a bijective continuous function, and therefore a homeomorphism. - - Finally, suppose we have a coreflexive equalizer pair - $$E \xhookrightarrow{i} A \overset{f}{\underset{g}{\rightrightarrows}} B$$ - with $r : B \to A$. We may assume that $i$ is a subspace inclusion map. We may use $r$ to think of $B$ as a bundle of compact spaces over $A$, with two sections $f, g$. We then need to show that - $$\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. - \end{proof} -\end{proposition} - -This shows that $\CompHaus^{\op}$ is equivalent to the category of algebras over the monad $S \mapsto \Hom_{\CompHaus}([0, 1]^S, [0, 1])$. We may view such algebras as being models of the infinitary algebraic theory of all continuous functions $[0,1]^S \to [0,1]$. In fact, we can show that any such function only depends on countably many coordinates in the domain, so that operations of this theory will be generated by the continuous functions $[0,1]^\omega \to [0,1]$. Indeed, we get the following somewhat stronger result: - -\begin{proposition} - The object $[0,1]$ of $\CompHaus$ is $\aleph_1$-copresentable. (Originally proved in \cite{GU71}, 6.5(c)) - - \begin{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 \INnz$. 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 := (\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$. - - To summarize, we have shown that for each $n \in \INnz$, there exists $i \in \I$ and a finite cover $\{ V_\lambda \mid \lambda \in \Lambda \}$ of $\im(p_i)$ such that whenever $p_i(x), p_i(y) \in V_\lambda$ for some $\lambda$, we have $|\varphi(x) - \varphi(y)| < 1/n$. Now choose such a $i_n$ and associated finite cover of $\im(p_{i_n})$ for each $n$. Then use the fact that $\I$ is $\aleph_1$-cofiltered to take a cone $(j, f_n : j \to i_n)$ of the objects $i_n$. We then see that whenever we have $x, y\in X$ with $p_j(x) = p_j(y)$, then $\varphi(x) = \varphi(y)$. Thus, $\varphi$ induces a well-defined function on the image of $p_j$. This function is continuous, since by construction for any $n\in \INnz$ and $x \in X$, there is a neighborhood $V$ of $p_j(x)$ such that whenever $p_j(y)\in V$ as well, $|\varphi(y) - \varphi(x)| < 1/n$. By the Tietze extension theorem, this induced function can then be extended to a continuous function $\psi : X_j \to [0,1]$. Then $\varphi = \psi \circ p_j$. - - This shows the canonical map - $$\colim_{i\in \I^{\op}} \Hom(X_i, [0,1]) \to \Hom(\lim_{i\in \I} X_i, [0,1])$$ - is surjective. - - Likewise, suppose we have $\alpha, \beta : X_i \rightrightarrows [0,1]$ such that $\alpha \circ p_i = \beta \circ p_i$. For each $n\in \INnz$, consider the set $D_n := \{ x \in X_i \mid |\alpha(x) - \beta(x)| \ge 1/n \}$. Note that $D_n$ is a closed subset of $X_i$, so it is compact. For any $x \in D_n$, we must have $x \notin \im(p_i)$. Using the contrapositive of lemma 1, we can conclude that there exists $f : j \to i$ such that $x \not\in \im(X_f)$. Indeed, suppose not: then the slice category $\I / i$ is cofiltered, with the limit over this slice category being the same as the limit over $\I$. Also, by the contrary assumption, we have that $x \in \im(X_f)$ for any $f : j \to i$, so $X_f^{-1}(\{ x \})$ is non-empty. Therefore, by lemma 1, the limit $p_i^{-1}(\{ x \})$ would be non-empty, contradicting the assumption. - - Now each $D_n \setminus \im(X_f)$ is open and we have just shown such sets cover $D_n$; taking a finite subcover and then using the cofiltering assumption again, we conclude that there is a single $f_n : j_n \to i$ such that $\im(X_{f_n})$ is disjoint from $D_n$. Using the $\aleph_1$-cofiltering assumption to take a cone of the $f_n$, we get that there is $f : k \to i$ such that $\im(X_f)$ is disjoint from all $D_n$. This implies that $\alpha \circ X_f = \beta \circ X_f$. - - This shows the canonical map - $$\colim_{i\in \I^{\op}} \Hom(X_i, [0,1])) \to \Hom(\lim_{i\in I} X_i, [0,1])$$ - is injective. - \end{proof} -\end{proposition} - -\begin{corollary} - The category $\CompHaus$ is locally $\aleph_1$-copresentable. - - \begin{proof} - It suffices to show that the monad $S \mapsto \Hom_{\CompHaus}([0, 1]^S, [0, 1])$ is $\aleph_1$-accessible. This monad is the composition of $[0, 1]^{-} : \Set \to \CompHaus^{\op}$ 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 $\calT \to \Set$ preserving countable products, where $\calT$ is the full subcategory of $\CompHaus$ of all spaces $[0,1]^A$ where $A$ is countable. Note that $\calT$ is essentially small. We thus reproduce a result from \cite{Isb82} 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 \cite{Marra_2017} refines this by providing a nice axiomatization of the relations of that theory. - \end{proof} -\end{corollary} - -\nocite{marra2020characterisationcategorycompacthausdorff} -\nocite{HUSEK2019251} -\bibliographystyle{plainnat} -\bibliography{comphaus_copresentable} - -\end{document} diff --git a/static/pdf/congruences_in_rel.pdf b/static/pdf/congruences_in_rel.pdf deleted file mode 100644 index 9dd15aa73..000000000 Binary files a/static/pdf/congruences_in_rel.pdf and /dev/null differ diff --git a/static/pdf/congruences_in_rel.tex b/static/pdf/congruences_in_rel.tex deleted file mode 100644 index 8d2c58750..000000000 --- a/static/pdf/congruences_in_rel.tex +++ /dev/null @@ -1,69 +0,0 @@ -\documentclass[a4paper,12pt,reqno]{amsart} -\usepackage[utf8]{inputenc} -\usepackage[top=25truemm,bottom=25truemm,left=20truemm,right=20truemm]{geometry} - -\usepackage{amsmath, amssymb, amsfonts, amscd, amsthm, mathtools} -\newtheorem{lemma}{Lemma} - -\title{A classification of congruences in the category of sets and relations} -\author{Daniel Schepler} -\date{\today} - -\begin{document} -\maketitle - -We will give a classification of congruences $i : E \hookrightarrow X \times X$ in the category $\mathbf{Rel}$ of sets and relations. Recall that products in $\mathbf{Rel}$ are actually given by disjoint unions at the level of underlying sets. Also, recall that a morphism $R : X \to Y$ in $\mathbf{Rel}$ is a monomorphism if and only if $R_* : P(X) \to P(Y), S \mapsto \{ y\in Y \mid \exists x\in S, (x, y) \in R \}$ is injective, and it is an isomorphism if and only if $R$ is the graph of a bijection $X \to Y$ in $\mathbf{Set}$. - -In particular, we get $i_* : P(E) \to P(X + X) \simeq P(X) \times P(X)$ which must be injective. It must also preserve arbitrary unions and in particular be inclusion-preserving. From the assumption that $i$ is a congruence, since the functor $(P, {-}_*) : \mathbf{Rel} \to \mathbf{Set}$ is representable by the object 1, we see that $i_*$ must have image given by an equivalence relation $\sim$ on $P(X)$. Note also that since $i_*$ preserves arbitrary unions, we must have that $\sim$ respects arbitrary unions. - -Since the symmetry morphism $s : E \to E$ satisfies $s^2 = \operatorname{id}$, it must be the graph of an involution $s_0$ on $E$, where $s_0$ is a morphism in $\mathbf{Set}$. - -{\bf Claim 1:} Consider the reflexivity morphism $r : X \to E$. For each $x \in X$, $r_*(\{ x \})$ must be either a singleton or a pair. - -To see this, $r_*(\{ x \})$ certainly cannot be empty, or we would have $i_*(r_*(\{ x \})) = (\varnothing, \varnothing) \ne (\{ x \}, \{ x \})$. On the other hand, if we had at least three distinct elements $a,b,c \in r_*(\{ x \})$, then $i_*(\varnothing), i_*(\{ a \}), i_*(\{ a, b \}), i_*(\{ a, b, c \})$ would have to be a chain of four distinct subsets of $i_*(r_*(\{ x \})) = (\{ x \}, \{ x \})$, which is impossible. - -{\bf Claim 2:} For each $x \in X$, if $r_*(\{ x \}) = \{ e, f \}$ with $e \ne f$, then $s_0(e) = f$ and $s_0(f) = e$; and we have either that $i_*(\{e\}) = (\varnothing, \{ x \})$ and $i_*(\{f\}) = (\{ x \}, \varnothing)$, or vice versa. Otherwise, if $r_*(\{ x \}) = \{ e \}$, then $s_0(e) = e$; and $i_*(\{ e \}) = (\{ x \}, \{ x \})$. - -To see this, if $r_*(\{ x \}) = \{ e, f \}$ with $e\ne f$, then we must have $\varnothing = i_*(\varnothing) \subsetneqq i_*(\{ e \}) \subsetneqq i_*(\{ e, f \}) = (\{ x \}, \{ x \})$, which means that $i_*(\{ e \})$ is equal to either $(\{ x \}, \varnothing)$ or $(\varnothing, \{ x \})$. By the same token, $i_*(\{ f \})$ is also one of those choices, and $i_*(\{ e \}) \ne i_*(\{ f \})$. Since $i_*(\{ s_0(e) \}) = i_*(s_*(\{ e \})) = i_*(\{ f \})$ in either choice of order, by injectivity of $i_*$ we must have that $s_0(e) = f$. Similarly, $s_0(f) = e$. Otherwise, if $r_*(\{ x \}) = \{ e \}$ is a singleton, $i_*(\{ s_0(e) \}) = i_*(s_*(\{ e \})) = i_*(\{ e \})$, so injectivity of $i_*$ gives $s_0(e) = e$. - -{\bf Claim 3:} For $x\in X$, suppose that $r_*(\{ x \}) = \{ e \}$. Then $\{ x \} \not\sim \varnothing$. - -If we did have $\{ x \} \sim \varnothing$, then there would have to be some subset of $E$ which maps to $(\varnothing, \{ x \})$. Similarly to previous steps, injectivity of $i_*$ implies the subset is non-empty, and if the subset had two distinct elements $a,b$, then we would have $i_*(\varnothing) \subsetneqq i_*(\{a\}) \subsetneqq i_*(\{a,b\}) \subseteq (\varnothing, \{ x \})$, giving a contradiction. Therefore, this subset of $E$ would have to be a singleton $\{ f_1 \}$. Similarly, $(\{ x \}, \varnothing)$ would have to be the image of a singleton $\{ f_2 \}$ with $f_1 \ne f_2$. But then $i_*(\{ f_1, f_2 \}) = (\{ x \}, \{ x \}) = i_*(\{ e \})$, contradicting the injectivity of $i_*$. - -{\bf Claim 4:} For any $e \in E$, $i_*(\{ e \})$ is of one of the forms $(\{ x \}, \varnothing)$, $(\varnothing, \{ x \})$, or $(\{ x \}, \{ x \})$. In the first two cases, $s_0(e) \ne e$ and $\{ x \} \sim \varnothing$; and in the third case, $s_0(e) = e$ and $\{ x \} \not\sim \varnothing$. - -To show this, let $e\in E$, and suppose that $i_*(\{ e \}) = (S, T)$. Then $i_*(\{ s_0(e) \}) = (T, S)$, so $i_*(\{ e, s_0(e) \}) = (S \cup T, S\cup T) = i_*(\bigcup_{x\in S\cup T} r_*(\{ x \}))$. It follows that $\bigcup_{x\in S\cup T} r_*(\{ x \}) = \{ e, s_0(e) \}$. Therefore, $e \in r_*(\{ x \})$ for some $x \in X$, and by claims 2 and 3, we get the desired conclusion. - -{\bf Claim 5:} For any $S, T \in P(X)$, $S \sim T$ if and only if $S\cap A = T\cap A$, where $A$ is the set of $x\in X$ such that $\{ x \} \not\sim \varnothing$. - -For the forward direction, suppose $(S, T) = i_*(U)$ for $U \subseteq E$. Then $(S, T) = \bigcup_{e\in U} i_*(\{ e \})$; $i_*(\{ e \})$ satisfies the relation of having equal intersections with $A$ for each $e\in E$ in any case from claim 4; and this relation respects unions. For the reverse implication, whenever $x\notin A$, we have $\{ x \} \sim \varnothing$. Therefore, since $S = (S \cap A) \cup \bigcup_{x\in S \setminus A} \{ x \}$, we must have $S \sim (S \cap A) \cup \bigcup_{x\in S \setminus A} \varnothing = S \cap A$. Similarly, $T \sim T \cap A$, so if $S\cap A = T\cap A$, then $S \sim T$. - -{\bf Claim 6:} Let $E'$ be the set pushout $X +_A X$ with inclusion maps $i_1, i_2 : X \to E'$. Define a morphism $E' \to X \times X$ in $\mathbf{Rel}$ given by the inverse relation of the graph $i_1 + i_2 : X + X \to E'$. Then the congruences $E$ and $E'$ are equivalent. - -We can define a bijection $E \to E'$ as follows: let $e \in E$. If $i_*(\{ e \}) = (\{ x \}, \varnothing)$ with $x\notin A$, then send $e \mapsto i_1(x)$; if $i_*(\{ e \}) = (\varnothing, \{ x \})$ with $x\notin A$, then send $e \mapsto i_2(x)$; and if $i_*(\{ e \}) = (\{ x \}, \{ x \})$ with $x \in A$, then send $e \mapsto i_1(x) = i_2(x)$. Transferring the congruence to $E'$, we see that it is exactly of the given form. - -~ - -Now, without loss of generality we will assume from now on that the congruence is of exactly this form. - -With this classification, we can show that $A$ is a quotient for the congruence, with quotient morphism $\Delta_A \subseteq A \times A \subseteq X \times A$. In fact, we can define a morphism $\Delta_A^\circ : A \to X$ as the inverse relation to $\Delta_A$, and a morphism $X \to E$ as the graph of $i_1$. It is then straightforward to verify that these maps together make $A$ a split coequalizer of $p_1 \circ i$ and $p_2 \circ i$. - -We can also conclude that $E$ is the kernel pair of this quotient, by the general result below. - -\begin{lemma} - Suppose we have a congruence $f, g : E \rightrightarrows X$ with a contractible coequalizer - $$ E \overset{f}{\underset{g}{\rightrightarrows}} X \overset{e}{\rightarrow} Q $$ - with maps in the reverse direction $s : Q \to X$ and $t : X \to E$. Then $E$ is the kernel pair of this quotient, i.e.~ we have a cartesian square - $$ - \begin{CD} - E @> f >> X \\ - @V g VV @V e VV \\ - X @> e >> A. - \end{CD} - $$ - \begin{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$. - \end{proof} -\end{lemma} - -\end{document} diff --git a/static/pdf/walking_parallel_pair_sifted_colimit.pdf b/static/pdf/walking_parallel_pair_sifted_colimit.pdf deleted file mode 100644 index f21415cbe..000000000 Binary files a/static/pdf/walking_parallel_pair_sifted_colimit.pdf and /dev/null differ diff --git a/static/pdf/walking_parallel_pair_sifted_colimit.tex b/static/pdf/walking_parallel_pair_sifted_colimit.tex deleted file mode 100644 index af0feabe1..000000000 --- a/static/pdf/walking_parallel_pair_sifted_colimit.tex +++ /dev/null @@ -1,112 +0,0 @@ -\documentclass[a4paper,12pt,reqno]{amsart} -\usepackage[utf8]{inputenc} -\usepackage[top=25truemm,bottom=25truemm,left=20truemm,right=20truemm]{geometry} - -\usepackage{amsmath, amssymb, amsfonts, mathtools} -\usepackage{tikz-cd} - -\title{The walking parallel pair has sifted colimits} -\author{Yuto Kawase} -\date{\today} - -\begin{document} -\maketitle - -Let $D\colon\mathcal{C}\to \{u,v\colon 0 \rightrightarrows 1\}$ be a functor from a sifted category. -If the object $1$ is not contained in the image under $D$, the object $0$ gives a colimit of $D$ because the sifted category $\mathcal{C}$ is connected. -In what follows, we suppose that there is an object $c_0\in\mathcal{C}$ such that $D(c_0)=1$. - -We first claim that for every object $c\in\mathcal{C}$ such that $D(c)=0$, there is a morphism $f\colon c \to x$ with $D(x)=1$; moreover, which of $u$ and $v$ such a morphism is sent to by $D$ is independent of the choice of $f$. -The existence of $f$ is easy. -Indeed, since $\mathcal{C}$ is sifted, there is a cospan $c \rightarrow x \leftarrow c_0$, and $D(x)=1$ follows from $D(c_0)=1$. - -To show the independence of the value of $D(f)$, suppose that there are morphisms $f\colon c \to x$ and $g\colon c\to y$ such that $D(f)=u$ and $D(g)=v$. -Since $\mathcal{C}$ is sifted, there is a cospan consisting of $p\colon x \rightarrow z$ and $q\colon z \leftarrow y$. -Since $\mathcal{C}$ is sifted again, two cospans $(p\circ f, q\circ g)$ and $(\mathrm{id}_c, \mathrm{id}_c)$ are connected to each other, that is, there are a zigzag consisting of $s_i\colon d_{i-1} \rightarrow e_i$ and $t_i\colon e_i \leftarrow d_i$ $(1 \le i \le n)$ and parallel pairs $(l_i,r_i)\colon c \rightrightarrows d_i$ $(0 \le i \le n)$ such that $d_0=z$, $l_0=p\circ f$, $r_0=q\circ g$, $d_n=c$, $l_n=r_n=\mathrm{id}_c$, $s_i \circ l_{i-1} = t_i \circ l_i$, and $s_i \circ r_{i-1} = t_i \circ r_i$ $(1\le i\le n)$. -\begin{equation*} - \begin{tikzcd}[column sep = 1.6em] - &[-1.2em] - & - & - & - & - c - \ar[dllll,bend right=25,shift right=1,"l_0 = p\circ f"',pos=0.8] - \ar[dllll,bend right=25,shift left=1,"r_0 = q\circ g",pos=0.8] - \ar[dll,bend right=10,shift right=1,"l_1"'] - \ar[dll,bend right=10,shift left=1,"r_1"] - \ar[d,shift right=1,"l_2"'] - \ar[d,shift left=1,"r_2"] - \ar[drrrr,bend left=25,equal] - \ar[drr,bend left=10,shift right=1,"l_{n-1}"{below left=-2}] - \ar[drr,bend left=10,shift left=1,"r_{n-1}"] - & - & - & - & - &[-1.2em] - \\[30pt] - z - \ar[r,equal] - & - d_0 - & - & - d_1 - & - & - d_2 - & - \cdots - & - d_{n-1} - & - & - d_n - & - c - \ar[l,equal] - \\ - & - & - e_1 - \ar[ul,leftarrow,"s_1"] - \ar[ur,leftarrow,"t_1"'] - & - & - e_2 - \ar[ul,leftarrow,"s_2"] - \ar[ur,leftarrow,"t_2"'] - & - & - & - & - e_n - \ar[ul,leftarrow,"s_n"] - \ar[ur,leftarrow,"t_n"'] - & - & - \end{tikzcd} -\end{equation*} -Then, the equality $D(t_1) \circ D(l_1) = D(s_1)\circ D(l_0) = u$ implies that either $D(l_1)=u$ or $D(t_1)=u$ holds, while $D(t_1) \circ D(r_1) = D(s_1)\circ D(r_0) = v$ implies that either $D(r_1)=v$ or $D(t_1)=v$ holds. -However, the only possible combination is $D(l_1)=u$ together with $D(r_1)=v$, and by repeating this argument, we have $D(l_n)=u$ and $D(r_n)=v$, which is a contradiction. - -By the claim, each object $c\in\mathcal{C}$ can be classified exclusively into the following three cases: -\begin{enumerate} - \item - $D(c)=1$; - \item - $D(c)=0$ and there is a morphism from itself sent to $u$ by $D$; - \item - $D(c)=0$ and there is a morphism from itself sent to $v$ by $D$. -\end{enumerate} -Now, we have a cocone $(\alpha_c\colon D(c) \to 1)_{c\in\mathcal{C}}$ under $D$ by letting $\alpha_c\coloneqq \mathrm{id}_1$ if $c$ is classified into the first case, $\alpha_c\coloneqq u$ for the second case, and $\alpha_c\coloneqq v$ for the third case. -Moreover, this is a unique cocone under $D$: -If $\beta$ is another cocone, its vertex should be $1$ by the existence of $c_0$. -If $c\in\mathcal{C}$ is classified into the first case, $\beta_c$ should be the identity. -For the second case, taking a morphism $f\colon c\to x$ such that $D(f)=u$, we can obtain $\beta_c = \beta_x \circ D(f) = D(f) = u$. -Similarly, we have $\beta_c = v$ for the third case. -This concludes $\beta=\alpha$, and since there is no non-trivial endomorphism on the vertex $1$, $\alpha$ gives a colimit. - - -\end{document}