centralizer_tensorProduct_eq_center_tensorProduct_left

English

Analogous to left version, the centralizer of map(id_A) on A ⊗ B equals the tensor product with the center of B.

Русский

Аналогично левой версии, центральизатор map(id_A) над A ⊗ B равен A ⊗ центр B.

LaTeX

$$$\operatorname{centralizer}_R\left(\operatorname{map}(\text{id}_R A, \operatorname{AlgHom.id} R B) \right) = \operatorname{range}(\operatorname{map}(\operatorname{center}_R(A), \operatorname{id}_R B))$$$

Lean4

theorem centralizer_tensorProduct_eq_center_tensorProduct_left [Module.Free R B] :
    Subalgebra.centralizer R (Algebra.TensorProduct.map (AlgHom.id R A) (Algebra.ofId R B)).range =
      (Algebra.TensorProduct.map (Subalgebra.center R A).val (AlgHom.id R B)).range :=
  by
  rw [← centralizer_coe_range_includeLeft_eq_center_tensorProduct]
  simp [Algebra.TensorProduct.map_range]

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