English
From an internal direct sum decomposition and bases in each summand, produce a basis for the whole module by gathering the coordinates; this yields a Basis for the indexed product.
Русский
Из внутреннего декомпозиции и баз для каждого слагаемого получать базис для всей модуля, собирая координаты.
LaTeX
$$$\text{collectedBasis} : (\text{IsInternal } A) \to (\text{Basis} (\Sigma i, \alpha i) R M)$$$
Lean4
/-- Given an internal direct sum decomposition of a module `M`, and a basis for each of the
components of the direct sum, the disjoint union of these bases is a basis for `M`. -/
noncomputable def collectedBasis (h : IsInternal A) {α : ι → Type*} (v : ∀ i, Basis (α i) R (A i)) :
Basis (Σ i, α i) R M where
repr :=
((LinearEquiv.ofBijective (DirectSum.coeLinearMap A) h).symm ≪≫ₗ
DFinsupp.mapRange.linearEquiv fun i ↦ (v i).repr) ≪≫ₗ
(sigmaFinsuppLequivDFinsupp R).symm
