Design improvements

content/Top-embeds-in-LRS.md

@@ -3,7 +3,7 @@ title: An embedding of the category of topological spaces in the category of loc
 description: Describes a functor which makes the category of topological spaces a coreflective and "almost reflective" subcategory of the category of locally ringed spaces. From the properties of this embedding, we can rule out several properties for the category of locally ringed spaces, using the corresponding failures of these properties for the category of topological spaces.
 ---
 
-## An embedding of the category of topological spaces in the category of locally ringed spaces
+# An embedding of the category of topological spaces in the category of locally ringed spaces
 
 For much of this development, we will be dealing with the case of $\LRS_k$ where $k$ is a field. We begin by describing $\Top$ as a reflective subcategory of $\LRS_k$.
 

content/cocongruences_of_groups.md

@@ -3,7 +3,7 @@ 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.
 ---
 
-## Cocongruences on groups are effective
+# 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.
 

content/cogenerators_in_product_categories.md

@@ -3,7 +3,7 @@ title: Cogenerators in product categories
 description: How to construct a cogenerator in a product category
 ---
 
-## Cogenerators in product categories
+# Cogenerators in product categories
 
 ::: Lemma
 For a family of categories $(\C_i)_{i \in I}$, each having a cogenerator $Q_i$ which is weakly terminal, the object $(Q_i)_{i \in I}$ is a cogenerator in the product category $\prod_{i \in I} \C_i$.

content/comphaus_copresentable.md

@@ -3,7 +3,7 @@ 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.
 ---
 
-## Local ℵ₁-copresentability of the category of compact Hausdorff spaces
+# 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.
 
