algebraMap_def — Mathlib

English

For r in R, the algebra map from R to the graded tensor product sends r to (algebraMap_R A r) ⊗ 1.

Русский

Для r в R алгебраическое отображение из R в градуированное тензорное произведение отправляет r в (algebraMap_R A r) ⊗ 1.

LaTeX

$$$\mathrm{algebraMap}_R(\mathcal{A} \otimes_R \mathcal{B})(r) = (\mathrm{algebraMap}_R A r) \otimes 1$$$

Lean4

theorem algebraMap_def (r : R) : algebraMap R (𝒜 ᵍ⊗[R] ℬ) r = algebraMap R A r ᵍ⊗ₜ[R] 1 :=
  rfl

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