Formal Rules for Categorical Duality

Question

EDIT: My question is not about what categorical duality is. I generally understand the idea, but my problem is that for every theorem, finding the dual theorem requires us to think about what it means, so that we can translate it into the opposite category by reversing the arrows. I am looking for a concrete set of "algebraic manipulations" that lets us take a statement to its dual, without understanding what anything means. In the example of negating a logical statement (in the final paragraph of the question), we can swap the symbols around without knowing what $P$ is, and more generally without understanding what things mean.

Duality is very important in category theory, but as far as I have seen, statements that "follow by duality" are often taken to be obvious, even though in reality there are lots of details to be checked. People seem to follow some informal procedure of replacing all instances of "left" with "right", "right" with "left", "limit" with "colimit" and so on.

This is reminiscent of the method for negating logical statements. For example, the statement $(\forall x, \exists y: P(x,y))$ has negation $(\exists x:\forall y, \neg P(x,y))$. We can obtain this negation by swapping $(\forall)$ with $(\exists)$, $(:)$ with $(,)$, and $(P)$ with $(\neg P)$. The set of rules for converting a statement of this form is well-known and easy to implement. It is also completely rigorous because we can actually prove in general that the rules apply.

Is there a similar set of rules for converting categorical statements into their duals?

Answer 1

Inductive definition of duality operator $\_{}˘$

Here is a fragment of the categorial language,

|  src f | tgt f |
|  Idₐ   | f ∘ g |
|  p + q | p × q |

Then, we can define the dual $e ˘$ of an expression $e$ as follows.

(src f)˘ = tgt (f ˘)
(tgt f)˘ = src (f ˘)
(Idₐ)˘   = Idₐ
(p + q)˘ = p ˘ × q ˘
(p × q)˘ = p ˘ + q ˘
p ˘      = p   provided p is an object OR a variable name

By induction (over the possible fragement of terms), one can show that this operator is self-inverse: $e ˘ ˘ = e$.

Example 1: Duality switches arrow argument positions

Then, we can apply these rules as follows: For any morphism expression $f$,

  (f : A ⟶ B)˘
≡     Arrow is defined in terms of source, target
  (src f = A  ∧  tgt f = B)˘
≡     Distribute duality over non-categoiral terms
  (src f)˘ = A ˘  ∧  (tgt f)˘ = B ˘
≡     Dual of an object is just the object unchanged
  (src f)˘ = A  ∧  (tgt f)˘ = B
≡     Duality slips src and tgt
  tgt (f ˘) = A  ∧  src (f ˘) = B
≡    Arrow notation
  f˘ : B ⟶ A

Example 2: Duality flips terminals and initials

   ( is terminal)˘
 ≡   Expand definitions
   (∀ X • ∃₁ f • f : X ⟶ )˘
 ≡   Distribute duality over non-categorial operators
   ∀ X • ∃₁ f • (f : X ⟶ )˘
 ≡   Above calculation: Duality flips arrow arguments
   ∀ X • ∃₁ f • f˘ :  ⟶ X
 ≡   Duality does nothing to variable names
   ∀ X • ∃₁ f • f :  ⟶ X
 ≡   Foldup using definitions
   I is initial

Duality is functorial

Moreover, notice that _˘ : ⟶ is an identity-on-objects functor ;-)

Answer 2

The idea of duality is that, whenever you have a purely categorical statement (or concept), you can look at what that statement means for a category $ C $ when applied to $ C^{\mathrm{op}} $: this gives you the dual statement or concept. Then, if you have a statement that is true in any category, then its dual statement is also necessarily true, since it is true for $ C^\mathrm{op} $. Finding out the dualized statement is then just a matter of properly writing down the statement in the dual category and interpreting it in the original one (which can often be tedious).

As an example, you can see how the definition of an initial object in $ C^{\mathrm{op}} $ coincides with that of a terminal object in $ C $! Thus, the dualized statement of "all initial items are uniquely isomorphic" is "all terminal objects are uniquely isomorphic". Same goes for limits/colimits, continuous/co-continuous functors, left/right-adjoints (note here that there are two categories involved, both of which you end up dualizing), left/right Kan extensions, kernels/cokernels, images/coimages in an abelian category, etc. In the end, you can apply duality to whatever statement you want, it is just a matter of practicing that conceptually simple but powerful tool.

I do think though that the lack of details is just typical of users of categories in general, and not just of duality, but that is another topic altogether.