map_restrictScalars_comp_includeRight

English

The inverse associator sends a ⊗ (b ⊗ c) to (a ⊗ b) ⊗ c.

Русский

Обратный ассоциатор отправляет a ⊗ (b ⊗ c) в (a ⊗ b) ⊗ c.

LaTeX

$$$ (\\mathrm{assoc}_{R,S,A,C,D})^{-1}(a \\otimes (b \\otimes c)) = (a \\otimes b) \\otimes c $$$

Lean4

@[simp]
theorem map_restrictScalars_comp_includeRight (f : A →ₐ[S] C) (g : B →ₐ[R] D) :
    ((map f g).restrictScalars R).comp includeRight = includeRight.comp g :=
  AlgHom.ext <| by simp

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