Finitely generated (additive commutative) groups

Stream: Is there code for X?

[Michael Stoll]

Does Mathlib have a notion of "finitely generated commutative group"?
Looking via loogle for names containing "fin" and "gen" does not turn up anything useful...
(And then I will be looking for the fact that a finitely generated commutative torsion-free group is free...)

[Eric Wieser]

docs#AddGroup.FG is maybe what you want?

[Damiano Testa]

There are a few versions of docs#AddCommGroup.equiv_free_prod_directSum_zmod.

[Kevin Buzzard]

(deleted)

[Riccardo Brasca]

We have docs#Module.basisOfFiniteTypeTorsionFree that mathematically is what you want.

[Riccardo Brasca]

There are various versions of this result, but I think using ℤ-modules is better (we have a reasonable API for free modules).

[Michael Stoll]

Thanks! I'll have a look (but may not have a lot of time before the weekend).

[Michael Stoll]

PS: It did not occur to me to look for "FG"...

[Terence Tao]

I started a publicly editable Google Doc for various mathematical notions that are not always obvious to locate in Mathlib, and added finitely generated groups to the list: https://docs.google.com/spreadsheets/d/1ap8ByJDvXw9c1G629UxRRoag3gTcMpPsRpm3_yCINyo/edit#gid=0 . Any further additions welcome!

[Michael Stoll]

