Singleton basis projections commute with label-preserving equivalences
Provedmme_basisLabelProjection_comp_equiv_of_maps_basisbasisequivalencelinear-algebraprojection
Let two finite-dimensional modules carry bases indexed by the same finite label set. If a linear equivalence sends every source basis vector to the target basis vector with the same label, then it commutes with projection onto any singleton basis label.
Preamble
import Definitions.Def_mme_dwz_step1_mixed_selected_full_map_data open MME Module universe u set_option autoImplicit false
Formal statement
theorem mme_basisLabelProjection_comp_equiv_of_maps_basis
{K : Type u} [Field K]
{V V' : Type u} [AddCommGroup V] [Module K V]
[AddCommGroup V'] [Module K V']
{I : Type u} [Fintype I] [DecidableEq I]
(b : Basis I K V) (b' : Basis I K V') (e : V ≃ₗ[K] V')
(hbasis : ∀ a, e (b a) = b' a) (selected : I) :
(MME.DWZComponentRestriction.basisLabelProjection
b' id {selected}).comp e.toLinearMap =
e.toLinearMap.comp
(MME.DWZComponentRestriction.basisLabelProjection
b id {selected}) := by
sorrySource
Standard linear algebra: verification on a basis.