Two cyclic groups of the same order are isomorphic

Stream: Is there code for X?

[Michael Stoll]

I'm looking for something like this:

example {G G' : Type u} [Group G] [Group G'] [Finite G] [Finite G'] [IsCyclic G] [IsCyclic G']
    (h : Nat.card G = Nat.card G') :
    G ≃* G' := ...

but I can't seem to find anything similar.

[Michael Stoll]

@loogle IsCyclic, MulEquiv

[loogle]

:shrug: nothing found

[Yaël Dillies]

We don't have it.

[Michael Stoll]

But we should ...

[Yaël Dillies]

Also surely you don't need the finiteness assumptions?

[Michael Stoll]

Right.

[Michael Stoll]

What would be a reasonable way to do this?

[Michael Stoll]

@loogle IsCyclic, MulHom

[loogle]

:shrug: nothing found

[Yaël Dillies]

Get a generator for each group, map one to the other, extend to a hom. I don't know how to do that last step.

[Michael Stoll]

My feeling is that this is going to be ugly, but I don't have a better idea.

[Yaël Dillies]

At worse, you can do it by hand using the choose tactic on the ∀ x, x ∈ zpowers g assumption.

[Michael Stoll]

BTW, why is loogle not finding docs#MonoidHom.map_cyclic ?

[Yaël Dillies]

@loogle IsCyclic, MonoidHom

[loogle]

:search: commGroupOfCycleCenterQuotient, commutative_of_cyclic_center_quotient, and 2 more

[Yaël Dillies]

It does :tada:

[Michael Stoll]

Would be nice if it would know that a MonoidHom is also a MulHom...

[Yaël Dillies]

Probably not, as it would result in a lot of noise from all the stronger structures than the one you're looking for (and arguably sometimes you would instead like Loogle to know that if it can get you a MulHom it should return it when you asked for MonoidHom).

[Michael Stoll]

Why does docs#orderOf_eq_card_of_forall_mem_zpowers assume finiteness?

[Michael Stoll]

I guess because it uses docs#Fintype.card and not docs#Nat.card ...

[Michael Stoll]

The more general lemma for docs#Nat.card seems to be missing.

[Yongyi Chen]

I made some theorems related to this a while ago upon finding they were missing. Would a PR be welcome?

[Michael Stoll]

So far, I have this:

import Mathlib

noncomputable
def monoidHomFromGenerator {G G' : Type u} [Group G] [Group G'] {g : G} (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    {g' : G'} (hg' : orderOf g' ∣ orderOf g) :
    G →* G' where
  toFun x := g' ^ (Classical.choose <| Subgroup.mem_zpowers_iff.mp <| hg x)
  map_one' := orderOf_dvd_iff_zpow_eq_one.mp <|
    ((Mathlib.Tactic.Zify.nat_cast_dvd _ _).mp hg').trans <| orderOf_dvd_iff_zpow_eq_one.mpr <|
    Classical.choose_spec <| Subgroup.mem_zpowers_iff.mp <| hg 1
  map_mul' x y := by
    simp only [← zpow_add, zpow_eq_zpow_iff_modEq]
    apply Int.ModEq.of_dvd ((Mathlib.Tactic.Zify.nat_cast_dvd _ _).mp hg')
    rw [← zpow_eq_zpow_iff_modEq, zpow_add]
    simp [fun x ↦ Classical.choose_spec <| Subgroup.mem_zpowers_iff.mp <| hg x]

[Michael Stoll]

Yongyi Chen said:

I made some theorems related to this a while ago upon finding they were missing. Would a PR be welcome?

Definitely!

[Yongyi Chen]

Cool! Finally I have something to answer "What would I like to work on" for the github request thread...

[Junyan Xu]

Jujian Zhang made this when showing the category of abelian groups has enough injectives.

@[simps!] noncomputable def equivZModSpanAddOrderOf :
    (ℤ ∙ a) ≃ₗ[ℤ] ℤ ⧸ Ideal.span {(addOrderOf a : ℤ)} :=

we should combine it with something like IsCyclic.equivSpanSingleton which can be constructed via topEquiv and IsCyclic.top_eq_span_singleton.

[Michael Stoll]

(And there should be a multiplicative version.)

[Jireh Loreaux]

I had some work recently where I was trying to make it easier to talk about generator of cyclic groups. I didn't PR it because I ran into an issue with to_additive that I mentioned to @Floris van Doorn privately. I have just pushed the branch#j-loreaux/generator. Probably it would help with the arguments above, but I don't have time to check right now.

[Jireh Loreaux]

The issue with to_additive is that I wanted it to not additivize certain things. For instance, I provided an equiv between the type Group.Generator G of generators of G and (ZMod (Fintype.card G))ˣ, and I wanted it to not try and additivize the second bit.

[Michael Stoll]

It looks like there is some interest in having these results. So maybe the various people who have already produced some code can coordinate?

[Yaël Dillies]

Jireh Loreaux said:

The issue with to_additive is that I wanted it to not additivize certain things. For instance, I provided an equiv between the type Group.Generator G of generators of G and (ZMod (Fintype.card G))ˣ, and I wanted it to not try and additivize the second bit.

This should be fixed by marking ZMod as a "fixed type". I don't think to_additive reasons like this yet but it would be very useful if it did.

[Jireh Loreaux]

Yes, that's the conversation I had with Floris. It seems that this need for fixed types arises in other places as well (e.g., convolutions).

[Yongyi Chen]

This is my code from that while ago, which I edited to allow for infinite cardinality.

import Mathlib

open Group Subgroup AddSubgroup

theorem multiplicative_mod_zpowers_mulEquiv_multiplicative_mod_zmultiples [AddCommGroup G] (g : G) : Multiplicative G ⧸ zpowers (Multiplicative.ofAdd g) ≃* Multiplicative (G ⧸ zmultiples g) := by rfl

theorem zpowersHom_ker_eq [Group G] (g : G) : (zpowersHom G g).ker = zpowers (Multiplicative.ofAdd (orderOf g : ℤ)) := by
  ext n
  rw [MonoidHom.mem_ker, mem_zpowers_iff, zpowersHom_apply, ← orderOf_dvd_iff_zpow_eq_one]
  let m : ℤ := n
  change _ ∣ m ↔ ∃ k, k * (orderOf g : ℤ) = m
  conv in _ * _ = _ => rw [mul_comm, eq_comm]

/-- **Isomorphism from ZMod n to any cyclic group of Nat.card equal to n** -/
noncomputable def multiplicative_zmod_mulEquiv_of_cyclic [Group G] (h : IsCyclic G) : Multiplicative (ZMod (Nat.card G)) ≃* G := by
  let n := Nat.card G
  let ⟨g, f_surj⟩ := Classical.indefiniteDescription _ h.exists_generator
  have f_ker : ((zpowersHom G) g).ker = zpowers (Multiplicative.ofAdd ↑(Nat.card G)) := by
    rw [zpowersHom_ker_eq]
    congr
    rw [← Nat.card_zpowers]
    exact Nat.card_congr (Equiv.subtypeUnivEquiv f_surj)
  exact (Int.quotientZmultiplesNatEquivZMod n).toMultiplicative |>.symm.trans (multiplicative_mod_zpowers_mulEquiv_multiplicative_mod_zmultiples (n : ℤ) |>.symm.trans (QuotientGroup.quotientMulEquivOfEq f_ker |>.symm.trans (QuotientGroup.quotientKerEquivOfSurjective (zpowersHom G g) f_surj)))

theorem mulEquiv_of_cyclic_same_card [Group G] [Group H] (hG : IsCyclic G) (hH : IsCyclic H) (hcard : Nat.card G = Nat.card H) : G ≃* H := hcard ▸ (multiplicative_zmod_mulEquiv_of_cyclic hG).symm |>.trans (multiplicative_zmod_mulEquiv_of_cyclic hH)

theorem mulEquiv_of_same_prime_order [Fintype G] [Fintype H] [Group G] [Group H] [Fact p.Prime] (hG : Fintype.card G = p) (hH : Fintype.card H = p) : G ≃* H := by
  apply mulEquiv_of_cyclic_same_card (isCyclic_of_prime_card hG) (isCyclic_of_prime_card hH)
  rw [← Nat.card_eq_fintype_card] at hG hH
  exact hG.trans hH.symm

[Yongyi Chen]

This would be my first time adding something into Mathlib. I would love suggestions on naming and what files would be appropriate to put this in.

[Junyan Xu]

You can type #find_home zpowersHom_ker_eq etc. to find the appropriate files.
Mind that lots of your lines exceed the 100 character limit ...

[Michael Stoll]

Jireh Loreaux said:

I had some work recently where I was trying to make it easier to talk about generator of cyclic groups. I didn't PR it because I ran into an issue with to_additive that I mentioned to Floris van Doorn privately. I have just pushed the branch#j-loreaux/generator. Probably it would help with the arguments above, but I don't have time to check right now.

This looks quite good to me. I hope the problem with to_additive will be fixed soon...

[Yongyi Chen]

Junyan Xu said:

Mind that lots of your lines exceed the 100 character limit ...

Yep, I did type an egregious line. How strict is the limit? Would this

theorem zpowersHom_ker_eq [Group G] (g : G) : (zpowersHom G g).ker = zpowers (Multiplicative.ofAdd ↑(orderOf g)) := by
  ext n
  rw [MonoidHom.mem_ker, mem_zpowers_iff, zpowersHom_apply, ← orderOf_dvd_iff_zpow_eq_one]
  let m : ℤ := n
  change _ ∣ m ↔ ∃ k, k * (orderOf g : ℤ) = m
  conv in _ * _ = _ => rw [mul_comm, eq_comm]

need the first line broken up since it is 111 characters?

[Michael Stoll]

The linter will complain about any line over 100 characters.

[Yongyi Chen]

Oh, how do I run the linter locally?

[Junyan Xu]

#lint at the bottom of the file

[Michael Stoll]

Does that include the line-length linter? I think it didn't in the Lean3 days.

[Yongyi Chen]

Ah I see. It's not identifying character limit issues -- do I have an incorrect setting?

[Yaël Dillies]

No, those you can find by Ctrl + F .{101} with regex turned on.

[Junyan Xu]

It should complain at least one def/lemma issue ... since the last declaration is def it should be named like mulEquivOfPrimeCardEq

You should check out https://leanprover-community.github.io/contribute/naming.html#general-conventions

[Junyan Xu]

No, those you can find by Ctrl + F .{101} with regex turned on.

If you use VSCode there should be a vertical bar at the 100-char cutoff at the right end. That's usually good enough except in rare cases when the line includes some very special characters (that the monospace font doesn't support, I suppose).

[Mario Carneiro]

unfortunately this trick is not quite as effective as it used to be because #align lines go over the limit

[Mario Carneiro]

although I think you could filter those out in the same regex

[Yongyi Chen]

Made my first pull request! https://github.com/leanprover-community/mathlib4/pull/9038