algebraMap_def' — Mathlib

English

A refined unit formula for the algebra map into the graded tensor product, using an inclusion to express the map as unit tensor algebra image.

Русский

Уточнённая формула единицы для алгебраического отображения в градуированное тензорное произведение, через включение.

LaTeX

$$$\mathrm{algebraMap}_R(\mathcal{A} ⊗[R] \mathcal{B}) r = 1 ⊗_Rr$$$

Lean4

theorem algebraMap_def' (r : R) : algebraMap R (𝒜 ᵍ⊗[R] ℬ) r = 1 ᵍ⊗ₜ[R] algebraMap R B r :=
  (includeRight 𝒜 ℬ).commutes r |>.symm

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