Irreducible Lie submodules are the atoms of the submodule lattice

LieModule.IsIrreducible R L N is a statement about the lattice LieSubmodule R L N of the Lie submodules of N itself, whereas IsAtom N is a statement about the position of N in the lattice LieSubmodule R L M of the Lie submodules of the ambient module. This file proves that the two agree, so that a lattice-theoretic decomposition into atoms may be read as a decomposition into irreducibles. It also records that every nonzero vector of an irreducible module generates the whole module as a Lie submodule, and, dually, that the quotient by a Lie submodule is irreducible exactly when that submodule is a coatom.

Both directions move along the inclusion N.incl : N →ₗ⁅R,L⁆ M, whose map and comap connect the two lattices: LieSubmodule.map_incl_lt_iff_lt_top says that a proper Lie submodule of N maps to a Lie submodule strictly below N, while LieSubmodule.comap_incl_eq_top and LieSubmodule.comap_incl_eq_bot read the two extremes of a comap back in the ambient module. The coatom statement runs the same way along the projection LieSubmodule.Quotient.mk' N instead.

Main results

• Ado.isIrreducible_iff_isAtom: a Lie submodule is irreducible as a Lie module exactly when it is an atom of the lattice of Lie submodules of the ambient module.
• Ado.lieSpan_singleton_eq_top_of_ne_zero: every nonzero vector of an irreducible Lie module generates the whole module.
• Ado.lieSpan_singleton_eq_top_of_lieSpan_eq: the generator of a cyclic Lie submodule generates that submodule, read as a Lie module in its own right.
• Ado.eq_top_of_mem_of_lieSpan_singleton_eq_top: a Lie submodule containing a generator of the ambient module is the whole module.
• Ado.isIrreducible_quotient_iff_isCoatom: the quotient of a Lie module by a Lie submodule is irreducible exactly when that submodule is a coatom of the lattice of Lie submodules.

References

This supports Layer 0 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, where TauCeti/Algebra/Lie/Sl2/Decomposition.lean decomposes a finite-dimensional sl₂-module into irreducibles by decomposing its lattice of Lie submodules into atoms.

theorem Ado.lieSpan_singleton_eq_top_of_ne_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule.IsIrreducible R L M] {m : M} (hm : m ≠ 0) : LieSubmodule.lieSpan R L {m} = ⊤

Every nonzero vector generates an irreducible Lie module. If M is irreducible and m : M is nonzero, then the Lie submodule spanned by m is all of M.

theorem Ado.lieSpan_singleton_eq_top_of_lieSpan_eq {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {m : M} (h : LieSubmodule.lieSpan R L {m} = N) : LieSubmodule.lieSpan R L {⟨m, ⋯⟩} = ⊤

The generator of a cyclic Lie submodule generates it. If a Lie submodule N of M is spanned by a single vector m, then that vector, read inside N, spans the whole of N. Otherwise the Lie submodule of N it spans would map to a Lie submodule strictly below N (LieSubmodule.map_incl_lt_iff_lt_top), which nonetheless still contains m.

theorem Ado.eq_top_of_mem_of_lieSpan_singleton_eq_top {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {m : M} (hm : m ∈ N) (hgen : LieSubmodule.lieSpan R L {m} = ⊤) : N = ⊤

A Lie submodule containing a generator of the ambient module is the whole module.

theorem Ado.isIrreducible_iff_isAtom {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : LieModule.IsIrreducible R L ↥N ↔ IsAtom N

The irreducible Lie submodules are the atoms. A Lie submodule N of M is irreducible as a Lie module exactly when it is an atom of LieSubmodule R L M, that is, when N ≠ ⊥ and the only Lie submodule of M strictly below N is ⊥.

theorem Ado.isIrreducible_quotient_iff_isCoatom {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieAlgebra R L] [LieModule R L M] {N : LieSubmodule R L M} : LieModule.IsIrreducible R L (M ⧸ N) ↔ IsCoatom N

The quotient by a Lie submodule is irreducible exactly when that submodule is a coatom. A Lie submodule of M ⧸ N pulls back along the projection to a Lie submodule of M containing N, which a coatom N forces to be either N itself, when the submodule is ⊥, or all of M, when it is ⊤. Conversely, a Lie submodule strictly above N has a nonzero, hence full, image in an irreducible M ⧸ N, and it contains N, so it is everything.

This is the Lie analogue of isSimpleModule_iff_isCoatom, which does not apply: the Lie submodules of M ⧸ N are not the submodules of M ⧸ N.