An internal direct sum of Lie submodules is an external one #
A family N : ι → LieSubmodule R L M whose underlying submodules decompose M
(DirectSum.IsInternal) presents M as the external direct sum ⨁ i, N i, which carries
Mathlib's Lie module structure on a direct sum. This file records the comparison: the sum map
⨁ i, N i → M is a morphism of Lie modules (DirectSum.coeLieModuleHom), and it is an equivalence
exactly when the decomposition is internal (DirectSum.lieModuleEquivOfIsInternal).
DirectSum.IsInternal is a statement about the underlying Submodules, so it carries no
equivariance on its own; that is what is added here. With the equivalence in hand, a construction
applied to M can be computed summand by summand, which is how the multiplicity of an irreducible
in M is read off a decomposition of M into irreducibles in
TauCeti/Algebra/Lie/Multiplicity.lean.
The file closes with the regrouping theorem
DirectSum.nonempty_lieModuleEquiv_sigma_of_isInternal: a decomposition of M whose summands are
labelled by a map c : ι → σ, the summand N i being equivalent to a fixed module S (c i),
rewrites as M ≃ ⨁_{s} S s ^ m s with m s the number of indices carrying the label s. It is
the shape in which a decomposition into irreducibles is packaged once the summands are named: σ
is a set of names for the irreducibles, c sends a summand to the name of its isomorphism class,
and m is the multiplicity.
Main definitions #
DirectSum.coeLieModuleHom: the sum map⨁ i, N i →ₗ⁅R,L⁆ M, refining Mathlib'sDirectSum.coeLinearMap.DirectSum.lieModuleEquivOfIsInternal: the resulting equivalence of Lie modules⨁ i, N i ≃ₗ⁅R,L⁆ M, for an internal decomposition.
Main results #
DirectSum.coeLieModuleHom_toLinearMapandDirectSum.coeLieModuleHom_bijective_iff: the sum map refinesDirectSum.coeLinearMap, so its bijectivity isDirectSum.IsInternal.DirectSum.IsInternal.lieModuleProjection: the canonical equivariant projection onto one summand, included back into the ambient module.DirectSum.IsInternal.sum_lieModuleProjection_apply: over a finite index type these projections sum to the identity.DirectSum.nonempty_lieModuleEquiv_sigma_of_isInternal: an internal decomposition regrouped by the labels of its summands.Ado.LieModule.finrank_lieModuleHom_eq_sum_of_isInternal: the finrank of a morphism space is additive over an internal decomposition of its target.
Roadmap #
This is infrastructure for the decomposition toolkit of Layer 6 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose multiplicity target
isotypicMultiplicity counts the summands of a decomposition of M into irreducibles; the
decompositions it counts are produced by Ado.exists_isInternal_isIrreducible of
TauCeti/Algebra/Lie/Submodule/Decomposition.lean, in exactly the DirectSum.IsInternal form
consumed here.
The sum map of a family of Lie submodules, ⨁ i, N i → M, as a morphism of Lie modules.
Its underlying linear map is DirectSum.coeLinearMap
(DirectSum.coeLieModuleHom_toLinearMap), so DirectSum.IsInternal is exactly the statement that
it is bijective.
Equations
- DirectSum.coeLieModuleHom N = { toLinearMap := DirectSum.coeLinearMap fun (i : ι) => ↑(N i), map_lie' := ⋯ }
Instances For
The underlying linear map of the sum map of a family of Lie submodules is Mathlib's
DirectSum.coeLinearMap of the underlying submodules.
The sum map of a family of Lie submodules is bijective exactly when the family decomposes M
internally: by DirectSum.coeLieModuleHom_toLinearMap the two statements are about the same
underlying map.
An internal direct sum of Lie submodules, as an external one. A family of Lie submodules
whose underlying submodules decompose M presents M as the direct sum of the family, as Lie
modules.
Equations
Instances For
The underlying linear equivalence of the internal Lie-module decomposition is the canonical
equivalence supplied by DirectSum.IsInternal.
The canonical projection onto an internal Lie-module summand. It extracts one component through the internal direct-sum equivalence and includes that component back into the ambient module.
Equations
- h.lieModuleProjection i = (N i).incl.comp ((DirectSum.lieModuleComponent R ι L (fun (j : ι) => ↥(N j)) i).comp (DirectSum.lieModuleEquivOfIsInternal N h).symm.toLieModuleHom)
Instances For
Applying the canonical projection returns the selected internal direct-sum component.
The underlying linear map of the equivariant summand projection is the canonical projection of the underlying internal direct sum, followed by the summand inclusion.
Over a finite index type the equivariant projections onto the summands sum to the identity.
The canonical projection fixes every element of the selected summand.
The canonical projection vanishes on every other summand.
The canonical projection is idempotent.
The range of the canonical projection is exactly its selected summand.
An internal decomposition regrouped by the labels of its summands. Suppose the Lie
submodules N i decompose M internally, that each N i is equivalent to a member S (c i) of a
family of Lie modules indexed by σ, and that m s counts the indices labelled s. Then M is
the direct sum, over the pairs of a label s and a counter in Fin (m s), of S s.
Only Nonempty is asserted: the equivalence depends on the labelling and on the choice of an
equivalence N i ≃ S (c i) for each i, so there is no canonical one to name.
Additivity of the morphism space over a decomposition of the target. If the Lie submodules
N i decompose M and every component morphism space is finite-dimensional, the finrank of
S →ₗ⁅K,L⁆ M is the sum of the finranks of the S →ₗ⁅K,L⁆ N i.