component_sumInv — Mathlib

English

Let ι be finite and x be in AdicCompletion I (⨁ j, M_j). Then the j-th component of sumInv I M x equals map I (component R ι _ j) x for every j. In words, the j-th coordinate of sumInv corresponds to applying the map on the j-th coordinate.

Русский

Пусть ι конечно, и x ∈ AdicCompletion I (⨁ j, M_j). Тогда j-я компонента sumInv I M x равна map I (component R ι _ j) x; то есть коэффициент по j-ой координате равен соответствующему отображению.

LaTeX

$$$ component\,(AdicCompletion I R)\ ι\ _ j\ (sumInv I M\ x) = map I\ (component R ι _ j)\ x $$$

Lean4

@[simp]
theorem component_sumInv (x : AdicCompletion I (⨁ j, M j)) (j : ι) :
    component (AdicCompletion I R) ι _ j (sumInv I M x) = map I (component R ι _ j) x :=
  by
  apply induction_on I _ x (fun x ↦ ?_)
  rfl

Похожие утверждения