So I’d like to take some time to talk about a #math thing I did today—specifically in #abstractalgebra. I actually formalized it in #Agda!
But before we get to that, I need to take you on a journey, one that will involve building an algebraic structure that looks completely unfamiliar and strange and then discovering that it’s actually a very familiar structure indeed, just looked at from a new angle.
We begin, as always, by defining our stuff and structure.
We’ll need a carrier set C, of course.
We’ll also want a specified element of C; call it ▪︎.
Finally, we need a ternary operator: - ⟪ - ⟫ - : C × C × C → C. We refer to the first and third inputs as the sides and the second input as the center, for hopefully obvious reasons.
That’s all for our structure!
But before we can state the axioms for this thing, we need a few convenience definitions.
Say that the successor of an element a ∈ C is defined as ▪︎ ⟪ a ⟫ ▪︎; furthermore, define ⬥ to be the successor of ▪︎, and likewise define ● to be the successor of ⬥.
With these definitions in place, we are now finally ready to express our axioms!
The first five axioms are pretty straightforward, relating each of our named elements to the ternary operator in its own way.
▪︎ can be swapped across the sides: ▪︎ ⟪ a ⟫ b = b ⟪ a ⟫ ▪︎
⬥ can also be swapped across the sides, and when it’s there the whole thing reduces to just the center input, discarding the other side: ⬥ ⟪ a ⟫ b = b ⟪ a ⟫ ⬥ = a
● can also be swapped across the sides, and when it’s there the other side and the center can swap with each other too: ● ⟪ a ⟫ b = b ⟪ a ⟫ ● = a ⟪ b ⟫ ● = ● ⟪ b ⟫ a
When ▪︎ is on one side, and the center and other side are the same as each other, the whole thing cancels to ⬥: ▪︎ ⟪ a ⟫ a = a ⟪ a ⟫ ▪︎ = ⬥
Lastly, when ● is on one side and ⬥ is in the center, the whole thing reduces to the other side: ● ⟪ ⬥ ⟫ a = a ⟪ ⬥ ⟫ ● = a
The next three axioms are a bit stranger; you can think of them as distribution laws of a sort, describing the behavior of nesting our ternary operator on one side of itself, but I find a better intuition for them is as a “pulling out” of the inner center into the outer one, and adjustments to let that happen, or what happens when there’s already a “hole” in one of the centers. Here they are:
a ⟪ b ⟫ (c ⟪ d ⟫ e) = a ⟪ (a ⟪ b ⟫ d) ⟫ (c ⟪ ⬥ ⟫ e)
(a ⟪ b ⟫ c) ⟪ d ⟫ e = (a ⟪ ⬥ ⟫ c) ⟪ (b ⟪ d ⟫ e) ⟫ e
(a ⟪ ⬥ ⟫ b) ⟪ c ⟫ d = a ⟪ c ⟫ (b ⟪ ⬥ ⟫ d)
The final axiom is thankfully much more intuitive. It’s a kind of double-exchange rule, letting us swap between inner and outer sides when the nesting is in the center:
a ⟪ (b ⟪ c ⟫ d) ⟫ e = b ⟪ (a ⟪ c ⟫ e) ⟫ d
There’s an optional additional axiom, which further constrains our structure.
a ⟪ b ⟫ c = c ⟪ b ⟫ a
We won’t assume it by default but some instances of the structure usefully satisfy it. I’ll call it the reversibility axiom, and say that our structure is reversible if it satisfies it.
Here you should pause and contemplate this structure! What is it, exactly? How does it behave? What intuition can you gain for these axioms and how they interact?
Here are some theorems I’ve proven about this structure, without commentary; see if you can prove them too:
● ⟪ a ⟫ (● ⟪ b ⟫ c) = ● ⟪ (● ⟪ a ⟫ b) ⟫ c
● ⟪ a ⟫ (b ⟪ c ⟫ d) = ● ⟪ c ⟫ (b ⟪ a ⟫ d)
● ⟪ a ⟫ (b ⟪ ⬥ ⟫ c) = b ⟪ a ⟫ c
When you feel like you have a decent grasp of how this structure operates, proceed!
Surprise! This structure is completely isomorphic to the standard notion of a ring. Making the structure reversible gets us a commutative ring.
As partial proof, here is the conversion from our structure to the typical notation:
a + b = ● ⟪ a ⟫ b
a - b = ▪︎ ⟪ a ⟫ b
-a = ▪︎ ⟪ ⬥ ⟫ a
a • b = a ⟪ ⬥ ⟫ b
0 = ⬥
1 = ●
And here is the conversion in the other direction:
▪︎ = -1
a ⟪ b ⟫ c = (a • c) + b
The successor operation from the very beginning is just adding one!
The proofs of the axioms in each direction are left as exercises for the reader…
…or you can inspect the Agda file I’ve linked here, which contains all of the above and more formalized and computer-checked! (Note that the notation is slightly different in the code; I use -𝟷# instead of ▪︎ and 𝚏𝚖𝚊 𝚊 𝚋 𝚌 instead of a ⟪ c ⟫ b.)
https://gist.github.com/pthariensflame/4063a4ecfd6db8e7e744dae5b9cdeb3b
As a bonus (not formalized in the linked file), think about what the ring of n×n square matrices with elements taken from a given ring looks like when both the element ring and the matrix ring are represented this way! What is negative one for matrices? What is our ternary operator? (Hint: you can express it with just the ternary operator on the element ring, and don’t need any of our specific values.)
So I decided to give these structures a name, despite being “just” rings by a different characterization, because that difference puts them in a new conceptual hierarchy of mathematical objects that just so happens to coincide with rings at that point. I call one of these things a “fumula” (/ˈfju.mju.lə/, FYOO-myoo-luh), after FUsed MULtiply-Add.
One reason I wanted to give them a name is because there’s a further structure I call a “fupomula” (/fju.ˈpɔu.mju.lə/, fyoo-POH-myoo-luh), after FUsed POwer-MULtiply-Add. As the naming suggests, this is a structure with a specified element (intended as -1) and a tetrary operator (intended as (aᵇ • c) + d), along with a predicate that calls certain elements “purely negative” and an allowance that the tetrary operator is undefined when a = 0 and b is purely negative.
From here we construct a successor function similarly to a fumula, by filling in a = b = c = -1, and define 0 as the successor of -1 and 1 as the successor of 0 just as before.
We then need axioms that say -1 and 0 are purely negative and 1 isn’t, and some generalization of the fumula axioms to account for the additional power input, plus probably a few more axioms to handle pure negativity and the power input more generally.
So what does this get us? Well, we can take reciprocals by setting the power to -1, so we have arbitrary division and thus arbitrary rationals. But that means we can take rational powers, so we have all algebraic numbers. And moreover we can take rational powers of -1 too, so we have all complex roots of unity! I’m not entirely sure what structure this gets us (it’s a skew field with all exponents that don’t imply a division by 0, but I’m not aware of a specific name for that).
That feels specifically weird enough to me to give the higher members of this hierarchy new names. (The member below fumulas should just be the usual characterization of Abelian groups, I think.)