Exterior images of subrepresentations

The image of the exterior power of a subcomodule is a subcomodule of the ambient exterior power. Over a field, the image of the top exterior power of a finite-dimensional subcomodule W is a line in the ambient nth exterior power, where n = finrank W. When the subcomodule is invariant only after restricting to a subgroup, this line still lies in the restriction of the ambient nth exterior-power representation.

This constructs the invariant line used in Chevalley's subspace-to-line passage, inside a finite-dimensional ambient representation whenever the original representation is finite-dimensional. It includes the zero subspace, whose determinant line has degree zero.

References

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

noncomputable def TauCeti.Subcomodule.exteriorPowerImage {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [Module.Flat R H] [AddCommGroup M] [Module R M] [Comodule R H M] (W : Subcomodule R H M) (n : ℕ) : Subcomodule R H ↥(⋀[R]^n M)

The image of the nth exterior power of a subrepresentation in the ambient exterior representation.

Equations

• W.exteriorPowerImage n = (TauCeti.Comodule.Hom.exteriorPowerMap n W.subtype).range

@[simp]

theorem TauCeti.Subcomodule.exteriorPowerImage_toSubmodule {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [Module.Flat R H] [AddCommGroup M] [Module R M] [Comodule R H M] (W : Subcomodule R H M) (n : ℕ) : (W.exteriorPowerImage n).toSubmodule = (exteriorPower.map n W.toSubmodule.subtype).range

The exterior image has the range of the induced exterior-power map as its carrier.

@[simp]

theorem TauCeti.Subcomodule.mem_exteriorPowerImage {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [Module.Flat R H] [AddCommGroup M] [Module R M] [Comodule R H M] (W : Subcomodule R H M) (n : ℕ) (x : ↥(⋀[R]^n M)) : x ∈ W.exteriorPowerImage n ↔ ∃ (y : ↥(⋀[R]^n ↥W.toSubmodule)), (exteriorPower.map n W.toSubmodule.subtype) y = x

Membership in the exterior image is membership in the image of the exterior power of the underlying subspace.

theorem TauCeti.Subcomodule.instFlat {k : Type u_1} {H : Type u_2} [Field k] [CommSemiring H] [Bialgebra k H] : Module.Flat k H

@[simp]

theorem TauCeti.Subcomodule.finrank_exteriorPowerImage {k : Type u_1} {H : Type u_2} {M : Type u_3} [Field k] [CommSemiring H] [Bialgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (W : Subcomodule k H M) [Module.Finite k ↥W.toSubmodule] (n : ℕ) : Module.finrank k ↥(W.exteriorPowerImage n).toSubmodule = (Module.finrank k ↥W.toSubmodule).choose n

The exterior image of a finite-dimensional subrepresentation has the expected binomial dimension.

theorem TauCeti.Subcomodule.finrank_exteriorPowerImage_finrank {k : Type u_1} {H : Type u_2} {M : Type u_3} [Field k] [CommSemiring H] [Bialgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (W : Subcomodule k H M) [Module.Finite k ↥W.toSubmodule] : Module.finrank k ↥(W.exteriorPowerImage (Module.finrank k ↥W.toSubmodule)).toSubmodule = 1

The top exterior image of a finite-dimensional subrepresentation is a line.

theorem TauCeti.Subcomodule.instFlat_1 {k : Type u_1} [Field k] {K : Type u_4} [CommSemiring K] [Bialgebra k K] : Module.Flat k K

theorem TauCeti.Subcomodule.exists_line_corestrict_exteriorPower {k : Type u_1} {H : Type u_2} {M : Type u_3} [Field k] [CommSemiring H] [Bialgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] {K : Type u_4} [CommSemiring K] [Bialgebra k K] (f : H →ₐc[k] K) (W : Subcomodule k K M) : Module.Finite k ↥W.toSubmodule → have n := Module.finrank k ↥W.toSubmodule; ∃ (L : Subcomodule k K ↥(⋀[k]^n M)), L.toSubmodule = (exteriorPower.map n W.toSubmodule.subtype).range ∧ Module.finrank k ↥L.toSubmodule = 1

A finite-dimensional subrepresentation of a restricted representation determines an invariant line in the restriction of the ambient nth exterior-power representation, where n is the dimension of the subrepresentation. The carrier is the image of its top exterior power, with no basis choices.