English
Let R be a semiring and (M_i) be a family of R-modules indexed by ι. For any equivalence h: ι ≃ κ, there is a canonical linear isomorphism between the direct sum ⨁_i M_i and the direct sum ⨁_k M_{h^{-1}(k)} obtained by re-indexing coordinates. Concretely, (lequivCongrLeft R h)(f) evaluated at k equals f evaluated at h.symm k.
Русский
Пусть R — полугруппа на кольцах, а {M_i} — семейство модулей над R, индексированное ι. Для любой биекция h: ι ≃ κ существует каноническое линейное изоморфизм между прямой суммой ⨁_i M_i и прямой суммой ⨁_k M_{h^{-1}(k)}, получаемый перестановкой координат. Явно, для f в ⨁_i M_i и k в κ имеет место (lequivCongrLeft R h f)(k) = f(h.symm k).
LaTeX
$$$ (\operatorname{lequivCongrLeft} \, R \, h \, f)\, k = f \,(h^{-1}(k)). $$$
Lean4
@[simp]
theorem lequivCongrLeft_apply (h : ι ≃ κ) (f : ⨁ i, M i) (k : κ) : lequivCongrLeft R h f k = f (h.symm k) :=
equivCongrLeft_apply _ _ _
