English
Let η be a finite index set. For each j in η let M_j be an R-module with basis s_j. Consider the product space ∏_{j∈η} M_j with the product basis (Pi.basis s). Then for every j∈η and i in the index set of s_j, the coordinate of the vector Pi.single j (s_j i) with respect to this product basis is the function that is 1 at (j,i) and 0 elsewhere, i.e. its coefficient is Finsupp.single ⟨j,i⟩ 1.
Русский
Пусть η — конечное множество индексов. Для каждого j ∈ η пусть M_j — модуль над R, имеющий базис s_j. Рассматривая произведение ∏_{j∈η} M_j и базис Pi.basis s, коэффициент в координате ⟨j,i⟩ элемента Pi.single j (s_j i) по этому базису равен 1, во всех остальных координатах — 0; то есть он задаётся как Finsupp.single ⟨j,i⟩ 1.
LaTeX
$$$(\Pi\text{-basis } s).repr\ (\Pi\text{-single } j (s j i)) = \mathrm{Finsupp}.single \langle j, i\rangle\ 1$$$
Lean4
@[simp]
theorem basis_repr_single [DecidableEq η] (s : ∀ j, Basis (ιs j) R (Ms j)) (j i) :
(Pi.basis s).repr (Pi.single j (s j i)) = Finsupp.single ⟨j, i⟩ 1 := by
classical
ext ⟨j', i'⟩
by_cases hj : j = j'
· subst hj
simp only [Pi.basis, LinearEquiv.trans_apply, LinearEquiv.piCongrRight,
Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply, Basis.repr_symm_apply, LinearEquiv.coe_mk]
symm
simp [Finsupp.single_apply]
simp only [Pi.basis, LinearEquiv.trans_apply, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
LinearEquiv.piCongrRight]
dsimp
rw [Pi.single_eq_of_ne (Ne.symm hj), LinearEquiv.map_zero, Finsupp.zero_apply, Finsupp.single_eq_of_ne]
rintro ⟨⟩
contradiction