@@ -101,7 +101,7 @@ The first automatically preserves $\aleph_1$-filtered colimits (and in fact all
 Alternately, applying the general framework of Lawvere theories shows that $\CompHaus^{\op}$ is equivalent to the category of functors $\T \to \Set$ preserving countable products, where $\T$ is the full subcategory of $\CompHaus$ of all spaces $[0,1]^A$ where $A$ is countable. Note that $\T$ is essentially small. We thus reproduce a result from [Isb82](#references) which also provides a nice description of a small set of generators of the operations of the $\aleph_0$-ary algebraic theory. A more recent treatment in [MR17](#references) refines this by providing a nice axiomatization of the relations of that theory.
 :::
 
-### References
+## References
 
 [Dus69]  J. Duskin, _Variations on Beck’s tripleability criterion_. Reports of the Midwest Category Seminar III, pages 74–129. Springer Berlin Heidelberg, 1969
 

content/congruences_in_rel.md

@@ -3,7 +3,7 @@ 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.
 ---
 
-## A classification of congruences in the category of sets and relations
+# 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.
 

content/constant_morphisms.md

@@ -3,7 +3,7 @@ title: Results on constant morphisms
 description: We prove some results that help determine whether a morphism in a category is constant.
 ---
 
-## Results on constant morphisms
+# Results on constant morphisms
 
 ::: Lemma 1
 A [constant morphism](/morphism-property/constant) in $\Set$ is the same as a constant map in the usual sense.

content/contribute.md

@@ -3,24 +3,24 @@ title: How to contribute to CatDat
 description: CatDat welcomes contributions from the community, including filling in missing information or discovering new combinations of properties
 ---
 
-## How to contribute
+# How to contribute
 
 _CatDat_ is developed in an open-source [GitHub repository](https://github.com/ScriptRaccoon/catdat) by [Martin Brandenburg](https://ncatlab.org/nlab/show/Martin+Brandenburg). It welcomes contributions from the community, including filling in missing information or discovering new combinations of properties.
 
 [**Video tutorial**](https://www.youtube.com/watch?v=NoZWdMFfQfg)
 
 There are three ways to contribute:
 
-### Option 1: Use the Suggestion Form
+## Option 1: Use the Suggestion Form
 
 On most pages of CatDat, you will find a suggestion form at the bottom. Use it to contribute new data, report an issue, or make a suggestion. After submission, the form automatically creates a GitHub issue, which we then review and try to resolve and implement.
 
 This option does not require any knowledge of GitHub or coding, making it accessible to everyone. It also does not require following any guidelines for adding new data.
 
-### Option 2: Create an Issue
+## Option 2: Create an Issue
 
 Create an [issue](https://github.com/ScriptRaccoon/CatDat/issues/new) on GitHub. You will need a GitHub account.
 
-### Option 3: Create a Pull Request
+## Option 3: Create a Pull Request
 
 Create a [pull request](https://github.com/ScriptRaccoon/CatDat/pulls) on GitHub. You will need a GitHub account and some coding knowledge. Make sure to follow the [contribution guidelines](https://github.com/ScriptRaccoon/CatDat/blob/main/CONTRIBUTING.md).

content/coslice-effective-congruences.md

@@ -3,7 +3,7 @@ title: Inheritance of effective congruences in coslice categories
 description: An extensive category has effective congruences when some of its coslice categories has effective congruences.
 ---
 
-## Inheritance of effective congruences in coslice categories
+# Inheritance of effective congruences in coslice categories
 
 ::: Lemma
 Let $\C$ be an extensive category, and $A$ an object of $\C$. If the coslice category $A \backslash \C$ has effective congruences, then so does $\C$.

content/dual-properties.md

@@ -3,33 +3,33 @@ title: Dual properties
 description: A short explanation of what we mean by dual properties in CatDat.
 ---
 
-## Dual properties
+# Dual properties
 
-### Categories
+## Categories
 
 Given a property $P$ of categories, its dual property $P^{\op}$ is defined as follows: a category $\C$ satisfies $P^{\op}$ if and only if its dual category $\C^{\op}$ satisfies $P$.
 
 For example, since a category has an [initial object](/category-property/initial_object) if and only if its dual category has a [terminal object](/category-property/terminal_object), the property "has an initial object" is dual to the property "has a terminal object". In practice, dual properties can be obtained by reversing all arrows.
 
 Notice that $(P^{\op})^{\op} = P$, and that $\C$ satisfies $P$ if and only if $\C^{\op}$ satisfies $P^{\op}$.
 
-### Functors
+## Functors
 
 Given a property $P$ of functors, its dual property $P^{\op}$ is defined as follows: a functor $F : \C \to \D$ satisfies $P^{\op}$ if and only if its dual functor $F^{\op} : \C^{\op} \to \D^{\op}$ satisfies $P$. Notice that taking the dual does not reverse the direction of the functor.
 
 For example, since a functor is [essentially injective](/functor-property/essentially_injective) if and only if its dual is essentially injective, the property "is essentially injective" is self-dual. In particular, it is _not_ dual to the property "is [essentially surjective](/functor-property/essentially_surjective)", which is itself also self-dual.
 
 Again, notice that $(P^{\op})^{\op} = P$, and that $F : \C \to \D$ satisfies $P$ if and only if $F^{\op} : \C^{\op} \to \D^{\op}$ satisfies $P^{\op}$.
 
-### Morphisms
+## Morphisms
 
 Given a property $P$ of morphisms, its dual property $P^{\op}$ is defined as follows: a morphism $f : X \to Y$ in a category $\C$ satisfies $P^{\op}$ if and only if its dual morphism $f^{\op} : Y \to X$ in the dual category $\C^{\op}$ satisfies $P$.
 
 For example, the property [monomorphism](/morphism-property/monomorphism) is dual to [epimorphism](/morphism-property/epimorphism) since $f$ is an epimorphism if and only if $f^{\op}$ is a monomorphism.
 
 Notice that $(P^{\op})^{\op} = P$, and that $f$ satisfies $P$ if and only if $f^{\op}$ satisfies $P^{\op}$.
 
-### Symmetric Monoidal Categories
+## Symmetric Monoidal Categories
 
 The dual of a symmetric monoidal category $(\C,\otimes,1)$ is defined by $(\C^{\op},\otimes,1)$ (and the obvious coherence isomorphisms). Given a property $P$ of symmetric monoidal categories, its dual property $P^{\op}$ is defined as follows: a symmetric monoidal category satisfies $P^{\op}$ if and only if its dual satisfies $P$.
 

content/effective-congruence-quotients.md

@@ -3,7 +3,7 @@ title: Quotients of effective congruences are strict quotients
 description: Quotients by effective congruences are characterized via a pullback
 ---
 
-## Quotients of effective congruences are strict quotients
+# Quotients of effective congruences are strict quotients
 
 ::: Lemma
 Let $f, g : E \rightrightarrows X$ be an effective congruence. If $f, g$ have a coequalizer $p : X \to X/E$, then in fact we have a cartesian square

content/foundations.md

@@ -3,11 +3,11 @@ title: Foundations
 description: How to make sense of categories in set theory
 ---
 
-## Foundations
+# Foundations
 
 In _CatDat_, we work with the following convenient set-theoretic foundation for category theory.
 
-### Sets, collections, and hypercollections
+## Sets, collections, and hypercollections
 
 We work with [ZFC](https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory) and two [Grothendieck universes](https://en.wikipedia.org/wiki/Grothendieck_universe), which we denote by
 $$\mathrm{Set} \in \mathrm{Set}^+.$$
@@ -35,7 +35,7 @@ A family $(X_i)_{i \in I}$ of collections is called _small_ when its index colle
 
 A collection is called _countable_ if it admits a surjective map from $\IN$. In particular, every finite collection is countable.
 
-### Categories
+## Categories
 
 A _category_ $\C$ consists of a pair of collections $O, M$, whose elements are called _objects_ and _morphisms_, respectively, together with maps
 
@@ -62,7 +62,7 @@ For example, the category of sets $\Set$ has $\Ob(\Set) = \mathrm{Set}$, the col
 
 Collections are the objects of a hypercategory $\Set^+$.
 
-### Functors
+## Functors
 
 A _functor_ $F : \C \to \D$ between two categories (or small categories, or hypercategories) is defined as usual; it consists of maps
 $$\Ob(F) : \Ob(\C) \to \Ob(\D),$$
@@ -77,7 +77,7 @@ If $\C, \D$ are categories, we can construct the functor category $[\C, \D]$ as
 
 It is better to state explicitly when the assumption of being locally small is needed.
 
-### Representable Functors
+## Representable Functors
 
 If $\C$ is any category and $A \in \C$, we have the Hom-functor
 
@@ -89,18 +89,18 @@ Adjunctions are defined as usual via natural isomorphisms
 $$\Hom(F(A),B) \cong \Hom(A,G(B))$$
 of functors valued in $\Set^+$. No local smallness assumption is required. Equivalently, they can be defined via morphisms of functors $\id \to G \circ F$ and $F \circ G \to \id$ satisfying the triangle identities.
 
-### Limits and Colimits
+## Limits and Colimits
 
 Let $\C$ be a category. If $D : \I \to \C$ is a functor (in this context called a _diagram_), a _cone_ over $D$ is an object $X \in \C$ equipped with morphisms $p_i : X \to D(i)$ for all $i \in \I$ such that for every morphism $i \to j$ the evident triangle commutes. Cones form a category, and a terminal object in this category is called a _limit_ of $D$. The dual notion is a _colimit_.
 
 Unless stated otherwise, we consider only small diagrams and hence small limits and colimits, i.e. those where $\I$ is a small (or essentially small) category. This is because large limits rarely exist and it is cumbersome to specify "small" each time.
 
 There are special types of limits, such as equalizers, products, and cofiltered limits, and their duals, such as coequalizers, coproducts, and filtered colimits. By convention, products and coproducts are indexed by a set, not a collection (unless stated otherwise). Filtered colimits are indexed by a small filtered category (unless stated otherwise).
 
-### Well-powered categories
+## Well-powered categories
 
 If $A$ is an object of a category, the collection of all monomorphisms $B \to A$ need not be a set. If, for every $A$, there exists a small family of such monomorphisms such that every monomorphism $B \to A$ is isomorphic over $A$ to one in the family, then the category is called _well-powered_. The dual notion of being _well-copowered_ is defined using epimorphisms $A \to B$. Every small category is well-powered, but there are many well-powered categories that are not small and not even equivalent to a small category.
 
-### Conclusion
+## Conclusion
 
 There is much more to say about set-theoretic foundations for category theory (in fact, many papers have been written on the subject, and the approach developed above is just _one_ of [many](https://xkcd.com/927/) approaches), but this suffices for the purposes of _CatDat_.

content/functors_on_discrete_categories.md

@@ -3,7 +3,7 @@ title: Functors on discrete categories
 description: We describe which functors on discrete categories are continuous or cocontinuous.
 ---
 
-## Functors on discrete categories
+# Functors on discrete categories
 
 Let $\S$ be a discrete category. Thus, a functor $F : \S \to \C$ is the same as a family of objects $F(s) \in \C$ indexed by the objects $s \in \S$. Here, we want to determine under which conditions $F$ is continuous (or cocontinuous). The case $\S = \varnothing$ is rather boring, which is why we assume from now on that $\S \neq \varnothing$, i.e. that $\S$ is inhabited.
 

content/generator_construction.md

@@ -3,7 +3,7 @@ title: Construction of generators
 description: How to construct a generator from a generating set
 ---
 
-## Construction of generators
+# Construction of generators
 
 ::: Lemma
 In a category let $S$ be a generating set which is [strongly connected](/category-property/strongly_connected), i.e. between any two objects $G,G' \in S$ there is a morphism $G \to G'$. If the coproduct $U \coloneqq \coprod_{G \in S} G$ exists, then it is a generator. Moreover, if $S$ is an extremal generating set, then $U$ is an extremal generator.

content/inclusion-functors.md

@@ -3,7 +3,7 @@ title: Inclusion functors
 description: We gather results about inclusion functors
 ---
 
-## Inclusion functors
+# Inclusion functors
 
 ::: Lemma 1
 Let $\D$ be category that has an extremal cogenerator $Q$. Let $\C \subseteq \D$ be a full subcategory that contains $Q$. Then the inclusion functor $U : \C \hookrightarrow \D$ preserves all colimits that exist in $\C$ and in $\D$. In particular, if $\D$ is cocomplete, $U$ is cocontinuous.

content/missing_cogenerating_sets.md

@@ -3,7 +3,7 @@ title: Missing cogenerating sets
 description: A generalization of the proof that the category of commutative rings has no cogenerating set.
 ---
 
-## Missing cogenerating sets
+# Missing cogenerating sets
 
 ::: Lemma
 Let $\C$ be a category with a faithful functor $U: \C \to \Set$. Assume there exists a collection of objects $\F \subseteq \Ob(\C)$ satisfying the following conditions:

content/missing_cogenerator.md

@@ -3,7 +3,7 @@ title: Missing cogenerator
 description: A generalization of the proof that the category of groups has no cogenerator.
 ---
 
-## Missing cogenerator
+# Missing cogenerator
 
 ::: Lemma
 

content/monic_sequential_colimits.md

@@ -3,7 +3,7 @@ title: The colimit of a sequence of monomorphisms
 description: We find conditions under which a countably extensive category has colimits of sequences of monomorphisms.
 ---
 
-## The colimit of a sequence of monomorphisms
+# The colimit of a sequence of monomorphisms
 
 ::: Lemma 1
 Let $\C$ be a countably extensive category with quotients of congruences. Then $\C$ has colimits of sequences of monomorphisms.

content/natural_numbers_objects.md

@@ -3,7 +3,7 @@ title: Natural numbers objects
 description: We prove some results on natural numbers objects.
 ---
 
-## Natural numbers objects
+# Natural numbers objects
 
 The definition of a [natural numbers object](/category-property/natural_numbers_object) a priori only allows for recursively defined morphisms in which the next value $\Phi(s(n))$ depends only on the previous value $\Phi(n)$. In many cases, however, we would also like to use $n$ itself to define $\Phi(s(n))$. This can be done in categories with finite products:
 

content/preadditive_structure_unique.md

@@ -3,7 +3,7 @@ title: Uniqueness of preadditive structures
 description: In the presence of finite products, a preadditive structure on a given category is uniquely determined.
 ---
 
-## Uniqueness of preadditive structures
+# Uniqueness of preadditive structures
 
 ::: Lemma
 Let $\C$ be a preadditive category (or more generally, a category enriched in commutative monoids) with finite products and finite coproducts. Then for all objects $X,Y$ the canonical morphism

content/pushouts-of-monos-via-congruence-quotients.md

@@ -3,7 +3,7 @@ title: Construction of a pushout of monomorphisms as a quotient of a congruence
 description: An extensive category with quotients of congruences has pushouts of monomorphisms.
 ---
 
-## Construction of a pushout of monomorphisms as a quotient of a congruence
+# Construction of a pushout of monomorphisms as a quotient of a congruence
 
 ::: Lemma
 Let $\C$ be an extensive category with quotients of congruences. Then $\C$ has pushouts of monomorphisms.

content/relationships-epis-monos.md

@@ -3,11 +3,11 @@ title: Relationships between epimorphisms and monomorphisms
 description: A graphical overview of the relationships between the various types of epimorphisms and monomorphisms
 ---
 
-## Relationships between epimorphisms and monomorphisms
+# Relationships between epimorphisms and monomorphisms
 
 There are several [properties of morphisms](/morphism-properties), including various types of epimorphisms and monomorphisms. The [implications](/morphism-implications) establish various relationships between these types. Here we present a graphical overview of these relationships.
 
-### The various types of epimorphisms
+## The various types of epimorphisms
 
 In the diagram, an arrow $X \Longrightarrow Y$ means that every morphism with property $X$ also has property $Y$. If it is labelled with a category property $P$, the implication does not hold in general, but it holds in categories satisfying $P$. For example, in a category with pullbacks, every strict epimorphism is effective.
 
@@ -25,7 +25,7 @@ In the diagram, an arrow $X \Longrightarrow Y$ means that every morphism with pr
 
 Fun fact: This describes a category in itself: We define the composition of $P : X \Rightarrow Y$ and $Q : Y \Rightarrow Z$ as $P \wedge Q : X \Rightarrow Z$.
 
-### The various types of monomorphisms
+## The various types of monomorphisms
 
 This diagram is just the dual of the previous diagram. The same notation applies.
 

content/resources.md

@@ -3,7 +3,7 @@ title: Resources on category theory
 description: This is an (incomplete) list of resources on category theory.
 ---
 
-## Resources on category theory
+# Resources on category theory
 
 This is an (incomplete) list of resources on category theory.
 

content/sifted-colimits-in-groupoids.md

@@ -3,7 +3,7 @@ title: Sifted colimits in groupoids
 description: A description of sifted colimits in groupoids, yielding a proof that every essentially small groupoid is a generalized variety.
 ---
 
-## Sifted colimits in groupoids
+# Sifted colimits in groupoids
 
 While the combination of [this result](/category-implication/groupoid_consequence) and [this result](/category-implication/sifted_colimits_criterion) already implies that groupoids have sifted colimits, we can make these colimits more explicit and also prove their existence without using any non-trivial theorem. We also do this in a more general setting.