division rig



Linear algebra

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology



Paths and cylinders

Homotopy groups

Basic facts







A division rig is a rig in which every nonzero element has a multiplicative inverse and 010 \neq 1 (which may be combined as: an element is invertible if and only if it is nonzero).

Constructive notions

Division rigs are (arguably) not a purely algebraic notion in that they don't form an algebraic category (see discussion below). For this reason, it should be unsurprising that in constructive mathematics (including the internal logic of a topos) there are different inequivalent ways to define a division rig. In this case the classical definition is not usually the best one; for instance, the non-negative real numbers do not satisfy it. There are several potential replacements with their own advantages and disadvantages.


If we replace “an element is invertible iff it is nonzero” in Definition by “an element is invertible xor it equals zero” (which is equivalent in classical logic but stronger in constructive logic), then we obtain the notion of discrete division rig. This condition means that every element is either 00 or invertible, and it also implies that 010\neq 1.

Such a division rig RR is ‘discrete’ in that it decomposes as a coproduct R={0}R ×R = \{0\} \sqcup R^\times (where R ×R^\times is the subset of invertible elements). An advantage is that this is a coherent theory and hence also a geometric theory. A disadvantage is that this axiom is not satisfied (constructively) by the rig of non-negative real numbers (however these are defined), although it is satisfied by the rig of non-negative rationals.


If we interpret ‘nonzero’ in Definition as a reference to a tight apartness relation, thus defining the apartness relation #\# by x#yx # y iff xyx - y is invertible, then we obtain the notion of Heyting division rig, where the rig operations become strongly extensional functions. In addition to 0#10\# 1, the condition then means that every element apart from 00 is invertible.

This is how ‘practising’ constructive analysts of the Bishop school usually define the simple word ‘division rig’. An advantage is that the (located Dedekind) non-negative real numbers form a Heyting division rig, although (for example) the (less located) non-negative MacNeille real numbers need not form a Heyting division rig; another disadvantage is that this is not a coherent axiom and so cannot be internalized in as many categories.

Every discrete division rig is also a Heyting division rig. A Heyting division rig is a discrete division rig if and only if equality is decidable; it is in this sense that a discrete division rig is ‘discrete’.



There are the division rigs of:

Last revised on July 12, 2021 at 10:17:59. See the history of this page for a list of all contributions to it.