Add Field to Cubical.Algebra

[m-yac]

In the style of Ring, etc. from #284. I think it would be good to have this so we could show ℚ is a field.

[mortberg]

I agree. Note that there are some subtleties in how to define fields in constructive algebra

[felixwellen]

In constructive algebra, it is most common to call a commutative ring, where all non-zero elements have an inverse, a field. So I vote for using this definition. It also 'agrees' with the classical notion for rings with decidable equality.

[felixwellen]

I'm mostly done with this one. It is on top of my current PR on quotient rings, but I could move it, if that's good for anything.
So what I'm doing exactly is:

• Define isField for a CommRing (done)
• Show that isField is a prop (almost)
• Use that to show that isomorphic fields (that means they are isomorphic as rings) are equal (not done).

[martinescardo]

But in constructive algebra "non-zero" should mean "apart from zero" rather than "different from zero" in the definition of field. So fields should include an apartness relation as part of its axiomatics. Then I wonder if the isomorphisms should be "extensional", that is, reflect the apartness relation, for the SIP to apply.

[martinescardo]

Or is any isomorphism automatically extensional in this sense?

[felixwellen]

I would call a commutative ring where 'a apart from b' implies that a-b is a unit, a Heyting Field, but I'm really not an expert on (current) names in constructive algebra. We could have that as a second notion of field which comes with an apartness relation.
And I could rename the definition of 'field' with the denial inequality to 'denial field', since that is really a special case of what is usually called 'field' which comes with a more general inequality (I'm using the definitions of Mines and his coauthors of the '88 book A course in constructive algebra - I don't know of they are outdated).

[mortberg]

I think it makes sense to follow to the Mines-Richman-Ruitenburg as much as possible for terminology. It would also be good to check what Lombardi-Quitté use in https://www.springer.com/gp/book/9789401799430

I like the name "apartness field" for fields where the axiom is expressed using apartness.

[mortberg]

There was a discussion over at UniMath about this some years ago: UniMath/UniMath#254

[felixwellen]

Thanks for the pointer, I'll read that. I also like the name "apartness field".

[felixwellen]

I forget to exclude the zero ring in #325 ...
I plan to add as a condition, that 0 and 1 should not be equal.

[guillaumebrunerie]

Did you just find the field with one element? 😄

[felixwellen]

Yes, there was a one element field a commit ago ;)
Not a good one though.

[felixwellen]

Ohno. I just learned I was wrong about fixing that. In the book of Mines et al. and Lombardi/Quitté, the zero ring is a field. I guess we should just go with that, even if its wierd from a classical commutative algebra background.
Also, in a 'DenialField' the zero ideal {0} should be prime, which I'll fix next in #325 .

[felixwellen]

There is a PR on this #325, which is now closed, because the contents were too far away from the current library code. The discussions might still be useful when defining Fields.

[felixwellen]

I have merged #797 which contains a basic definition of field, which can be extended if there is demand.