Properties of centers and centralizers

This file contains theorems about the center and centralizer of a subalgebra.

Main results

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.

theorem Subalgebra.centralizer_sup {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (S T : Subalgebra R A) : centralizer R ↑(S ⊔ T) = centralizer R ↑S ⊓ centralizer R ↑T

theorem Subalgebra.centralizer_range_includeLeft_eq_center_tensorProduct (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (B : Type u_3) [Semiring B] [Algebra R B] [Module.Free R B] : centralizer R ↑Algebra.TensorProduct.includeLeft.range = (Algebra.TensorProduct.map (center R A).val (AlgHom.id R B)).range

Let R be a commutative ring and A, B be R-algebras where B is free as R-module. Then the centralizer of A ⊆ A ⊗ B is C(A) ⊗ B where C(A) is the center of A.

theorem Subalgebra.centralizer_range_includeRight_eq_center_tensorProduct (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (B : Type u_3) [Semiring B] [Algebra R B] [Module.Free R A] : centralizer R ↑Algebra.TensorProduct.includeRight.range = (Algebra.TensorProduct.map (AlgHom.id R A) (center R B).val).range

Let R be a commutative ring and A, B be R-algebras where A is free as R-module. Then the centralizer of B ⊆ A ⊗ B is A ⊗ C(B) where C(B) is the center of B.

theorem Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_left (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (B : Type u_3) [Semiring B] [Algebra R B] [Module.Free R B] : centralizer R ↑(Algebra.TensorProduct.map (AlgHom.id R A) (Algebra.ofId R B)).range = (Algebra.TensorProduct.map (center R A).val (AlgHom.id R B)).range

theorem Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_right (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (B : Type u_3) [Semiring B] [Algebra R B] [Module.Free R A] : centralizer R ↑(Algebra.TensorProduct.map (Algebra.ofId R A) (AlgHom.id R B)).range = (Algebra.TensorProduct.map (AlgHom.id R A) (center R B).val).range