Bialgebra structure on SymmetricAlgebra R M

The symmetric algebra S(M) over an R-module M is the universal cocommutative graded connected commutative R-bialgebra on M: there is a unique bialgebra map from S(M) to any cocommutative graded connected commutative bialgebra extending a given linear map out of M. The coproduct is determined by the shuffle condition that each generator ι x is primitive:

• Δ(ι x) = ι x ⊗ 1 + 1 ⊗ ι x,
• ε(ι x) = 0.

The counit is SymmetricAlgebra.algebraMapInv, the canonical algebra left-inverse of algebraMap R (S(M)). Cocommutativity follows from the symmetry of ι x ⊗ 1 + 1 ⊗ ι x under swap.

The Hopf algebra extension (antipode ι x ↦ −ι x, requiring CommRing R) lives in Linglib/Core/RingTheory/HopfAlgebra/SymmetricAlgebra.lean.

Main definitions

• SymmetricAlgebra.instBialgebra — the Bialgebra R (SymmetricAlgebra R M) instance, built via Bialgebra.ofAlgHom. Provides Coalgebra, Bialgebra instances; downstream code gets Bialgebra.comulAlgHom, Bialgebra.counitAlgHom, comul_algebraMap, comul_natCast, comul_pow, counit_* analogs via typeclass projection.
• SymmetricAlgebra.instIsCocomm — cocommutativity.
• Simp lemmas algebraMapInv_ι, comul_ι, counit_ι on generators.

Status

[UPSTREAM] candidate. Natural home is Mathlib/RingTheory/Bialgebra/SymmetricAlgebra.lean. Mathlib currently has no coproduct on SymmetricAlgebra, TensorAlgebra, ExteriorAlgebra, or FreeAlgebra.

This file follows the Bialgebra.ofAlgHom route: build the comultiplication and counit as algebra homomorphisms, check coassoc

• counit laws at AlgHom level, hand off to mathlib's Bialgebra.ofAlgHom constructor (which builds the Coalgebra instance internally and registers Bialgebra). This is the simplest path for from-scratch constructions; cf. Mathlib/RingTheory/HopfAlgebra/TensorProduct.lean using the analogous HopfAlgebra.ofAlgHom.

When upstreaming, replace the three import lines with

module
public import Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
public import Mathlib.RingTheory.Bialgebra.Basic
public import Mathlib.RingTheory.TensorProduct.Maps

and prepend @[expose] public section to the docstring; the file-level noncomputable section and Type* style already match mathlib convention. The set_option autoImplicit false line becomes redundant under the module system.

References

• Sweedler, Hopf Algebras (1969) — primitive elements in cocommutative graded connected Hopf algebras, of which S(M) is the universal example.

Apply lemma for algebraMapInv on generators

@[simp]

theorem SymmetricAlgebra.algebraMapInv_ι (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (x : M) : algebraMapInv ((ι R M) x) = 0

Evaluating algebraMapInv (the canonical algebra hom S(M) →ₐ[R] R sending generators to zero) on ι x yields 0.

Comultiplication

Δ : S(M) →ₐ[R] S(M) ⊗[R] S(M) is the unique algebra homomorphism extending x ↦ ι x ⊗ 1 + 1 ⊗ ι x on M. The target is a commutative R-algebra, so the universal property SymmetricAlgebra.lift applies.

comulAlgHom is kept private: downstream code uses Bialgebra.comulAlgHom once the instance registers, avoiding namespace collision.

Coalgebra axioms at AlgHom level

Proved on generators via SymmetricAlgebra.algHom_ext; transferred to the LinearMap-level fields of Coalgebra inside Bialgebra.ofAlgHom.

Bialgebra instance

Bialgebra.ofAlgHom consumes the AlgHom-level coassoc/counit identities above and builds both the Coalgebra and Bialgebra instances in one shot.

@[implicit_reducible]

instance SymmetricAlgebra.instBialgebra (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] : Bialgebra R (SymmetricAlgebra R M)

The canonical Bialgebra structure on SymmetricAlgebra R M.

Equations

• SymmetricAlgebra.instBialgebra R M = Bialgebra.ofAlgHom (SymmetricAlgebra.comulAlgHom✝ R M) SymmetricAlgebra.algebraMapInv ⋯ ⋯ ⋯

Public simp lemmas on Coalgebra.comul / Coalgebra.counit

User-facing forms: simp on Coalgebra.comul (ι R M x) reduces to ι x ⊗ 1 + 1 ⊗ ι x.

@[simp]

theorem SymmetricAlgebra.comul_ι (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (x : M) : CoalgebraStruct.comul ((ι R M) x) = (ι R M) x ⊗ₜ[R] 1 + 1 ⊗ₜ[R] (ι R M) x

@[simp]

theorem SymmetricAlgebra.counit_ι (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (x : M) : CoalgebraStruct.counit ((ι R M) x) = 0

Cocommutativity

instance SymmetricAlgebra.instIsCocomm (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] : Coalgebra.IsCocomm R (SymmetricAlgebra R M)