stdBasis_repr_eq_matrixToStdBasis_mul

English

The coordinate of commMap K x in the standard basis equals the product of matrixToStdBasis with x composed with indexEquiv.

Русский

Координаты образа под отображением commMap в стандартном базисе равны произведению matrixToStdBasis на x, композицию с indexEquiv.

LaTeX

$$$ ((stdBasis K).repr (commMap K x) c : \mathbb{C}) = (matrixToStdBasis K *ᵥ (x \circ (indexEquiv K))) c $$$

Lean4

/-- Let `x : (K →+* ℂ) → ℂ` such that `x_φ = conj x_(conj φ)` for all `φ : K →+* ℂ`, then the
representation of `commMap K x` on `stdBasis` is given (up to reindexing) by the product of
`matrixToStdBasis` by `x`. -/
theorem stdBasis_repr_eq_matrixToStdBasis_mul (x : (K →+* ℂ) → ℂ)
    (hx : ∀ φ, conj (x φ) = x (ComplexEmbedding.conjugate φ)) (c : index K) :
    ((stdBasis K).repr (commMap K x) c : ℂ) = (matrixToStdBasis K *ᵥ (x ∘ (indexEquiv K))) c :=
  by
  simp_rw [commMap, matrixToStdBasis, LinearMap.coe_mk, AddHom.coe_mk, mulVec, dotProduct, Function.comp_apply, index,
    Fintype.sum_sum_type, diagonal_one, reindex_apply, ← univ_product_univ, sum_product, indexEquiv_apply_isReal,
    Fin.sum_univ_two, indexEquiv_apply_isComplex_fst, indexEquiv_apply_isComplex_snd, smul_of, smul_cons, smul_eq_mul,
    mul_one, Matrix.smul_empty, Equiv.prodComm_symm, Equiv.coe_prodComm]
  cases c with
  | inl w =>
    simp_rw [stdBasis_apply_isReal, fromBlocks_apply₁₁, fromBlocks_apply₁₂, one_apply, Matrix.zero_apply, ite_mul,
      one_mul, zero_mul, sum_ite_eq, mem_univ, ite_true, add_zero, sum_const_zero, add_zero, ← conj_eq_iff_re,
      hx (embedding w.val), conjugate_embedding_eq_of_isReal w.prop]
  | inr c =>
    rcases c with ⟨w, j⟩
    fin_cases j
    · simp only [Fin.zero_eta, Fin.isValue, stdBasis_apply_isComplex_fst, re_eq_add_conj, mul_neg, fromBlocks_apply₂₁,
        zero_apply, zero_mul, sum_const_zero, fromBlocks_apply₂₂, submatrix_apply, Prod.swap_prod_mk,
        blockDiagonal_apply, of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one, ite_mul, cons_val_one,
        sum_add_distrib, sum_ite_eq, mem_univ, ↓reduceIte, ← hx (embedding w), zero_add]
      field_simp
    · simp only [Fin.mk_one, Fin.isValue, stdBasis_apply_isComplex_snd, im_eq_sub_conj, mul_neg, fromBlocks_apply₂₁,
        zero_apply, zero_mul, sum_const_zero, fromBlocks_apply₂₂, submatrix_apply, Prod.swap_prod_mk,
        blockDiagonal_apply, of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_one, ite_mul,
        neg_mul, sum_add_distrib, sum_ite_eq, mem_univ, ↓reduceIte, ← hx (embedding w), zero_add]
      ring_nf; simp [field]

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