G/nG is a finite group of size n^d

Stream: Is there code for X?

[Yaël Dillies]

Suppose G is an abelian group free of rank d as a ℤ-module. Then G/nG is a finite group of rank d as a ZMod n-module. Is this easy to get from mathlib? We have a proof in PFR, but it's quite horrible.

[Yaël Dillies]

import Mathlib.LinearAlgebra.Dimension.Finrank
import Mathlib.LinearAlgebra.FreeModule.Basic
import Mathlib.RingTheory.Finiteness

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

variable (G n) in
abbrev modN : Type _ := G ⧸ LinearMap.range (LinearMap.lsmul ℤ G n)

/-- If `G` is a rank `d` free `ℤ`-module, then `G/nG` is a finite group of cardinality `n ^ d`. -/
example : Finite (modN G n) ∧ Nat.card (modN G n) = n ^ Module.finrank ℤ G := sorry

[Kevin Buzzard]

One could use the iso $G/nG\cong G\otimes_{\Z}\Z/n\Z.$

[Yaël Dillies]

And can this be generalised away from ℤ?

[Yaël Dillies]

Kevin Buzzard said:

One could use the iso $G/nG\cong G\otimes_{\Z}\Z/n\Z.$

:idea: Does this have a name in mathlib?

[Riccardo Brasca]

We have Module.Free.tensor

[Riccardo Brasca]

see its proof to get the explicit basis if you need the rank

[Riccardo Brasca]

no sorry, this is not what you need

[Riccardo Brasca]

we may have something like that in flt-regular

[Riccardo Brasca]

@Andrew Yang

[Andrew Yang]

Not sure but the iso Kevin mentioned is
docs#quotTensorEquivQuotSMul