François G. Dorais

Topics
• Type Theory

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 $R$ with two constants $\mathsf{O},\mathsf{I}:1\to R$, one unary operation ${-\square}:R \to R$, two binary operations ${\square+\square},{\square\cdot\square}:R \times R \to R$ along with the usual axioms: ${\small\fbox{\(\phantom{b}\)group\(\phantom{q}\)}}(\mathsf{O},-\square,\square+\square)$, ${\small\fbox{\(\phantom{b}\)monoid\(\phantom{q}\)}}(\mathsf{I},{\square\cdot\square})$,

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 $\operatorname{\mathsf{unit}}(x)$ are pairs $(y,p)$, where $y:R$ and $p: x \cdot y =_R \mathsf{I}$. Because $R$ is a set and inverses are unique, there is always at most one such $(y,p)$, which means that $\operatorname{\mathsf{unit}}(x)$ is a proposition. Therefore, we can comprehend the set of units:

(Subset comprehension is discussed in §3.5 of the book.) Technically, elements of $R^\times$ are triples $(x,y,p)$ where $x,y:R$ and $p:(x \cdot y =_R \mathsf{I})$. Thus $R^\times$ is not merely a subset of $R$ but each element of $R^\times$ comes equipped with a justification for being in $R^\times$. Since for each $x:R$ there is at most one $(x,y,p):R^\times$, we can identify the two without much confusion but the extra coordinates are actually helpful for proving things about $R^\times$.

To illustrate this, let’s outline the verification that $R^\times$ is a group under multiplication. We will view elements of $R^\times$ as pairs $(x,y)$ but we will forget the path witnessing that $x \cdot y =_R \mathsf{I}$. Since we’re working with sets, we shouldn’t worry about paths anyway.1 To begin, we need to isolate the group operations:

• First, we see that $(\mathsf{I},\mathsf{I}):R^\times$ since we have a path $\mathsf{I}\cdot\mathsf{I}=_R \mathsf{I}$ by the identity axiom; this will be our group identity.

• Next, we see that if $(x_0,y_0),(x_1,y_1):R^\times$ then $(x_0 \cdot x_1,y_1 \cdot y_0):R^\times$. Indeed, if $x_0 \cdot y_0 =_R \mathsf{I}$ and $x_1 \cdot y_1 =_R \mathsf{I}$ then

  $$x_0 \cdot x_1 \cdot y_1 \cdot y_0 =_R x_0 \cdot \mathsf{I}\cdot y_0 =_R x_0 \cdot y_0 =_R \mathsf{I}.$$

  From this, we directly extract our group multiplication $\square\cdot\square:R^\times \times R^\times \to R^\times$.

• Finally, we see that if $(x,y):R^\times$ then $(y,x):R^\times$. (This is immediate from commutativity but a slightly longer argument shows that this works even without this assumption.) As a result, we get the group inverse $\square^{-1}:R^\times \to R^\times$.

To conclude the argument, it suffices to verify that ${\small\fbox{\(\phantom{b}\)group\(\phantom{q}\)}}(R^\times,\square^{-1},\square\cdot\square)$ is inhabited. Associativity and identity are immediate consequences of ${\small\fbox{\(\phantom{b}\)monoid\(\phantom{q}\)}}(R,\mathsf{I},\square\cdot\square)$. The tacit path coordinates are handy for inverses: the path $(x,y)\cdot(y,x) =_{R^\times} (\mathsf{I},\mathsf{I})$ simply consists of the two implied paths $x \cdot y =_R \mathsf{I}$ and $y \cdot x =_R \mathsf{I}$!

The key difference between this proof and the classical proof that $R^\times$ is a group is the way we used the definition of $R^\times$. At each step of the classical proof, we need to invoke the definition of $R^\times$ to get the relevant inverses, do the same computations, and then forget the extra information. In the proof-relevant argument, the subset $R^\times$ 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 $R^\times$ 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 $(x,y)$ aren’t arbitrary pairs, they are pairs such that $x \cdot y =_R \mathsf{I}$. This is what the seemingly irrelevant path coordinate does, the relevant data is not the path itself, it is the type $x \cdot y =_R \mathsf{I}$ 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 $(\mathsf{I},\mathsf{I}):R^\times$ since […]” and “we see that if $(x,y):R^\times$ then $(y,x):R^\times$.” 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 $\in$ 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 $R^\times$ is a group under multiplication. To begin, we need to isolate the group operations:

