toDirectSum_tensorPower_tprod — Mathlib

English

The direct sum embedding of the tprod over Fin n equals the direct sum embedding of the tensor power factors.

Русский

Встраивание прямой суммы tprod по Fin n эквивалентно встраиванию каждой факторной тензорной степени в прямую сумму.

LaTeX

$$$ toDirectSum (tprod R M n x) = DirectSum.of _ n (PiTensorProduct.tprod R x) $$$

Lean4

theorem toDirectSum_tensorPower_tprod {n} (x : Fin n → M) :
    toDirectSum (tprod R M n x) = DirectSum.of _ n (PiTensorProduct.tprod R x) :=
  by
  rw [tprod_apply, map_list_prod, List.map_ofFn]
  simp_rw [Function.comp_def, toDirectSum_ι]
  rw [DirectSum.list_prod_ofFn_of_eq_dProd]
  apply DirectSum.of_eq_of_gradedMonoid_eq
  rw [GradedMonoid.mk_list_dProd]
  rw [TensorPower.list_prod_gradedMonoid_mk_single]

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