Exterior powers as comodules

The homogeneous exterior powers of a right comodule over a commutative bialgebra are comodules in their own right. The grading splits their inclusions into the exterior algebra, so no flatness assumption on the bialgebra is needed. Mathlib's finite-generation instance makes these finite comodules whenever the original module is finite.

The inclusion and maps induced by comodule morphisms are equivariant. The wedge formula for the point action describes this finite representation inside the scalar extension of the exterior algebra. It is the homogeneous representation used to replace a subspace stabilizer by the stabilizer of its top exterior line.

References

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

The construction uses Mathlib's DirectSum.subtype_rTensor_injective and LinearMap.codRestrictOfInjective, as does the flat-subcomodule construction in TauCeti.Algebra.Coalgebra.Subcomodule.Induced; the exterior grading replaces flatness here.

noncomputable def TauCeti.Comodule.exteriorPowerCoact (R : Type u_1) (H : Type u_2) (M : Type u_3) [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (n : ℕ) : ↥(⋀[R]^n M) →ₗ[R] TensorProduct R (↥(⋀[R]^n M)) H

The coaction on the nth exterior power, obtained by restricting the multiplicative coaction on the exterior algebra to its homogeneous degree n.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Comodule.subtype_rTensor_exteriorPowerCoact {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (n : ℕ) (x : ↥(⋀[R]^n M)) : (LinearMap.rTensor H (⋀[R]^n M).subtype) ((exteriorPowerCoact R H M n) x) = (exteriorAlgebraCoact R H M) ↑x

Including the exterior-power coaction recovers the coaction on the exterior algebra.

@[implicit_reducible]

noncomputable def TauCeti.Comodule.exteriorPower (R : Type u_1) (H : Type u_2) (M : Type u_3) [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (n : ℕ) : Comodule R H ↥(⋀[R]^n M)

The nth exterior power of a comodule. This is not a global instance: select it explicitly, as with Comodule.exteriorAlgebra. No flatness hypothesis on H is needed.

Equations

• TauCeti.Comodule.exteriorPower R H M n = TauCeti.Comodule.ofInjective (TauCeti.Comodule.exteriorPowerCoact R H M n) (⋀[R]^n M).subtype ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.Comodule.exteriorPower_coact {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (n : ℕ) : coact = exteriorPowerCoact R H M n

The exterior-power comodule has the homogeneous restriction coaction.

noncomputable def TauCeti.Comodule.Hom.exteriorPowerSubtype (R : Type u_1) (H : Type u_2) (M : Type u_3) [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (n : ℕ) : Hom R H (↥(⋀[R]^n M)) (ExteriorAlgebra R M)

The inclusion of a homogeneous exterior power into the exterior algebra, as a comodule morphism.

Equations

• TauCeti.Comodule.Hom.exteriorPowerSubtype R H M n = { toLinearMap := (⋀[R]^n M).subtype, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.exteriorPowerSubtype_toLinearMap {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (n : ℕ) : (exteriorPowerSubtype R H M n).toLinearMap = (⋀[R]^n M).subtype

@[simp]

theorem TauCeti.Comodule.Hom.exteriorPowerSubtype_apply {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (n : ℕ) (x : ↥(⋀[R]^n M)) : (exteriorPowerSubtype R H M n) x = ↑x

noncomputable def TauCeti.Comodule.Hom.exteriorPowerMap {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] (n : ℕ) (f : Hom R H M N) : Hom R H ↥(⋀[R]^n M) ↥(⋀[R]^n N)

The map of exterior powers induced by a comodule morphism, with Mathlib's exteriorPower.map as its underlying linear map.

Equations

• TauCeti.Comodule.Hom.exteriorPowerMap n f = { toLinearMap := exteriorPower.map n f.toLinearMap, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.exteriorPowerMap_toLinearMap {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] (n : ℕ) (f : Hom R H M N) : (exteriorPowerMap n f).toLinearMap = exteriorPower.map n f.toLinearMap

@[simp]

theorem TauCeti.Comodule.Hom.exteriorPowerMap_apply {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] (n : ℕ) (f : Hom R H M N) (x : ↥(⋀[R]^n M)) : (exteriorPowerMap n f) x = (exteriorPower.map n f.toLinearMap) x

theorem TauCeti.Comodule.Hom.exteriorPowerMap_id {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (n : ℕ) : exteriorPowerMap n (id R H M) = id R H ↥(⋀[R]^n M)

Exterior-power maps preserve identity morphisms.

@[simp]

theorem TauCeti.Comodule.Hom.exteriorPowerMap_comp {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] [AddCommGroup P] [Module R P] [Comodule R H P] (n : ℕ) (g : Hom R H N P) (f : Hom R H M N) : exteriorPowerMap n (g.comp f) = (exteriorPowerMap n g).comp (exteriorPowerMap n f)

Exterior-power maps preserve composition.

@[simp]

theorem TauCeti.Comodule.Hom.exteriorPowerSubtype_comp_exteriorPowerMap {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] (n : ℕ) (f : Hom R H M N) : (exteriorPowerSubtype R H N n).comp (exteriorPowerMap n f) = f.exteriorAlgebraMap.comp (exteriorPowerSubtype R H M n)

Exterior-power maps commute with their homogeneous inclusions.

theorem TauCeti.Comodule.baseChange_subtype_endOfPoint_ιMulti {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] {A : Type u_6} [CommSemiring A] [Algebra R A] (n : ℕ) (g : H →ₐ[R] A) (a : A) (v : Fin n → M) : (LinearMap.baseChange A (⋀[R]^n M).subtype) ((endOfPoint (↥(⋀[R]^n M)) g) (a ⊗ₜ[R] (exteriorPower.ιMulti R n) v)) = a • (List.ofFn fun (i : Fin n) => (LinearMap.baseChange A (ExteriorAlgebra.ι R)) ((endOfPoint M g) (1 ⊗ₜ[R] v i))).prod

In the scalar-extended exterior algebra, a point acts on a pure wedge by acting on each generator and multiplying. This describes the point action on the finite-degree comodule, including degree zero and nonreduced value algebras.