English
For a submodule N of a free integral module M, the quotient M/N is finite iff finrank(N) = finrank(M).
Русский
Для подмодуля N свободного целочисленного модуля M фактор-модуль M/N конечен тогда и только тогда, когда finrank(N) = finrank(M).
LaTeX
$$$$ \mathrm{Finite}(M / N) \iff \mathrm{finrank}_{\mathbb{Z}} N = \mathrm{finrank}_{\mathbb{Z}} M. $$$$
Lean4
theorem finiteQuotient_iff [Module.Free ℤ M] [Module.Finite ℤ M] (N : Submodule ℤ M) :
Finite (M ⧸ N) ↔ Module.finrank ℤ N = Module.finrank ℤ M :=
by
refine
⟨fun h ↦
le_antisymm (finrank_le N) <|
((LinearMap.lsmul ℤ M (Nat.card (M ⧸ N))).codRestrict N fun x ↦ ?_).finrank_le_finrank_of_injective ?_,
fun h ↦ finiteQuotientOfFreeOfRankEq N h⟩
· simpa using AddSubgroup.nsmul_index_mem N.toAddSubgroup x
· refine (LinearMap.lsmul_injective ?_).codRestrict _
exact Int.ofNat_ne_zero.mpr <| Nat.card_ne_zero.mpr ⟨Set.nonempty_iff_univ_nonempty.mpr Set.univ_nonempty, h⟩
