mulMap_bot_left_eq — Mathlib

English

The product map with the bottom subalgebra on the left is the left inclusion composed with the left tensor map.

Русский

Произведение с нижним слева является композицией включения слева и левого тензорного отображения.

LaTeX

$$$\text{mulMap } \bot \; A = A.{val} \circ A.lTensorBot.toAlgHom$$$

Lean4

theorem mulMap_bot_left_eq : mulMap ⊥ A = A.val.comp A.lTensorBot.toAlgHom :=
  AlgHom.toLinearMap_injective (toSubmodule A).mulMap_one_left_eq

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