Schur's lemma for simple modules

This file packages the two forms of Schur's lemma used by the semisimple-algebra development.

For simple modules over an arbitrary ring, Mathlib proves that a linear map is either bijective or zero (LinearMap.bijective_or_eq_zero). Consequently the entire hom group vanishes exactly when the two modules are not linearly equivalent. When an equivalence does exist, Mathlib's LinearEquiv.arrowCongrAddEquiv identifies the hom group with either endomorphism ring by composition; no separate construction is needed here.

Over an algebraically closed field k, a domain algebra that is integral over k is k itself. The proof uses Mathlib's theorem that the algebra map from an algebraically closed field into such an algebra is bijective; a finite-dimensional division algebra is the special case that the roadmap names, integrality there coming from finite dimensionality. The same collapse for the endomorphism ring of a finite-dimensional simple module is Mathlib's IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed, packaged here as an algebra equivalence.

Both forms are then read as statements about dimensions, for a k-algebra A acting on modules that are k-modules compatibly: the hom space between inequivalent simple modules has dimension 0, and between equivalent finite-dimensional simple modules it is a line. Transporting a hom space along an isomorphism of its target, TauCeti.homCongrRight, is what carries the endomorphism computation to an arbitrary equivalent target.

Main definitions

• TauCeti.homCongrRight: isomorphic A-modules have k-isomorphic hom spaces out of a fixed module. This is LinearEquiv.congrRight for a noncommutative A, with the auxiliary scalars k supplying the linear structure that A cannot; it is assembled from Mathlib's LinearMap.compRight.

Main results

• TauCeti.hom_eq_zero_of_isEmpty_linearEquiv: every map between inequivalent simple modules is zero.
• TauCeti.subsingleton_linearMap_iff_isEmpty_linearEquiv: the corresponding characterization of the whole hom group.
• TauCeti.nontrivial_linearMap_iff_nonempty_linearEquiv: two simple modules are equivalent exactly when their hom group is nontrivial.
• TauCeti.nonempty_algEquiv_self_of_isIntegral: a domain algebra over an algebraically closed field that is integral over that field is isomorphic to it as an algebra, with TauCeti.nonempty_algEquiv_self_of_finiteDimensional_divisionRing the finite-dimensional division algebra special case, also available under the name the roadmap pins, TauCeti.algEquiv_self_of_finiteDimensional_divisionRing.
• TauCeti.endAlgEquivSelfOfIsSimpleModule: the endomorphism ring of a finite-dimensional simple module over an algebraically closed field collapses to that field, canonically, as the inverse of the structure map; TauCeti.nonempty_end_algEquiv_self_of_isSimpleModule is its existence form.
• TauCeti.finrank_linearMap_eq_zero_of_isEmpty_linearEquiv and TauCeti.finrank_linearMap_eq_one_of_nonempty_linearEquiv: the two forms of Schur's lemma in dimensions, with TauCeti.finiteDimensional_linearMap_of_isSimpleModule recording that the hom space is finite-dimensional either way.

References

This implements Layer 1, "Schur, assembled", of the semisimple algebras roadmap. See N. Jacobson, Basic Algebra II, Chapter 3, or T. Y. Lam, A First Course in Noncommutative Rings, Chapter 1.

Maps between simple modules

theorem TauCeti.hom_eq_zero_of_isEmpty_linearEquiv {R : Type u} [Ring R] {M : Type v} {N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsSimpleModule R M] [IsSimpleModule R N] (h : IsEmpty (M ≃ₗ[R] N)) (f : M →ₗ[R] N) : f = 0

Schur's lemma, vanishing form. A linear map between simple modules is zero if the two modules are not linearly equivalent.

The IsEmpty hypothesis is the constructive form of saying that no equivalence exists.

theorem TauCeti.subsingleton_linearMap_of_isEmpty_linearEquiv {R : Type u} [Ring R] {M : Type v} {N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsSimpleModule R M] [IsSimpleModule R N] (h : IsEmpty (M ≃ₗ[R] N)) : Subsingleton (M →ₗ[R] N)

The hom group between simple modules is a subsingleton if the modules are not linearly equivalent.

theorem TauCeti.subsingleton_linearMap_iff_isEmpty_linearEquiv {R : Type u} [Ring R] {M : Type v} {N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsSimpleModule R M] [IsSimpleModule R N] : Subsingleton (M →ₗ[R] N) ↔ IsEmpty (M ≃ₗ[R] N)

