English
The canonical map out of a direct sum of a family of submodules is injective when the submodules are iSupIndep.
Русский
Каноническое отображение из прямой суммы подмодулей инъективно, если подмодули образуют iSupIndep.
LaTeX
$$$\text{If } i\!\text{SupIndep } p, \; \text{then } \operatorname{lsum} \; \text{map} (p_i).subtype \; \text{is injective}.$$$
Lean4
/-- The canonical map out of a direct sum of a family of submodules is injective when the submodules
are `iSupIndep`.
Note that this is not generally true for `[Semiring R]`, for instance when `A` is the
`ℕ`-submodules of the positive and negative integers.
See `Counterexamples/DirectSumIsInternal.lean` for a proof of this fact. -/
theorem dfinsupp_lsum_injective {p : ι → Submodule R N} (h : iSupIndep p) :
Function.Injective (lsum ℕ fun i => (p i).subtype) := by
-- simplify everything down to binders over equalities in `N`
rw [iSupIndep_iff_forall_dfinsupp] at h
suffices LinearMap.ker (lsum ℕ fun i => (p i).subtype) = ⊥ by
-- Lean can't find this without our help
letI thisI : AddCommGroup (Π₀ i, p i) := inferInstance
rw [LinearMap.ker_eq_bot] at this
exact this
rw [LinearMap.ker_eq_bot']
intro m hm
ext i : 1
-- split `m` into the piece at `i` and the pieces elsewhere, to match `h`
rw [DFinsupp.zero_apply, ← neg_eq_zero]
refine h i (-m i) m ?_
rwa [← erase_add_single i m, LinearMap.map_add, lsum_single, Submodule.subtype_apply, add_eq_zero_iff_eq_neg, ←
Submodule.coe_neg] at hm
