Zulip Chat Archive

Stream: Is there code for X?

Topic: Subgroups of the integers


view this post on Zulip Heather Macbeth (Sep 29 2020 at 15:59):

Does mathlib have the classification of subgroups of Z\mathbb{Z}?

example (H : add_subgroup ) :  (a : ), H = add_subgroup.closure {a}

view this post on Zulip Kevin Buzzard (Sep 29 2020 at 18:41):

I guess this could be proved for all subgroups of a cyclic group. And for all add_subgroups of an add_cyclic group...

view this post on Zulip Heather Macbeth (Sep 29 2020 at 18:44):

It can be generalised in several different directions (in addition to the direction you mention), the version I and Patrick currently have is:

import algebra.archimedean
import group_theory.subgroup

variables {G : Type*} [decidable_linear_ordered_add_comm_group G] [archimedean G]

lemma subgroup_cyclic_of_min {H : add_subgroup G} {a : G}
  (ha : is_least {g : G | g  H  0 < g} a) : H = add_subgroup.closure {a} :=

view this post on Zulip Heather Macbeth (Sep 29 2020 at 18:46):

and Patrick also pointed out to me that it follows from the fact that subgroups of Z\mathbb{Z} are ideals, via
docs#euclidean_domain.to_principal_ideal_domain
docs#int.euclidean_domain

view this post on Zulip Heather Macbeth (Sep 29 2020 at 18:46):

But is it possible that none of these versions are currently in mathlib? :)

view this post on Zulip Heather Macbeth (Sep 29 2020 at 19:14):

Kevin Buzzard said:

I guess this could be proved for all subgroups of a cyclic group. And for all add_subgroups of an add_cyclic group...

For the benefit of future readers -- this is docs#subgroup.is_cyclic

view this post on Zulip Kevin Buzzard (Sep 29 2020 at 19:17):

Is this only for multiplicative groups?

view this post on Zulip Heather Macbeth (Sep 29 2020 at 19:19):

Is there no @[to_additive] for that lemma? Oh no!

view this post on Zulip Heather Macbeth (Oct 02 2020 at 04:18):

now PR'd as docs#int.subgroup_cyclic


Last updated: May 07 2021 at 22:14 UTC