The Hopf structure on a symmetric algebra

Mathlib equips SymmetricAlgebra R M with the cocommutative bialgebra structure in which each generator ι x is primitive, Δ(ι x) = ι x ⊗ 1 + 1 ⊗ ι x and ε(ι x) = 0, but it stops short of the antipode. Over a commutative ring R the symmetric algebra is a Hopf algebra: the antipode is the algebra map sending each ι x to -ι x.

Main declarations

• TauCeti.SymmetricAlgebra.instHopfAlgebra: the Hopf algebra structure on SymmetricAlgebra R M over a commutative ring R.
• TauCeti.SymmetricAlgebra.antipode_ι: the Hopf antipode sends each generator to its negative.
• TauCeti.SymmetricAlgebra.lift_symm_apply: the inverse of SymmetricAlgebra.lift evaluates an algebra map at generators.
• TauCeti.SymmetricAlgebra.convMul_apply_ι: convolution of algebra maps evaluates on generators by adding their values.

References

The cocommutative bialgebra structure on the symmetric algebra is Robert Hawkins' Mathlib work in Mathlib.RingTheory.Bialgebra.SymmetricAlgebra. The Hopf-algebra-from-an-antipode constructor HopfAlgebra.ofAlgHom is from Mathlib.RingTheory.HopfAlgebra.Basic.

noncomputable def TauCeti.SymmetricAlgebra.antipodeHom (R : Type u) [CommRing R] (M : Type v) [AddCommMonoid M] [Module R M] : SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M

The antipode of the symmetric-algebra Hopf algebra: the R-algebra map sending each generator ι x to -ι x.

Equations

• TauCeti.SymmetricAlgebra.antipodeHom R M = SymmetricAlgebra.lift (-SymmetricAlgebra.ι R M)

@[simp]

theorem TauCeti.SymmetricAlgebra.antipodeHom_ι (R : Type u) [CommRing R] (M : Type v) [AddCommMonoid M] [Module R M] (x : M) : (antipodeHom R M) ((SymmetricAlgebra.ι R M) x) = -(SymmetricAlgebra.ι R M) x

@[instance_reducible]

noncomputable instance TauCeti.SymmetricAlgebra.instHopfAlgebra (R : Type u) [CommRing R] (M : Type v) [AddCommMonoid M] [Module R M] : HopfAlgebra R (SymmetricAlgebra R M)

The symmetric algebra over a commutative ring is a Hopf algebra: its antipode sends each generator ι x to -ι x.

Equations

• TauCeti.SymmetricAlgebra.instHopfAlgebra R M = HopfAlgebra.ofAlgHom (TauCeti.SymmetricAlgebra.antipodeHom R M) ⋯ ⋯

@[simp]

theorem TauCeti.SymmetricAlgebra.antipode_ι (R : Type u) [CommRing R] (M : Type v) [AddCommMonoid M] [Module R M] (x : M) : (HopfAlgebraStruct.antipode R) ((SymmetricAlgebra.ι R M) x) = -(SymmetricAlgebra.ι R M) x

The Hopf-algebra antipode on a symmetric algebra sends each generator ι x to -ι x.

@[simp]

theorem TauCeti.SymmetricAlgebra.lift_symm_apply {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {A : Type w} [CommSemiring A] [Algebra R A] (H : SymmetricAlgebra R M →ₐ[R] A) (x : M) : (SymmetricAlgebra.lift.symm H) x = H ((SymmetricAlgebra.ι R M) x)

The inverse of the symmetric-algebra lift evaluates an algebra map at a generator: it sends H to the linear map x ↦ H (ι x).

@[simp]

theorem TauCeti.SymmetricAlgebra.convMul_apply_ι {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {A : Type w} [CommSemiring A] [Algebra R A] (F G : WithConv (SymmetricAlgebra R M →ₐ[R] A)) (x : M) : (F * G).ofConv ((SymmetricAlgebra.ι R M) x) = F.ofConv ((SymmetricAlgebra.ι R M) x) + G.ofConv ((SymmetricAlgebra.ι R M) x)

The convolution product of two points of a symmetric algebra is, on each generator, the sum of their values: (F * G)(ι x) = F(ι x) + G(ι x).