English
The composite of sum and sumInv is the identity on the direct sum; hence the canonical pairing is an isomorphism.
Русский
Состав суммирования и sumInv изделует тождественное отображение на прямой сумме; следовательно, каноническое сопоставление является изоморфизмом.
LaTeX
$$$ \text{sum} I M \circ \text{sumInv} I M = \mathrm{Id}$$$
Lean4
theorem sum_comp_sumInv : sum I M ∘ₗ sumInv I M = LinearMap.id :=
by
ext f n
simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq, mk_apply_coe, Submodule.mkQ_apply]
rw [← DirectSum.sum_univ_of (((sumInv I M) ((AdicCompletion.mk I (⨁ (j : ι), M j)) f)))]
simp only [sumInv_apply, map_mk, map_sum, sum_of, val_sum_apply, mk_apply_coe, AdicCauchySequence.map_apply_coe]
simp only [← Submodule.mkQ_apply, ← map_sum, ← apply_eq_component, lof_eq_of, DirectSum.sum_univ_of]
