Rational abelian groups #1451
Rational abelian groups #1451
Conversation
merging nix upgrade to 2.7.0; faster typechecking for all
merging no-postfix-projections PR into branches
merging upstream commits
merging upstream commits
merging upstream commits
pulling up to date
merging upstream
merging upstream
…he cavalry for the last few goals
|
This PR is clearly not ready yet. There are holes in elementary-number-theory/field-of-rational-numbers, group-theory/monomorphisms-groups and group-theory/rational-abelian-groups, dealing with path algebra and universe level stuff. I have some stamina yet, but am asking if any other contributors have capacity to take a swing at these last few holes. Edits for better hygiene are welcome too, though their necessity I leave to the maintainers (?). |
|
With regards to style conventions these are required. You can find documentation on the website, e.g. https://unimath.github.io/agda-unimath/CODINGSTYLE.html, and they are partially enforced by the CI. During the review process we will point out any additional issues and suggest solutions. Don't hesitate to ask If you have particular questions about the conventions! |
fredrik-bakke
added
group-theory
ring-theory
elementary-number-theory
and removed
ring-theory
labels
A rational abelian group is an abelian group that is both divisible and torsion-free. These are special among the abelian groups as they are precisely the left modules over the ring of rational numbers. This pull builds infrastructure for formalizing the theory of rational abelian groups, with eyes towards rational homotopy theory and commutative algebra.