Index of submodules of free ℤ-modules (considered as an AddSubgroup).

This file provides lemmas about when a submodule of a free ℤ-module is a subgroup of finite index.

theorem Basis.SmithNormalForm.toAddSubgroup_index_eq_pow_mul_prod {ι : Type u_1} {R : Type u_2} {M : Type u_3} {n : ℕ} [CommRing R] [AddCommGroup M] [Fintype ι] [Module R M] {N : Submodule R M} (snf : Basis.SmithNormalForm N ι n) : N.toAddSubgroup.index = Nat.card R ^ (Fintype.card ι - n) * ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index

Given a submodule N in Smith normal form of a free R-module, its index as an additive subgroup is an appropriate power of the cardinality of R multiplied by the product of the indexes of the ideals generated by each basis vector.

theorem Basis.SmithNormalForm.toAddSubgroup_index_eq_ite {ι : Type u_1} {R : Type u_2} {M : Type u_3} {n : ℕ} [CommRing R] [AddCommGroup M] [Fintype ι] [Infinite R] [Module R M] {N : Submodule R M} (snf : Basis.SmithNormalForm N ι n) : N.toAddSubgroup.index = if n = Fintype.card ι then ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index else 0

Given a submodule N in Smith normal form of a free R-module, its index as an additive subgroup is infinite (represented as zero) if the submodule basis has fewer vectors than the basis for the module, and otherwise equals the product of the indexes of the ideals generated by each basis vector.

theorem Basis.SmithNormalForm.toAddSubgroup_index_ne_zero_iff {ι : Type u_1} {M : Type u_3} {n : ℕ} [AddCommGroup M] [Fintype ι] {N : Submodule ℤ M} (snf : Basis.SmithNormalForm N ι n) : N.toAddSubgroup.index ≠ 0 ↔ n = Fintype.card ι

Given a submodule N in Smith normal form of a free ℤ-module, it has finite index as an additive subgroup (i.e., N.toAddSubgroup.index ≠ 0) if and only if the submodule basis has as many vectors as the basis for the module.

theorem Int.submodule_toAddSubgroup_index_ne_zero_iff {ι : Type u_1} [Finite ι] {N : Submodule ℤ (ι → ℤ)} : N.toAddSubgroup.index ≠ 0 ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

theorem Int.addSubgroup_index_ne_zero_iff {ι : Type u_1} [Finite ι] {H : AddSubgroup (ι → ℤ)} : H.index ≠ 0 ↔ Nonempty (↥H ≃+ (ι → ℤ))

theorem Int.subgroup_index_ne_zero_iff {ι : Type u_1} [Finite ι] {H : Subgroup (ι → Multiplicative ℤ)} : H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))