English
Given an internal direct sum decomposition of M and bases v_i for each A_i, the disjoint union of these bases forms a basis for M. The repr of the collected basis is obtained by composing the inverse of the isomorphism with the map that collects coordinates from the v_i.
Русский
При заданном внутреннем разложении M и базах v_i для каждого A_i, несмежная объединение этих баз образует базис для M. Представление объединённого базиса получается как композиция обратного изоморфизма и операции сбора координат по v_i.
LaTeX
$$$\text{collectedBasis} : (\text{IsInternal } A) \to (\text{Basis} (\Sigma i, α_i) R M)$ и его_repr = (LinearEquiv.ofBijective(\mathrm{coeLinearMap} A) \;\text{h}).symm ≫ DFinsupp.mapRange.linearEquiv (v i).repr ≫ (\sigmaFc)^{-1}$$$
Lean4
@[simp]
theorem ofBijective_coeLinearMap_same (h : IsInternal A) {i : ι} (x : A i) :
(LinearEquiv.ofBijective (coeLinearMap A) h).symm x i = x := by
rw [← coeLinearMap_of, LinearEquiv.ofBijective_symm_apply_apply, of_eq_same]
