Hopf algebra structure on SymmetricAlgebra R M

When R is a commutative ring, SymmetricAlgebra R M carries a Hopf algebra structure extending the bialgebra structure from Linglib/Core/RingTheory/Bialgebra/SymmetricAlgebra.lean. The antipode is the algebra homomorphism

`S(ι x) = −ι x`   for `x : M`,

extended multiplicatively. Equivalently, S is the unique algebra endomorphism of S(M) whose restriction to M is negation.

The CommRing R requirement is essential: negation on SymmetricAlgebra R M is gated by CommRing R in mathlib (SymmetricAlgebra/Basic.lean); it cannot be loosened to [CommSemiring R] [AddCommGroup M] without a separate upstream PR providing a Ring (SymmetricAlgebra R M) instance under those hypotheses.

Main definitions

• SymmetricAlgebra.antipodeAlgHom — the antipode as an algebra homomorphism, lifted from -ι R M : M →ₗ[R] S(M).
• SymmetricAlgebra.instHopfAlgebra — the HopfAlgebra R (SymmetricAlgebra R M) instance, registered via HopfAlgebra.ofAlgHom.

Status

[UPSTREAM] candidate. Natural home is Mathlib/RingTheory/HopfAlgebra/SymmetricAlgebra.lean, completing the Bialgebra/HopfAlgebra pair alongside the sibling Mathlib/RingTheory/Bialgebra/SymmetricAlgebra.lean.

When upstreaming, replace the imports with

module
public import Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
public import Mathlib.RingTheory.HopfAlgebra.TensorProduct

plus @[expose] public section.

Antipode

def SymmetricAlgebra.antipodeAlgHom (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommMonoid M] [Module R M] : SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M

The antipode of SymmetricAlgebra R M as an algebra homomorphism: S(ι x) = −ι x for x : M, extended multiplicatively.

Equations

• SymmetricAlgebra.antipodeAlgHom R M = SymmetricAlgebra.lift (-SymmetricAlgebra.ι R M)

@[simp]

theorem SymmetricAlgebra.antipodeAlgHom_ι (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommMonoid M] [Module R M] (x : M) : (antipodeAlgHom R M) ((ι R M) x) = -(ι R M) x

Hopf algebra instance

HopfAlgebra.ofAlgHom (defined for commutative bialgebras at Mathlib/RingTheory/HopfAlgebra/TensorProduct.lean) consumes the antipode as an AlgHom and reduces the antipode axioms to AlgHom-level equations. Each axiom is checked on generators via SymmetricAlgebra.algHom_ext:

• (S ⊗ id) ∘ Δ (ι x) = (-ι x) · 1 + 1 · ι x = 0 = ε(ι x) · 1,
• symmetrically for the right antipode law.

@[implicit_reducible]

noncomputable instance SymmetricAlgebra.instHopfAlgebra (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommMonoid M] [Module R M] : HopfAlgebra R (SymmetricAlgebra R M)

Equations

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