François G. Dorais

Research in Logic and Foundations of Mathematics


HoTT Math 3: Unit group of a ring

In this installment of HoTT Math, we are taking one more step toward elementary field theory by exploring the unit group of a ring.


A commutative (unital) ring is a set with two constants , one unary operation , two binary operations along with the usual axioms: , ,

and

Commutativity of addition can be derived as usual using the fact that

If you want to test your path manipulation skills, you can try to write down the resulting term for

However, as we discussed last time, this is not necessary since the proof is ultimately not relevant when the carrier of an algebra is a set.

Reading off the usual definition of unit, we obtain the type

Elements of type are pairs , where and . Because is a set and inverses are unique, there is always at most one such , which means that is a proposition. Therefore, we can comprehend the set of units:

(Subset comprehension is discussed in §3.5 of the book.) Technically, elements of are triples where and . Thus is not merely a subset of but each element of comes equipped with a justification for being in . Since for each there is at most one , we can identify the two without much confusion but the extra coordinates are actually helpful for proving things about .

To illustrate this, let’s outline the verification that is a group under multiplication. We will view elements of as pairs but we will forget the path witnessing that . Since we’re working with sets, we shouldn’t worry about paths anyway.1 To begin, we need to isolate the group operations:

To conclude the argument, it suffices to verify that is inhabited. Associativity and identity are immediate consequences of . The tacit path coordinates are handy for inverses: the path simply consists of the two implied paths and !

The key difference between this proof and the classical proof that is a group is the way we used the definition of . At each step of the classical proof, we need to invoke the definition of to get the relevant inverses, do the same computations, and then forget the extra information. In the proof-relevant argument, the subset incorporates its definition and the relevant inverses are already there to be used in computations. To keep the argument from involving too many (ultimately irrelevant) path computations, we still forgot one piece of the definition of in the outline above. This kind of selective unraveling can be useful since formal definitions can rapidly become unwieldy. We did end up invoking the path coordinates at the very end to verify the identity axiom. However, we didn’t really need the paths themselves, we just needed to remember that elements aren’t arbitrary pairs, they are pairs such that . This is what the seemingly irrelevant path coordinate does, the relevant data is not the path itself, it is the type of the path that matters.


The lesson is that while proof-relevant mathematics does force you to carry extra baggage, that baggage is actually handy. Moreover, you can always manage the burden by selectively unraveling the contents of the baggage. In fact, you also carry this baggage when doing classical mathematics except that you conceal the baggage in your memory, recalling each item as you need it. The problem with this strategy is that it’s easy to forget things if you are not careful. Proof-relevant mathematics forces you to keep track of everything!


Post Scriptum

In the comments, Toby Bartels pointed out that the argument above contains a major type-theoretic faux pas: using type declarations as propositions. The cause of this is the deliberate omission of the path coordinate which leads to phrases like “we see that since […]” and “we see that if then .” The problem is that type declarations are either correct or not (and this is decidable!) but not true or false. Indeed, true and false are both values that can be used but correct and incorrect are not — there is no value in being incorrect! This may seem like a subtle difference but it is actually a very important one in type theory since there is little other separation of syntax and semantics.

Below, I produced three more variants of the above argument that avoid the trouble with Version 0 above. The first is simply does not omit the path coordinates. The second uses the membership relation where the original used an erroneous type declaration. The third is a direct translation of the classical proof, also using the membership relation. To facilitate comparison, I tried to keep the three versions as close as possible to the original. I am curious to know which of the four versions you prefer, or if you have yet another version that you prefer!


Version 1. Let’s outline the verification that is a group under multiplication. To begin, we need to isolate the group operations:

To conclude the argument, it suffices to verify that is inhabited. Associativity and identity are immediate consequences of . The path is composed of , , and the paths must match since is a set.


Version 2. Let’s outline the verification that is a group under multiplication. By virtue of univalence, there are multiple ways to look at . Instead of viewing it as a subset of we can also view it as a subset of , namely

Thus denotes the proposition It turns out that this view of will be easier to work with. To begin, we need to isolate the group operations:

To conclude the argument, it suffices to verify that is inhabited. Associativity and identity are immediate consequences of . The path is composed of and , which hold because .


Version 3. Let’s outline the verification that is a group under multiplication. Per definition of , we will write to mean . To begin, we need to isolate the group operations:

To conclude the argument, it suffices to verify that is inhabited. Associativity and identity are immediate consequences of . The remaining identity follows immediately from the definition of group inverses.


CC0 Originally posted on by François G. Dorais. To the extent possible under law, François G. Dorais has waived all copyright and neigboring rights to this work.


Comments