algebraMap_basisOfBasisRight_repr_apply

English

The coordinates of the right basis under the representation correspond to the coordinates under the original basis via the algebra map.

Русский

Координаты базиса справа под представлением соответствуют координатам исходного базиса через алгебраическое отображение.

LaTeX

$$$\text{algebraMap}_{A E}( (H.basisOfBasisRight H' b).repr x i ) = \text{algebraMap}_{F E}( b.repr x i )$$$

Lean4

theorem algebraMap_basisOfBasisRight_repr_apply (H : A.LinearDisjoint B) (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤)
    {ι : Type*} (b : Basis ι F B) (x : B) (i : ι) :
    algebraMap A E ((H.basisOfBasisRight H' b).repr x i) = algebraMap F E (b.repr x i) :=
  (linearDisjoint_iff'.mp H).algebraMap_basisOfBasisRight_repr_apply H' b x i

Похожие утверждения