Isotypic Lie modules through the universal enveloping algebra

This file transports Mathlib's isotypic-module interface across the universal-enveloping-algebra dictionary. For an irreducible target type, semisimplicity enters only in the characterization of an isotypic module by its unique component.

The generic equivalence and submodule interfaces live with the rest of the enveloping-algebra dictionary in TauCeti.Algebra.Lie.UniversalEnveloping.Module. The UEA-independent Lie-level predicates and component live in TauCeti.Algebra.Lie.Isotypic; this file identifies them with Mathlib's IsIsotypicOfType, IsIsotypic, and isotypicComponent through those interfaces.

Main results

• LieModule.isIsotypicOfType_iff_isIsotypicOfType_of_ι_smul: fixed-type isotypy transport for compatible actions.
• LieModule.isIsotypic_iff_isIsotypic_of_ι_smul: pairwise isotypy transport for compatible actions.
• LieModule.lieSubmoduleOrderIso_isotypicComponent: component transport for compatible actions.
• LieModule.isIsotypicOfType_isotypicComponent: the isotypic component of an irreducible type is isotypic of that type, so it really is the largest Lie submodule built from copies of it.
• LieModule.mem_isotypicComponent_iff_mem_isotypicComponent_asModule: canonical component membership normalization.
• LieModule.isotypicComponent_eq_top_iff_of_ι_smul: the top-component criterion for an irreducible type.

Roadmap

This is the universal-enveloping-algebra bridge for Layer 6 of the Lie highest-weight roadmap. It deliberately stops before highest-weight classification: consumers such as Kostant-form modules can state that all irreducible Lie submodules are equivalent without rebuilding ring-level isotypic machinery.

References

• Mathlib/RingTheory/SimpleModule/Isotypic.lean (Junyan Xu): the module-theoretic isotypic interface and top-component criterion transported through the enveloping-algebra dictionary.

theorem LieModule.isIsotypicOfType_iff_isIsotypicOfType_of_ι_smul {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (S : Type u_1) [AddCommGroup S] [Module R S] [LieRingModule L S] [LieModule R L S] [Module (UniversalEnvelopingAlgebra R L) S] [IsScalarTower R (UniversalEnvelopingAlgebra R L) S] (hS : ∀ (x : L) (s : S), (UniversalEnvelopingAlgebra.ι R) x • s = ⁅x, s⁆) : IsIsotypicOfType R L M S ↔ _root_.IsIsotypicOfType (UniversalEnvelopingAlgebra R L) M S

Lie-module isotypy of a fixed type is exactly Mathlib's module isotypy for compatible U(L)-actions.

theorem LieModule.isIsotypic_iff_isIsotypic_of_ι_smul {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) : IsIsotypic R L M ↔ _root_.IsIsotypic (UniversalEnvelopingAlgebra R L) M

Lie-module isotypy is exactly Mathlib's module isotypy for a compatible U(L)-action.

theorem LieModule.lieSubmoduleOrderIso_isotypicComponent {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (S : Type u_1) [AddCommGroup S] [Module R S] [LieRingModule L S] [LieModule R L S] [Module (UniversalEnvelopingAlgebra R L) S] [IsScalarTower R (UniversalEnvelopingAlgebra R L) S] (hS : ∀ (x : L) (s : S), (UniversalEnvelopingAlgebra.ι R) x • s = ⁅x, s⁆) : (TauCeti.UniversalEnvelopingAlgebra.lieSubmoduleOrderIso hM) (isotypicComponent R L M S) = _root_.isotypicComponent (UniversalEnvelopingAlgebra R L) M S

A compatible submodule dictionary maps the Lie isotypic component to Mathlib's U(L)-isotypic component.

theorem LieModule.mem_isotypicComponent_iff_mem_isotypicComponent_of_ι_smul {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) {S : Type u_1} [AddCommGroup S] [Module R S] [LieRingModule L S] [LieModule R L S] [Module (UniversalEnvelopingAlgebra R L) S] [IsScalarTower R (UniversalEnvelopingAlgebra R L) S] (hS : ∀ (x : L) (s : S), (UniversalEnvelopingAlgebra.ι R) x • s = ⁅x, s⁆) {m : M} : m ∈ isotypicComponent R L M S ↔ m ∈ _root_.isotypicComponent (UniversalEnvelopingAlgebra R L) M S

Membership in the Lie isotypic component is membership in the corresponding isotypic component for compatible U(L)-actions.

theorem LieModule.isotypicComponent_eq_top_iff_of_ι_smul {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (S : Type u_1) [AddCommGroup S] [Module R S] [LieRingModule L S] [LieModule R L S] [Module (UniversalEnvelopingAlgebra R L) S] [IsScalarTower R (UniversalEnvelopingAlgebra R L) S] (hS : ∀ (x : L) (s : S), (UniversalEnvelopingAlgebra.ι R) x • s = ⁅x, s⁆) [IsIrreducible R L S] [ComplementedLattice (LieSubmodule R L M)] : isotypicComponent R L M S = ⊤ ↔ IsIsotypicOfType R L M S

For compatible U(L)-actions, an irreducible type S, and a completely reducible Lie module, the isotypic component of type S is the whole module exactly when the Lie module is isotypic of type S.

@[simp]

theorem LieModule.mem_isotypicComponent_iff_mem_isotypicComponent_asModule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {S : Type u_1} [AddCommGroup S] [Module R S] [LieRingModule L S] [LieModule R L S] {m : M} : m ∈ isotypicComponent R L M S ↔ m ∈ _root_.isotypicComponent (UniversalEnvelopingAlgebra R L) M S

Membership in the Lie isotypic component is membership in the corresponding canonical U(L)-isotypic component.

theorem LieModule.isIsotypicOfType_isotypicComponent {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (S : Type u_1) [AddCommGroup S] [Module R S] [LieRingModule L S] [LieModule R L S] [IsIrreducible R L S] : IsIsotypicOfType R L (↥(isotypicComponent R L M S)) S

The Lie isotypic component of an irreducible type is isotypic of that type: every irreducible Lie submodule of the S-isotypic component of M is equivalent to S. This is Mathlib's IsIsotypicOfType.isotypicComponent read through the dictionary, and it is what makes the component the largest Lie submodule built from copies of S.