English
A quotient by a full-rank submodule of a finite free module decomposes into a product of cyclic quotients.
Русский
Фактор-модуль по подмодулю полного ранга конечного свободного модуля распадается на прямую сумму циклических частичных модулей.
LaTeX
$$$$ (M \;/ N) \cong \bigoplus_i R \;/ (\text{span}(\{\mathrm{smithNormalFormCoeffs}_i\})) $$$$
Lean4
/-- We can write the quotient by a submodule of full rank over a PID as a product of quotients
by principal ideals.
-/
noncomputable def quotientEquivPiSpan (N : Submodule R M) (b : Basis ι R M)
(h : Module.finrank R N = Module.finrank R M) :
(M ⧸ N) ≃ₗ[R] Π i, R ⧸ Ideal.span ({smithNormalFormCoeffs b h i} : Set R) :=
by
haveI := Fintype.ofFinite ι
let a := smithNormalFormCoeffs b h
let b' := smithNormalFormTopBasis b h
let ab := smithNormalFormBotBasis b h
have ab_eq := smithNormalFormBotBasis_def b h
have mem_I_iff : ∀ x, x ∈ N ↔ ∀ i, a i ∣ b'.repr x i :=
by
intro x
simp_rw [ab.mem_submodule_iff', ab, ab_eq]
have : ∀ (c : ι → R) (i), b'.repr (∑ j : ι, c j • a j • b' j) i = a i * c i :=
by
intro c i
simp only [← MulAction.mul_smul, b'.repr_sum_self, mul_comm]
constructor
· rintro ⟨c, rfl⟩ i
exact ⟨c i, this c i⟩
· rintro ha
choose c hc using ha
exact
⟨c, b'.ext_elem fun i => Eq.trans (hc i) (this c i).symm⟩
-- Now we map everything through the linear equiv `M ≃ₗ (ι → R)`,
-- which maps `N` to `N' := Π i, a i ℤ`.
let N' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span R ({a i} : Set R)
have : Submodule.map (b'.equivFun : M →ₗ[R] ι → R) N = N' :=
by
ext x
simp only [N', Submodule.mem_map, Submodule.mem_pi, mem_span_singleton, Set.mem_univ, mem_I_iff, smul_eq_mul,
forall_true_left, LinearEquiv.coe_coe, Basis.equivFun_apply, mul_comm _ (a _), eq_comm (b := (x _))]
constructor
· rintro ⟨y, hy, rfl⟩ i
exact hy i
· rintro hdvd
refine ⟨∑ i, x i • b' i, fun i => ?_, ?_⟩ <;> rw [b'.repr_sum_self]
· exact hdvd i
refine (Submodule.Quotient.equiv N N' b'.equivFun this).trans (re₂₃ := inferInstance) (re₃₂ := inferInstance) ?_
classical exact Submodule.quotientPi (show _ → Submodule R R from fun i => span R ({a i} : Set R))
