piScalarRight — Mathlib

English

The scalar-tensor right isomorphism piScalarRight relates A ⊗_R (ι → R) with functions i ↦ A, acting by i-th scalar.

Русский

Изоморфизм масштаба справа piScalarRight связывает A ⊗_R (ι → R) с ι→A, действуя на i-ю координату.

LaTeX

$$piScalarRight : A ⊗_R (ι → R) ≃_A (ι → A)$$

Lean4

/-- Variant of `Algebra.TensorProduct.piRight` with constant factors. -/
def piScalarRight : A ⊗[R] (ι → R) ≃ₐ[S] ι → A :=
  (piRight R S A (fun _ : ι ↦ R)).trans <| AlgEquiv.piCongrRight (fun _ ↦ Algebra.TensorProduct.rid R S A)

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