Hopf algebra structure on SymmetricAlgebra R M

The generators ι R M x of the symmetric algebra are primitive. When M is an additive group the antipode is the algebra endomorphism induced by negation on M, over any commutative semiring R: it sends a polynomial f(x₁, …, xₙ) to f(-x₁, …, -xₙ), and over a ring it multiplies a product of k generators by (-1) ^ k.

[UPSTREAM] Belongs in Mathlib/RingTheory/HopfAlgebra/SymmetricAlgebra.lean, except the ιMulti lemmas, which follow SymmetricAlgebra.ιMulti.

References

• [GR20]

theorem SymmetricAlgebra.isPrimitiveElem_ι {M : Type u_1} (R : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] (x : M) : Bialgebra.IsPrimitiveElem R ((ι R M) x)

@[instance_reducible]

instance SymmetricAlgebra.instHopfAlgebra {M : Type u_1} (R : Type u_3) [CommSemiring R] [AddCommGroup M] [Module R M] : HopfAlgebra R (SymmetricAlgebra R M)

Equations

• SymmetricAlgebra.instHopfAlgebra R = HopfAlgebra.ofAlgHom (SymmetricAlgebra.lift (SymmetricAlgebra.ι R M ∘ₗ (-LinearMap.id))) ⋯ ⋯

@[simp]

theorem SymmetricAlgebra.antipode_ι {M : Type u_1} (R : Type u_3) [CommSemiring R] [AddCommGroup M] [Module R M] (x : M) : (HopfAlgebraStruct.antipode R) ((ι R M) x) = (ι R M) (-x)

theorem SymmetricAlgebra.antipodeAlgHom_eq {M : Type u_1} (R : Type u_3) [CommSemiring R] [AddCommGroup M] [Module R M] : HopfAlgebra.antipodeAlgHom R (SymmetricAlgebra R M) = lift (ι R M ∘ₗ (-LinearMap.id))

theorem SymmetricAlgebra.antipode_ιMulti {M : Type u_1} {κ : Type u_2} [Fintype κ] (R : Type u_3) [CommSemiring R] [AddCommGroup M] [Module R M] (x : κ → M) : (HopfAlgebraStruct.antipode R) ((ιMulti R M κ) x) = (ιMulti R M κ) (-x)

See Example 1.4.18 in [GR20].

theorem SymmetricAlgebra.antipode_ιMulti_eq_smul {M : Type u_1} {κ : Type u_2} [Fintype κ] (R : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (x : κ → M) : (HopfAlgebraStruct.antipode R) ((ιMulti R M κ) x) = (-1) ^ Fintype.card κ • (ιMulti R M κ) x