Hom-ring, ℤ, ℚ, etc.

[malarbol]

This PR aims to fill some gaps in ring-theoretical relations between ℤ and ℚ:

• rational-ℤ is the initial ring homomorphism ℤ → ℚ;
• elements of ℤ⁺ are invertible in ℚ;
• any ring homomorphism ℚ → R inverts positive integers;
• misc. elementary algebraic properties;

We also introduce the concepts:

• rational rings R such that the image of ℤ⁺ by the initial ring homomorphism ℤ → R consists of invertible elements; with the following results:

  • the initial ring homomorphism ι : ℤ → R into a rational ring extends to a map ℚ → R by
    γ : p/q ↦ (ι p)(ι q)⁻¹;
  • any ring that admits a ring homomorphism f : ℚ → R is rational and f is homotopic to γ;
  • all ring homomorphisms ℚ → R are equal;
  • a ring is rational if and only if there exists some ring homomorphism ℚ → R.

• the rational ring of rational numbers:

  • ℚ is a rational ring;
  • the rational extension γ : p/q ↦ (ι p)(ι q)⁻¹ of the initial ring homomorphism ι : ℤ → R into a rational ring is a ring homomorphism ℚ → R ;
  • ℚ is the initial rational ring;
  • ℚ is the localization of ℤ at ℤ⁺.

• rational modules: Abelian groups whose ring of endomorphisms are rational. It is equivalent to the type of left/right modules over the ring of rational numbers.

Co-authored-by: Garrett Figueroa garrett.figueroa@gmail.com

[malarbol]

I still have a few more ideas that I think could be useful for #1451. If @djspacewhale wants to join in / take anything interesting, they are welcome.

[malarbol]

This should fill most of the blanks of #1451.
Independently, I think I introduces some interesting results (unity of ring homomorphisms ℚ → R, unicity of left rational module structure, etc.) which could also be useful for #1435 (rational rings are good candidates to define the exponential series, maybe even without convergence nor commutativity).

[malarbol]

This overlaps a bit with #1451 so if this gets merged, @djspacewhale could be credited in this PR.
I keep getting new ideas but this is already quite big so I think I'll stop here.

[fredrik-bakke]

Very nice work!

[fredrik-bakke]

Please add an explanation for what a rational ring is so the reader does not have to go on a goose chase to get to the definition.

[malarbol]

see cfa7266

[fredrik-bakke]

A lot of this file is about initiality of the rational ring of rationals. Could this be factored into a new file elementary-number-theory.rational-ring-of-rational-numbers? Please also add a "see also" link from ring-of-rational-numbers to rational-ring-of-rational-numbers

[malarbol]

see 6a4ccd0 current version

[fredrik-bakke]

This overlaps a bit with #1451 so if this gets merged, @djspacewhale could be credited in this PR. I keep getting new ideas but this is already quite big so I think I'll stop here.

See here for how to add a co-author: https://docs.github.com/en/pull-requests/committing-changes-to-your-project/creating-and-editing-commits/creating-a-commit-with-multiple-authors
You can add the relevant line to your main pull request message.

[malarbol]

This overlaps a bit with #1451 so if this gets merged, @djspacewhale could be credited in this PR. I keep getting new ideas but this is already quite big so I think I'll stop here.

See here for how to add a co-author: https://docs.github.com/en/pull-requests/committing-changes-to-your-project/creating-and-editing-commits/creating-a-commit-with-multiple-authors You can add the relevant line to your main pull request message.

Do you mean like I did in the main message of the PR? You'll be the one eventually merging this and I'm not sure how the commit message will be handled.