Quotienting out a free ℤ-module

If G is a rank d free ℤ-module, then G/nG is a finite group of cardinality n ^ d.

@[reducible, inline]

abbrev ModN (G : Type u_1) [AddCommGroup G] (n : ℕ) : Type u_1

ModN G n denotes the quotient of G by multiples of n

Equations

• ModN G n = (G ⧸ ((LinearMap.lsmul ℤ G) ↑n).range)

@[instance_reducible]

instance ModN.instModuleZMod {G : Type u_1} [AddCommGroup G] {n : ℕ} : Module (ZMod n) (ModN G n)

Equations

• ModN.instModuleZMod = QuotientAddGroup.zmodModule ⋯

def ModN.liftEquiv {G : Type u_1} {M : Type u_3} [AddCommGroup G] {n : ℕ} [AddMonoid M] : (ModN G n →+ M) ≃ { φ : G →+ M // ∀ (g : G), n • φ g = 0 }

The universal property of ModN G n in terms of monoids: Monoid homomorphisms from ModN G n are the same as monoid homomorphisms from G whose values are n-torsion.

Equations

• One or more equations did not get rendered due to their size.

def ModN.liftEquiv' {G : Type u_1} {H : Type u_2} [AddCommGroup G] {n : ℕ} [AddCommGroup H] [Module (ZMod n) H] : (ModN G n →ₗ[ZMod n] H) ≃ { φ : G →+ H // ∀ (g : G), n • φ g = 0 }

The universal property of ModN G n in terms of ZMod n-modules: ZMod n-linear maps from ModN G n are the same as monoid homomorphisms from G whose values are n-torsion.

Equations

• ModN.liftEquiv' = (AddMonoidHom.toZModLinearMapEquiv n).symm.trans ModN.liftEquiv

def ModN.mkQ {G : Type u_1} [AddCommGroup G] (n : ℕ) : G →+ ModN G n

The quotient map G → G / nG.

Equations

• ModN.mkQ n = ↑((LinearMap.lsmul ℤ G) ↑n).range.mkQ

noncomputable def ModN.basis {G : Type u_1} [AddCommGroup G] {n : ℕ} [NeZero n] {ι : Type u_4} (b : Module.Basis ι ℤ G) : Module.Basis ι (ZMod n) (ModN G n)

Given a free module G over ℤ, construct the corresponding basis of G / ⟨n⟩ over ℤ / nℤ.

Equations

• One or more equations did not get rendered due to their size.

theorem ModN.basis_apply_eq_mkQ {G : Type u_1} [AddCommGroup G] {n : ℕ} [NeZero n] {ι : Type u_4} (b : Module.Basis ι ℤ G) (i : ι) : (basis b) i = (mkQ n) (b i)

theorem ModN.isAddTorsion {G : Type u_1} [AddCommGroup G] {n : ℕ} [NeZero n] : IsAddTorsion (ModN G n)

The quotient ModN G n is a torsion group.

instance ModN.instFinite {G : Type u_1} [AddCommGroup G] {n : ℕ} [NeZero n] [Module.Finite ℤ G] : Finite (ModN G n)

instance ModN.instModuleFinite {G : Type u_1} [AddCommGroup G] {n : ℕ} [NeZero n] [Module.Finite ℤ G] : Module.Finite (ZMod n) (ModN G n)

@[simp]

theorem ModN.natCard_eq (G : Type u_1) [AddCommGroup G] (n : ℕ) [NeZero n] [Module.Finite ℤ G] [Module.Free ℤ G] : Nat.card (ModN G n) = n ^ Module.finrank ℤ G