- Type Theory
HoTT Math 4: Local rings and fields
It’s been a while since the last edition of HoTT Math. Fall is always very busy for me and I’ve been composing this installment one at a time… We are finally arriving at our destination: fields!
The main issue with fields is to correctly handle the implicit negation in the term nonzero. Since the natural logic of HoTT is intuitionistic rather than classical, this is much more subtle than one would expect.
One issue with the basic commutative ring theory we developed last time is that there is a one-element ring. This is a feature of every equational theory since all identities are satisfied in the trivial algebra with one element. The problem is that equational logic doesn’t have negation so there is no way to state a nontriviality axiom like in this context. These issues are not new and not special to HoTT but the problem is amplified since logic in HoTT is may have more truth values than just true and false. Consequently, negation in HoTT always needs a little more care.
The usual way to say is the strongest one, namely that is the empty type or:
This is stronger than just saying that isn’t inhabited and it may exclude more than just the one element ring in the absence of the law of excluded middle [§3.4].
In general, we define inequality by
So we can simply write instead of To see this in action, let’s look at nonunits. The usual definition gives
The recursion and induction rules for -types [§1.6] show that is equivalent to the negation 1 In classical mathematics, a local ring is one where the nonunits form an ideal, which is then necessarily the unique maximal ideal of the ring. Assuming we see that is inhabited. It is also easy to see that
is always inhabited. Thus, all that is missing is the axiom:
Classically, fields are local rings where the maximal ideal has only one element So a reasonable axiom for fields is
(Note that implies ) Classically, these are indeed the fields we know and love but things break down in an intuitionistic setting. If these were fields, then we should be able to conclude that nonzero elements are units. However, from we can only conclude that and the conclusion there is the double negative rather than the positive statement The fact is that we cannot conclude that every nonzero element is a unit from this axiom without using the law of excluded middle! A similar issue arises with local rings as defined above: the axiom does not imply the property that if is a unit then at least one of and is a unit.
The solution to this isssue is to reverse the relation between equality and inequality. What if instead of inequality being the negation of equality we had that equality was the negation of inequality? This may sound counterintuitive at first but this is often how things work. Consider the case of two computable real numbers and that is real numbers for which we have an algorithm which on input gives us a rational approximation within of the real number in question. How do I determine whether and are equal?
- To show that they are different, I can use the two algorithms compute sufficiently good rational approximations to and to tell them apart.
- To show that they are equal, I need to argue that they are not different: given any input the two algorithms give rational approximations that are within of each other.
So, for computable real numbers, inequality is more primitive than equality!
This leads us to apartness relations: a binary relation that satisfies the following two axioms
These axioms ensure that the negation of is an equivalence relation; a tight apartness relation is one where
and thus the negation of is equality. In classical logic, every apartness relation is the negation of an equivalence relation but this is not true intuitionistically. In fact, the negation of equality is not necessarily an apartness relation!
Without further ado, let us state exactly how we can define local rings using apartness. For example, a more positive way to define local rings is that
is an apartness relation. The first apartness axiom actually follows from since The second apartness axiom boils down to to the fact discussed above that if is a unit then at least one of and is a unit. It is tempting to use the type
to describe this but this doesn’t work because of the exclusive nature of sum types. Instead, we must use the propositional truncation which is how the logical disjunction is defined [§3.7]. Thus a strongly local ring is a a nontrivial ring that satisfies
Before going further with these ideas, let’s practice some our intuitionistic reasoning by verifying that
Actually, we won’t be practicing our intuitionistic reasoning, we’ll just verify our logic by thinking in terms of functions between types rather than logical implication between propositions. Although an implication is not always equivalent to its contrapositive in intuitionistic logic, we do always have that
In terms of types and functions, this the special case of
where This looks even more familiar when uncurried:
Thus, we see that
Now recall that the disjunction is defined as the propositional truncation [§3.7]. This means that is a proposition such that
for any proposition 2 Since is a proposition, we see that
where the left equivalence is the special case of
Finally, recombining the above, we obtain
which is equivalent to because
Analogously to positive axiom for local rings, the positive axiom for fields is
which implies both and To see that we will make use of the distributive law
which follows from the general equivalence
by taking propositional truncations. In particular,
Since and we see that
and it follows that To see that we will make use of the fact that
This also follows from the distributive law above. Indeed,
because is Note that is stronger than since it implies that
and thus that has decidable equality [§3.4]. In other words, gives the equivalence
which means that is an apartness relation, whereas only gives that is a tight apartness relation:
The analysis above gives three plausible definitions for fields:
- A residual field is a nontrivial ring that satisfies
- A Heyting field is a nontrivial ring that satisfies and
- A discrete field is a nontrivial ring that satisfies
While each is stronger than the previous, they all have their uses and there is no choice which is always better than the others. Discrete fields behave the same as fields in classical logic since has decidable equality. Heyting fields are preferred in constructive circles and most definitions of the field of real numbers yield Heyting fields that are not necessarily discrete [§11.2, §11.3]. While residual fields are harder to work with, they do have their uses since the quotient of a nontrivial ring by a maximal ideal is a residual field which is not necessarily Heyting.
It is common for classical equivalences to break down in intuitionistic logic and therefore many natural concepts that are classically equivalent separate in intuitionistic settings. While this can be an annoyance, it is quite natural in the context of proof-relevant mathematics. Indeed, when we prove that a theorem about fields in a proof-relevant way, we cannot merely argue that every field satisfies the conclusion, we must proceed from known properties of fields and work our way to the desired conclusion. The precise properties used in this process naturally leads to a more refined understanding of the hypotheses of the theorem.
Before closing this installment of HoTT Math, let me draw your attention to an important lesson from the above:
While the logic of HoTT is intuitionistic, knowledge of intuitionistic logic is not necessary to work in HoTT.
Thinking in terms of types and functions as we did above works very well. To illustrate once more, consider the following classical equivalences:
Which are valid in intuitionistic logic? When translated into types and functions, we get that these are the special cases of
where The first classical equivalence is intuitionistically valid. After uncurrying both sides of
we obtain the obvious equivalence
On the other hand, the general form of the second equivalence makes no sense at all. Taking to be just about anything other than leads to obviously false equivalences such as when Indeed, the second classical equivalence is not intuitionistically valid since taking leads to
and double negation elimination is not intuitionistically valid.
The equivalence of is the dependent type analogue of currying/uncurrying. Indeed, if instead of the dependent type we have a simple type we obtain the familiar equivalence In full generality, we have the unwieldly equivalence where and [§2.15]. ↩
This is the standard trick to work with propositional truncations: so long as is a proposition, is equivalent to This is very important for handling disjunctions and existential quantifiers. Since “forgets” which of and holds, it is not generally possible to do a case analysis. However, if is a proposition then is equivalent to and the coproduct does allow for case analysis. This explains why in addition to the following “halves” of De Morgan’s laws hold in intuitionistic logic while their converses do not. ↩