11. Dimension as a Forgetful Functor
PropertyKindCalculus does not discard PhysLib's Dimension; it keeps it as a forgetful
functor. Dimension answers the coarse question — "are these even commensurable in
the SI base quantities?" — and the kind layer answers the fine one. The forgetful
map, its multiplicativity, and the dimension-1 disambiguation it makes possible
are now realized, sorry-free, in the Dimension library; the full coherence law
— that \dim is a homomorphism over the interaction algebra — is realized in the
Interaction module and stated as the homomorphism capstone below.
Two terms recur below; in plain engineering terms they mean this. A forgetful
functor is a deliberately lossy, one-way map: \dim keeps only a kind's SI
base-quantity exponents (length, mass, time, …) and discards everything else that
distinguishes it, so many kinds share one dimension and there is no inverse. A
homomorphism is a map that respects an operation: here \dim respects
multiplication — the dimension of a product is the product of the dimensions, the
exponents adding — which is exactly the bookkeeping of everyday dimensional
analysis, stated and proved here as a law rather than performed by hand.