English
A nonzero index of a submodule N implies the existence of a linear equivalence between N and the ambient indexed function space ι → ℤ; conversely such an equivalence yields a nonzero index.
Русский
Не нулевой индекс подмодуля N эквилен существованию линейного эквивалента между N и ι → ℤ; наоборот, наличие такого эквивалента даёт ненулевой индекс.
LaTeX
$$N.toAddSubgroup.index ≠ 0 ↔ ∃ e, N ≃_R (ι → ℤ)$$
Lean4
theorem submodule_toAddSubgroup_index_ne_zero_iff {N : Submodule ℤ (ι → ℤ)} :
N.toAddSubgroup.index ≠ 0 ↔ Nonempty (N ≃ₗ[ℤ] (ι → ℤ)) :=
by
obtain ⟨n, snf⟩ := N.smithNormalForm <| .ofEquivFun <| .refl ..
have := Fintype.ofFinite ι
rw [snf.toAddSubgroup_index_ne_zero_iff]
rcases snf with ⟨-, bN, -, -, -⟩
refine ⟨fun h ↦ ?_, fun ⟨e⟩ ↦ ?_⟩
· subst h
exact ⟨(bN.reindex (Fintype.equivFin _).symm).equivFun⟩
· have hc := card_eq_of_linearEquiv ℤ <| bN.equivFun.symm.trans e
simpa using hc