• First, $(\mathsf{I},\mathsf{I},i):R^\times$ is our group identity where $i:\mathsf{I}\cdot\mathsf{I}=_R \mathsf{I}$ is an instance of the identity axiom.

• Next, the group product is defined by $(x_0,y_0,p_0)\cdot(x_1,y_1,p_1) := (x_0 \cdot x_1,y_1 \cdot y_0,q)$, where

  $$q:x_0 \cdot x_1 \cdot y_1 \cdot y_0 =_R x_0 \cdot \mathsf{I}\cdot y_0 =_R x_0 \cdot y_0 =_R \mathsf{I}.$$

• Finally, group inverses are defined by $(x,y,p)^{-1} := (y,x,q)$, where $q:y \cdot x =_R x \cdot y =_R \mathsf{I}.$ (A slightly longer argument shows that this works even without the commutativity assumption.)

To conclude the argument, it suffices to verify that ${\small\fbox{\(\phantom{b}\)group\(\phantom{q}\)}}(R^\times,\square^{-1},\square\cdot\square)$ is inhabited. Associativity and identity are immediate consequences of ${\small\fbox{\(\phantom{b}\)monoid\(\phantom{q}\)}}(R,\mathsf{I},\square\cdot\square)$. The path $(x,y,p)\cdot(y,x,q) =_{R^\times} (\mathsf{I},\mathsf{I},i)$ is composed of $p:x \cdot y =_R \mathsf{I}$, $q:y \cdot x =_R \mathsf{I}$, and the paths must match since $R$ is a set.

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

Thus $(x,y) \in_{R \times R} R^\times$ denotes the proposition $x \cdot y =_R \mathsf{I}.$ It turns out that this view of $R^\times$ will be easier to work with. To begin, we need to isolate the group operations:

• First, we see that $(\mathsf{I},\mathsf{I}) \in_{R\times R} R^\times$ since we have a path $\mathsf{I}\cdot\mathsf{I}=_R \mathsf{I}$ by the identity axiom; this will be our group identity.

• Next, we see that if $(x_0,y_0),(x_1,y_1) \in_{R \times R} R^\times$ then $(x_0 \cdot x_1,y_1 \cdot y_0) \in_{R \times R} R^\times$ too. Indeed, if $x_0 \cdot y_0 =_R \mathsf{I}$ and $x_1 \cdot y_1 =_R \mathsf{I}$ then

  $$x_0 \cdot x_1 \cdot y_1 \cdot y_0 =_R x_0 \cdot \mathsf{I}\cdot y_0 =_R x_0 \cdot y_0 =_R \mathsf{I}.$$

  From this, we directly extract our group multiplication $\square\cdot\square:R^\times \times R^\times \to R^\times$.

• Finally, we see that if $(x,y) \in_{R \times R} R^\times$ then $(y,x) \in_{R \times R} R^\times$ since $x \cdot y =_R \mathsf{I}$ implies $y \cdot x =_R \mathsf{I}$ by commutativity. (A slightly longer argument shows that this works even for non-commutative rings.) As a result, we get the group inverse $\square^{-1}:R^\times \to R^\times$.

To conclude the argument, it suffices to verify that ${\small\fbox{\(\phantom{b}\)group\(\phantom{q}\)}}(R^\times,\square^{-1},\square\cdot\square)$ is inhabited. Associativity and identity are immediate consequences of ${\small\fbox{\(\phantom{b}\)monoid\(\phantom{q}\)}}(R,\mathsf{I},\square\cdot\square)$. The path $(x,y)\cdot(y,x) =_{R^\times} (\mathsf{I},\mathsf{I})$ is composed of $x \cdot y =_R \mathsf{I}$ and $y \cdot x =_R \mathsf{I}$, which hold because $(x,y), (y,x) \in_{R \times R} R^\times$.

Version 3. Let’s outline the verification that $R^\times$ is a group under multiplication. Per definition of $R^\times$, we will write $x \in_R R^\times$ to mean $\mathsf{unit}(x)$. To begin, we need to isolate the group operations:

• First, we see that $\mathsf{I}\in_{R} R^\times$ since $\mathsf{I}\cdot\mathsf{I}=_R \mathsf{I}$ by the identity axiom; this will be our group identity.

