Lagmental Vicfred

Naturality Is a Family of Commuting Squares by Vicfred

A natural transformation assigns one morphism per object and requires compatibility with every arrow. I want the notation, the mechanism, and the failure mode visible at the same time.

Definitions first

Category theory records objects through their morphisms. A functor \(F:\mathcal C\to\mathcal D\) preserves identities and composition, while a natural transformation \(\eta:F\Rightarrow G\) compares functors uniformly.

$$ \eta:F\Rightarrow G,\qquad\eta_X:F(X)\to G(X) $$

I keep the defining relation \(\mathsf D\) above the derived relation \(\mathsf C\). This exposes whether cancellation used \(x\ne0\) and whether the conclusion is canonical.

$$ G(f)\circ\eta_X=\eta_Y\circ F(f) $$

A small case in full

The following line is the smallest calculation that still exercises the mechanism. It keeps nested delimiters and the order of operations explicit.

$$ \begin{array}{ccc}F(X)&\xrightarrow{F(f)}&F(Y)\\{\scriptstyle\eta_X}\downarrow&&\downarrow{\scriptstyle\eta_Y}\\G(X)&\xrightarrow{G(f)}&G(Y)\end{array} $$

The reusable statement

The two-row display is also a debugging tool: if the conclusion changes when only notation changes, some hidden choice has entered the argument.

$$ \begin{aligned} \mathsf{D}\;&:\quad \eta:F\Rightarrow G,\qquad\eta_X:F(X)\to G(X),\\[5pt] \mathsf{C}\;&:\quad G(f)\circ\eta_X=\eta_Y\circ F(f). \end{aligned} $$

A nearby false statement

An isomorphism of objects is stronger than a natural bijection of underlying sets unless that bijection respects all morphisms in the relevant category.

$$ \boxed{\begin{gathered} \text{compact conclusion}\\[-2pt] G(f)\circ\eta_X=\eta_Y\circ F(f) \end{gathered}} $$

The notation is dense, but it is doing honest work: every delimiter records scope and every index records dependence. Removing one should require a mathematical reason.

This article was posted on Sat 09 September 2023. Facts and circumstances may have changed since publication.
Please contact me before jumping to conclusions if something seems wrong or unclear.