The double centralizer theorem

Mathlib's Jacobson density theorem (Module.Finite.toModuleEnd_moduleEnd_surjective) says that for a semisimple R-module M which is finite over its endomorphism ring D = Module.End R M, the natural map R → Module.End D M is surjective. This file sharpens that to a bijection for a faithful such M, so that R is recovered from its action: R ≃+* Module.End D M.

The half that is missing upstream is injectivity, and injectivity is exactly faithfulness of M. Faithfulness is not automatic, but it is automatic in the case the structure theory cares about: a nontrivial module over a simple ring is faithful, because the elements killing M form a two-sided ideal not containing 1. So over a simple ring every nontrivial semisimple module finite over D gives R ≃+* Module.End D M. When M is simple, this is the Wedderburn presentation in module-internal form: no ambient base field is involved, only finiteness over D.

The last section restates the theorem in the form a representation uses: for a subalgebra A of Module.End K N over which N is semisimple, the double centralizer of A inside Module.End K N is A itself. Here faithfulness is automatic, A being a set of endomorphisms, so only Mathlib's surjectivity is needed; the centralizer A' is the ring of A-linear endomorphisms of N, and an element of A'' is exactly an A'-linear endomorphism. This is a different theorem from TauCeti.centralizer_centralizer of TauCeti/Algebra/CentralSimple/Centralizer.lean, which computes the double centralizer of a central simple subalgebra of a central simple algebra by a dimension count; neither hypothesis implies the other.

Main results

• TauCeti.faithfulSMul_of_isSimpleRing: a nontrivial module over a simple ring is faithful.
• TauCeti.toModuleEnd_moduleEnd_bijective: the double centralizer theorem. For a faithful semisimple module M finite over D = Module.End R M, the map R → Module.End D M is bijective; TauCeti.ringEquivEndEnd packages it as a ring isomorphism, and TauCeti.algEquivEndEnd as an algebra isomorphism over a compatible base ring.
• TauCeti.toModuleEnd_moduleEnd_bijective_of_isSimpleRing: the specialization to a nontrivial semisimple module over a simple ring, where faithfulness is automatic.
• LinearIndependent.exists_smul_eq: the Jacobson-Chevalley form of density. Over a simple module, a single element of R carries any finite D-linearly independent family to an arbitrary family of targets.
• TauCeti.algEquivEndEndOfIsSimpleRing: the finite-dimensional-algebra form, where the finiteness hypothesis is supplied by finiteness over a commutative base ring acting compatibly.
• Subalgebra.centralizer_centralizer_of_isSemisimpleModule: the subalgebra form. A subalgebra A of Module.End K N over which N is semisimple, N finite over Module.End A N, is its own double centralizer inside Module.End K N.
• AlgHom.centralizer_centralizer_range: the same statement for the image of a semisimple algebra, the form a representation supplies. The image, not the algebra itself, is what the double centralizer returns, since the representation need not be faithful.
• Subalgebra.exists_mem_centralizer_apply_eq_iff_of_isSemisimpleModule and AlgHom.exists_mem_centralizer_range_apply_eq_iff: an endomorphism commuting with A (respectively with the image of a semisimple algebra) carries w to x exactly when everything in A killing w kills x.

Implementation notes

The finiteness hypothesis is Module.Finite (Module.End R M) M, finiteness over the endomorphism ring itself, rather than finite-dimensionality over an unrelated base ring. That is the hypothesis surjectivity of the action needs. When a base ring K acts compatibly, its scalars are R-linear endomorphisms, so Module.Finite K M gives it by Module.Finite.of_restrictScalars_finite.

A faithful simple module makes R a primitive ring, not necessarily a simple one, so TauCeti.toModuleEnd_moduleEnd_bijective is genuinely more general than its simple-ring corollary. It is also stated for a merely semisimple M, which is all that Mathlib's surjectivity needs.

The main theorem is named after the Mathlib lemma it sharpens, Module.Finite.toModuleEnd_moduleEnd_surjective, keeping the surjective/bijective pair in step.

References

See T. Y. Lam, A First Course in Noncommutative Rings, GTM 131, Chapter 4, and N. Jacobson, Basic Algebra II, Chapter 4.

Faithfulness over a simple ring

theorem TauCeti.faithfulSMul_of_isSimpleRing {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsSimpleRing R] [Nontrivial M] : FaithfulSMul R M

A nontrivial module over a simple ring is faithful: the elements of R killing M are the kernel of a ring homomorphism out of R, a two-sided ideal not containing 1, hence ⊥.

The double centralizer theorem

