Explain dual properties

content/dual-properties.md

@@ -0,0 +1,22 @@
+---
+title: Dual properties
+description: A short explanation of what we mean by dual properties in CatDat.
+---
+
+## Dual properties
+
+### 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
+
+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}$.

databases/catdat/data/functor-properties/left-invertible.yaml

@@ -1,6 +1,6 @@
 id: left-invertible
 relation: is
-description: 'A <i>left inverse</i> of a functor $F : \C \to \D$ is a functor $G : \D \to \C$ satisfying $G \circ F \cong \id_{\C}$. We do not require $G \circ F = \id_{\C}$ here, which is often too strict. A functor is called <i>left-invertible</i> when it has a left inverse. This notion is self-dual in the sense that $F : \C \to \D$ is left-invertible iff $F^{\op} : \C^{\op} \to \D^{\op}$ is left-invertible.'
+description: 'A <i>left inverse</i> of a functor $F : \C \to \D$ is a functor $G : \D \to \C$ satisfying $G \circ F \cong \id_{\C}$. We do not require $G \circ F = \id_{\C}$ here, which is often too strict. A functor is called <i>left-invertible</i> when it has a left inverse.'
 nlab_link: https://ncatlab.org/nlab/show/inverse+functor
 invariant_under_equivalences: true
 dual_property: left-invertible

databases/catdat/data/functor-properties/right-invertible.yaml

@@ -1,6 +1,6 @@
 id: right-invertible
 relation: is
-description: 'A <i>right inverse</i> of a functor $F : \C \to \D$ is a functor $G : \D \to \C$ satisfying $F \circ G \cong \id_{\D}$. We do not require $F \circ G = \id_{\D}$ here, which is often too strict. A functor is called <i>right-invertible</i> when it has a right inverse. This notion is self-dual in the sense that $F : \C \to \D$ is right-invertible iff $F^{\op} : \C^{\op} \to \D^{\op}$ is right-invertible.'
+description: 'A <i>right inverse</i> of a functor $F : \C \to \D$ is a functor $G : \D \to \C$ satisfying $F \circ G \cong \id_{\D}$. We do not require $F \circ G = \id_{\D}$ here, which is often too strict. A functor is called <i>right-invertible</i> when it has a right inverse.'
 nlab_link: https://ncatlab.org/nlab/show/inverse+functor
 invariant_under_equivalences: true
 dual_property: right-invertible

src/pages/PropertyPage.svelte

@@ -55,7 +55,7 @@
 	<ul class="with-margins">
 		{#if property.dual_property_id}
 			<li>
-				<strong>Dual property:</strong>
+				<strong><a href="/content/dual-properties">Dual property:</a></strong>
 				<a href={get_property_url(property.dual_property_id, type)}
 					>{property.dual_property_id}</a
 				>