English
Let z ∈ M with hz as p-power torsion. Given a linear map f from R/(R ∙ p^k) to M/(R ∙ z), there exists x ∈ M such that p^k x = 0 and the coset of x modulo R z equals f(1); i.e. x maps to f(1).
Русский
Пусть z ∈ M имеет p-степенный torsion. При заданном линейном отображении f: R/(R ∙ p^k) → M/(R ∙ z) существует x ∈ M такое, что p^k x = 0 и образ x по модулю R z равен f(1); то есть coset x сопоставлен f(1).
LaTeX
$$$\\exists x \\in M,\\ p^k \\cdot x = 0 \\ \\\\wedge\\ [x] = f(1) \\in M/(R\\cdot z)$$$
Lean4
theorem exists_smul_eq_zero_and_mk_eq {z : M} (hz : Module.IsTorsionBy R M (p ^ pOrder hM z)) {k : ℕ}
(f : (R ⧸ R ∙ p ^ k) →ₗ[R] M ⧸ R ∙ z) :
∃ x : M, p ^ k • x = 0 ∧ Submodule.Quotient.mk (p := span R { z }) x = f 1 :=
by
have f1 := mk_surjective (R ∙ z) (f 1)
have : p ^ k • f1.choose ∈ R ∙ z :=
by
rw [← Quotient.mk_eq_zero, mk_smul, f1.choose_spec, ← f.map_smul]
convert f.map_zero; change _ • Submodule.Quotient.mk _ = _
rw [← mk_smul, Quotient.mk_eq_zero, Algebra.id.smul_eq_mul, mul_one]
exact Submodule.mem_span_singleton_self _
obtain ⟨a, ha⟩ := p_pow_smul_lift hp hM hz this
refine ⟨f1.choose - a • z, by rw [smul_sub, sub_eq_zero, ha], ?_⟩
rw [mk_sub, mk_smul, (Quotient.mk_eq_zero _).mpr <| Submodule.mem_span_singleton_self _, smul_zero, sub_zero,
f1.choose_spec]
