tprodMonoidHom — Mathlib

English

There is a natural monoid homomorphism from the product of the factors to the PiTensorProduct given by the tprod map; it preserves multiplication and unit.

Русский

Существует естественный моноидогомоморфизм из произведения факторов в PiTensorProduct, заданный отображением tprod; он сохраняет произведение и единицу.

LaTeX

$$$tprodMonoidHom\\ :\\ (\\prod_i A_i)\\to\\ ⨂_R i, A_i$$$

Lean4

/-- `PiTensorProduct.tprod` as a `MonoidHom`. -/
@[simps]
def tprodMonoidHom : (Π i, A i) →* ⨂[R] i, A i where
  toFun := tprod R
  map_one' := rfl
  map_mul' x y := (tprod_mul_tprod x y).symm

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