Functoriality of the PBW filtration

Every homomorphism of Lie algebras induces a filtered homomorphism of their universal enveloping algebras: a word of at most k canonical generators is sent to a word of at most k canonical generators. Passing to successive quotients gives linear maps on the homogeneous pieces and an algebra homomorphism of PBW associated gradeds. The canonical map from the symmetric algebra is natural with respect to these homomorphisms.

The image statements retain information which an inclusion alone would discard. A split epimorphism maps each filtration step onto the corresponding target step. For a split monomorphism, the image of a filtration step is exactly the target step intersected with the range of the enveloping-algebra map. Consequently, an equivalence of Lie algebras identifies the filtration steps by linear equivalences.

These results do not use the Poincare--Birkhoff--Witt basis theorem. The exact image statement for an arbitrary injective Lie map over a field uses PBW and is proved in TauCeti/Algebra/Lie/UniversalEnveloping/PBW/Subalgebra.lean.

Main definitions and results

• TauCeti.UniversalEnvelopingAlgebra.map_mem_pbwFiltration and TauCeti.UniversalEnvelopingAlgebra.map_pbwFiltration_le: induced maps preserve PBW degree.
• TauCeti.UniversalEnvelopingAlgebra.mapFiltration: the induced linear map between filtration steps, functorial in the Lie homomorphism.
• TauCeti.UniversalEnvelopingAlgebra.map_pbwFiltration_eq_of_surjective and TauCeti.UniversalEnvelopingAlgebra.mapFiltration_surjective_of_surjective: surjective Lie maps induce exact images and surjections between corresponding filtration steps.
• TauCeti.UniversalEnvelopingAlgebra.map_pbwFiltration_eq_of_rightInverse: split epimorphisms map each filtration step onto the corresponding target step.
• TauCeti.UniversalEnvelopingAlgebra.map_pbwFiltration_eq_inf_range_of_leftInverse: for a split monomorphism, a source step maps to the intersection of the target step with the map's range.
• TauCeti.UniversalEnvelopingAlgebra.mapEquivFiltration: a Lie equivalence induces a linear equivalence on every filtration step.
• TauCeti.UniversalEnvelopingAlgebra.mapGradedPiece: the induced linear map on each successive quotient.
• TauCeti.UniversalEnvelopingAlgebra.mapAssociatedGraded: the induced algebra homomorphism of PBW associated gradeds.
• TauCeti.UniversalEnvelopingAlgebra.mapAssociatedGraded_comp_pbwAssociatedGradedMap: the canonical map from the symmetric algebra is natural.