• Next, we see that if $x_0,x_1 \in_{R} R^\times$ then $x_0 \cdot x_1 \in_{R} R^\times$ too. Indeed, since $\mathsf{unit}(x_0)$ and $\mathsf{unit}(x_1)$ there are $y_0,y_1:R$ such that $x_0 \cdot y_0 =_R \mathsf{I}$ and $x_1 \cdot y_1 =_R \mathsf{I}.$ Then

  $$x_0 \cdot x_1 \cdot y_1 \cdot y_0 =_R x_0 \cdot \mathsf{I}\cdot y_0 =_R x_0 \cdot y_0 =_R \mathsf{I}$$

  which shows that $\mathsf{unit}(x_0 \cdot x_1).$ Thus our group multiplication is (the restriction of) the usual ring multiplication.

• Finally, we see that if $x \in_{R} R^\times$ then, by definition of the proposition $\mathsf{unit}(u)$, there is a unique $y:R$ such that $x \cdot y =_R \mathsf{I}$. By commutativity, $y \cdot x =_R \mathsf{I}$ which means that $y \in_{R} R^\times$ and this $y$ is the group inverse of $x$.

To conclude the argument, it suffices to verify that ${\small\fbox{\(\phantom{b}\)group\(\phantom{q}\)}}(R^\times,\square^{-1},\square\cdot\square)$ is inhabited. Associativity and identity are immediate consequences of ${\small\fbox{\(\phantom{b}\)monoid\(\phantom{q}\)}}(R,\mathsf{I},\square\cdot\square)$. The remaining identity $x \cdot x^{-1} =_{R^\times} \mathsf{I}$ follows immediately from the definition of group inverses.

Originally posted on July 14, 2013, 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

