English
The two canonical maps between the adic completion and the direct sum are inverses of each other, establishing an isomorphism between AdicCompletion I (⨁ j, M_j) and the corresponding direct sum.
Русский
Две канонические карты между адической очисткой и прямой суммой образуют изоморфизм между AdicCompletion I (⨁ j, M_j) и соответствующей прямой суммой.
LaTeX
$$$ (sum I M)^{-1} = sumInv I M $$$
Lean4
theorem sumInv_comp_sum : sumInv I M ∘ₗ sum I M = LinearMap.id :=
by
ext j x : 2
apply DirectSum.ext_component (AdicCompletion I R) (fun i ↦ ?_)
ext n
simp only [LinearMap.coe_comp, Function.comp_apply, sum_lof, map_mk, component_sumInv, mk_apply_coe,
AdicCauchySequence.map_apply_coe, Submodule.mkQ_apply, LinearMap.id_comp]
rw [DirectSum.component.of, DirectSum.component.of]
split
· next h => subst h; simp
· simp