The hom group between two simple modules is a subsingleton exactly when the modules are not linearly equivalent.

theorem TauCeti.nontrivial_linearMap_iff_nonempty_linearEquiv {R : Type u} [Ring R] {M : Type v} {N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsSimpleModule R M] [IsSimpleModule R N] : Nontrivial (M →ₗ[R] N) ↔ Nonempty (M ≃ₗ[R] N)

The hom group between two simple modules is nontrivial exactly when the modules are linearly equivalent. This is the existence form of Schur's lemma.

Domain algebras over algebraically closed fields

theorem TauCeti.nonempty_algEquiv_self_of_isIntegral {k : Type u} {D : Type v} [Field k] [IsAlgClosed k] [Ring D] [IsDomain D] [Algebra k D] [Algebra.IsIntegral k D] : Nonempty (D ≃ₐ[k] k)

A domain algebra over an algebraically closed field k that is integral over k is k itself, as an isomorphism of algebras.

Mathlib proves that the algebra map from an algebraically closed field to such an algebra is bijective; this packages that bijection as an algebra equivalence.

theorem TauCeti.nonempty_algEquiv_self_of_finiteDimensional_divisionRing {k : Type u} {D : Type v} [Field k] [IsAlgClosed k] [DivisionRing D] [Algebra k D] [FiniteDimensional k D] : Nonempty (D ≃ₐ[k] k)

A finite-dimensional division algebra over an algebraically closed field is the field itself, as an isomorphism of algebras. Finite dimensionality supplies integrality, so this is the special case of nonempty_algEquiv_self_of_isIntegral that the semisimple-algebra development uses.

theorem TauCeti.algEquiv_self_of_finiteDimensional_divisionRing {k : Type u} {D : Type v} [Field k] [IsAlgClosed k] [DivisionRing D] [Algebra k D] [FiniteDimensional k D] : Nonempty (D ≃ₐ[k] k)

The roadmap pins the previous theorem under this name; it is available under both.

Endomorphisms of a simple module over an algebraically closed field

