English
The coercion of the collectedBasis equals the pointwise combination of the bases: the basis element at (i, a) corresponds to v_i(a).
Русский
Понижение collectedBasis даёт элемент базиса в точности как сочетание баз v_i; элемент с индексом (i, a) соответствует v_i(a).
LaTeX
$$$\text{(h.collectedBasis v)} = (a \mapsto v_{a.1}(a.2)).$$$
Lean4
@[simp]
theorem collectedBasis_coe (h : IsInternal A) {α : ι → Type*} (v : ∀ i, Basis (α i) R (A i)) :
⇑(h.collectedBasis v) = fun a : Σ i, α i ↦ ↑(v a.1 a.2) :=
by
funext a
simp only [IsInternal.collectedBasis, coeLinearMap, Basis.coe_ofRepr, LinearEquiv.trans_symm, LinearEquiv.symm_symm,
LinearEquiv.trans_apply, sigmaFinsuppLequivDFinsupp_apply, AddEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe,
EquivLike.coe_coe, sigmaFinsuppAddEquivDFinsupp_apply, sigmaFinsuppEquivDFinsupp_single,
LinearEquiv.ofBijective_apply]
rw [DFinsupp.mapRange.linearEquiv_symm]
-- `DFunLike.coe (β := fun x ↦ ⨁ (i : ι), ↥(A i))`
-- appears in the goal, but the lemma is expecting
-- `DFunLike.coe (β := fun x ↦ Π₀ (i : ι), ↥(A i))`
erw [DFinsupp.mapRange.linearEquiv_apply]
simp only [DFinsupp.mapRange_single, Basis.repr_symm_apply, linearCombination_single, one_smul, toModule]
-- Similarly here.
erw [DFinsupp.lsum_single]
simp only [Submodule.coe_subtype]