theorem TauCeti.UniversalEnvelopingAlgebra.map_pbwFiltration_le (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (k : ℕ) : Submodule.map (map R f).toLinearMap (pbwFiltration R L k) ≤ pbwFiltration R M k

The image of a PBW filtration step under an induced enveloping-algebra map lies in the corresponding target step.

theorem TauCeti.UniversalEnvelopingAlgebra.map_mem_pbwFiltration (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) {k : ℕ} {x : UniversalEnvelopingAlgebra R L} (hx : x ∈ pbwFiltration R L k) : (map R f) x ∈ pbwFiltration R M k

A homomorphism of Lie algebras sends an element of PBW filtration degree at most k to one of degree at most k.

theorem TauCeti.UniversalEnvelopingAlgebra.map_pbwFiltrationPrevious_le (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (k : ℕ) : Submodule.map (map R f).toLinearMap (pbwFiltrationPrevious R L k) ≤ pbwFiltrationPrevious R M k

Induced enveloping-algebra maps also preserve the step immediately preceding a PBW filtration degree.

theorem TauCeti.UniversalEnvelopingAlgebra.map_mem_pbwFiltrationPrevious (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) {k : ℕ} {x : UniversalEnvelopingAlgebra R L} (hx : x ∈ pbwFiltrationPrevious R L k) : (map R f) x ∈ pbwFiltrationPrevious R M k

A homomorphism of Lie algebras sends an element of the step preceding PBW filtration degree k to one of the corresponding preceding step.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.mapFiltration (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (k : ℕ) : ↥(pbwFiltration R L k) →ₗ[R] ↥(pbwFiltration R M k)

The linear map between the k-th PBW filtration steps induced by a Lie homomorphism.

Equations

• TauCeti.UniversalEnvelopingAlgebra.mapFiltration R f k = (TauCeti.UniversalEnvelopingAlgebra.map R f).toLinearMap.restrict ⋯

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapFiltration_apply (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (k : ℕ) (x : ↥(pbwFiltration R L k)) : ↑((mapFiltration R f k) x) = (map R f) ↑x

The map between PBW filtration steps acts by the induced enveloping-algebra map.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapFiltration_id (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (k : ℕ) : mapFiltration R LieHom.id k = LinearMap.id

The identity Lie homomorphism induces the identity on each PBW filtration step.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapFiltration_comp (R : Type u) [CommRing R] {L : Type v} {M : Type w} {N : Type x} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [LieRing N] [LieAlgebra R N] (f : L →ₗ⁅R⁆ M) (g : M →ₗ⁅R⁆ N) (k : ℕ) : mapFiltration R (g.comp f) k = mapFiltration R g k ∘ₗ mapFiltration R f k

Composition of Lie homomorphisms becomes composition of their maps between PBW filtration steps.

theorem TauCeti.UniversalEnvelopingAlgebra.map_pbwFiltration_eq_of_surjective (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (hf : Function.Surjective ⇑f) (k : ℕ) : Submodule.map (map R f).toLinearMap (pbwFiltration R L k) = pbwFiltration R M k

A surjective Lie homomorphism maps each PBW filtration step onto the corresponding target step.

theorem TauCeti.UniversalEnvelopingAlgebra.map_pbwFiltrationPrevious_eq_of_surjective (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (hf : Function.Surjective ⇑f) (k : ℕ) : Submodule.map (map R f).toLinearMap (pbwFiltrationPrevious R L k) = pbwFiltrationPrevious R M k

A surjective Lie homomorphism also maps the step immediately preceding each PBW degree onto the corresponding preceding step.

theorem TauCeti.UniversalEnvelopingAlgebra.mapFiltration_surjective_of_surjective (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (hf : Function.Surjective ⇑f) (k : ℕ) : Function.Surjective ⇑(mapFiltration R f k)

The map between corresponding PBW filtration steps induced by a surjective Lie homomorphism is surjective.

theorem TauCeti.UniversalEnvelopingAlgebra.map_pbwFiltration_eq_of_rightInverse (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (g : M →ₗ⁅R⁆ L) (h : f.comp g = LieHom.id) (k : ℕ) : Submodule.map (map R f).toLinearMap (pbwFiltration R L k) = pbwFiltration R M k

A split epimorphism of Lie algebras maps every PBW filtration step onto the corresponding target step.

theorem TauCeti.UniversalEnvelopingAlgebra.map_pbwFiltration_eq_inf_range_of_leftInverse (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (g : M →ₗ⁅R⁆ L) (h : g.comp f = LieHom.id) (k : ℕ) : Submodule.map (map R f).toLinearMap (pbwFiltration R L k) = pbwFiltration R M k ⊓ (map R f).toLinearMap.range

For a split monomorphism of Lie algebras, the image of the k-th PBW filtration step is the intersection of the target step with the range of the induced enveloping-algebra map.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapEquiv_pbwFiltration (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (e : L ≃ₗ⁅R⁆ M) (k : ℕ) : Submodule.map (mapEquiv R e).toLinearMap (pbwFiltration R L k) = pbwFiltration R M k

A Lie algebra equivalence maps each PBW filtration step exactly onto the corresponding target step.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapEquiv_pbwFiltrationPrevious (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (e : L ≃ₗ⁅R⁆ M) (k : ℕ) : Submodule.map (mapEquiv R e).toLinearMap (pbwFiltrationPrevious R L k) = pbwFiltrationPrevious R M k

A Lie algebra equivalence maps each preceding PBW filtration step exactly onto the corresponding preceding target step.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.mapEquivFiltration (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (e : L ≃ₗ⁅R⁆ M) (k : ℕ) : ↥(pbwFiltration R L k) ≃ₗ[R] ↥(pbwFiltration R M k)

The linear equivalence between the k-th PBW filtration steps induced by a Lie algebra equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapEquivFiltration_apply (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (e : L ≃ₗ⁅R⁆ M) (k : ℕ) (x : ↥(pbwFiltration R L k)) : ↑((mapEquivFiltration R e k) x) = (mapEquiv R e) ↑x

The equivalence between PBW filtration steps acts by the enveloping-algebra equivalence.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapEquivFiltration_refl (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (k : ℕ) : mapEquivFiltration R LieEquiv.refl k = LinearEquiv.refl R ↥(pbwFiltration R L k)

The identity Lie equivalence induces the identity on each PBW filtration step.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapEquivFiltration_trans (R : Type u) [CommRing R] {L : Type v} {M : Type w} {N : Type x} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [LieRing N] [LieAlgebra R N] (e : L ≃ₗ⁅R⁆ M) (d : M ≃ₗ⁅R⁆ N) (k : ℕ) : mapEquivFiltration R e k ≪≫ₗ mapEquivFiltration R d k = mapEquivFiltration R (e.trans d) k

Composition of Lie equivalences becomes composition of their equivalences between PBW filtration steps.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapEquivFiltration_symm (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (e : L ≃ₗ⁅R⁆ M) (k : ℕ) : (mapEquivFiltration R e k).symm = mapEquivFiltration R e.symm k

Passing to the inverse Lie equivalence gives the inverse linear equivalence between PBW filtration steps.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.mapGradedPiece (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (k : ℕ) : PBWGradedPiece R L k →ₗ[R] PBWGradedPiece R M k

The linear map on the degree-k PBW graded pieces induced by a Lie homomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapGradedPiece_mk (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (k : ℕ) (x : ↥(Algebra.wordFiltration (↑(UniversalEnvelopingAlgebra.ι R)) k)) : (mapGradedPiece R f k) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨(map R f) ↑x, ⋯⟩

On quotient representatives, the induced map on a PBW graded piece is the enveloping-algebra map restricted to the corresponding filtration step.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapGradedPiece_id (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (k : ℕ) : mapGradedPiece R LieHom.id k = LinearMap.id

The identity Lie homomorphism induces the identity on every PBW graded piece.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapGradedPiece_comp (R : Type u) [CommRing R] {L : Type v} {M : Type w} {N : Type x} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [LieRing N] [LieAlgebra R N] (f : L →ₗ⁅R⁆ M) (g : M →ₗ⁅R⁆ N) (k : ℕ) : mapGradedPiece R (g.comp f) k = mapGradedPiece R g k ∘ₗ mapGradedPiece R f k

Composition of Lie homomorphisms becomes composition on each PBW graded piece.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapGradedPiece_gradedOne (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) : (mapGradedPiece R f 0) (Algebra.wordFiltration.gradedOne ↑(UniversalEnvelopingAlgebra.ι R)) = Algebra.wordFiltration.gradedOne ↑(UniversalEnvelopingAlgebra.ι R)

The induced map on degree zero preserves the homogeneous unit.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapGradedPiece_gradedMul (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (i j : ℕ) (x : PBWGradedPiece R L i) (y : PBWGradedPiece R L j) : (mapGradedPiece R f (i + j)) (((Algebra.wordFiltration.gradedMul (↑(UniversalEnvelopingAlgebra.ι R)) i j) x) y) = ((Algebra.wordFiltration.gradedMul (↑(UniversalEnvelopingAlgebra.ι R)) i j) ((mapGradedPiece R f i) x)) ((mapGradedPiece R f j) y)

The maps on PBW graded pieces preserve homogeneous multiplication.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.mapAssociatedGraded (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) : PBWAssociatedGraded R L →ₐ[R] PBWAssociatedGraded R M

The algebra homomorphism of PBW associated gradeds induced by a Lie homomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapAssociatedGraded_of (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (k : ℕ) (x : PBWGradedPiece R L k) : (mapAssociatedGraded R f) ((DirectSum.of (PBWGradedPiece R L) k) x) = (DirectSum.of (PBWGradedPiece R M) k) ((mapGradedPiece R f k) x)

On a homogeneous element, the induced associated-graded map is the map on that graded piece.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapAssociatedGraded_id (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] : mapAssociatedGraded R LieHom.id = AlgHom.id R (PBWAssociatedGraded R L)

The identity Lie homomorphism induces the identity on the PBW associated graded.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapAssociatedGraded_comp (R : Type u) [CommRing R] {L : Type v} {M : Type w} {N : Type x} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [LieRing N] [LieAlgebra R N] (f : L →ₗ⁅R⁆ M) (g : M →ₗ⁅R⁆ N) : mapAssociatedGraded R (g.comp f) = (mapAssociatedGraded R g).comp (mapAssociatedGraded R f)

Composition of Lie homomorphisms becomes composition on PBW associated gradeds.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapAssociatedGraded_pbwGradedGenerator (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (x : L) : (mapAssociatedGraded R f) ((pbwGradedGenerator R L) x) = (pbwGradedGenerator R M) (f x)

The associated-graded map sends a degree-one PBW generator to the generator induced by the original Lie homomorphism.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mapAssociatedGraded_comp_pbwAssociatedGradedMap (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) : (mapAssociatedGraded R f).comp (pbwAssociatedGradedMap R L) = (pbwAssociatedGradedMap R M).comp (SymmetricAlgebra.map R ↑f)

Naturality of the canonical symmetric-algebra map to the PBW associated graded.