Corestriction of comodule algebras #
A bialgebra morphism corestricts a comodule algebra by applying that morphism to the
coefficient factor of the coaction. In particular, a quotient of a coordinate Hopf algebra
restricts the regular action to the closed subgroup it represents. This uses the comodule
corestriction Comodule.Corestrict, retaining the original algebra structure.
@[implicit_reducible]
noncomputable def
TauCeti.ComoduleAlgebra.Corestrict
{R : Type u_1}
{H : Type u_2}
{K : Type u_3}
{A : Type u_4}
[CommSemiring R]
[Semiring H]
[Bialgebra R H]
[Semiring K]
[Bialgebra R K]
[Semiring A]
[Algebra R A]
[ComoduleAlgebra R H A]
(f : H →ₐc[R] K)
:
ComoduleAlgebra R K A
Corestriction of a comodule algebra along a bialgebra morphism.
Instances For
theorem
TauCeti.ComoduleAlgebra.toComodule_corestrict
{R : Type u_1}
{H : Type u_2}
{K : Type u_3}
{A : Type u_4}
[CommSemiring R]
[Semiring H]
[Bialgebra R H]
[Semiring K]
[Bialgebra R K]
[Semiring A]
[Algebra R A]
[ComoduleAlgebra R H A]
(f : H →ₐc[R] K)
:
The underlying comodule of a corestricted comodule algebra is its corestriction.
theorem
TauCeti.ComoduleAlgebra.corestrict_coact_apply
{R : Type u_1}
{H : Type u_2}
{K : Type u_3}
{A : Type u_4}
[CommSemiring R]
[Semiring H]
[Bialgebra R H]
[Semiring K]
[Bialgebra R K]
[Semiring A]
[Algebra R A]
[ComoduleAlgebra R H A]
(f : H →ₐc[R] K)
(a : A)
:
The corestricted coaction applies id ⊗ f to the original coaction.
@[simp]
theorem
TauCeti.ComoduleAlgebra.corestrict_coactAlgHom
{R : Type u_1}
{H : Type u_2}
{K : Type u_3}
{A : Type u_4}
[CommSemiring R]
[Semiring H]
[Bialgebra R H]
[Semiring K]
[Bialgebra R K]
[Semiring A]
[Algebra R A]
[ComoduleAlgebra R H A]
(f : H →ₐc[R] K)
:
The corestricted algebra coaction is the original coaction followed by id ⊗ f.