closure of element of infinite order

Stream: Is there code for X?

[Joachim Breitner]

If I have a group element with infinite order (order_of a = 0), where would I find lemmas about subgroup.closure {a}? In particular that it is isomorphic to Z?

[Kyle Miller]

The only relevant theorem I've found is docs#subgroup.mem_closure_singleton

[Joachim Breitner]

Looks like I need to do some yak-shaving :-D

[Yaël Dillies]

The mathlib community truly in need of a :yak: emoji.

[Eric Rodriguez]

I had never heard of yak-shaving before, it is very relatable!

[Kyle Miller]

This wasn't my yak to shave, but I needed a little break from grading final exams:

import group_theory.subgroup.basic
import group_theory.order_of_element

variables {G : Type*} [group G] (x : G)

lemma zpow_inj_iff_of_order_of_eq_zero (h : order_of x = 0) {n m : ℤ} :
  x ^ n = x ^ m ↔ n = m :=
begin
  cases n; cases m;
  simp [pow_inj_iff_of_order_of_eq_zero, h],
  sorry,
  sorry,
end

noncomputable
def inf_cyclic (h : order_of x = 0) :
  multiplicative ℤ ≃* subgroup.closure ({x} : set G) :=
{ to_fun := λ n, ⟨x ^ n.to_add, begin rw subgroup.mem_closure_singleton, use n, refl, end⟩,
  inv_fun := λ x, (subgroup.mem_closure_singleton.mp x.2).some,
  left_inv := begin
    intro n,
    simp,
    generalize_proofs h',
    have h' := h'.some_spec,
    simp only at h',
    rwa zpow_inj_iff_of_order_of_eq_zero _ h at h',
  end,
  right_inv := begin
    rintro ⟨x, hx⟩,
    simp,
    generalize_proofs h',
    exact h'.some_spec,
  end,
  map_mul' := begin
    intros m n,
    simp [zpow_add],
  end }

[Reid Barton]

For your first lemma surely there should already be something about x^m = x^n <-> order_of x \| m - n?

[Eric Rodriguez]

docs#pow_eq_pow_iff_modeq I think is the closest nope

[Floris van Doorn]

docs#zpow_eq_mod_order_of is pretty close, it's for zpow.

[Eric Rodriguez]

docs#pow_inj_iff_of_order_of_eq_zero seems the closest, but needs generalising to zpow

[Reid Barton]

Why are there like a dozen lemmas about "finite cancellative monoids"? Isn't there a better-known name for these objects?

[Reid Barton]

Anyways it looks to me like docs#order_of_dvd_iff_zpow_eq_one is on the right track

[Eric Rodriguez]

Reid Barton said:

Why are there like a dozen lemmas about "finite cancellative monoids"? Isn't there a better-known name for these objects?

funnily enough we have docs#fintype.group_with_zero_of_cancel but I don't think we have it for just normal groups

[Eric Rodriguez]

there's even a todo above docs#exists_pow_eq_one

[Eric Wieser]

Is it helpful to show that closure {a} = subgroup.powers a and state the lemma in terms of docs#subgroup.powers?