Q/Z and cyclic subgroups

Stream: Is there code for X?

[Leo Mayer]

I almost have a complete proof that the category of R-modules has enough injectives, and I'm getting stuck on showing that any nontrivial cyclic subgroup of an abelian group admits a nonzero map to Q/Z. Two specific questions I have are:

• Is there API for Q/Z? Including, for example, "the order of p/q is q"? I've been using an ad-hoc Q/Z, which I doubt is ideal
• Is there an easy way to work with cyclic subgroups? Something like the map determined by sending your generator to an element with an appropriate order.

Here's some of my scratchwork.

import Mathlib.Tactic
import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.GroupTheory.QuotientGroup
import Mathlib.GroupTheory.OrderOfElement

def ZinQ : AddSubgroup ℚ where
carrier := Set.image (Int.castAddHom ℚ) ⊤
add_mem' := by rintro a b ⟨a, -, rfl⟩ ⟨b, -, rfl⟩; use a + b; simp
zero_mem' := by use 0; simp
neg_mem' := by rintro a ⟨a, -, rfl⟩; use -a; simp

def QmodZ := ℚ ⧸ ZinQ

variable (M : Type) [AddCommGroup M] (m : M)

noncomputable def φ : AddSubgroup.zmultiples m →+ ℚ ⧸ ZinQ where
  toFun := fun ⟨x, hx⟩ => by
    let n := Exists.choose hx
    have hn : n•m = x := Exists.choose_spec hx
    by_cases h : IsOfFinAddOrder m
    . exact QuotientAddGroup.mk' ZinQ ((n : ℚ) / addOrderOf m)
    . exact QuotientAddGroup.mk' ZinQ ((n : ℚ) / 2)
  map_zero' := by
    by_cases h : IsOfFinAddOrder m <;> simp [h]
    . sorry
    . sorry
  map_add' := sorry

[Yaël Dillies]

QmodZ is just AddCircle (1 : Rat). You'll find more API that way.

[Julian Külshammer]

There is some API about cyclic groups in GroupTheory.SpecificGroups.Cyclic

[Leo Mayer]

Thanks for pointing out AddCircle!
I looked through GroupTheory.SpecificGroups.Cyclic, but there isn't anything about mapping out of it. I think for this specific application, I guess it would have to belong to the AddSubgroup.zmultiples API, since the map depends on the specific generator.

Here's a cleaner (and sorry free) version of what I'm looking for.

variables [AddCommGroup A] [AddCommGroup B] {a : A} {b : B}

noncomputable def lift_val (x : AddSubgroup.zmultiples a) : ℤ := Exists.choose x.2
lemma smul_lift_val_eq {x : AddSubgroup.zmultiples a} : (lift_val x) • a = x := Exists.choose_spec x.2

noncomputable def φ (hab : addOrderOf b ∣ addOrderOf a) : AddSubgroup.zmultiples a →+ B where
  toFun := fun x => lift_val x • b
  map_zero' := by
    show lift_val 0 • b = 0
    rw [← addOrderOf_dvd_iff_zsmul_eq_zero]
    have H : (addOrderOf a : ℤ) ∣ lift_val (0 : AddSubgroup.zmultiples a)
    . rw [addOrderOf_dvd_iff_zsmul_eq_zero]
      exact smul_lift_val_eq
    apply dvd_trans
    . show (addOrderOf b : ℤ) ∣ addOrderOf a
      norm_cast
    . exact H
  map_add' x y := by
    show lift_val (x + y) • b = lift_val x • b + lift_val y • b
    suffices (addOrderOf b : ℤ) ∣ lift_val (x + y) - lift_val x - lift_val y by
      rw [addOrderOf_dvd_iff_zsmul_eq_zero, sub_smul, sub_smul] at this
      rw [sub_eq_zero, sub_eq_iff_eq_add, add_comm (_ • _)] at this
      exact this
    suffices (lift_val (x + y) - lift_val x - lift_val y) • a = 0 by
      rw [← addOrderOf_dvd_iff_zsmul_eq_zero] at this
      apply dvd_trans
      . show (addOrderOf b : ℤ) ∣ addOrderOf a
        norm_cast
      exact this
    simp [sub_smul, smul_lift_val_eq]

Is this worth adding to mathlib if it isn't already there in some form?