Exterior comodules and restriction of representations

Exterior algebra and exterior power commute with corestriction along a morphism of commutative bialgebras. For coordinate algebras of affine groups, this says that taking exterior powers commutes with restricting a representation to a subgroup.

The equalities identify the two comodule structures on the same underlying module. They allow exterior powers of subgroup representations to be used inside the restriction of the ambient exterior representation. No flatness or finite-generation assumption is needed.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §3.2.
• J. S. Milne, Algebraic Groups (2017), Theorem 4.27 and Lemma 4.28.

theorem TauCeti.Comodule.exteriorAlgebraCoact_corestrict {R : Type u_1} {H : Type u_2} {K : Type u_3} {M : Type u_4} [CommRing R] [CommSemiring H] [Bialgebra R H] [CommSemiring K] [Bialgebra R K] [AddCommGroup M] [Module R M] [Comodule R H M] (f : H →ₐc[R] K) : have this := Corestrict f.toCoalgHom; exteriorAlgebraCoact R K M = (Algebra.TensorProduct.map (AlgHom.id R (ExteriorAlgebra R M)) ↑f).comp (exteriorAlgebraCoact R H M)

The multiplicative exterior coaction commutes with a bialgebra morphism.

theorem TauCeti.Comodule.exteriorAlgebra_corestrict {R : Type u_1} {H : Type u_2} {K : Type u_3} {M : Type u_4} [CommRing R] [CommSemiring H] [Bialgebra R H] [CommSemiring K] [Bialgebra R K] [AddCommGroup M] [Module R M] [Comodule R H M] (f : H →ₐc[R] K) : have this := exteriorAlgebra R H M; have restricted := Corestrict f.toCoalgHom; have this := Corestrict f.toCoalgHom; exteriorAlgebra R K M = restricted

Restricting the exterior-algebra representation agrees with taking the exterior algebra of the restricted representation.

theorem TauCeti.Comodule.exteriorPowerCoact_corestrict {R : Type u_1} {H : Type u_2} {K : Type u_3} {M : Type u_4} [CommRing R] [CommSemiring H] [Bialgebra R H] [CommSemiring K] [Bialgebra R K] [AddCommGroup M] [Module R M] [Comodule R H M] (f : H →ₐc[R] K) (n : ℕ) : have this := Corestrict f.toCoalgHom; exteriorPowerCoact R K M n = TensorProduct.map LinearMap.id f.toLinearMap ∘ₗ exteriorPowerCoact R H M n

The homogeneous exterior coaction commutes with a bialgebra morphism.

theorem TauCeti.Comodule.exteriorPower_corestrict {R : Type u_1} {H : Type u_2} {K : Type u_3} {M : Type u_4} [CommRing R] [CommSemiring H] [Bialgebra R H] [CommSemiring K] [Bialgebra R K] [AddCommGroup M] [Module R M] [Comodule R H M] (f : H →ₐc[R] K) (n : ℕ) : have this := exteriorPower R H M n; have restricted := Corestrict f.toCoalgHom; have this := Corestrict f.toCoalgHom; exteriorPower R K M n = restricted

Restricting an exterior-power representation agrees with taking the exterior power of the restricted representation, including degree zero.