English
The Smith normal form representation respects the smul action after embedding; the coordinate representations match under smf.a-scaling.
Русский
Представление SmithNormalForm сохраняет умножение на скаляры после вложения; координаты совпадают при умножении на smf.a.
LaTeX
$$$snf.bM.repr(m) \\circ snf.f = snf.a \\cdot snf.bN.repr(m)$$$
Lean4
@[simp]
theorem repr_apply_embedding_eq_repr_smul {i : Fin n} : snf.bM.repr m (snf.f i) = snf.bN.repr (snf.a i • m) i :=
by
obtain ⟨m, hm⟩ := m
obtain ⟨c, rfl⟩ := snf.bN.mem_submodule_iff.mp hm
replace hm :
(⟨Finsupp.sum c fun i t ↦ t • (↑(snf.bN i) : M), hm⟩ : N) = Finsupp.sum c fun i t ↦ t • ⟨snf.bN i, (snf.bN i).2⟩ :=
by ext; change _ = N.subtype _; simp [map_finsuppSum]
classical
simp_rw [hm, map_smul, map_finsuppSum, map_smul, Subtype.coe_eta, repr_self, Finsupp.smul_single, smul_eq_mul,
mul_one, Finsupp.sum_single, Finsupp.smul_apply, snf.snf, map_smul, repr_self, Finsupp.smul_single, smul_eq_mul,
mul_one, Finsupp.sum_apply, Finsupp.single_apply, EmbeddingLike.apply_eq_iff_eq, Finsupp.sum_ite_eq',
Finsupp.mem_support_iff, ite_not, mul_comm, ite_eq_right_iff]
exact fun a ↦ (mul_eq_zero_of_right _ a).symm
