search

UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
397 stars 23 forks source link

on the different kinds of fields in constructive mathematics #139

Closed ghost closed 2 years ago

ghost commented 2 years ago

Added some text about the different kinds of fields in constructive mathematics to section 8.1 of the textbook. I'm not sure exactly how references in LaTeX work, so I've just put the references at the end of the section.

ghost commented 2 years ago

Note: While this text mostly follows chapter 9 of Lombardi and Quitté's Commutative algebra: Constructive methods (Finite projective modules), the definition of field is slightly different from Lombardi and Quitté's definition of field; they define a field to be a Heyting field, while I define a field to be a "residue field" (cf. the nlab, Peter Johnstone's Rings, Fields, and Spectra, unrelated to the residue fields in algebraic geometry), which is slightly more general, and encompasses more sets of real numbers such as the MacNeille real numbers.

If people don't really care about the MacNeille real numbers for the sake of this book, then the definition of a field could be modified to directly be a Heyting field a la Lombardi and Quitté's textbook.

In addition, the trivial ring is a field in Lombardi and Quitté's textbook. If people wish to exclude the trivial ring from the definition of field, then the additional condition that $0 \neq 1$ or something similar could be added to the definition of field.

ghost commented 2 years ago

I have added a nontriviality condition to the definition of fields and local rings, and edited the rest of the section accordingly. I have also applied Dan Grayson's other suggestions above to the text. In nontrivial commutative rings the Lombardi and Quitté definition of non-invertible element is the same as the usual definition of non-invertible element as the logical negation of being invertible; it is only in the trivial commutative ring that the two definitions differ. As a result, I have changed the definition of non-invertible element to the usual definition of non-invertible element, since with these edits the trivial commutative ring is no longer relevant to the definition of a field.

DanGrayson commented 2 years ago

Thanks for the contribution!

If you send me your email address, we can send you an invitation to our weekly Zoom meeting.