leftMulMatrix_basisOfBasisRight_algebraMap

English

The left multiplication matrix of the A-basisRight basis under multiplication by x corresponds to the left multiplication matrix of b via the appropriate RingHom map.

Русский

Матрица левого умножения относительно базиса A применяется к x и совпадает с матрицей левого умножения по базису b через соответствующее отображение кольца.

LaTeX

$$$\\mathrm{leftMulMatrix}(H.basisOfBasisRight H' b)(\\mathrm{algebraMap}_{B\\to S} x) = \\mathrm{RingHom.mapMatrix}(\\mathrm{algebraMap}_{R\\to A}, \\mathrm{leftMulMatrix}_B b x)$$$

Lean4

theorem leftMulMatrix_basisOfBasisRight_algebraMap (H' : A ⊔ B = ⊤) {ι : Type*} [Fintype ι] [DecidableEq ι]
    (b : Basis ι R B) (x : B) :
    Algebra.leftMulMatrix (H.basisOfBasisRight H' b) (algebraMap B S x) =
      RingHom.mapMatrix (algebraMap R A) (Algebra.leftMulMatrix b x) :=
  by
  ext
  simp [Algebra.leftMulMatrix_eq_repr_mul, ← H.algebraMap_basisOfBasisRight_repr_apply H']

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