Commit 2025-01-25 06:17 7e84e128

feat(Algebra/Subalgebra): some lemmas about centralizers (#18764) Let R be a commutative ring and A and B two R-algebras.

• Subalgebra.centralizer_sup: if S and T are subalgebras of A, then the centralizer of S ⊔ T is the intersection of the centralizer of S and the centralizer of T.
• Subalgebra.centralizer_range_includeLeft_eq_center_tensorProduct: if B is free as a module, then the centralizer of A in A ⊗ B is C(A) ⊗ B where C(A) is the center of A.
• Subalgebra.centralizer_range_includeRight_eq_center_tensorProduct: if A is free as a module, then the centralizer of B in A ⊗ B is A ⊗ C(B) where C(B) is the center of B.