Semisimple

Results named in Tau Ceti's TauCeti.RingTheory.Semisimple modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe 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.

TauCeti.toModuleEnd_moduleEnd_bijective.{u_1, u_2} (R : Type u_1) [Ring R] (M : Type u_2)
  [AddCommGroup M] [_root_.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)

Lean

Formalized in Tau Ceti as TauCeti.toModuleEnd_moduleEnd_bijective.

Other forms

The double centralizer theorem for a finite module over a simple algebra. Formalized in Tau Ceti as TauCeti.algEquivEndEndOfIsSimpleRing.

TauCeti.algEquivEndEndOfIsSimpleRing.{u_1, u_2, u_3} (R : Type u_1) [Ring R] (M : Type u_2)
  [AddCommGroup M] [_root_.Module R M] (K : Type u_3) [CommSemiring K] [Algebra K R]
  [_root_.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 simple ring. Formalized in Tau Ceti as TauCeti.toModuleEnd_moduleEnd_bijective_of_isSimpleRing.

TauCeti.toModuleEnd_moduleEnd_bijective_of_isSimpleRing.{u_1, u_2} (R : Type u_1) [Ring R]
  (M : Type u_2) [AddCommGroup M] [_root_.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 the image of a semisimple algebra. Formalized in Tau Ceti as AlgHom.centralizer_centralizer_range.

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

The double centralizer theorem inside an endomorphism algebra. Formalized in Tau Ceti as Subalgebra.centralizer_centralizer_of_isSemisimpleModule.

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

Sources

• Tau Ceti documentation: TauCeti.toModuleEnd_moduleEnd_bijective
• Source of TauCeti.toModuleEnd_moduleEnd_bijective in TauCeti/RingTheory/Semisimple/DoubleCentralizer.lean

LeanTauCeti.toModuleEnd_moduleEnd_bijective · TauCeti.algEquivEndEndOfIsSimpleRing · TauCeti.toModuleEnd_moduleEnd_bijective_of_isSimpleRing · AlgHom.centralizer_centralizer_range · Subalgebra.centralizer_centralizer_of_isSemisimpleModule

Used by 1

Used bySchur-Weyl duality: the commutant of the image of k[S_d] is the image of k[GLₙ]

TheoremThe multiplicity theorem#

If M decomposes as a finite direct sum of simple modules N i, then the dimension of the space of A-linear maps from a simple module S into M is the number of factors isomorphic to S.

Only the right-hand side mentions the decomposition, so this is the statement that the multiplicity of S in M is an invariant of M; see TauCeti.natCard_eq_natCard_of_linearEquiv_pi.

TauCeti.finrank_linearMap_eq_natCard_of_linearEquiv_pi.{u_1, u_2, u_3, u_4, u_5, u_6} {k : Type u_1}
  {A : Type u_2} {S : Type u_3} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [AddCommGroup S]
  [_root_.Module k S] [_root_.Module A S] [IsScalarTower k A S] [IsSimpleModule A S]
  [FiniteDimensional k S] {ι : Type u_4} [Finite ι] {N : ι → Type u_5}
  [(i : ι) → AddCommGroup (N i)] [(i : ι) → _root_.Module k (N i)] [(i : ι) → _root_.Module A (N i)]
  [∀ (i : ι), IsScalarTower k A (N i)] [∀ (i : ι), IsSimpleModule A (N i)] {M : Type u_6}
  [AddCommGroup M] [_root_.Module k M] [_root_.Module A M] [IsScalarTower k A M]
  (e : M ≃ₗ[A] (i : ι) → N i) :
  Module.finrank k (S →ₗ[A] M) = Nat.card { i // Nonempty (S ≃ₗ[A] N i) }

Lean

Formalized in Tau Ceti as TauCeti.finrank_linearMap_eq_natCard_of_linearEquiv_pi.

Sources

• Tau Ceti documentation: TauCeti.finrank_linearMap_eq_natCard_of_linearEquiv_pi
• Source of TauCeti.finrank_linearMap_eq_natCard_of_linearEquiv_pi in TauCeti/RingTheory/Semisimple/Multiplicity.lean

LeanTauCeti.finrank_linearMap_eq_natCard_of_linearEquiv_pi

Uses 1 · Used by 2

Proof usesSchur's lemma, vanishing form

Used byThe isotypic decomposition of a semisimple module · Clifford's theorem, dimension form

TheoremThe multiplicity theorem for a product of simple modules#

The dimension of the space of A-linear maps from a simple module S into a finite product of simple modules counts the factors isomorphic to S.

TauCeti.finrank_linearMap_pi_eq_natCard.{u_1, u_2, u_3, u_4, u_5} {k : Type u_1} {A : Type u_2}
  {S : Type u_3} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [AddCommGroup S]
  [_root_.Module k S] [_root_.Module A S] [IsScalarTower k A S] [IsSimpleModule A S]
  [FiniteDimensional k S] {ι : Type u_4} [Finite ι] {N : ι → Type u_5}
  [(i : ι) → AddCommGroup (N i)] [(i : ι) → _root_.Module k (N i)] [(i : ι) → _root_.Module A (N i)]
  [∀ (i : ι), IsScalarTower k A (N i)] [∀ (i : ι), IsSimpleModule A (N i)] :
  Module.finrank k (S →ₗ[A] (i : ι) → N i) = Nat.card { i // Nonempty (S ≃ₗ[A] N i) }

Lean

Formalized in Tau Ceti as TauCeti.finrank_linearMap_pi_eq_natCard.

Sources

• Tau Ceti documentation: TauCeti.finrank_linearMap_pi_eq_natCard
• Source of TauCeti.finrank_linearMap_pi_eq_natCard in TauCeti/RingTheory/Semisimple/Multiplicity.lean

LeanTauCeti.finrank_linearMap_pi_eq_natCard

Uses 1

Proof usesSchur's lemma, vanishing form

TheoremSchur'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.

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

Lean

Formalized in Tau Ceti as TauCeti.hom_eq_zero_of_isEmpty_linearEquiv.

Other forms

Schur's lemma over an algebraically closed field. Formalized in Tau Ceti as TauCeti.endAlgEquivSelfOfIsSimpleModule.

TauCeti.endAlgEquivSelfOfIsSimpleModule.{u, v, w} {k : Type u} {A : Type v} {S : Type w} [Field k]
  [IsAlgClosed k] [Ring A] [Algebra k A] [AddCommGroup S] [_root_.Module k S] [_root_.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, in dimensions. Formalized in Tau Ceti as LinearEquiv.finrank_linearMap_eq_one.

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

Schur's lemma, vanishing form, in dimensions. Formalized in Tau Ceti as TauCeti.finrank_linearMap_eq_zero_of_isEmpty_linearEquiv.

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

Sources

• Tau Ceti documentation: TauCeti.hom_eq_zero_of_isEmpty_linearEquiv
• Source of TauCeti.hom_eq_zero_of_isEmpty_linearEquiv in TauCeti/RingTheory/Semisimple/Schur.lean

LeanTauCeti.hom_eq_zero_of_isEmpty_linearEquiv · TauCeti.endAlgEquivSelfOfIsSimpleModule · LinearEquiv.finrank_linearMap_eq_one · TauCeti.finrank_linearMap_eq_zero_of_isEmpty_linearEquiv

Used by 8

Used bySwan's theorem for ℤ_p[G] (NSW (5.6.10)(ii)) · The Biedenharn–Elliott pentagon identity · Burnside's vanishing theorem · The Frobenius formula · The general-field Cartan/Ext-Euler identity · Burnside density theorem · The multiplicity theorem · The multiplicity theorem for a product of simple modules

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.