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
        \ /
         .

theorem HopfAlgebra.antipode_mul_antidistrib {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] (a b : A) : (antipode R) (a * b) = (antipode R) b * (antipode R) a

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

theorem HopfAlgebra.antipode_mul {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

Alias of HopfAlgebra.antipode_mul_distrib.

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

• HopfAlgebra.antipodeAlgHom R A = AlgHom.ofLinearMap (HopfAlgebraStruct.antipode R) ⋯ ⋯

@[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

@[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

@[simp]

theorem LinearMap.antipode_mul_id {R : Type u_1} {C : Type u_3} [CommSemiring R] [Semiring C] [HopfAlgebra R C] : HopfAlgebraStruct.antipode R * id = 1

@[simp]

theorem LinearMap.id_mul_antipode {R : Type u_1} {C : Type u_3} [CommSemiring R] [Semiring C] [HopfAlgebra R C] : id * HopfAlgebraStruct.antipode R = 1

theorem LinearMap.comul_right_inv {R : Type u_1} {C : Type u_3} [CommSemiring R] [Semiring C] [HopfAlgebra R C] : CoalgebraStruct.comul * CoalgebraStruct.comul ∘ₗ HopfAlgebraStruct.antipode R = 1

theorem AlgHom.antipode_id_cancel {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] : HopfAlgebra.antipodeAlgHom R A * AlgHom.id R A = 1

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

noncomputable def BialgHom.antipodeBialgHom {R : Type u_1} {C : Type u_3} [CommSemiring R] [CommSemiring C] [HopfAlgebra R C] : C →ₐc[R] C

The antipode of a commutative cocommutative Hopf algebra as a coalgebra hom.

Equations

• BialgHom.antipodeBialgHom = { toFun := (↑↑(HopfAlgebra.antipodeAlgHom R C).toRingHom).toFun, map_add' := ⋯, map_smul' := ⋯, counit_comp := ⋯, map_comp_comul := ⋯, map_one' := ⋯, map_mul' := ⋯ }

noncomputable instance BialgHom.instInv_toric {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [CommSemiring A] [CommSemiring C] [HopfAlgebra R A] [HopfAlgebra R C] : Inv (C →ₐc[R] A)

Equations

• BialgHom.instInv_toric = { inv := BialgHom.antipodeBialgHom.comp }

theorem BialgHom.inv_def {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [CommSemiring A] [CommSemiring C] [HopfAlgebra R A] [HopfAlgebra R C] [Coalgebra.IsCocomm R C] (f : C →ₐc[R] A) : f⁻¹ = antipodeBialgHom.comp f

@[simp]

theorem BialgHom.inv_apply {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [CommSemiring A] [CommSemiring C] [HopfAlgebra R A] [HopfAlgebra R C] [Coalgebra.IsCocomm R C] (f : C →ₐc[R] A) (c : C) : f⁻¹ c = (HopfAlgebraStruct.antipode R) (f c)

noncomputable instance BialgHom.instCommGroup_toric {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [CommSemiring A] [CommSemiring C] [HopfAlgebra R A] [HopfAlgebra R C] [Coalgebra.IsCocomm R C] : CommGroup (C →ₐc[R] A)

Equations

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