-
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. |
This overlaps a bit with #1451 so if this gets merged, @djspacewhale could be credited in this PR. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Very nice work!
src/elementary-number-theory/unit-fractions-rational-numbers.lagda.md
Outdated
Show resolved
Hide resolved
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 |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
see cfa7266
There was a problem hiding this comment.
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
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
see 6a4ccd0 current version
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 |
Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
…agda.md Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
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. |
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