Symmetric algebras of comodules as comodule algebras

This file equips the symmetric algebra of a comodule with its natural comodule-algebra structure. It also records that homogeneous components of coinvariants remain coinvariant and constructs the equivariant algebra map induced by the inclusion of a subcomodule into a comodule algebra.

Main declarations

• TauCeti.ComoduleAlgebra.symmetricAlgebra: the comodule-algebra structure on the symmetric algebra of a comodule.
• TauCeti.ComoduleAlgebra.decompose_mem_coinvariants_symmetricAlgebra: homogeneous components of a coinvariant in a symmetric algebra are coinvariant.
• TauCeti.ComoduleAlgebra.liftSubcomoduleHom: the equivariant algebra map from the symmetric algebra of a subcomodule into a comodule algebra.

@[implicit_reducible]

noncomputable def TauCeti.ComoduleAlgebra.symmetricAlgebra (R : Type u_1) (H : Type u_2) (M : Type u_3) [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] : ComoduleAlgebra R H (SymmetricAlgebra R M)

The symmetric algebra of a comodule over a commutative bialgebra is a comodule algebra, with the multiplicative coaction TauCeti.Comodule.symmetricAlgebraCoact.

Like TauCeti.Comodule.symmetricAlgebra, this is not a global instance.

theorem TauCeti.ComoduleAlgebra.symmetricAlgebra_coact {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] : Comodule.coact = (Comodule.symmetricAlgebraCoact R H M).toLinearMap

The coaction of the symmetric-algebra comodule algebra is TauCeti.Comodule.symmetricAlgebraCoact. Unlike TauCeti.Comodule.symmetricAlgebra_coact, it rewrites with the comodule structure underlying this comodule algebra.

theorem TauCeti.ComoduleAlgebra.decompose_mem_coinvariants_symmetricAlgebra {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {x : SymmetricAlgebra R M} (hx : x ∈ coinvariants R H (SymmetricAlgebra R M)) (n : ℕ) : ↑(((DirectSum.decompose (SymmetricAlgebra.homogeneousSubmodule R M)) x) n) ∈ coinvariants R H (SymmetricAlgebra R M)

The homogeneous components of an invariant of the symmetric algebra of a comodule are invariant.

noncomputable def TauCeti.ComoduleAlgebra.liftSubcomoduleHom {R : Type u} [CommSemiring R] {H : Type v} [CommSemiring H] [Bialgebra R H] {A : Type w} [CommSemiring A] [Algebra R A] [ComoduleAlgebra R H A] [Module.Flat R H] (V : Subcomodule R H A) : Comodule.Hom R H (SymmetricAlgebra R ↥V) A

The algebra homomorphism from the symmetric algebra of a subcomodule of a comodule algebra, extending the inclusion, is a comodule morphism.

@[simp]

theorem TauCeti.ComoduleAlgebra.liftSubcomoduleHom_apply {R : Type u} [CommSemiring R] {H : Type v} [CommSemiring H] [Bialgebra R H] {A : Type w} [CommSemiring A] [Algebra R A] [ComoduleAlgebra R H A] [Module.Flat R H] (V : Subcomodule R H A) (x : SymmetricAlgebra R ↥V) : (liftSubcomoduleHom V) x = (SymmetricAlgebra.lift (SMulMemClass.subtype V)) x

The underlying map of the equivariant lift is the symmetric-algebra lift.