Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.Rees.ZeroFiber

The symmetric-algebra fibre of the PBW Rees algebra #

For a Lie algebra free over a commutative ring, quotienting its PBW Rees algebra by the central parameter gives the symmetric algebra. The quotient map sends j(x) = ι(x)t to the symmetric generator x. In particular, it is not ambient evaluation at zero, which kills j(x).

The comparison composes the generic word-filtration symbol map with the inverse of the native PBW equivalence pbwAssociatedGradedEquiv. Its coefficientwise kernel description records precisely the loss of one filtration step needed to divide a commutator by the parameter and then take its symbol.

source
noncomputable def TauCeti.UniversalEnvelopingAlgebra.reesSpecializationZero (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] :
↥(reesAlgebra R L) →ₐ[R] SymmetricAlgebra R L

The zero-parameter specialization of the PBW Rees algebra to the symmetric algebra.

Instances For
    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.reesSpecializationZero_reesGenerator (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] (x : L) :
    (reesSpecializationZero R L) ((reesGenerator R L) x) = (SymmetricAlgebra.ι R L) x

    A linear Rees generator specializes to the corresponding symmetric generator.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.reesSpecializationZero_surjective (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] :
    Function.Surjective ⇑(reesSpecializationZero R L)

    The PBW zero specialization is surjective.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.reesSpecializationZero_eq_zero_iff (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] (p : ↥(reesAlgebra R L)) :
    (reesSpecializationZero R L) p = 0 ↔ ∀ (n : ℕ), (↑p).coeff n ∈ pbwFiltrationPrevious R L n

    A Rees polynomial specializes to zero exactly when every coefficient has lower PBW degree.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.reesSpecializationZero_reesParameter (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] :
    (reesSpecializationZero R L) (reesParameter R L) = 0

    The central Rees parameter specializes to zero.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.ker_reesSpecializationZero (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] :
    RingHom.ker ↑(reesSpecializationZero R L) = Ideal.span {reesParameter R L}

    The kernel of PBW zero specialization is the ideal generated by the central parameter.

    source
    noncomputable def TauCeti.UniversalEnvelopingAlgebra.reesZeroFiberEquiv (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] :
    (↥(reesAlgebra R L) ⧸ Ideal.span {reesParameter R L}) ≃ₐ[R] SymmetricAlgebra R L

    The PBW zero fibre is canonically the symmetric algebra, without a choice of basis.

    Instances For
      source
      @[simp]
      theorem TauCeti.UniversalEnvelopingAlgebra.reesZeroFiberEquiv_mk (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] (p : ↥(reesAlgebra R L)) :
      (reesZeroFiberEquiv R L) ((Ideal.Quotient.mk (Ideal.span {reesParameter R L})) p) = (reesSpecializationZero R L) p

      The zero-fibre equivalence is induced by zero specialization.

      source
      @[simp]
      theorem TauCeti.UniversalEnvelopingAlgebra.reesZeroFiberEquiv_symm_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] (x : L) :
      (reesZeroFiberEquiv R L).symm ((SymmetricAlgebra.ι R L) x) = (Ideal.Quotient.mk (Ideal.span {reesParameter R L})) ((reesGenerator R L) x)

      The inverse comparison lifts each symmetric generator to the class of its Rees generator.