English
Analogous statement for IncludeRight: the centralizer of the image under IncludeRight is the range of a map built from the centralizer of S in B.
Русский
Аналогичное утверждение для IncludeRight: центральизатор образа IncludeRight равен области значений отображения, построенного из центральизатора S в B.
LaTeX
$$$\operatorname{centralizer}_R(\operatorname{image}(\text{IncludeRight}(S))) = \operatorname{range}(\text{map}(id, C_R(S)))$$$
Lean4
/-- Let `R` be a commutative ring and `A, B` be `R`-algebras where `B` is free as `R`-module.
For any subset `S ⊆ 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_image_includeRight_eq_center_tensorProduct (S : Set B) [Module.Free R A] :
Subalgebra.centralizer R (Algebra.TensorProduct.includeRight '' S) =
(Algebra.TensorProduct.map (AlgHom.id R A) (Subalgebra.centralizer R (S : Set B)).val).range :=
by
have eq1 := centralizer_coe_image_includeLeft_eq_center_tensorProduct R B A S
apply_fun Subalgebra.comap (Algebra.TensorProduct.comm R A B).toAlgHom at eq1
convert eq1
· ext x
simpa [mem_centralizer_iff] using
⟨fun h b hb ↦ (Algebra.TensorProduct.comm R A B).symm.injective <| by aesop, fun h b hb ↦
(Algebra.TensorProduct.comm R A B).injective <| by aesop⟩
· ext x
simp only [AlgHom.mem_range, AlgEquiv.toAlgHom_eq_coe, mem_comap, AlgHom.coe_coe]
constructor
· rintro ⟨x, rfl⟩
exact ⟨(Algebra.TensorProduct.comm R _ _) x, by rw [Algebra.TensorProduct.comm_comp_map_apply]⟩
· rintro ⟨y, hy⟩
refine ⟨(Algebra.TensorProduct.comm R _ _) y, (Algebra.TensorProduct.comm R A B).injective ?_⟩
rw [← hy, comm_comp_map_apply, ← comm_symm, AlgEquiv.symm_apply_apply]
