Subgroup of finitely gen. abelian group is finitely gen.

Stream: Is there code for X?

[Terence Tao]

Is this result in Mathlib somewhere? For minor technical reasons I'd prefer it in the module form

import Mathlib

variable {G: Type*} [AddCommGroup G] [Module ℤ G] [Module.Finite ℤ G]

lemma subgroup_finite (H: AddSubgroup G) : Module.Finite ℤ H := by sorry

but I'll be happy to take the abelian group version

import Mathlib

variable {G: Type*} [AddCommGroup G]

lemma subgroup_finite (H: AddSubgroup G) (h: AddGroup.FG G)  : AddSubgroup.FG H := by sorry

(I also only need it in the case when G is free, though that's not such a big help since it's easy to reduce to that case.) I suppose I could try to equate my free abelian group with a Zlattice and use the machinery in Mathlib.Algebra.Module.Zlattice, but this is a somewhat weird approach (using geometry to prove a purely algebraic statement) and I was wondering if there was a more direct route.

[Junyan Xu]

It should follow from that Z is a Noetherian ring ...

[Junyan Xu]

We have docs#isNoetherian_of_isNoetherianRing_of_finite and then all submodules are FG by definition. Let me look up how to convert between Submodule.FG and AddSubgroup.FG ...

[Junyan Xu]

That's docs#Submodule.fg_iff_add_subgroup_fg
and docs#AddSubgroup.toIntSubmodule too

[Terence Tao]

Ah, I should have tried thinking like an algebraist and generalizing to a more abstract setting. :grinning_face_with_smiling_eyes: Thanks!

[Terence Tao]

Ah and I have discovered (for the third time in two days) that I have unintentionally made life difficult for myself by redundantly declaring an instance (in this case, Module ℤ G), causing all sorts of weird defeq issues.

[Terence Tao]

Got it to work. Thanks again!

variable {G: Type*} [AddCommGroup G] [Module.Finite ℤ G]

lemma subgroup_finite (H: AddSubgroup G) : Module.Finite ℤ H := by
  rw [Module.Finite.iff_addGroup_fg, AddGroup.fg_iff_addSubgroup_fg, <-AddSubgroup.toIntSubmodule_toAddSubgroup H, <-Submodule.fg_iff_add_subgroup_fg]
  exact isNoetherian_def.mp (by infer_instance) _

[Junyan Xu]

... which can be golfed to

variable {G : Type*} [AddCommGroup G] [Module.Finite ℤ G]
lemma subgroup_finite (H : AddSubgroup G) : Module.Finite ℤ H :=
  (AddSubgroup.toIntSubmodule H).fg_iff_finite.mp (IsNoetherian.noetherian _)

Here I'm using that ↥H is defeq to ↥(AddSubgroup.toIntSubmodule H) even though H doesn't have the same type as AddSubgroup.toIntSubmodule H. The reason is that ↥H is defined to be {x // x ∈ H} and x ∈ AddSubgroup.toIntSubmodule H is defined to be x ∈ H.

[Terence Tao]

Maybe this proof (or the abelian subgroup version) is suitable for Mathlib? I could imagine that other people might have use of this basic fact.

[Terence Tao]

For sake of completeness, here is the matching lemma for freeness. (Following @Junyan Xu 's example, I ended up exploring the theory of modules over a PID. Brings back memories of grad school algebra quals...)

import Mathlib

variable {G : Type*} [AddCommGroup G]

lemma subgroup_finite (H: AddSubgroup G) [Module.Finite ℤ G] : Module.Finite ℤ H :=
   (AddSubgroup.toIntSubmodule H).fg_iff_finite.mp (IsNoetherian.noetherian _)

lemma subgroup_free (H : AddSubgroup G) [Module.Finite ℤ G] [Module.Free ℤ G] : Module.Free ℤ H := by
  rcases Submodule.nonempty_basis_of_pid (Module.Free.chooseBasis ℤ G) (AddSubgroup.toIntSubmodule H) with ⟨ n, ⟨ b ⟩ ⟩
  exact Module.Free.of_basis b

[Andrew Yang]

Just noting that there is also docs#AddGroup.FG (and arguably these lemmas should be stated in terms of this) and we can translate between them via docs#Module.Finite.iff_addGroup_fg.

[Andrew Yang]

And AddGroup.FG -> Module.Finite ℤ can potentially be an instance?

[Terence Tao]

I'll defer to others on instances, they seem to be double-edged swords.

To write subgroup_free in purely group theoretic terms, it would be nice to have

import Mathlib

variable {G : Type*} [AddCommGroup G]

lemma AddCommGroup.free_iff_torsion_free [Module.Finite ℤ G] : Module.Free ℤ G ↔ AddMonoid.IsTorsionFree G := by
  sorry

but I can't find a slick proof of this; docs#Module.free_of_finite_type_torsion_free' comes sort of close, but it's a pain to get from NoZeroSMulDivisors to AddMonoid.IsTorsionFree. I feel like there could be a bit more API here.

[Johan Commelin]

Andrew Yang said:

And AddGroup.FG -> Module.Finite ℤ can potentially be an instance?

Yes, we should definitely try that. Maybe it wasn't because it would create a loop in Lean 3?

[Johan Commelin]

@Terence Tao Note that diamonds are only an issue for instances that carry data. Prop-valued instances don't have that double edge.

[Terence Tao]

More generally I have the sense that the classification of finitely generated abelian groups is implicitly in Mathlib, but somehow scattered across a bunch of different APIs (in principle it's all extractable from Mathlib.LinearAlgebra.FreeModule.PID , but for a non-algebraist like myself this wasn't so easy to work with).

[Andrew Yang]

The main result is docs#Module.equiv_free_prod_directSum but yes we should definitely specialize them to groups.

[Terence Tao]

Huh, so docs#AddCommGroup.equiv_free_prod_directSum_zmod does exist, but the API around it is skimpy. (For instance, no mention of invariant factors, and no relations between the classification of a f.g. abelian group and that of its subgroups or quotients.)

[Andrew Yang]

Terence Tao said:

It's a pain to get from NoZeroSMulDivisors to AddMonoid.IsTorsionFree.

Done in #9345. Something similar was needed in FLT-regular as well.

[Yaël Dillies]

Terence Tao said:

Huh, so docs#AddCommGroup.equiv_free_prod_directSum_zmod does exist, but the API around it is skimpy.

I have a bit more in https://github.com/YaelDillies/LeanAPAP/blob/master/LeanAPAP/Mathlib/GroupTheory/FiniteAbelian.lean if that helps.