constantBaseRingEquiv — Mathlib

English

The algebra isomorphism from the tensor product over R of the constant family R with values indexed by ι to R itself sends the simple tensor tprod R x to the product ∏ i x_i.

Русский

Алгебраическое изоморфизм тензорного произведения по константному семейству R к R самим отображает элемент-«простую тензор»-tprod R x в произведение по индексам ∏_i x_i.

LaTeX

$$$\\text{constantBaseRingEquiv }_{ι,R}:\\; (⨂[R] _ : ι, R) \\cong\\_R R \\\\ (tprod\\ R\\ x) \\mapsto \\prod_i x_i$$$

Lean4

/-- The algebra equivalence from the tensor product of the constant family with
value `R` to `R`, given by multiplication of the entries.
-/
noncomputable def constantBaseRingEquiv : (⨂[R] _ : ι, R) ≃ₐ[R] R :=
  letI toFun := lift (MultilinearMap.mkPiAlgebra R ι R)
  AlgEquiv.ofAlgHom
    (AlgHom.ofLinearMap toFun ((lift.tprod _).trans Finset.prod_const_one)
      (by
        -- one of these is required, the other is a performance optimization

        letI : IsScalarTower R (⨂[R] x : ι, R) (⨂[R] x : ι, R) := IsScalarTower.right (R := R) (A := ⨂[R] (x : ι), R)
        letI : SMulCommClass R (⨂[R] x : ι, R) (⨂[R] x : ι, R) := Algebra.to_smulCommClass (R := R) (A := ⨂[R] x : ι, R)
        rw [LinearMap.map_mul_iff]
        ext
        change toFun (tprod R _ * tprod R _) = toFun (tprod R _) * toFun (tprod R _)
        simp_rw [tprod_mul_tprod, toFun, lift.tprod, MultilinearMap.mkPiAlgebra_apply, Pi.mul_apply,
          Finset.prod_mul_distrib]))
    (Algebra.ofId _ _) (by ext) (by classical ext)

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