English
Let R be a commutative semiring and M an R-module. Suppose M is torsion with respect to the powers of p and that a finite family s: Fin d → M spans M. Then there exists an index j such that the entire module M is killed by p^{pOrder(hM, s_j)}; equivalently, M has p^{pOrder(hM, s_j)}-torsion.
Русский
Пусть R — коммутативное полугруппа, M — модуль над R. Пусть M является торсионным относительно степеней элемента p и множество s = (s_i)_i из d элементов порождает M. Тогда существует индекс j, для которого вся модульная структура уничтожается действием p^{pOrder(hM, s_j)}; т.е. p^{pOrder(hM, s_j)}-торсии существует на всём M.
LaTeX
$$$\\exists j : Fin d,\\; Module.IsTorsionBy R M (p^{\\, pOrder hM (s j)})$$$
Lean4
theorem exists_isTorsionBy {p : R} (hM : IsTorsion' M <| Submonoid.powers p) (d : ℕ) (hd : d ≠ 0) (s : Fin d → M)
(hs : span R (Set.range s) = ⊤) : ∃ j : Fin d, Module.IsTorsionBy R M (p ^ pOrder hM (s j)) :=
by
let oj := List.argmax (fun i => pOrder hM <| s i) (List.finRange d)
have hoj : oj.isSome :=
Option.ne_none_iff_isSome.mp fun eq_none => hd <| List.finRange_eq_nil.mp <| List.argmax_eq_none.mp eq_none
use Option.get _ hoj
rw [isTorsionBy_iff_torsionBy_eq_top, eq_top_iff, ← hs, Submodule.span_le, Set.range_subset_iff]
intro i; change (p ^ pOrder hM (s (Option.get oj hoj))) • s i = 0
have : pOrder hM (s i) ≤ pOrder hM (s <| Option.get _ hoj) :=
List.le_of_mem_argmax (List.mem_finRange i) (Option.get_mem hoj)
rw [← Nat.sub_add_cancel this, pow_add, mul_smul, pow_pOrder_smul, smul_zero]