I'm trying to prove that a finitely generated torsion-free additive abelian group is free via docs#AddCommGroup.equiv_free_prod_directSum_zmod (idea: show that the finite part in the decomposition is trivial), but I'm running into the problem that the function e in this statement (which gives the exponents of the prime powers) is not required to take only nonzero values (so that one needs to deal with a potential product of trivial groups). Is this just an oversight, or is there a reason for not requiring positive exponents? (The proof uses docs#Module.equiv_free_prod_directSum, which has the same problem.)

[Brendan Seamas Murphy]

Terence Tao said:

I started a publicly editable Google Doc for various mathematical notions that are not always obvious to locate in Mathlib, and added finitely generated groups to the list: https://docs.google.com/spreadsheets/d/1ap8ByJDvXw9c1G629UxRRoag3gTcMpPsRpm3_yCINyo/edit#gid=0 . Any further additions welcome!

This is a great idea! It might be worth trying to integrate it into mathlib's documentation as somewhere for longevity

[Michael Stoll]

I now have a solution to my problem (see below), but I found that I had to work around missing API lemmas (or at least lemmas I was unable to find) and DTT problems. I wonder if there is a better way (staying within abelian group land)...

import Mathlib.GroupTheory.FiniteAbelian
-- import Mathlib.Algebra.Lie.OfAssociative -- suggested by `#minimize_imports` with `import Mathlib`

lemma AddEquiv.IsTorsionFree {A B : Type*} [AddMonoid A] [AddMonoid B] (h : A ≃+ B)
    (hA : AddMonoid.IsTorsionFree A) : AddMonoid.IsTorsionFree B := by
  unfold AddMonoid.IsTorsionFree at hA ⊢
  contrapose! hA
  obtain ⟨g, hg₀, hg⟩ := hA
  refine ⟨h.symm g, (map_ne_zero_iff (symm h)).mpr hg₀, ?_⟩
  simp only [IsOfFinAddOrder, Function.periodicPts, Function.IsPeriodicPt, Function.IsFixedPt,
    add_left_iterate, add_left_eq_self, Set.mem_setOf_eq] at hg ⊢
  peel hg with n hn
  exact ⟨hn.1, by simpa only [add_zero, map_nsmul, map_zero] using congr_arg h.symm hn.2⟩

lemma AddCommGroup.equiv_free {A : Type*} [AddCommGroup A] [AddGroup.FG A]
    (ht : AddMonoid.IsTorsionFree A) :
    ∃ n, Nonempty (A ≃+ (Fin n →₀ ℤ)) := by
  obtain ⟨n, ι, ftι, p, hp, e, h⟩ := AddCommGroup.equiv_free_prod_directSum_zmod A
  use n
  let φ := h.some
  suffices key : ∀ i : ι, e i = 0
  · have Hu : Unique (DirectSum ι fun i ↦ ZMod (p i ^ e i))
    -- I'd like to rewrite `p i ^ e i` to `1` ussing `key`, but trying that I keep
    -- ending up in DTT hell. So work with an equivalence instead:
    · refine Equiv.unique (?H : _ ≃ DirectSum ι fun _ ↦ ZMod 1)
      -- It should be possible to do that without using `Fintype ι`...
      refine DFinsupp.equivFunOnFintype.trans <| Equiv.trans ?_ DFinsupp.equivFunOnFintype.symm
      simp only
      exact Equiv.piCongrRight fun i ↦ by rw [key, pow_zero]
    exact Nonempty.intro <| φ.trans AddEquiv.prodUnique -- needs `Hu`
  replace ht := φ.IsTorsionFree ht
  contrapose! ht
  simp only [AddMonoid.IsTorsionFree, IsOfFinAddOrder, Function.periodicPts, Function.IsPeriodicPt,
    add_left_iterate, Set.mem_setOf_eq, Prod.forall, Prod.mk_eq_zero, exists_prop, ne_eq]
  push_neg
  classical -- to have `DecidableEq ι`
  obtain ⟨i, hi⟩ := ht
  refine ⟨0, DFinsupp.single i 1, ⟨fun _ H ↦ ?_, ⟨p i ^ e i, pow_pos (hp i).pos _, ?_⟩⟩⟩
  · apply_fun (· i) at H
    simp only [DFinsupp.single_apply, ↓reduceDite, DirectSum.zero_apply] at H
    rw [eq_comm, subsingleton_iff_zero_eq_one, ZMod.subsingleton_iff] at H
    exact (hp i).ne_one <| (pow_eq_one_iff hi).mp H
  · -- in the line below, `simp` in place of `rw` gives
    -- failed to synthesize
    -- NoZeroSMulDivisors ℕ ((Fin n →₀ ℤ) × DirectSum ι fun i => ZMod (p i ^ e i))
    -- (deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached
    -- (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
    rw [Function.IsFixedPt, Prod.smul_mk, smul_zero, add_zero, Prod.mk_eq_zero]
    refine ⟨rfl, ?_⟩
    rw [← DFinsupp.single_smul, nsmul_eq_mul, mul_one, CharP.cast_eq_zero, DFinsupp.single_zero]

For AddEquiv.IsTorsionFree and similar statements, it would be nice if one could argue "IsTorsionFree is defined purely in terms of the additive monoid structure, so carries over via an AddEquiv". Is there some kind of tactic that can do such things?

[Eric Wieser]

No, there is no such tactic

[Eric Wieser]

Usually the right approach is to introduce lemmas at every level

[Eric Wieser]

Here's a golfed version:

lemma addOrderOf_dvd_addOrderOf_of_injective
    {A B : Type*} [AddMonoid A] [AddMonoid B]
    (f : A →+ B) (hf : Function.Injective f) (a : A) :
    addOrderOf a ∣ addOrderOf (f a) :=
  addOrderOf_dvd_of_nsmul_eq_zero <| hf <| (map_nsmul _ _ _).trans <| (addOrderOf_nsmul_eq_zero _).trans (map_zero _).symm

lemma AddEquiv.IsTorsionFree {A B : Type*} [AddMonoid A] [AddMonoid B] (e : A ≃+ B)
    (hA : AddMonoid.IsTorsionFree A) : AddMonoid.IsTorsionFree B :=
  e.surjective.forall.2 <| fun x hx h' =>
    hA x ((map_ne_zero_iff e).mp hx) <| h'.mono <| addOrderOf_dvd_addOrderOf_of_injective e e.injective _

[Eric Wieser]

There's a missing lemma about IsOfFinAddOrder there too

[Eric Wieser]

One reason that you should expect to write these lemmas is that many properties require only injectivity or surjectivity, and not a full bijection

[Eric Wieser]

So even if the tactic you ask for did exist, it would often be preferable to avoid it

[Antoine Chambert-Loir]

(deleted)

[Antoine Chambert-Loir]

Michael Stoll said:

I'm trying to prove that a finitely generated torsion-free additive abelian group is free via docs#AddCommGroup.equiv_free_prod_directSum_zmod (idea: show that the finite part in the decomposition is trivial), but I'm running into the problem that the function e in this statement (which gives the exponents of the prime powers) is not required to take only nonzero values (so that one needs to deal with a potential product of trivial groups). Is this just an oversight, or is there a reason for not requiring positive exponents? (The proof uses docs#Module.equiv_free_prod_directSum, which has the same problem.)

Why don't you want to use docs#Module.free_iff_noZeroSMulDivisors