Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.Rees.OneFiber

The PBW Rees fibre at one #

Specializing the PBW deformation parameter to one recovers the universal enveloping algebra. We give both the quotient by the central two-sided ideal (t - 1) and the actual tensor base change along evaluation R[t] → R at one. The comparison sends j(x) to ι(x); its inverse sends ι(x) to the specialized Rees generator.

These comparisons require neither freeness of the Lie algebra nor a characteristic hypothesis. They use the exhaustive PBW filtration.

References #

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

The quotient of the PBW Rees algebra by t - 1 is the enveloping algebra.

Instances For
    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.quotientReesParameterSubOneEquiv_mk (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (p : ↥(reesAlgebra R L)) :
    (quotientReesParameterSubOneEquiv R L) ((Ideal.Quotient.mk (Ideal.span {reesParameter R L - 1})) p) = (coeffSubalgebra.evalOne (pbwFiltration R L)) p

    The quotient comparison evaluates any representative at parameter one.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.quotientReesParameterSubOneEquiv_symm_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :
    (quotientReesParameterSubOneEquiv R L).symm ((UniversalEnvelopingAlgebra.ι R) x) = (Ideal.Quotient.mk (Ideal.span {reesParameter R L - 1})) ((reesGenerator R L) x)

    The inverse quotient comparison takes an enveloping generator to the Rees generator class.

    source
    noncomputable def TauCeti.UniversalEnvelopingAlgebra.reesOneFiberEquiv (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
    TensorProduct (Polynomial R) R ↥(reesAlgebra R L) ≃ₐ[R] UniversalEnvelopingAlgebra R L

    Tensor base change of the PBW Rees algebra at one is the enveloping algebra. The polynomial parameter acts on the left tensor factor by evaluation at one.

    Instances For
      source
      @[simp]
      theorem TauCeti.UniversalEnvelopingAlgebra.reesOneFiberEquiv_tmul (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (r : R) (p : ↥(reesAlgebra R L)) :
      (reesOneFiberEquiv R L) (r ⊗ₜ[Polynomial R] p) = r • (coeffSubalgebra.evalOne (pbwFiltration R L)) p

      The fibre comparison evaluates the Rees factor and multiplies by the scalar factor.

      source
      @[simp]
      theorem TauCeti.UniversalEnvelopingAlgebra.reesOneFiberEquiv_symm_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :
      (reesOneFiberEquiv R L).symm ((UniversalEnvelopingAlgebra.ι R) x) = 1 ⊗ₜ[Polynomial R] (reesGenerator R L) x

      The inverse fibre comparison takes an enveloping generator to the specialized Rees generator.