English
Let I be an ideal of R and (M i) an indexed family of R-modules. For j in ι and x in AdicCompletion I (M j), the sum over the direct sum of all components after applying the lof projection to the j-th component equals the map of the lof from R to the j-th component applied to x.
Русский
Пусть I — идеал кольца R и (M_i) — семейство R-модулей индексированное. Для j и элемента x ∈ AdicCompletion I (M_j) сумма поDirectSum после применения lof к j-му компоненту равняется отображению map I (lof R ι M j) к x.
LaTeX
$$$ sum\, I\, M\, \\big( (DirectSum.lof (AdicCompletion I R) ι (fun i \\mapsto AdicCompletion I (M i)) j)\\, x \\big) = map I (lof R ι M j)\\, x $$$
Lean4
@[simp]
theorem sum_lof [DecidableEq ι] (j : ι) (x : AdicCompletion I (M j)) :
sum I M ((DirectSum.lof (AdicCompletion I R) ι (fun i ↦ AdicCompletion I (M i)) j) x) = map I (lof R ι M j) x := by
simp [sum]
