map_toAlgHom — Mathlib

English

The map f g, viewed as a tensor-product morphism, coincides with the AlgHom version: (map f g) = Algebra.TensorProduct.map (f) (g).

Русский

Отображение map f g совпадает с алгебраическим отображением типа Algebra.TensorProduct.map, полученным от f и g.

LaTeX

$$$\text{map } f\ g = \mathrm{Algebra.TensorProduct.map} (f) (g)$$$

Lean4

@[simp]
theorem map_toAlgHom (f : A →ₐc[S] C) (g : B →ₐc[R] D) :
    (map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D) = Algebra.TensorProduct.map (f : A →ₐ[S] C) (g : B →ₐ[R] D) :=
  rfl

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