English
Given an index i and a function c with c(i)=0, there is a linear equivalence on finitely supported functions that adds c(j) to the i-th coordinate and preserves most structure, acting as the identity on the i-th basis element.
Русский
Пусть задан индекс i и функция c такая, что c(i)=0; существует линейное эквивалентное преобразование на функциях с конечной поддержкой, добавляющее c(j) к j-ой координате и сохраняющее основную структуру, в частности, инвариантно относительно i-й базисной вектор.
LaTeX
$$$\text{addSingleEquiv}_i^c: (\iota \to_0 R) \simeq_\ell (\iota \to_0 R)$ при условии $c(i)=0$$$
Lean4
/-- Given `c : ι → R` and an index `i` such that `c i = 0`, this is the linear isomorphism sending
the `j`-th standard basis vector to itself plus `c j` multiplied with the `i`-th standard basis
vector (in particular, the `i`-th standard basis vector is kept invariant). -/
def addSingleEquiv : (ι →₀ R) ≃ₗ[R] (ι →₀ R) :=
by
refine
.ofLinear (linearCombination _ fun j ↦ single j 1 + single i (c j))
(linearCombination _ fun j ↦ single j 1 - single i (c j)) ?_ ?_ <;>
ext j k <;>
obtain rfl | hk := eq_or_ne i k
· simp [h₀]
· simp [hk]
· simp [h₀]
· simp [hk]
