right_isScalarTower — Mathlib

English

There is a specialized extensionality principle for AlgHom on A ⊗_R B to C: two homomorphisms are equal if they agree on pure tensors and satisfy the scalar-tower coherence.

Русский

Существует специализированный принцип экстентности для AlgHom на A ⊗_R B → C: два гомоморфизма равны, если они согласованы на чистых тензорах и удовлетворяют совместимости со структурой скаляров.

LaTeX

$$$\forall a,b:\ f(a\otimes b)=g(a\otimes b)\Rightarrow f=g$$$

Lean4

instance right_isScalarTower : IsScalarTower R B (A ⊗[R] B) :=
  IsScalarTower.of_algebraMap_eq fun r => (Algebra.TensorProduct.includeRight.commutes r).symm

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