Point actions on exterior powers and scalar extension

Let M be a comodule over a commutative bialgebra H, and let g be an A-point of H. There are two ways to let g act on exterior powers after extending scalars to A: through the exterior algebra over A of its action on A ⊗[R] M, or through the exterior-algebra comodule of M and its homogeneous pieces. The comparison TauCeti.exteriorAlgebraEquivBaseChange intertwines the two actions.

As a consequence, for a submodule W of M, the point stabilizes the scalar extension of the exterior image ⋀ⁿ W → ⋀ⁿ M of W in the finite-degree comodule ⋀ⁿ M exactly when it stabilizes the nth power of A ⊗ W inside the exterior algebra over A. Over a field, for n = dim W the latter is the top exterior line of A ⊗ W, which turns a subspace stabilizer into the stabilizer of a line in a rational representation. No flatness or reducedness assumption is needed.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 4.27 and Lemma 4.28.

@[simp]

theorem TauCeti.exteriorAlgebraEquivBaseChange_map_endOfPoint {R : Type u_1} {H : Type u_2} {M : Type u_3} {A : Type u_4} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] [CommRing A] [Algebra R A] (g : H →ₐ[R] A) (x : ExteriorAlgebra A (TensorProduct R A M)) : (exteriorAlgebraEquivBaseChange A) ((ExteriorAlgebra.map (Comodule.endOfPoint M g)) x) = (Comodule.endOfPoint (ExteriorAlgebra R M) g) ((exteriorAlgebraEquivBaseChange A) x)

Scalar extension of exterior algebras intertwines the exterior algebra of a point action with the point action on the exterior-algebra comodule.

theorem TauCeti.Comodule.map_endOfPoint_baseChange_range_exteriorPowerMap_eq_iff {R : Type u_1} {H : Type u_2} {M : Type u_3} {A : Type u_4} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] [CommRing A] [Algebra R A] (W : Submodule R M) (n : ℕ) (g : H →ₐ[R] A) : Submodule.map (endOfPoint (↥(⋀[R]^n M)) g) (Submodule.baseChange A (exteriorPower.map n W.subtype).range) = Submodule.baseChange A (exteriorPower.map n W.subtype).range ↔ Submodule.map (ExteriorAlgebra.map (endOfPoint M g)).toLinearMap (Submodule.map (ExteriorAlgebra.ι A) (Submodule.baseChange A W) ^ n) = Submodule.map (ExteriorAlgebra.ι A) (Submodule.baseChange A W) ^ n

A point stabilizes the scalar extension of the exterior image of ⋀ⁿ W in the comodule ⋀ⁿ M if and only if the exterior algebra of its action stabilizes the nth power of the scalar-extended subspace A ⊗ W.