English
The direct sum decomposition for S/ I matches the coordinatewise quotients by smithCoeffs, giving a basis-compatible direct sum decomposition.
Русский
Разложение S/ I по прямой сумме согласовано с координатной декомпозицией по smithCoeffs.
LaTeX
$$S/I ≃_F ⨁ i, R/ span({I.smithCoeffs b hI i})$$
Lean4
/-- The universal property of `ModN G n` in terms of monoids: Monoid homomorphisms from `ModN G n`
are the same as monoid homomorphisms from `G` whose values are `n`-torsion. -/
protected def liftEquiv [AddMonoid M] : (ModN G n →+ M) ≃ { φ : G →+ M // ∀ g, n • φ g = 0 }
where
toFun
f :=
⟨f.comp (QuotientAddGroup.mk' _), fun g ↦
by
let Gn : AddSubgroup G := (LinearMap.range (LinearMap.lsmul ℤ G n)).toAddSubgroup
suffices n • g ∈ (QuotientAddGroup.mk' Gn).ker
by
simp only [AddMonoidHom.coe_comp, comp_apply, ← map_nsmul]
change
f (QuotientAddGroup.mk' Gn (n • g)) =
0 -- Can we avoid `change`?
rw [this, map_zero]
simp [QuotientAddGroup.ker_mk', Gn]⟩
invFun φ := QuotientAddGroup.lift _ φ <| by rintro - ⟨g, rfl⟩; simpa using φ.property g
left_inv
f := by
ext x
induction x using QuotientAddGroup.induction_on
rfl -- Should `simp` suffice here?
right_inv φ := by aesop
