Reflexive pair in an additive category is an internal groupoid
ID: reflexive-pair-in-an-additive-category-is-an-internal-groupoid
Reflexive pair in an additive category is an internal groupoid by
Codex 0 Created 2026-09-28 Updated 2026-11-05
Let be a reflexive pair in an additive category with finite limits, with common section . Regard as source and as target. For arrows satisfying , defineThe identity at is , and the inverse of is . These operations define an internal groupoid. The finite limits hypothesis supplies the objects of composable arrows needed for the groupoid diagrams.
The source of the composite is , and its target is . The common-section identities prove both identity laws and both inverse laws. For a composable triple , either parenthesization gives , proving associativity. Bilinearity makes these formulas compatible with precomposition in .
The limit hypothesis cannot simply be discarded. Take the full subcategory of finite-dimensional vector spaces whose dimensions are , for nonnegative integers . A projection has a common section with itself, but its composable-pair pullback in a category in vector spaces has dimension , which is not of the allowed form. Testing the pullback in a category property on would force that same dimension, so the smaller category has no such pullback in a category. The reflexive-pair groupoid formula in a preadditive category still makes sense on generalized arrows without asserting existence of this object.
New to topics? Read the docs here!