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