• François G. Dorais wrote on July 14, 2013, at 20:39

  In the definition of units, I chose to use right inverses instead of left inverses. This makes no difference since the ring is commutative. In fact, this makes no difference even if the ring is not commutative. If we use the left inverse definition

  $$\operatorname{\mathsf{unit}}'(y) :\equiv \sum_{x:R} (x \cdot y =_R \mathsf{I}),$$

  we realize that the group of units $\set{y : R \mid \operatorname{\mathsf{unit}}'(y)}$ is actually the exact same as the one above: they both equal

  $$\sum_{x,y:R} (x \cdot y =_R \mathsf{I})$$

  by univalence! The proof that this is a group is actually the same seen from the left or from the right. (Note that the verification that left and right inverses are the same is the main content of the definition of the group inverse.)

  I guess there is a side lesson here: univalence applies to proofs too! In HoTT, what we used to call “symmetric arguments” are actually the exactly the same…

  ---

• Toby Bartels wrote on July 15, 2013, at 17:49

  I don’t like to see typing declarations used as if they were propositions. To some extent they are; a term may or may not have a certain type. But it’s an important feature of intensional type theory that this question is decidable (and, usually, immediately so); you can see from the form of the term whether it has the claimed type or not. But when you abbreviate (x, y, p) as (x, y), then this is no longer decidable (which would solve the word problem for rings).

  This is where type theorists (at least those who use the colon for typing declarations) use the set membership symbol ‘∈’, with the benefit that we actually have a proposition internal to the type theory (rather than merely the external proposition that a term has a given type). Although you defined the set of units of R as a subset of R, it can also be realised as a subset of R × R, and that is how you are using it. In general, given any set S, any subset A of S, and any element e of S, there is a mere proposition e ∈ A (with a subscript S on the ‘∈’ to be most proper) that indicates that e belongs to A (which I’m sure is defined somewhere in the HoTT book and which you can probably write down for yourself).

  ---

• François G. Dorais replied to Toby Bartels on July 15, 2013, at 19:37

  You’re right but the point I’m trying to make is that there is a right balance for doing things informally, which is actually in between forgetting everything (the fully extensional way) and remembering everything (the fully intensional way).

  If I work the fully intensional way, then I need to do something with the paths all the time. If I think of elements of $R^\times$ as triples $(x,y,p)$ then the group product is

  $$(x_0,y_0,p_0)\cdot(x_1,y_1,p_1) := (x_0 \cdot x_1,y_1 \cdot y_0,\text{messy path}),$$

  and I am compelled to write it that way (perhaps relying on my proof assistant to write the messy path for me). That’s an unnecessary burden since the path is always uniquely determined and almost never used.

  If I work the fully extensional way, then I need to recall all the necessary data all the time. That’s also an unnecessary burden. We’re all used to it but anyone who spent time teaching intro to proofs at the college level knows how hard it is to communicate the idea of “using definitions”…

  The middle ground I used seems just right to me: all the data I need is right there and the data I don’t need to worry about is out of sight. Note that I still remember the extra data is there, I just choose to ignore it since I know in advance that I don’t need to worry about it.

  ---

• François G. Dorais replied to Toby Bartels on July 15, 2013, at 19:53

  Regarding your alternative of using the $\in$ relation. I’m not too fond of that. In this case, the $\in$ relation takes $x \in R^\times$ to $\mathsf{unit}(x)$. You need to remember how $R^\times$ is defined to figure out what $\in$ actually means. That’s just a sneaky way of mapping proof-irrelevant mathematics into proof-relevant mathematics. There is no point in doing proof-relevant mathematics if it’s done that way. I do see your point that one way to formalize my in-between solution is to have $(x,y) \in R^\times$ map to $x\cdot y =_R \mathsf{I}$. That’s neat but there is nothing there to suggest that I had an a priori reason for doing that.

  ---

• François G. Dorais replied to Toby Bartels on July 15, 2013, at 20:31

  Actually, since I also had to explain my a priori reason for dropping the path component, there may be more merit to using $(x,y) \in R^\times$ than I thought. It is a more explicit way of forgetting the path coordinate without contaminating the intensional theory with bits of extensionality.

  I’m still not feeling great about this. The $\in$ relation is just a kludge to eliminate the set builder notation – $x \in \set{x : A \mid P(x)}$ is defined as $P(x)$ – and the set builder notation is already something I was trying to avoid. More importantly, there is also the temptation to use it to forget things that are actually useful…

  ---

• François G. Dorais replied to Toby Bartels on July 15, 2013, at 21:16

  I added a note explaining this. You’re completely right about this but I still have a hard time with it. This is magnified by another problem I was dealing with: to find a good way to handle partial functions. The confounding thing is that a partial function is $F$ actually equal to its domain of definition $D$, what’s even more confusing is that $F(x)$ is also equal to $x \in D$! Most of the time, I think that’s pretty neat, but it also gives me some bad headaches…

  ---

• François G. Dorais replied to Toby Bartels on July 15, 2013, at 23:49

  After thinking about this some more, I decided to actually write out three variants of the proof, one spelling out the paths, another using $\in_{R \times R}$, and a third using $\in_R$ (which is really just the classical proof recast in HoTT). I will insert these at the end of the post when I’m done typing them so that I can compare all three and see the pros and cons of each.

  ---

• François G. Dorais wrote on July 16, 2013, at 01:27

  My favorite is Version 1. My main problem is that it was harder to write since I wanted to minimize the effect of the paths. I also hated wasting valuable letters to name these paths. This is probably just me, but it was hard to resist computing the paths in my head as I was composing the proof. Summary: this is fantastic for reading, but not for writing.

  Currently, Version 0 and Version 2 are tied for second place. The basic arguments are identical, so there is no distinction there. Version 2 does correct the error of Version 0, but it introduces a new one. In the end, writing $(x,y)\cdot(y,x) =_{R^\times} (\mathsf{I},\mathsf{I})$ is technically incorrect. The operation $\square\cdot\square$ is on $R^\times$, not on $R \times R$. One could argue that the same error is in Version 0, but there $(x,y)$ abbreviates $(x,y,p):R^\times$, so this usage is consistent with the local conventions. The other drawback of Version 2 is that the group operations are defined by specifying each individual value, I prefer the expressions in Version 0.

  ---

• Toby Bartels replied to François G. Dorais on July 17, 2013, at 18:52

  Version 1 really gives the flavour of fully proof-relevant mathematics, albeit at the cost of ultimately irrelevant verbiage. I wonder if you might rewrite ‘A slightly longer argument shows that this works even without the commutativity assumption.’ as ‘A slightly longer construction of q shows that this works even without the commutativity assumption.’ in that version. (That sentence was also left out of Version 3, I assume accidentally.)

  ---