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 ⊗ 1 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 1 ⊗ B in A ⊗ B is A ⊗ C(B) where C(B) is the center of B.

theorem Subalgebra.le_centralizer_iff {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (S T : Subalgebra R A) : S ≤ centralizer R ↑T ↔ T ≤ centralizer R ↑S

theorem Subalgebra.centralizer_coe_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_coe_iSup {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {ι : Sort u_3} (S : ι → Subalgebra R A) : centralizer R ↑(⨆ (i : ι), S i) = ⨅ (i : ι), centralizer R ↑(S i)

theorem Subalgebra.centralizer_coe_image_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] (S : Set A) [Module.Free R B] : centralizer R (⇑Algebra.TensorProduct.includeLeft '' S) = (Algebra.TensorProduct.map (centralizer R S).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. For any subset S ⊆ 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 Subalgebra.centralizer_coe_image_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] (S : Set B) [Module.Free R A] : centralizer R (⇑Algebra.TensorProduct.includeRight '' S) = (Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val).range

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 Subalgebra.centralizer_coe_map_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] (S : Subalgebra R A) [Module.Free R B] : centralizer R ↑(map Algebra.TensorProduct.includeLeft S) = (Algebra.TensorProduct.map (centralizer R ↑S).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. 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 Subalgebra.centralizer_coe_map_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] (S : Subalgebra R B) [Module.Free R A] : centralizer R ↑(map Algebra.TensorProduct.includeRight S) = (Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R ↑S).val).range

Let R be a commutative ring and A, B be R-algebras where A is free as R-module. For any subalgebra S of 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 Subalgebra.centralizer_coe_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 ⊗ 1 ⊆ 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 1 ⊗ 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