Subgroup of all roots of unity

Stream: Is there code for X?

[Yakov Pechersky]

I am working on the proof (via Hensel's lemma) that Z_p has p - 1 roots of unity. That can be stated as HasEnoughRootsOfUnity ℤ_[p] (p - 1) and also as rootsOfUnity (p - 1) ℤ_[p] ≃* (ZMod p)ˣ.

In fact, there only p - 1 roots of unity for p != 2. I'd like to say something like allRootsOfUnity ℤ_[p] ≃* (ZMod p)ˣ. Do we have something like an allRootsOfUnity subgroup?

[Aaron Liu]

that would be CommGroup.torsion (ZMod p)ˣ

[Kevin Buzzard]

For p=2 the roots of unity are canonically $(\Z/p^2\Z)^\times.$

[Aaron Liu]

I think I saw something saying that in an arbitrary field F all nonzero elements are roots of unity iff F has positive characteristic and is algebraic over its prime subfield

[Aaron Liu]

Aaron Liu said:

https://math.stackexchange.com/q/4193256

[Kevin Buzzard]

That's true, but this is about p-adic integers which aren't a field

[Aaron Liu]

why is it called p if it's not prime

[Aaron Liu]

why would you do this to me

[Aaron Liu]

oh

[Aaron Liu]

I get it now

[Aaron Liu]

I misread sorry

[Aaron Liu]

this is what happens when you don't do algebra all day

[Yakov Pechersky]

Do we have anything that links CommGroup.torsion with the product of rootsOfUnity?

[Aaron Liu]

probably not

[Aaron Liu]

do we have an additive version of rootsOfUnity

[Yakov Pechersky]

I think I need to understand torsion better. In the meantime, I'll show that CommGroup.torsion ℤ_[p]ˣ = rootsOfUnity (p - 1) ℤ_[p].

[Yakov Pechersky]

(Again, for p != 2)

[Aaron Liu]

working with torsion recently has been confusing I think because it was being refactored

[Scott Carnahan]

Do we (eventually) want a statement using Witt vectors, e.g., mu(W(k)) always embeds in mu(W_2(k)) and surjects to mu(W_1(k))?

[Violeta Hernández]

$\mathbb Z_p$ for the p-adic integers and for GF(p) is one of the worst notation clashes in mathematics

[Adam Topaz]

I think we eventually also want the analogous assertion in $\mathcal{O}_K$ for any p-adic field $K$. Namely, that the projection $\mathcal{O}_K^\times \to k^\times$ splits where $k$ is the residue field. (@Dagur Asgeirsson and I were discussing this just yesterday!)

[Yakov Pechersky]

There are two ways to do this, it seems. To prove surjectivity, one either needs to apply hensels lemma (do we have that such fields are henselian?), or by the construction of a root of unity by taking the limit of the Cauchy sequence iteratively applying x^p.

[Yakov Pechersky]

I have it all done for Z_p, just need to PR it...

[Adam Topaz]

Yakov Pechersky said:

do we have that such fields are henselian?

I think so? It should be essentially this IsAdicComplete.henselianRing

[Adam Topaz]

Well, I guess that depends on how you define "p-adic field", but I think @Andrew Yang et al. formalized that whatever definition they settled on implies adic completeness?

[Andrew Yang]

If you are talking about the local field definition, we only showed that it is docs#CompleteSpace (as a metric space) but not yet that it docs#IsAdicComplete

[Adam Topaz]

Aha, okay.

[Kevin Buzzard]

Adam Topaz said:

I think we eventually also want the analogous assertion in $\mathcal{O}_K$ for any p-adic field $K$.

Surely it's at least true for all nonarch local fields, and maybe even for any field complete wrt a nontrivial nonarch norm or something like that?

[Yakov Pechersky]

Just the Z_p p-1 case handled here: #29425. The general case would follow a similar argument. Would need more API work to prepare the general statement, so I thought to get this one on the review queue for now.

[Yakov Pechersky]

#29517 for

lemma torsion_eq_biSup_rootsOfUnity :
    CommGroup.torsion Mˣ = ⨆ (n : ℕ) (_hn : n ≠ 0), rootsOfUnity n M := by