theorem TauCeti.toModuleEnd_moduleEnd_bijective (R : Type u_1) [Ring R] (M : Type u_2) [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [FaithfulSMul R M] [Module.Finite (Module.End R M) M] : Function.Bijective ⇑(Module.toModuleEnd (Module.End R M) M)

The double centralizer theorem. Let M be a faithful semisimple R-module which is finite over its endomorphism ring D = Module.End R M. Then the natural map R → Module.End D M is bijective: R is exactly the ring of D-linear endomorphisms of M.

This sharpens Mathlib's Module.Finite.toModuleEnd_moduleEnd_surjective from surjectivity to bijectivity; the extra input is faithfulness, which is what makes the map injective.

noncomputable def TauCeti.ringEquivEndEnd (R : Type u_1) [Ring R] (M : Type u_2) [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [FaithfulSMul R M] [Module.Finite (Module.End R M) M] : R ≃+* Module.End (Module.End R M) M

The double centralizer theorem as a ring isomorphism: a faithful semisimple module finite over its endomorphism ring D identifies R with Module.End D M.

Equations

• TauCeti.ringEquivEndEnd R M = RingEquiv.ofBijective (Module.toModuleEnd (Module.End R M) M) ⋯

@[simp]

theorem TauCeti.ringEquivEndEnd_apply {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [FaithfulSMul R M] [Module.Finite (Module.End R M) M] (r : R) (m : M) : ((ringEquivEndEnd R M) r) m = r • m

@[simp]

theorem TauCeti.ringEquivEndEnd_symm_smul {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [FaithfulSMul R M] [Module.Finite (Module.End R M) M] (f : Module.End (Module.End R M) M) (m : M) : (ringEquivEndEnd R M).symm f • m = f m

noncomputable def TauCeti.algEquivEndEnd (R : Type u_1) [Ring R] (M : Type u_2) [AddCommGroup M] [Module R M] (K : Type u_3) [CommSemiring K] [Algebra K R] [Module K M] [IsScalarTower K R M] [IsSemisimpleModule R M] [FaithfulSMul R M] [Module.Finite (Module.End R M) M] : R ≃ₐ[K] Module.End (Module.End R M) M

The double centralizer isomorphism as an isomorphism of K-algebras, for a commutative base ring K acting on M compatibly with R.

Equations

• TauCeti.algEquivEndEnd R M K = AlgEquiv.ofRingEquiv ⋯

@[simp]

theorem TauCeti.algEquivEndEnd_apply {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] (K : Type u_3) [CommSemiring K] [Algebra K R] [Module K M] [IsScalarTower K R M] [IsSemisimpleModule R M] [FaithfulSMul R M] [Module.Finite (Module.End R M) M] (r : R) (m : M) : ((algEquivEndEnd R M K) r) m = r • m

@[simp]

theorem TauCeti.algEquivEndEnd_symm_smul {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] (K : Type u_3) [CommSemiring K] [Algebra K R] [Module K M] [IsScalarTower K R M] [IsSemisimpleModule R M] [FaithfulSMul R M] [Module.Finite (Module.End R M) M] (f : Module.End (Module.End R M) M) (m : M) : (algEquivEndEnd R M K).symm f • m = f m

theorem TauCeti.toModuleEnd_moduleEnd_bijective_of_isSimpleRing (R : Type u_1) [Ring R] (M : Type u_2) [AddCommGroup M] [Module R M] [IsSimpleRing R] [IsSemisimpleModule R M] [Nontrivial M] [Module.Finite (Module.End R M) M] : Function.Bijective ⇑(Module.toModuleEnd (Module.End R M) M)

The double centralizer theorem for a simple ring. A nontrivial semisimple module over a simple ring is automatically faithful. If it is finite over its endomorphism ring D, it presents R as Module.End D M.

Jacobson-Chevalley density

theorem LinearIndependent.exists_smul_eq {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsSimpleModule R M] {ι : Type u_3} [Finite ι] {v : ι → M} (hv : LinearIndependent (Module.End R M) v) (w : ι → M) : ∃ (r : R), ∀ (i : ι), r • v i = w i

Jacobson-Chevalley density. For a simple module M, a finite linearly independent family over D = Module.End R M can be carried to an arbitrary family of targets by a single scalar from R. No finiteness assumption on M is needed.

Linear independence is essential: a D-linear relation among the v i is inherited by the r • v i, so the targets could not be arbitrary.

The finite-dimensional algebra case

noncomputable def TauCeti.algEquivEndEndOfIsSimpleRing (R : Type u_1) [Ring R] (M : Type u_2) [AddCommGroup M] [Module R M] (K : Type u_3) [CommSemiring K] [Algebra K R] [Module K M] [IsScalarTower K R M] [Module.Finite K M] [IsSimpleRing R] [IsSemisimpleModule R M] [Nontrivial M] : R ≃ₐ[K] Module.End (Module.End R M) M

The double centralizer theorem for a finite module over a simple algebra. If R is a simple K-algebra and M a nontrivial semisimple R-module finite as a K-module, then M presents R as the algebra of D-linear endomorphisms of M, where D = Module.End R M.

Equations

• TauCeti.algEquivEndEndOfIsSimpleRing R M K = TauCeti.algEquivEndEnd R M K

@[simp]

theorem TauCeti.algEquivEndEndOfIsSimpleRing_apply {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] (K : Type u_3) [CommSemiring K] [Algebra K R] [Module K M] [IsScalarTower K R M] [Module.Finite K M] [IsSimpleRing R] [IsSemisimpleModule R M] [Nontrivial M] (r : R) (m : M) : ((algEquivEndEndOfIsSimpleRing R M K) r) m = r • m

@[simp]

theorem TauCeti.algEquivEndEndOfIsSimpleRing_symm_smul {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] (K : Type u_3) [CommSemiring K] [Algebra K R] [Module K M] [IsScalarTower K R M] [Module.Finite K M] [IsSimpleRing R] [IsSemisimpleModule R M] [Nontrivial M] (f : Module.End (Module.End R M) M) (m : M) : (algEquivEndEndOfIsSimpleRing R M K).symm f • m = f m

The double centralizer of a subalgebra of an endomorphism algebra

theorem Subalgebra.centralizer_centralizer_of_isSemisimpleModule {K : Type u_3} [CommRing K] {N : Type u_4} [AddCommGroup N] [Module K N] (A : Subalgebra K (Module.End K N)) [Module.Finite (Module.End (↥A) N) N] [IsSemisimpleModule (↥A) N] : centralizer K ↑(centralizer K ↑A) = A

The double centralizer theorem inside an endomorphism algebra. Let A be a K-subalgebra of Module.End K N, and suppose N is semisimple as an A-module and finite over Module.End A N. Then A is its own double centralizer: an endomorphism commuting with everything that commutes with A already lies in A.

The inclusion A ≤ A'' is formal (Subalgebra.le_centralizer_centralizer); the content is the reverse one, which is Jacobson density. The centralizer A' is the ring of A-linear endomorphisms of N, so an element of A'' is an A'-linear endomorphism, and density writes every such endomorphism as the action of an element of A.

Finiteness is over Module.End A N, the hypothesis density actually needs; a caller with a finite K-module N gets it from Module.Finite.of_restrictScalars_finite.

theorem AlgHom.centralizer_centralizer_range {K : Type u_3} [CommRing K] {N : Type u_4} [AddCommGroup N] [Module K N] [Module.Finite K N] {S : Type u_5} [Ring S] [Algebra K S] [IsSemisimpleRing S] (ρ : S →ₐ[K] Module.End K N) : Subalgebra.centralizer K ↑(Subalgebra.centralizer K ↑ρ.range) = ρ.range

The double centralizer theorem for the image of a semisimple algebra. The image of a semisimple K-algebra S in Module.End K N, for a finite K-module N, is its own double centralizer.

The image is a quotient of S, hence semisimple, so N is a semisimple module over it and Subalgebra.centralizer_centralizer_of_isSemisimpleModule applies, its finiteness hypothesis coming from Module.Finite.of_restrictScalars_finite. It is the image and not S that is recovered: the representation S → Module.End K N need not be injective.

theorem Subalgebra.exists_mem_centralizer_apply_eq_iff_of_isSemisimpleModule {K : Type u_3} [CommRing K] {N : Type u_4} [AddCommGroup N] [Module K N] (A : Subalgebra K (Module.End K N)) [IsSemisimpleModule (↥A) N] {w x : N} : (∃ f ∈ centralizer K ↑A, f w = x) ↔ ∀ a ∈ A, a w = 0 → a x = 0

The centralizer moves vectors as freely as annihilators allow. Let A be a K-subalgebra of Module.End K N over which N is semisimple. Some endomorphism commuting with A sends w to x if and only if every element of A annihilating w also annihilates x.

theorem AlgHom.exists_mem_centralizer_range_apply_eq_iff {K : Type u_3} [CommRing K] {N : Type u_4} [AddCommGroup N] [Module K N] {S : Type u_5} [Ring S] [Algebra K S] [IsSemisimpleRing S] (ρ : S →ₐ[K] Module.End K N) {w x : N} : (∃ f ∈ Subalgebra.centralizer K (Set.range ⇑ρ), f w = x) ↔ ∀ (s : S), (ρ s) w = 0 → (ρ s) x = 0

The centralizer of a semisimple image moves vectors as freely as annihilators allow. For a semisimple K-algebra S acting on N through ρ, some endomorphism commuting with the image of ρ sends w to x if and only if every s with ρ s w = 0 also has ρ s x = 0.