External direct sums of Lie modules #
This file supplements Mathlib/Algebra/Lie/DirectSum.lean, which puts a Lie module structure on an
external direct sum ⨁ i, Pᵢ and provides the inclusion DirectSum.lieModuleOf and the projection
DirectSum.lieModuleComponent as morphisms of Lie modules. Those two come with no application
lemmas; the ones saying they are the underlying DirectSum.of and evaluation are recorded here, so
that no consumer has to unfold either definition.
They are what makes the morphism space additive over a direct sum in its target: a morphism
from a Lie module S into a finite external direct sum is the family of its components, and a
finite family of components reassembles to the element it came from. That is
Ado.LieModule.lieModuleHomDirectSumEquiv.
The file also refines the two ways an external direct sum is transported to Mathlib's Lie module
structure: along a family of morphisms of the summands (DirectSum.lieModuleMap, refining
DirectSum.lmap, and DirectSum.lieModuleEquivCongrRight, refining
DirectSum.congrLinearEquiv) and along an equivalence of the index type
(DirectSum.lieModuleEquivCongrLeft, refining DirectSum.lequivCongrLeft). The bracket acts
summand by summand, so in each case the only thing to check is that Mathlib's underlying linear map
is equivariant; the _toLinearMap and _toLinearEquiv lemmas record which map that is, so that
Mathlib's API for it stays reachable.
Main definitions #
Ado.LieModule.lieModuleHomDirectSumEquiv: the morphism space is additive over a direct sum in its target,(S →ₗ⁅R,L⁆ ⨁ i, Pᵢ) ≃ₗ[R] Π i, (S →ₗ⁅R,L⁆ Pᵢ).DirectSum.lieModuleMapandDirectSum.lieModuleEquivCongrRight: a family of morphisms, respectively of equivalences, of the summands acts on the external direct sum.DirectSum.lieModuleEquivCongrLeft: reindexing an external direct sum of Lie modules along an equivalence of index types.
Main results #
DirectSum.lieModuleOf_applyandDirectSum.lieModuleComponent_apply: the inclusion and the projection of an external direct sum of Lie modules areDirectSum.ofand evaluation.
Roadmap #
This is infrastructure for the decomposition toolkit of Layer 6 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md: additivity of the morphism space
is the ingredient that TauCeti/Algebra/Lie/Schur.lean names as missing from its dimension form of
Schur's lemma, and with which TauCeti/Algebra/Lie/Multiplicity.lean reads a multiplicity off
dim_K (S →ₗ⁅K,L⁆ M). The transport definitions are what regroup a decomposition of a module into
irreducibles by isomorphism type, in
TauCeti/Algebra/Lie/Submodule/DirectSum.lean.
The inclusion of a summand into an external direct sum of Lie modules is DirectSum.of.
The projection of an external direct sum of Lie modules onto a summand is evaluation.
A family of morphisms of the summands, as a morphism of the external direct sums. Its
underlying linear map is Mathlib's DirectSum.lmap, so it acts componentwise; the bracket does
too, which is all that equivariance needs.
Equations
- DirectSum.lieModuleMap f = { toLinearMap := DirectSum.lmap fun (i : ι) => ↑(f i), map_lie' := ⋯ }
Instances For
The underlying linear map of a family of morphisms of the summands is Mathlib's
DirectSum.lmap, which is how its API is reached.
A family of equivalences of the summands, as an equivalence of the external direct sums.
Its underlying linear equivalence is Mathlib's DirectSum.congrLinearEquiv, whose inverse is
already the family of inverses; equivariance is that of the underlying DirectSum.lieModuleMap.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The underlying linear equivalence of a family of equivalences of the summands is Mathlib's
DirectSum.congrLinearEquiv, which is how its API is reached.
The inverse of a family of equivalences of the summands is the family of inverses.
Reindexing an external direct sum of Lie modules along an equivalence of index types. Its
underlying linear equivalence is Mathlib's DirectSum.lequivCongrLeft.
Equations
- DirectSum.lieModuleEquivCongrLeft R L h = { toLinearMap := ↑(DirectSum.lequivCongrLeft R h), map_lie' := ⋯, invFun := (DirectSum.lequivCongrLeft R h).invFun, left_inv := ⋯, right_inv := ⋯ }
Instances For
The underlying linear equivalence of a reindexing is Mathlib's DirectSum.lequivCongrLeft,
which is how its API is reached.
The morphism space is additive over a direct sum in its target. A morphism from S into a
finite external direct sum of Lie modules is the family of its components, and conversely a family
of morphisms assembles to one; this is an isomorphism of R-modules.
Equations
- One or more equations did not get rendered due to their size.