English
Equality of centralizers for the left tensor product: centralizer of map(id_A) on A ⊗ B equals centralizer of center on A tensored with id_B.
Русский
Равенство центральизаторов для левого тензорного произведения: centralizer( map(id_A) ) = centralizer(center(A)) ⊗ B.
LaTeX
$$$\operatorname{centralizer}_R\left(\operatorname{map}(\operatorname{id}_R A, \text{Algebra.TensorProduct}.includeLeft) \right) = \operatorname{range}(\operatorname{map}(\operatorname{center}_R(A), \mathrm{id}_B))$$$
Lean4
/-- Let `R` be a commutative ring and `A, B` be `R`-algebras where `A` is free as `R`-module.
Then the centralizer of `1 ⊗ B ⊆ A ⊗ B` is `A ⊗ C(B)` where `C(B)` is the center of `B`.
-/
theorem centralizer_range_includeRight_eq_center_tensorProduct [Module.Free R A] :
Subalgebra.centralizer R (Algebra.TensorProduct.includeRight : B →ₐ[R] A ⊗[R] B).range =
(Algebra.TensorProduct.map (AlgHom.id R A) (center R B).val).range :=
by
rw [← centralizer_univ, ← Algebra.coe_top (R := R) (A := B), ←
centralizer_coe_map_includeRight_eq_center_tensorProduct R A B ⊤]
ext
simp [includeRight]
