Isotypic Lie modules

This file defines isotypy for Lie modules over a commutative ring. It is the Lie-module analogue of Mathlib's module-theoretic IsIsotypicOfType, IsIsotypic, and isotypicComponent interface. The definitions here do not depend on a universal enveloping algebra; the comparison with Mathlib's module-theoretic interface lives in TauCeti.Algebra.Lie.UniversalEnveloping.Isotypic.

Main definitions

• LieModule.IsIsotypicOfType and LieModule.IsIsotypic: Lie-module isotypy.
• LieModule.isotypicComponent: the sum of Lie submodules equivalent to a fixed type.

Roadmap

This is the generic Lie-isotypy interface used by Layer 6 of the Lie highest-weight roadmap and its universal-enveloping-algebra dictionary.

References

• Mathlib/RingTheory/SimpleModule/Isotypic.lean (Junyan Xu): the module-theoretic definitions and proof pattern ported here to Lie submodules and Lie-module equivalences.

def LieModule.IsIsotypicOfType (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Type u_1) [AddCommGroup S] [Module R S] [LieRingModule L S] : Prop

A Lie module M is isotypic of type S if every irreducible Lie submodule of M is equivalent to S.

Equations

• LieModule.IsIsotypicOfType R L M S = ∀ (P : LieSubmodule R L M) [LieModule.IsIrreducible R L ↥P], Nonempty (↥P ≃ₗ⁅R,L⁆ S)

theorem LieModule.isIsotypicOfType_iff (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Type u_1) [AddCommGroup S] [Module R S] [LieRingModule L S] : IsIsotypicOfType R L M S ↔ ∀ (P : LieSubmodule R L M) [IsIrreducible R L ↥P], Nonempty (↥P ≃ₗ⁅R,L⁆ S)

Lie isotypy of a fixed type means that every irreducible Lie submodule is equivalent to that type.

def LieModule.IsIsotypic (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Prop

A Lie module is isotypic if all its irreducible Lie submodules are equivalent.

Equations

• LieModule.IsIsotypic R L M = ∀ (P : LieSubmodule R L M) [LieModule.IsIrreducible R L ↥P], LieModule.IsIsotypicOfType R L M ↥P

theorem LieModule.isIsotypic_iff (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : IsIsotypic R L M ↔ ∀ (P : LieSubmodule R L M) [IsIrreducible R L ↥P], IsIsotypicOfType R L M ↥P

A Lie module is isotypic exactly when it is isotypic of the type of each irreducible Lie submodule.

theorem LieModule.IsIsotypicOfType.isIsotypic {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {S : Type u_1} [AddCommGroup S] [Module R S] [LieRingModule L S] (h : IsIsotypicOfType R L M S) : IsIsotypic R L M

A fixed isotypic type makes every pair of irreducible Lie submodules equivalent.

noncomputable def LieModule.isotypicComponent (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Type u_1) [AddCommGroup S] [Module R S] [LieRingModule L S] : LieSubmodule R L M

The Lie isotypic component of type S, defined as the sum of all Lie submodules equivalent to S.

Equations

• LieModule.isotypicComponent R L M S = sSup {P : LieSubmodule R L M | Nonempty (↥P ≃ₗ⁅R,L⁆ S)}

theorem LieModule.isotypicComponent_def (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Type u_1) [AddCommGroup S] [Module R S] [LieRingModule L S] : isotypicComponent R L M S = sSup {P : LieSubmodule R L M | Nonempty (↥P ≃ₗ⁅R,L⁆ S)}

The Lie isotypic component is the sum of all Lie submodules equivalent to its type.

@[simp]

theorem LieModule.isotypicComponent_le_iff (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Type u_1) [AddCommGroup S] [Module R S] [LieRingModule L S] (N : LieSubmodule R L M) : isotypicComponent R L M S ≤ N ↔ ∀ (P : LieSubmodule R L M), Nonempty (↥P ≃ₗ⁅R,L⁆ S) → P ≤ N

The Lie isotypic component is below N exactly when every submodule equivalent to its type is below N.

theorem LieSubmodule.le_isotypicComponent_of_equiv (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (P : LieSubmodule R L M) (S : Type u_1) [AddCommGroup S] [Module R S] [LieRingModule L S] (h : Nonempty (↥P ≃ₗ⁅R,L⁆ S)) : P ≤ LieModule.isotypicComponent R L M S

A Lie submodule equivalent to S is contained in the Lie isotypic component of type S.

theorem LieSubmodule.le_isotypicComponent (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (P : LieSubmodule R L M) : P ≤ LieModule.isotypicComponent R L M ↥P

A Lie submodule is contained in its Lie isotypic component.