toMatrix₂'_compl₁₂ — Mathlib

English

Recover the original bilinear form from its matrix by applying the two-step process and using the standard identifications; the map from Matrix to LinearMap₂' is inverse to LinearMap.toMatrix₂'.

Русский

Восстановите билинейную форму по ее матрице через двукратное соответствие; отображение Matrix→LinearMap₂′ является обратным по отношению к LinearMap.toMatrix₂'.

LaTeX

$$$\mathrm{toLinearMap}_{\mathrm{sl}2}'(R, \sigma_1, \sigma_2)\bigl(\mathrm{toMatrix}_{\mathrm{sl}2}'(R)\Bigr) = B$ for appropriate $B$; equivalently, the two identifications are inverses.$$

Lean4

@[simp]
theorem toMatrix₂'_compl₁₂ (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (l : (n' → R) →ₗ[R] n → R) (r : (m' → R) →ₗ[R] m → R) :
    toMatrix₂' R (B.compl₁₂ l r) = (toMatrix' l)ᵀ * toMatrix₂' R B * toMatrix' r :=
  by
  ext i j
  simp only [LinearMap.toMatrix₂'_apply, LinearMap.compl₁₂_apply, transpose_apply, Matrix.mul_apply,
    LinearMap.toMatrix', LinearEquiv.coe_mk, LinearMap.coe_mk, AddHom.coe_mk, sum_mul]
  rw [sum_comm]
  conv_lhs => rw [← LinearMap.sum_repr_mul_repr_mul (Pi.basisFun R n) (Pi.basisFun R m) (l _) (r _)]
  rw [Finsupp.sum_fintype]
  · apply sum_congr rfl
    rintro i' -
    rw [Finsupp.sum_fintype]
    · apply sum_congr rfl
      rintro j' -
      simp only [smul_eq_mul, Pi.basisFun_repr, mul_assoc, mul_comm, mul_left_comm, Pi.basisFun_apply, of_apply]
    · intros
      simp only [zero_smul, smul_zero]
  · intros
    simp only [zero_smul, Finsupp.sum_zero]

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