English
The centralizer of the range of IncludeLeft equals the range of the map from the center of A to B; i.e., centralizer of IncludeLeft.range = map(center(A), id).range.
Русский
Центральизатор диапазона IncludeLeft равен диапазону отображения от центра A к B; то есть centralizer(IncludeLeft.range) = map(center(A), id).range.
LaTeX
$$$\operatorname{centralizer}_R\bigl(\operatorname{IncludeLeft}.range\bigr) = \operatorname{range}(\operatorname{map}(\operatorname{center}_R(A), \text{id}))$$$
Lean4
/-- Let `R` be a commutative ring and `A, B` be `R`-algebras where `B` is free as `R`-module.
Then the centralizer of `A ⊗ 1 ⊆ A ⊗ B` is `C(A) ⊗ B` where `C(A)` is the center of `A`.
-/
theorem centralizer_coe_range_includeLeft_eq_center_tensorProduct [Module.Free R B] :
Subalgebra.centralizer R (Algebra.TensorProduct.includeLeft : A →ₐ[R] A ⊗[R] B).range =
(Algebra.TensorProduct.map (Subalgebra.center R A).val (AlgHom.id R B)).range :=
by
rw [← centralizer_univ, ← Algebra.coe_top (R := R) (A := A), ←
centralizer_coe_map_includeLeft_eq_center_tensorProduct R A B ⊤]
ext
simp [includeLeft, includeLeftRingHom]
