1 Introduction
1.1 Definition of a Wheel
Algebraic wheels are structures generalising a commutative semiring, attempting to make sense of ‘division’ by zero.
Loosely speaking, given a semiring \(R\) and it’s associated monoids, one may extend the semi-ring in a variety of well-known ways. Considering an additive inverse extends a commutative semiring, to a structure with a given name: a commutative ring, and attempting the same succesfully for the multiplicative monoid yields a field.
Working backwards, given a set \(M\) with two monoids – one in additive notation and one in multiplicative. The path to obtain a semiring is clear, a wheel however generalises the semiring by removing the usual distributivity and defines a new unary map \(wDiv\).
A Wheel \(W\) is an algebraic structure which has two binary operations \((+,*)\), like a ring. Similarly to a commutative ring, a Wheel is a commutative monoid in both operations. Additionally, there is a multiplicative unary map \(wDiv\) which is an involution, as well as a few idiosyncratic properties in the interactions of the \(+\),\(*\) and \(wDiv\).
Involution: \(\forall w \in W, wDiv(wDiv(w)) = w\)
Multiplicative automophism: \(\forall w, v \in W, wDiv(wv) = wDiv(w)wDiv(v)\)
Right distributivity rule 1: \(\forall w, v, u \in W, (w + v)u + 0u= wu + vu\)
Right distributivity rule 2: \(\forall w, v, u \in W, (w + 0v)u + 0u= wu + 0v\)
Right wDiv distributivity: \(\forall w, v, u \in W, (w + uv)wDiv(u) = wDiv(u)+ v+0u\)
Division by 0: \(\forall w \in W, 0Div(0) + w = 0Div(0)\)
Zero squared: \(0*0 = 0\)
Division rule: \(\forall w, v \in W, wDiv(w + 0v) = wDiv(w) +0v\)
Whenever not specified, the notation for the monoids is assumed to be \((+,*)\) with neutral elements \(0\) and \(1\) respectively.
1.1.1 Basic results
Here we collate some very simple propositions that are straightforward given the Wheel definition. These are designed to be auxillary and thus somewhat assorted and perhaps trivial, however mechanisation demands specification of what is typically deemed trivial.
Define the notation \(\backslash _{a} := wDiv \) for brevity.
Given a Wheel \(W\) , then \(\backslash _{a} 1 = 1\) where \(1\) is the neutral element of the multiplicative commutative monoid.
Given a Wheel \(W\) and any two elements \(a,b \in W\), then:
Given a Wheel \(W\) and any element \(a \in W\), then:
Given a Wheel \(W\) and any element \(a \in W\), then:
Given a Wheel \(W\) and any elements \(a,b,c \in W\) such that \(a*c = b*c\), then:
Given a Wheel \(W\) , \(wDiv\) is a monoid automorphism for \((1,*)\).