productLeftAlgHom — Mathlib

English

The two-sided tensor product symmetry is itself symmetric under swapping the bases.

Русский

Симметрия тензорного произведения слева и справа симметрична при обмене базисов.

LaTeX

$$tensorTensorTensorComm_symm : (tensorTensorTensorComm R R' S T A B C D).symm = tensorTensorTensorComm R S R' T A C B D$$

Lean4

/-- If `A`, `B`, `C` are `R`-algebras, `A` and `C` are also `S`-algebras (forming a tower as
`·/S/R`), then the product map of `f : A →ₐ[S] C` and `g : B →ₐ[R] C` is an `S`-algebra
homomorphism.

This is just a special case of `Algebra.TensorProduct.lift` for when `C` is commutative. -/
abbrev productLeftAlgHom (f : A →ₐ[S] C) (g : B →ₐ[R] C) : A ⊗[R] B →ₐ[S] C :=
  lift f g (fun _ _ => Commute.all _ _)

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