centralizer_tensorProduct_eq_center_tensorProduct_right

English

Equality of centralizers for right-tensor construction with A-free: centralizer of map(id_A) on A ⊗ B equals centralizer of center(B).

Русский

Повторное утверждение центральизатора для правого тензорного произведения: centralizer = центр B.

LaTeX

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

Lean4

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

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