English
Dual statement to IncludeLeft: the centralizer of the image under IncludeRight is the image of the centralizer under the right map.
Русский
Двойственное утверждение IncludeRight: центральизатор образа IncludeRight равен образу центральizатора через правое отображение.
LaTeX
$$$\operatorname{centralizer}_R\left(\operatorname{map}(\text{id}, \operatorname{centralizer}_R(S))\right) = \operatorname{range}(\operatorname{map}(\text{id}, \operatorname{centralizer}_R(S)))$$$
Lean4
/-- Let `R` be a commutative ring and `A, B` be `R`-algebras where `A` is free as `R`-module.
For any subalgebra `S` of `B`, the centralizer of `1 ⊗ S ⊆ A ⊗ B` is `A ⊗ C_B(S)` where `C_B(S)` is
the centralizer of `S` in `B`.
-/
theorem centralizer_coe_map_includeRight_eq_center_tensorProduct (S : Subalgebra R B) [Module.Free R A] :
Subalgebra.centralizer R (S.map (Algebra.TensorProduct.includeRight (R := R) (A := A))) =
(Algebra.TensorProduct.map (AlgHom.id R A) (Subalgebra.centralizer R (S : Set B)).val).range :=
centralizer_coe_image_includeRight_eq_center_tensorProduct R A B S
