Skip to content

Hom-ring, ℤ, ℚ, etc. #1452

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 49 commits into
base: master
Choose a base branch
from
Open

Conversation

malarbol
Copy link
Collaborator

@malarbol malarbol commented Jul 12, 2025

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
Copy link
Collaborator Author

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 malarbol marked this pull request as draft July 14, 2025 20:55
@malarbol malarbol marked this pull request as ready for review July 15, 2025 23:52
@malarbol
Copy link
Collaborator Author

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
Copy link
Collaborator Author

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.

Copy link
Collaborator

@fredrik-bakke fredrik-bakke left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very nice work!

A {{#concept "rational module" Agda=Rational-Module}} is an
[Abelian group](group-theory.abelian-groups.md) whose
[ring of endomorphisms](group-theory.endomorphism-rings-abelian-groups.md) is
[rational](ring-theory.rational-rings.md). The type of **rational modules** is
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

see cfa7266

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

@malarbol malarbol Jul 20, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

see 6a4ccd0 current version

@fredrik-bakke
Copy link
Collaborator

fredrik-bakke commented Jul 20, 2025

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 malarbol requested a review from fredrik-bakke July 22, 2025 19:08
@malarbol
Copy link
Collaborator Author

malarbol commented Jul 22, 2025

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants