mathlib

mathlib copied to clipboard

Since injective groups are divisible and vice versa, we show AddCommGroup has enough "divisibles": for any group $A$, we embed $A$ into $\prod_{f : A \to \mathbb{Q}/\mathbb{Z}} \mathbb{Q}/\mathbb{Z}$, since $\mathbb{Q}/\mathbb{Z}$ is divisible, we just it to show $A \to \prod_{f : A \to \mathbb{Q}/\mathbb{Z}} \mathbb{Q}/\mathbb{Z}$ is injective. It turns out this boils down to show that for any nonzero $a\in A$, there exists some $\mathbb{Z}$-linear map $\langle a\rangle \to \mathbb{Q}/\mathbb{Z}$ such that $f a \ne 0$. This PR shows that this is true when $a$ has infinite order. For $a$ with finite order, the proof is in #16115

---

Please choose a different name for this PR. Because you only actually show that AddCommGroup has enough injectives in a follow-up PR, right?

Please choose a different name for this PR. Because you only actually show that AddCommGroup has enough injectives in a follow-up PR, right?

I have changed the title.

The build seems to be failing

The build seems to be failing

It fails at hensel file that I didn’t touch.

It fails at hensel file that I didn’t touch.

You should still try to fix it or else it won't come up on the queue, and the PR is unlikely to be merged if the error persists. Somethings you can try are

• Rerunning CI
• Merging master to see if it is already squeezed
• Squeezing the file yourself
• Asking on Zulip for someone who knows the file better to squeeze the file

A lot of this file doesn't follow the naming conventions. I encourage you to take a step back and look at which parts of this PR could be reusable apart from what your current goal is. After identifying those pieces, give them a proper name and place in mathlib.

I still see a lot of local notation and things like that. Of course that helps making this current file readable. But will it also create a usable API outside of this file? Or will everything become very hard to read, because now the local notation is not available? I expect so. Hence I think it is better to create definitions instead of relying on local notation. Please take a step back from this PR, and look at it from a global-library-design point of view.