Bialgebra structure on SymmetricAlgebra R M

SymmetricAlgebra R M is the cocommutative commutative R-bialgebra on M in which each generator ι x is primitive: Δ(ι x) = ι x ⊗ 1 + 1 ⊗ ι x and ε(ι x) = 0.

@[instance_reducible]

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

Equations

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

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

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

@[simp]

theorem SymmetricAlgebra.counitAlgHom_eq (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] : Bialgebra.counitAlgHom R (SymmetricAlgebra R M) = algebraMapInv