Documentation

Mathlib.RingTheory.HopfAlgebra.Convolution

Convolution product on Hopf algebra maps #

This file constructs the ring structure on bialgebra homs C → A where C and A are Hopf algebras and multiplication is given by

         |
         μ
|   |   / \
f * g = f g
|   |   \ /
         δ
         |

diagrammatically, where μ stands for multiplication and δ for comultiplication.

source
theorem HopfAlgebra.antipode_comp_mul_comp_comm {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] :
antipode R ∘ₗ LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A) = LinearMap.mul' R A ∘ₗ TensorProduct.map (antipode R) (antipode R)
source
theorem HopfAlgebra.antipode_mul_antidistrib {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a b : A) :
(antipode R) (a * b) = (antipode R) b * (antipode R) a
source
@[deprecated HopfAlgebra.antipode_mul_antidistrib (since := "2026-06-05")]
theorem HopfAlgebra.antipode_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a b : A) :
(antipode R) (a * b) = (antipode R) b * (antipode R) a

Alias of HopfAlgebra.antipode_mul_antidistrib.

source
noncomputable def HopfAlgebra.antipodeAlgHomOp (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [HopfAlgebra R A] :
A →ₐ[R] Aᵐᵒᵖ

The antipode of a commutative Hopf algebra as an anti-algebra hom.

Equations
Instances For
    source
    @[simp]
    theorem HopfAlgebra.antipodeAlgHomOp_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a : A) :
    (antipodeAlgHomOp R A) a = MulOpposite.op ((antipode R) a)
    source
    theorem HopfAlgebra.antipode_mul_distrib {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] (a b : A) :
    (antipode R) (a * b) = (antipode R) a * (antipode R) b
    source
    noncomputable def HopfAlgebra.antipodeAlgHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] :
    A →ₐ[R] A

    The antipode of a commutative Hopf algebra as an algebra hom.

    Equations
    Instances For
      source
      @[simp]
      theorem HopfAlgebra.antipodeAlgHom_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] (a : A) :
      (antipodeAlgHom R A) a = (antipode R) a
      source
      @[simp]
      theorem HopfAlgebra.toLinearMap_antipodeAlgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] :
      (antipodeAlgHom R A).toLinearMap = antipode R
      source
      @[simp]
      theorem LinearMap.antipode_mul_id {R : Type u_1} {C : Type u_3} [CommSemiring R] [Semiring C] [HopfAlgebra R C] :
      WithConv.toConv (HopfAlgebraStruct.antipode R) * WithConv.toConv id = 1
      source
      @[simp]
      theorem LinearMap.id_mul_antipode {R : Type u_1} {C : Type u_3} [CommSemiring R] [Semiring C] [HopfAlgebra R C] :
      WithConv.toConv id * WithConv.toConv (HopfAlgebraStruct.antipode R) = 1
      source
      theorem LinearMap.comul_right_inv {R : Type u_1} {C : Type u_3} [CommSemiring R] [Semiring C] [HopfAlgebra R C] :
      WithConv.toConv CoalgebraStruct.comul * WithConv.toConv (CoalgebraStruct.comul ∘ₗ HopfAlgebraStruct.antipode R) = 1
      source
      @[implicit_reducible]
      noncomputable instance AlgHom.convInv {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R C] [HopfAlgebra R A] :
      Inv (WithConv (A →ₐ[R] C))
      Equations
      source
      @[implicit_reducible]
      noncomputable instance AlgHom.convGroup {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R C] [HopfAlgebra R A] :
      Group (WithConv (A →ₐ[R] C))
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[implicit_reducible]
      noncomputable instance AlgHom.instCommGroupWithConvOfIsCocomm {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R C] [HopfAlgebra R A] [Coalgebra.IsCocomm R A] :
      CommGroup (WithConv (A →ₐ[R] C))
      Equations
      source
      theorem AlgHom.antipode_id_cancel {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] :
      WithConv.toConv (HopfAlgebra.antipodeAlgHom R A) * WithConv.toConv (AlgHom.id R A) = 1
      source
      theorem AlgHom.counitAlgHom_comp_antipodeAlgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] :
      (Bialgebra.counitAlgHom R A).comp (HopfAlgebra.antipodeAlgHom R A) = Bialgebra.counitAlgHom R A