Documentation

TauCeti.QuantumGroups.UqSl2.Hopf

The Hopf algebra structure on U_q(sl₂) #

For a nonzero parameter, the presentation of UqSl2 q carries the coproduct ΔE = E ⊗ 1 + K ⊗ E, ΔF = F ⊗ K⁻¹ + 1 ⊗ F, and ΔK = K ⊗ K. The counit and antipode have their standard rank-one values. These maps descend through the presentation's universal property. The coproduct supplies actions on tensor products of representations, while the antipode supplies the corresponding dual actions.

The conventions follow A. Virelizier, Quantum groups, Sections 2.3--2.4.

source
def TauCeti.UqSl2.comul (q : ℂ) [Fact (q ≠ 0)] :
UqSl2 q →ₐ[ℂ] TensorProduct ℂ (UqSl2 q) (UqSl2 q)

The coproduct with E skew primitive relative to K and F relative to K⁻¹.

Instances For
    source
    def TauCeti.UqSl2.counit (q : ℂ) :
    UqSl2 q →ₐ[ℂ] ℂ

    The unconditional augmentation, taking both weight generators to one and both root generators to zero.

    Instances For
      source
      @[simp]
      theorem TauCeti.UqSl2.counit_apply_e (q : ℂ) :
      (counit q) (e q) = 0

      The unconditional augmentation sends the raising generator to zero.

      source
      @[simp]
      theorem TauCeti.UqSl2.counit_apply_f (q : ℂ) :
      (counit q) (f q) = 0

      The unconditional augmentation sends the lowering generator to zero.

      source
      @[simp]
      theorem TauCeti.UqSl2.counit_apply_k (q : ℂ) :
      (counit q) (k q) = 1

      The unconditional augmentation sends the weight generator to one.

      source
      @[simp]
      theorem TauCeti.UqSl2.counit_apply_kInv (q : ℂ) :
      (counit q) (kInv q) = 1

      The unconditional augmentation sends the inverse weight generator to one.

      source
      @[instance_reducible]
      noncomputable instance TauCeti.UqSl2.instBialgebra (q : ℂ) [Fact (q ≠ 0)] :
      Bialgebra ℂ (UqSl2 q)

      The bialgebra structure determined by the presentation's coproduct and counit.

      source
      def TauCeti.UqSl2.antipodeOp (q : ℂ) [Fact (q ≠ 0)] :
      UqSl2 q →ₐ[ℂ] (UqSl2 q)ᵐᵒᵖ

      The antipode as an algebra homomorphism into the opposite algebra.

      Instances For
        source
        @[instance_reducible]
        noncomputable instance TauCeti.UqSl2.instHopfAlgebra (q : ℂ) [Fact (q ≠ 0)] :
        HopfAlgebra ℂ (UqSl2 q)

        The Hopf algebra structure of the rank-one quantized enveloping algebra.

        source
        @[simp]
        theorem TauCeti.UqSl2.comul_e (q : ℂ) [Fact (q ≠ 0)] :
        CoalgebraStruct.comul (e q) = e q ⊗ₜ[ℂ] 1 + k q ⊗ₜ[ℂ] e q

        The coproduct of the raising generator.

        source
        @[simp]
        theorem TauCeti.UqSl2.comul_f (q : ℂ) [Fact (q ≠ 0)] :
        CoalgebraStruct.comul (f q) = f q ⊗ₜ[ℂ] kInv q + 1 ⊗ₜ[ℂ] f q

        The coproduct of the lowering generator.

        source
        @[simp]
        theorem TauCeti.UqSl2.comul_k (q : ℂ) [Fact (q ≠ 0)] :
        CoalgebraStruct.comul (k q) = k q ⊗ₜ[ℂ] k q

        The weight generator is group-like for the coproduct.

        source
        @[simp]
        theorem TauCeti.UqSl2.comul_kInv (q : ℂ) [Fact (q ≠ 0)] :
        CoalgebraStruct.comul (kInv q) = kInv q ⊗ₜ[ℂ] kInv q

        The inverse weight generator is group-like for the coproduct.

        source
        @[simp]
        theorem TauCeti.UqSl2.counit_e (q : ℂ) [Fact (q ≠ 0)] :
        CoalgebraStruct.counit (e q) = 0

        The raising generator has zero counit.

        source
        @[simp]
        theorem TauCeti.UqSl2.counit_f (q : ℂ) [Fact (q ≠ 0)] :
        CoalgebraStruct.counit (f q) = 0

        The lowering generator has zero counit.

        source
        @[simp]
        theorem TauCeti.UqSl2.counit_k (q : ℂ) [Fact (q ≠ 0)] :
        CoalgebraStruct.counit (k q) = 1

        The weight generator has counit one.

        source
        @[simp]
        theorem TauCeti.UqSl2.counit_kInv (q : ℂ) [Fact (q ≠ 0)] :
        CoalgebraStruct.counit (kInv q) = 1

        The inverse weight generator has counit one.

        source
        @[simp]
        theorem TauCeti.UqSl2.antipode_e (q : ℂ) [Fact (q ≠ 0)] :
        (HopfAlgebraStruct.antipode ℂ) (e q) = -(kInv q * e q)

        The antipode of the raising generator.

        source
        @[simp]
        theorem TauCeti.UqSl2.antipode_f (q : ℂ) [Fact (q ≠ 0)] :
        (HopfAlgebraStruct.antipode ℂ) (f q) = -(f q * k q)

        The antipode of the lowering generator.

        source
        @[simp]
        theorem TauCeti.UqSl2.antipode_k (q : ℂ) [Fact (q ≠ 0)] :
        (HopfAlgebraStruct.antipode ℂ) (k q) = kInv q

        The antipode interchanges the weight generators.

        source
        @[simp]
        theorem TauCeti.UqSl2.antipode_kInv (q : ℂ) [Fact (q ≠ 0)] :
        (HopfAlgebraStruct.antipode ℂ) (kInv q) = k q

        The antipode interchanges the inverse weight generators.

        source
        theorem TauCeti.UqSl2.isGroupLikeElem_kInv (q : ℂ) [Fact (q ≠ 0)] :
        IsGroupLikeElem ℂ (kInv q)

        The inverse weight generator is group-like.

        source
        @[simp]
        theorem TauCeti.UqSl2.comul_apply (q : ℂ) [Fact (q ≠ 0)] (x : UqSl2 q) :
        (comul q) x = CoalgebraStruct.comul x

        The constructed coproduct agrees with the native coalgebra operation.

        source
        @[simp]
        theorem TauCeti.UqSl2.counit_apply (q : ℂ) [Fact (q ≠ 0)] (x : UqSl2 q) :
        (counit q) x = CoalgebraStruct.counit x

        The constructed counit agrees with the native coalgebra operation.

        source
        @[simp]
        theorem TauCeti.UqSl2.antipodeOp_apply (q : ℂ) [Fact (q ≠ 0)] (x : UqSl2 q) :
        (antipodeOp q) x = MulOpposite.op ((HopfAlgebraStruct.antipode ℂ) x)

        The opposite-valued antipode agrees with the native linear antipode.