toTensorAlgebra_gMul — Mathlib

English

The embedding respects multiplication: the image of a product of graded components equals the product of images.

Русский

Встраивание сохраняет умножение: образ произведения компонент градации равен произведению их образов.

LaTeX

$$$ TensorPower.toTensorAlgebra (GradedMonoid.GMul.mul a b) = TensorPower.toTensorAlgebra a \; * \; TensorPower.toTensorAlgebra b $$$

Lean4

@[simp]
theorem toTensorAlgebra_gMul {i j} (a : (⨂[R]^i) M) (b : (⨂[R]^j) M) :
    TensorPower.toTensorAlgebra (@GradedMonoid.GMul.mul _ (fun n => ⨂[R]^n M) _ _ _ _ a b) =
      TensorPower.toTensorAlgebra a * TensorPower.toTensorAlgebra b :=
  by
  -- change `a` and `b` to `tprod R a` and `tprod R b`

  rw [TensorPower.gMul_eq_coe_linearMap, ← LinearMap.compr₂_apply, ← @LinearMap.mul_apply' R, ← LinearMap.compl₂_apply,
    ← LinearMap.comp_apply]
  refine LinearMap.congr_fun (LinearMap.congr_fun ?_ a) b
  clear! a b
  ext (a b)
  simp only [LinearMap.compMultilinearMap_apply, LinearMap.compr₂_apply, ← gMul_def, TensorProduct.mk_apply,
    LinearEquiv.coe_coe, tprod_mul_tprod, toTensorAlgebra_tprod, TensorAlgebra.tprod_apply, LinearMap.comp_apply,
    LinearMap.compl₂_apply]
  refine Eq.trans ?_ List.prod_append
  congr
  rw [List.ofFn_comp' _ (TensorAlgebra.ι R), List.ofFn_comp' _ (TensorAlgebra.ι R),
    List.ofFn_comp' _ (TensorAlgebra.ι R), ← List.map_append, List.ofFn_fin_append]

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