Structure of `(ZMod n)ˣ`

Stream: Is there code for X?

[Snir Broshi]

Is there code that shows how (ZMod n)ˣ decomposes into a product of ZMods?
https://en.wikipedia.org/wiki/Multiplicative_group_of_integers_modulo_n#Structure
More specifically I'm looking for when that group is cyclic (iff n is 1, 2, 4, p^k, 2*p^k for odd primes p).

[Thomas Browning]

Yup! docs#ZMod.isCyclic_units_iff

[Snir Broshi]

Thanks! I kinda expected the proof to decompose it into ZMods but I'm not seeing that, does it exist?

[Thomas Browning]

You can get that from the Chinese remainder theorem ring isomorphism and docs#Units.mapEquiv

[Snir Broshi]

Thomas Browning said:

You can get that from the Chinese remainder theorem ring isomorphism and docs#Units.mapEquiv

Yes but that only decomposes ZMod units to ZMod units and not to ZMods.
With CRT and the odd prime powers being cyclic we're almost done, the only thing missing is (ZMod (2 ^ n))ˣ ≃* ZMod 2 × ZMod (2 ^ (n - 2)) for 3 ≤ n.

[Junyan Xu]

The proof just shows (ZMod 8)ˣ is not cyclic because every element has order at most 2, and then all higher (ZMod (2 ^ n))ˣ are not cyclic because they have (ZMod 8)ˣ as a quotient. To get the isomorphism you want we need the splitting lemma which seems to be missing in mathlib (I could only find a LinearEquiv version docs#lequivProdOfLeftSplitExact, not MulEquiv).

[Aaron Liu]

we have

• docs#CategoryTheory.ShortComplex.Splitting.ofExactOfRetraction
• docs#CategoryTheory.ShortComplex.Splitting.ofExactOfSection
• docs#CategoryTheory.ShortComplex.Splitting.ofHasBinaryBiproduct
• docs#CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct

[Aaron Liu]

I think that's most of the splitting lemma I'm too lazy to find the rest unless you really need it

[Snir Broshi]

I think I can prove orderOf (3 : (ZMod (2 ^ n))ˣ) = 2 ^ (n - 2) for 4 ≤ n by a simple induction.
I think this shows that ZMod (2 ^ (n - 2)) must be a subgroup, and together with the fact that (ZMod (2 ^ n))ˣ isn't cyclic will that finish the proof without the splitting lemma?

[Junyan Xu]

I don't think category theory is the way to go.
We already have ZMod.orderOf_five, what proof do you want to finish? (The 5 is in ZMod (2^(n+2)), and this is nicer since it also holds for n=0,1.)
Actually docs#lequivProdOfLeftSplitExact is applicable here, since abelian groups are Z-modules ...
It seems we're also missing that the supremum (Max.max) of two disjoint submodules/subgroups is isomorphic to their product ...

[Snir Broshi]

Junyan Xu said:

We already have ZMod.orderOf_five, what proof do you want to finish? (The 5 is in ZMod (2^(n+2)), and this is nicer since it also holds for n=0,1.)

I'm really not sure what the point of this 5 theorem is. It's talking about addition, not multiplication, the statement is orderOf (5 : ZMod (2 ^ (n + 2))) = 2 ^ n. How does it help? it looks trivial to me
Apparently there's docs#addOrderOf, and the lack of the units symbol in docs#ZMod.orderOf_five doesn't make it about multiplication, so it is what we need

[Junyan Xu]

You mean "doesn't make it about addition" :) Yeah the lack of the units symbol means we consider the order in the multiplicative monoid, and taking units is essentially passing to a submonoid and doesn't affect the result.

[Kevin Buzzard]

Snir Broshi said:

I think I can prove orderOf (3 : (ZMod (2 ^ n))ˣ) = 2 ^ (n - 2) for 4 ≤ n by a simple induction.
I think this shows that ZMod (2 ^ (n - 2)) must be a subgroup, and together with the fact that (ZMod (2 ^ n))ˣ isn't cyclic will that finish the proof without the splitting lemma?

Slightly more optimal is that the order of 5 mod 2^n is 2^(n-2) as this works for all n>=2 (same induction proof). The reason you want to prove this is that you can then deduce that for n>=2 you have (Z/2^nZ)^* is +-1 x (1 mod 4) (obvious) and (1 mod 4) is cyclic because you just wrote down an element of the order of this subgroup.