Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.PBW.Homogeneous

Homogeneous pieces of the PBW map #

The degree-n piece of a symmetric algebra is defined to be the n-th power of the range of its canonical generator map, and these pieces form an internal direct sum. For a Lie algebra L over a commutative ring R, the canonical map

SymmetricAlgebra R L →ₐ[R] gr U(L)

sends this submodule into the n-th PBW graded piece. This file packages the resulting degreewise linear map, proves that it is surjective, and deduces surjectivity of the ambient map.

The proof uses the spanning half of PBW. A word of length exactly n maps to the corresponding product of degree-one classes. A shorter word represents zero in the n-th successive quotient. Consequently every class in that quotient has a homogeneous symmetric representative of degree n.

The component maps also govern injectivity. An element of the kernel of the canonical map decomposes into homogeneous terms, each of which lands in a distinct summand of the associated graded and hence lies in the kernel of its own component map. So the canonical map is injective, giving the linear-independence half of the Poincaré--Birkhoff--Witt theorem, exactly when every component map is; the componentwise description reduces both halves to a degreewise statement, while retaining the global associated-graded map.

Main definitions and results #

References #

source
noncomputable def TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousComponentMap (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) :
↥(SymmetricAlgebra.homogeneousSubmodule R L n) →ₗ[R] PBWGradedPiece R L n

The degree-n component of the canonical PBW map. Its source is the homogeneous symmetric submodule, and its target is the n-th PBW graded quotient.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousComponentMap_apply (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (p : ↥(SymmetricAlgebra.homogeneousSubmodule R L n)) :
    (pbwHomogeneousComponentMap R L n) p = (DirectSum.component R ℕ (PBWGradedPiece R L) n) ((pbwAssociatedGradedMap R L) ↑p)

    The degree-n component map is the n-th direct-sum component of the canonical PBW map.

    This is not a simp lemma: together with pbwAssociatedGradedMap_apply_homogeneous, which rewrites in the opposite direction, it would cycle.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap_apply_homogeneous (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (p : ↥(SymmetricAlgebra.homogeneousSubmodule R L n)) :
    (pbwAssociatedGradedMap R L) ↑p = (DirectSum.of (PBWGradedPiece R L) n) ((pbwHomogeneousComponentMap R L n) p)

    A homogeneous symmetric element maps to the direct-sum inclusion of its degreewise PBW component.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousComponentMap_prod_map_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (l : List L) :
    (pbwHomogeneousComponentMap R L l.length) ⟨(List.map (⇑(SymmetricAlgebra.ι R L)) l).prod, ⋯⟩ = Submodule.Quotient.mk ⟨(List.map (⇑(UniversalEnvelopingAlgebra.ι R)) l).prod, ⋯⟩

    The degree-n component map sends a product of n symmetric-algebra generators to the class of the corresponding word of Lie generators.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousComponentMap_surjective (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) :
    Function.Surjective ⇑(pbwHomogeneousComponentMap R L n)

    Every PBW graded piece has a homogeneous symmetric representative of the same degree. This is the degreewise form of surjectivity of the canonical map Sym(L) → gr U(L).

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap_surjective (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
    Function.Surjective ⇑(pbwAssociatedGradedMap R L)

    The canonical map from the symmetric algebra onto the PBW associated graded is surjective. It is enough to hit each homogeneous generator of the direct sum, which is the degreewise statement.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap_eq_map_decompose (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : SymmetricAlgebra R L) :
    (pbwAssociatedGradedMap R L) x = (DirectSum.map fun (n : ℕ) => (pbwHomogeneousComponentMap R L n).toAddMonoidHom) ((DirectSum.decompose (SymmetricAlgebra.homogeneousSubmodule R L)) x)

    The canonical map is the direct sum of its degreewise components: it first decomposes a symmetric element into its homogeneous parts and then applies pbwHomogeneousComponentMap in each degree.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap_injective_iff (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
    Function.Injective ⇑(pbwAssociatedGradedMap R L) ↔ ∀ (n : ℕ), Function.Injective ⇑(pbwHomogeneousComponentMap R L n)

    The canonical map Sym(L) → gr U(L) is injective exactly when all of its degreewise components are. This is the degreewise reduction of the linear-independence half of the Poincaré--Birkhoff--Witt theorem: the homogeneous submodules decompose the symmetric algebra, and the canonical map carries the degree-n piece into the n-th summand of the associated graded.