The discrete field of rational numbers

[malarbol]

The main goal of this pull request is to introduce the discrete field structure on the rational numbers. In order to do so, we introduce a few basic results in elementary number theory and ring theory.

Elementary number theory

• strict inequality on the rational numbers is invariant by translation;
• the multiplicative monoid of rational numbers;
• the nonzero rational numbers:
  • standard definition via is-nonzero-ℚ;
  • basic properties;
  • nonzero rational numbers are a multiplicative submonoid;
• the positive integer fractions:
  • fractions with positive numerator;
  • basic properties;
• positive integer fractions are invertible up to the similarity relation;
• the positive rational numbers:
  • rational numbers with positive underlying fractions, or, equivalently, with positive numerator;
  • basic properties and notations;
  • positive rational numbers are an additive subsemigroup;
  • positive rational numbers are a multiplicative submonoid;
  • positive rational numbers are invertible;
• the multiplicative group of positive rational numbers;
• the ring of rational numbers is a division ring;
• the discrete field of the rational numbers;
• the multiplicative group of rational numbers:
  • the group of units of the ring of rational numbers;
  • basic properties and notations.

    Ring theory

• invertible elements of rings are stable under negatives;
• invertible elements of nontrivial rings are nonzero.

[malarbol]

Hey again! Still working towards the field structure on rational numbers. This PR introduces new notations and types for nonzero and positive rational numbers, which will be used to define the inverses. There should be enough do define the commutative multiplicative monoid of (nonzero|positive) rational numbers but I didn't try to reproduce all the properties we wrote for positive etc. integers.

[EgbertRijke]

Hi Malarbol!

Thank you so much for your excellent work recently. It is very nice to have all that new infrastructure for rational numbers. It's great to see that you've been making so much progress on it.

[malarbol]

Hi Malarbol!

Thank you so much for your excellent work recently. It is very nice to have all that new infrastructure for rational numbers. It's great to see that you've been making so much progress on it.

It's a real (pleasure|honor) to contribute to the library. I know my contributions are a bit basic and I hope they don't interfere with your global view of the project.

[EgbertRijke]

Hi Malarbol! Thank you so much for your excellent work recently. It is very nice to have all that new infrastructure for rational numbers. It's great to see that you've been making so much progress on it.

It's a real (pleasure|honor) to contribute to the library. I know my contributions are a bit basic and I hope they don't interfere with your global view of the project.

The most basic contributions are the most impactful. Especially important stuff such as the ring of rational numbers! I can only applaud you for taking on the task of developing this part of the library. It is a big help!

[malarbol]

Hey @malarbol, I hope you're doing well. Thanks for another awesome contribution!

Hey @fredrik-bakke. Thanks for your feedback. It looks like it's time to address your concerns from https://github.com/UniMath/agda-unimath/pull/1100#discussion_r1543590103

I'll go with the mutliplicative-monoid-of-rational-numbers (renaming group-of-rational-numbers to additive-group-of-rational-numbers on the way, as you foresaw) and try to make this cleaner.

[malarbol]

Hello again. Introducing the multiplicative-monoid-of-rational-numbers module lead me to rewrite a bit the "inverse structure" on rational numbers, focusing more on the algebraic structures than the operations. I think it looks quite cleaner this way.

[malarbol]

Thanks for your review and your patience. I suspected that the main challenge of this PR would be to find good names and a good hierarchy between modules, more that about the maths itself. I hope it's not a problem for you; maybe you didn't plan to address these naming issues "right now"?

I'm not 100% convinced about your naming scheme (multiplicative|additive)-[structure]-[carrier-type]. For structures where the operation is neither add nor mul (like elementary-number-theory.monoid-of-natural-numbers-with-maximum, or if the multiplication is the composition of maps, or a convolution product, I think it will be difficult to find good adjectives to extend this scheme.

What do you think of the template [structure]-[op]-[carrier-type], like

• group-add-ℚ;
• monoid-mul-ℚ;
• abelian-group-mul-ℚˣ;
• monoid-max-ℕ;
• etc. Would this conflict with other established notation?

From a user perspective, I think it can also help to have the name of the operator spelled out in the name of object; like if you see abelian-group-mul-ℚ⁺ you know that the operation of the group is mul-ℚ⁺, etc.

[malarbol]

To follow up with my suggestion of [structure]-[op]-[carrier-type], I think it could fit well with the existing name schemes. For exemple, we'd have things like

• type-[Structure] [structure]-[op]-[carrier-type] = [carrier-type]:
  • type-Group group-mul-ℚ⁺ = ℚ⁺;
  • type-Monoid monoid-mul-ℚ = ℚ;
  • etc.
• [structure-op]-[Structure] [structure]-[op]-[carrier-type] = [op]-[carrier-type]
  • mul-Group group-add-ℚ = add-ℚ;
  • add-Ab abelian-group-mul-ℚ⁺ = mul-ℚ⁺;
  • etc.

[fredrik-bakke]

Thanks for your review and your patience. I suspected that the main challenge of this PR would be to find good names and a good hierarchy between modules, more that about the maths itself. I hope it's not a problem for you; maybe you didn't plan to address these naming issues "right now"?

I'm not 100% convinced about your naming scheme (multiplicative|additive)-[structure]-[carrier-type]. For structures where the operation is neither add nor mul (like elementary-number-theory.monoid-of-natural-numbers-with-maximum, or if the multiplication is the composition of maps, or a convolution product, I think it will be difficult to find good adjectives to extend this scheme.

What do you think of the template [structure]-[op]-[carrier-type], like

• group-add-ℚ;
• monoid-mul-ℚ;
• abelian-group-mul-ℚˣ;
• monoid-max-ℕ;
• etc. Would this conflict with other established notation?

From a user perspective, I think it can also help to have the name of the operator spelled out in the name of object; like if you see abelian-group-mul-ℚ⁺ you know that the operation of the group is mul-ℚ⁺, etc.

Ah, indeed your suggestion seems to extend better than what I have suggested!

[malarbol]

Ah, indeed your suggestion seems to extend better than what I have suggested!

I'll try this name scheme for these modules. If it's convincing enough we can extend it to the rest of the elementary-number-theory module (rename Z-Group, monoid-ℕ-Max, etc.) in a separate PR.

[fredrik-bakke]

Ah, indeed your suggestion seems to extend better than what I have suggested!

I'll try this name scheme for these modules. If it's convincing enough we can extend it to the rest of the elementary-number-theory module (rename Z-Group, monoid-ℕ-Max, etc.) in a separate PR.

Yeah, that sounds good!

[malarbol]

This new name scheme looks pretty good to me. Let's see how you like it.

[malarbol]

Your work looks excellent! I have only some very minor comments. Let's merge this PR after they have been resolved :)

Thanks! If you're satisfied with the new names, could you resolve the conversations you opened, or do you want me to do it?

Maybe we should add some more ## See also to cross-reference between the modules? You can make me a short list of which module should point where and I'll do it; or you can add them directly if you want. (or maybe it's ok for you as it is?)