diff --git a/content/dual-properties.md b/content/dual-properties.md new file mode 100644 index 00000000..5c2d8517 --- /dev/null +++ b/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}$. diff --git a/databases/catdat/data/functor-properties/left-invertible.yaml b/databases/catdat/data/functor-properties/left-invertible.yaml index 82282809..95fa1ddb 100644 --- a/databases/catdat/data/functor-properties/left-invertible.yaml +++ b/databases/catdat/data/functor-properties/left-invertible.yaml @@ -1,6 +1,6 @@ id: left-invertible relation: is -description: 'A left inverse 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 left-invertible 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 left inverse 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 left-invertible when it has a left inverse.' nlab_link: https://ncatlab.org/nlab/show/inverse+functor invariant_under_equivalences: true dual_property: left-invertible diff --git a/databases/catdat/data/functor-properties/right-invertible.yaml b/databases/catdat/data/functor-properties/right-invertible.yaml index b5a8c90e..d0883f87 100644 --- a/databases/catdat/data/functor-properties/right-invertible.yaml +++ b/databases/catdat/data/functor-properties/right-invertible.yaml @@ -1,6 +1,6 @@ id: right-invertible relation: is -description: 'A right inverse 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 right-invertible 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 right inverse 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 right-invertible when it has a right inverse.' nlab_link: https://ncatlab.org/nlab/show/inverse+functor invariant_under_equivalences: true dual_property: right-invertible diff --git a/src/pages/PropertyPage.svelte b/src/pages/PropertyPage.svelte index 3272561a..91b8a2d3 100644 --- a/src/pages/PropertyPage.svelte +++ b/src/pages/PropertyPage.svelte @@ -55,7 +55,7 @@