Infinite cyclic group isomorphic to Z

Stream: Is there code for X?

[Edison Xie]

import Mathlib

noncomputable def infiniteCyclicIsoZ (A : Type*) [AddCommGroup A] [Infinite A] (i : A)
    (h : ∀ x : A, x ∈ AddSubgroup.zmultiples i) : A ≃+ ℤ where
  toFun x := h x|>.choose
  map_add' x y := by
    have := h (x + y) |>.choose_spec.trans (by simp [(h x).choose_spec, (h y).choose_spec] :
      _ = (h x).choose • i + (h y).choose • i)
    rw [← add_smul, ← sub_eq_zero, ← sub_smul, ← addOrderOf_dvd_iff_zsmul_eq_zero,
      Infinite.addOrderOf_eq_zero_of_forall_mem_zmultiples h] at this
    simpa [sub_eq_zero] using this
  invFun m := m • i
  left_inv x := by simp; exact h x|>.choose_spec
  right_inv m := by
    have := h (m • i)|>.choose_spec
    rw [← sub_eq_zero, ← sub_smul, ← addOrderOf_dvd_iff_zsmul_eq_zero,
      Infinite.addOrderOf_eq_zero_of_forall_mem_zmultiples h] at this
    simpa [sub_eq_zero] using this

Do we have this in mathlib?

[Aaron Liu]

you probably want to state that with docs#IsAddCyclic

[Aaron Liu]

you can get an equivalence with ZMod 0 by using docs#zmodAddCyclicAddEquiv and docs#Nat.card_eq_zero_of_infinite

[Yakov Pechersky]

docs#LinearOrderedAddCommGroup.int_orderAddMonoidIso_of_isLeast_pos and other things in that file

[Aaron Liu]

Yakov Pechersky said:

docs#LinearOrderedAddCommGroup.int_orderAddMonoidIso_of_isLeast_pos and other things in that file

It's not ordered

[Yakov Pechersky]

True, but it actually has one by the zpower necessary to hit reach it

[Yakov Pechersky]

And really the hypothesis is that closure {i} = \top

[Aaron Liu]

going from ZMod 0 to Int is surprisingly tricky but I think you can get there with docs#Int.quotientSpanNatEquivZMod, docs#Ideal.span_zero, docs#Ideal.quotEquivOfEq, docs#RingEquiv.quotientBot

[Edison Xie]

def ZModZero : ZMod 0 ≃+ ℤ := AddEquiv.refl _
I found that this would just work

[Aaron Liu]

yeah but that's defeq abuse

[Aaron Liu]

..probably

[Edison Xie]

isn't ZMod 0 literaly defined as Int? :joy:

[Aaron Liu]

yes

[Kenny Lau]

Aaron Liu said:

yeah but that's defeq abuse

what if you state it and use it, so it's no longer defeq abuse but the "canonical map"

[Aaron Liu]

it stops being defeq abuse once you start relying on it

[Kenny Lau]

Aaron Liu said:

you probably want to state that with docs#IsAddCyclic

the key difference here (as Buzzard would likely happily announce to you) is that there are actually two isomorphisms from A to Z, and it depends on the choice of the generator which is i here. If you use IsAddCyclic then you lose the freedom to depend on a generator.

[Aaron Liu]

then add DecidableEq A to make it computable too

[Kenny Lau]

i'm saying that you need to be able to feed in a generator in the input