-
Notifications
You must be signed in to change notification settings - Fork 82
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
base: master
Are you sure you want to change the base?
Hom-ring, ℤ, ℚ, etc. #1452
Conversation
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. |
This should fill most of the blanks of #1451. |
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. |
src/elementary-number-theory/rational-ring-of-rational-numbers.lagda.md
Outdated
Show resolved
Hide resolved
Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
This PR aims to fill some gaps in ring-theoretical relations between ℤ and ℚ:
rational-ℤ
is the initial ring homomorphismℤ → ℚ
;ℤ⁺
are invertible inℚ
;ℚ → R
inverts positive integers;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:ι : ℤ → R
into a rational ring extends to a mapℚ → R
byγ : p/q ↦ (ι p)(ι q)⁻¹
;f : ℚ → R
is rational andf
is homotopic toγ
;ℚ → R
are equal;ℚ → R
.the rational ring of rational numbers:
ℚ
is a rational ring;γ : 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