English
Under irreducible p and a p-power torsion structure on M, for elements x,y ∈ M and k ∈ ℕ, if p^k x lies in the span of y and y has appropriate torsion, then there exists a ∈ R with p^k x = p^k a y; if k exceeds the p-order, the trivial choice a = 0 suffices.
Русский
При ирредуцируемом p и p-степенном torsion-структуре на M, для элементов x,y ∈ M и k ∈ ℕ, если p^k x лежит в линейной оболочке y и y имеет подходящий torsion, существует a ∈ R с p^k x = p^k a y; если k превышает p-orden, достаточно взять a = 0.
LaTeX
$$$\\text{Let } hM' : \\text{Module.IsTorsionBy } R\\ M\\ (p^{pOrder\\ hM\\ y})\\ \\text{and } h: p^k \\! \\cdot x \\in R \\cdot y.\\ Then ∃ a \\in R,\\ p^k \\cdot x = p^k \\cdot a \\cdot y.$$$
Lean4
theorem p_pow_smul_lift {x y : M} {k : ℕ} (hM' : Module.IsTorsionBy R M (p ^ pOrder hM y)) (h : p ^ k • x ∈ R ∙ y) :
∃ a : R, p ^ k • x = p ^ k • a • y := by
by_cases hk : k ≤ pOrder hM y
· let f := ((R ∙ p ^ (pOrder hM y - k) * p ^ k).quotEquivOfEq _ ?_).trans (quotTorsionOfEquivSpanSingleton R M y)
· have : f.symm ⟨p ^ k • x, h⟩ ∈ R ∙ Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k) (p ^ k) :=
by
rw [← Quotient.torsionBy_eq_span_singleton, mem_torsionBy_iff, ← f.symm.map_smul]
· convert f.symm.map_zero; ext
rw [coe_smul_of_tower, coe_mk, coe_zero, smul_smul, ← pow_add, Nat.sub_add_cancel hk, @hM' x]
· exact mem_nonZeroDivisors_of_ne_zero (pow_ne_zero _ hp.ne_zero)
rw [Submodule.mem_span_singleton] at this; obtain ⟨a, ha⟩ := this; use a
rw [f.eq_symm_apply, ← Ideal.Quotient.mk_eq_mk, ← Quotient.mk_smul] at ha
dsimp only [smul_eq_mul, LinearEquiv.trans_apply, Submodule.quotEquivOfEq_mk,
quotTorsionOfEquivSpanSingleton_apply_mk] at ha
rw [smul_smul, mul_comm]; exact congr_arg ((↑) : _ → M) ha.symm
· symm; convert Ideal.torsionOf_eq_span_pow_pOrder hp hM y
rw [← pow_add, Nat.sub_add_cancel hk]
· use 0
rw [zero_smul, smul_zero, ← Nat.sub_add_cancel (le_of_not_ge hk), pow_add, mul_smul, hM', smul_zero]
