Lemmas about index and multiplication-by-n

In this file we collect some results involving the multiplication-by-n map nsmulAddMonoidHom n (for a natural number n) on a commutative additive group and the (relative) index of subgroups.

theorem AddSubgroup.index_range_nsmul (M : Type u_1) [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (n : ℕ) : (nsmulAddMonoidHom n).range.index = n ^ Module.finrank ℤ M

The index of the image of the multiplication-by-n map on an additive group M that is free and finitely generated as a ℤ-module is n ^ finrank ℤ M.

theorem AddSubgroup.relIndex_map_nsmul {M : Type u_1} [AddCommGroup M] (n : ℕ) (S : AddSubgroup M) [Module.Free ℤ ↥(toIntSubmodule S)] [Module.Finite ℤ ↥(toIntSubmodule S)] : (map (nsmulAddMonoidHom n) S).relIndex S = n ^ Module.finrank ℤ ↥S

The relative index in S of the image of the multiplication-by-n map on an additive subgroup S of an additive group such that S is free and finitely generated as a ℤ-module is n ^ finrank ℤ S.

theorem AddSubgroup.distribSMulToLinearMap_injective_of_isTorsionFree {M : Type u_1} [AddCommGroup M] [Module.IsTorsionFree ℤ M] {n : ℕ} (hn : n ≠ 0) : Function.Injective ⇑(DistribSMul.toLinearMap ℤ M n)

On an additive group that is torsion-free as a ℤ-module, the linear map given by multiplication by n : ℕ is injective (when n ≠ 0).

theorem AddSubgroup.nsmulAddMonoidHom_injective_of_isTorsionFree {M : Type u_1} [AddCommGroup M] [Module.IsTorsionFree ℤ M] {n : ℕ} (hn : n ≠ 0) : Function.Injective ⇑(nsmulAddMonoidHom n)

On an additive group that is torsion-free as a ℤ-module, the multiplication-by-n map is injective (when n ≠ 0).

theorem AddSubgroup.finrank_eq_of_finiteIndex {M : Type u_1} [AddCommGroup M] [Module.Finite ℤ M] [Module.IsTorsionFree ℤ M] (A : AddSubgroup M) [A.FiniteIndex] : Module.finrank ℤ ↥A = Module.finrank ℤ M

If A is a subgroup of finite index of an additive group M that is finitely generated and torsion-free as a ℤ-module, then A and M have the same rank.

theorem AddSubgroup.finrank_eq_of_isFiniteRelIndex {M : Type u_1} [AddCommGroup M] {A B : AddSubgroup M} [Module.Finite ℤ ↥B] [Module.IsTorsionFree ℤ ↥B] (h : A ≤ B) [A.IsFiniteRelIndex B] : Module.finrank ℤ ↥A = Module.finrank ℤ ↥B

If A ≤ B are subgroups of an additive group M such that A has finite relative index in B, where B is finitely generated and torsion-free as a ℤ-module, then A and B have the same rank.