noncomputable def TauCeti.endAlgEquivSelfOfIsSimpleModule {k : Type u} {A : Type v} {S : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [IsSimpleModule A S] [FiniteDimensional k S] : Module.End A S ≃ₐ[k] k

Schur's lemma over an algebraically closed field. The endomorphism ring of a finite-dimensional simple module over a k-algebra is the field k itself.

Mathlib's IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed proves that every such endomorphism is a scalar; this packages that bijection as an algebra equivalence. Finite dimensionality is needed: an infinite-dimensional simple module can have a larger division endomorphism ring.

The equivalence involves no choices: it is the inverse of the structure map k → End A S, which Schur's lemma proves bijective. Its inverse is therefore algebraMap on the nose, and the scalar attached to an endomorphism is characterized by TauCeti.endAlgEquivSelfOfIsSimpleModule_smul.

Equations

• TauCeti.endAlgEquivSelfOfIsSimpleModule = (AlgEquiv.ofBijective (Algebra.ofId k (Module.End A S)) ⋯).symm

@[simp]

theorem TauCeti.endAlgEquivSelfOfIsSimpleModule_symm_apply {k : Type u} {A : Type v} {S : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [IsSimpleModule A S] [FiniteDimensional k S] (c : k) : endAlgEquivSelfOfIsSimpleModule.symm c = (algebraMap k (Module.End A S)) c

The inverse of the Schur equivalence is the structure map of the endomorphism algebra.

@[simp]

theorem TauCeti.endAlgEquivSelfOfIsSimpleModule_smul {k : Type u} {A : Type v} {S : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [IsSimpleModule A S] [FiniteDimensional k S] (f : Module.End A S) (s : S) : endAlgEquivSelfOfIsSimpleModule f • s = f s

The scalar attached to an endomorphism of a simple module is the scalar it acts by.

theorem TauCeti.nonempty_end_algEquiv_self_of_isSimpleModule {k : Type u} {A : Type v} {S : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [IsSimpleModule A S] [FiniteDimensional k S] : Nonempty (Module.End A S ≃ₐ[k] k)

The existence statement of Schur's lemma over an algebraically closed field, for consumers that only need to know that some algebra equivalence exists.

Transporting a hom space along an isomorphism of the target

def TauCeti.homCongrRight (k : Type u_1) {A : Type u_2} [CommSemiring k] [Semiring A] [Algebra k A] {S : Type u_3} [AddCommMonoid S] [Module A S] {N : Type u_4} [AddCommMonoid N] [Module A N] [Module k N] [IsScalarTower k A N] {P : Type u_5} [AddCommMonoid P] [Module A P] [Module k P] [IsScalarTower k A P] (e : N ≃ₗ[A] P) : (S →ₗ[A] N) ≃ₗ[k] S →ₗ[A] P

Isomorphic targets give isomorphic hom spaces. An A-linear isomorphism e : N ≃ₗ[A] P carries S →ₗ[A] N to S →ₗ[A] P by postcomposition, k-linearly.

This is LinearEquiv.congrRight with the auxiliary scalars k in place of a commutativity assumption on A: since A is not assumed commutative the hom spaces are not A-modules, and k, acting on the targets compatibly with A, supplies the linear structure instead. The two directions are LinearMap.compRight.

Equations

• TauCeti.homCongrRight k e = LinearEquiv.ofLinearMap (LinearMap.compRight k ↑e) (LinearMap.compRight k ↑e.symm) ⋯ ⋯

@[simp]

theorem TauCeti.homCongrRight_apply (k : Type u_1) {A : Type u_2} [CommSemiring k] [Semiring A] [Algebra k A] {S : Type u_3} [AddCommMonoid S] [Module A S] {N : Type u_4} [AddCommMonoid N] [Module A N] [Module k N] [IsScalarTower k A N] {P : Type u_5} [AddCommMonoid P] [Module A P] [Module k P] [IsScalarTower k A P] (e : N ≃ₗ[A] P) (f : S →ₗ[A] N) (s : S) : ((homCongrRight k e) f) s = e (f s)

@[simp]

theorem TauCeti.homCongrRight_symm_apply (k : Type u_1) {A : Type u_2} [CommSemiring k] [Semiring A] [Algebra k A] {S : Type u_3} [AddCommMonoid S] [Module A S] {N : Type u_4} [AddCommMonoid N] [Module A N] [Module k N] [IsScalarTower k A N] {P : Type u_5} [AddCommMonoid P] [Module A P] [Module k P] [IsScalarTower k A P] (e : N ≃ₗ[A] P) (f : S →ₗ[A] P) (s : S) : ((homCongrRight k e).symm f) s = e.symm (f s)

Schur's lemma in dimension form

theorem TauCeti.finrank_linearMap_eq_zero_of_isEmpty_linearEquiv {k : Type u_1} {A : Type u_2} {S : Type u_3} {N : Type u_4} [Field k] [Ring A] [Algebra k A] [AddCommGroup S] [Module A S] [IsSimpleModule A S] [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N] [IsSimpleModule A N] (h : IsEmpty (S ≃ₗ[A] N)) : Module.finrank k (S →ₗ[A] N) = 0

Schur's lemma, vanishing form, in dimensions. Between inequivalent simple modules the hom space is trivial, hence of dimension zero.

theorem TauCeti.finiteDimensional_linearMap_of_isEmpty_linearEquiv {k : Type u_1} {A : Type u_2} {S : Type u_3} {N : Type u_4} [Field k] [Ring A] [Algebra k A] [AddCommGroup S] [Module A S] [IsSimpleModule A S] [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N] [IsSimpleModule A N] (h : IsEmpty (S ≃ₗ[A] N)) : FiniteDimensional k (S →ₗ[A] N)

The hom space between inequivalent simple modules is finite-dimensional, being trivial.

theorem TauCeti.finrank_linearMap_eq_one_of_nonempty_linearEquiv {k : Type u_1} {A : Type u_2} {S : Type u_3} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [IsSimpleModule A S] [FiniteDimensional k S] {N : Type u_4} [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N] (e : S ≃ₗ[A] N) : Module.finrank k (S →ₗ[A] N) = 1

Schur's lemma over an algebraically closed field, in dimensions. Between equivalent finite-dimensional simple modules the hom space is a line: every map is a scalar multiple of a fixed isomorphism.

theorem TauCeti.finiteDimensional_linearMap_of_isSimpleModule {k : Type u_1} {A : Type u_2} {S : Type u_3} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [IsSimpleModule A S] [FiniteDimensional k S] {N : Type u_4} [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N] [IsSimpleModule A N] : FiniteDimensional k (S →ₗ[A] N)

The hom space out of a finite-dimensional simple module into a simple module is finite-dimensional: by Schur's lemma it is a line or trivial.