The top exterior line of a subspace

For a subspace W of dimension d, the submodule (W.map (ExteriorAlgebra.ι k)) ^ d is its top exterior line inside the exterior algebra of the ambient space. After extension to any commutative value algebra, a linear automorphism stabilizes this line exactly when it stabilizes the extended subspace. No reducedness assumption on the value algebra is needed.

This supplies the linear-algebra step in Chevalley's realization of a closed subgroup as a line stabilizer. The line is described intrinsically by a submodule power, independently of an adapted basis. Its comparison with scalar extension of the original exterior representation is a separate construction.

References

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

theorem Module.Basis.exteriorPower_eq_span_ιMulti {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (b : Basis (Fin n) R M) : ⋀[R]^n M = R ∙ (ExteriorAlgebra.ιMulti R n) ⇑b

The top exterior power, viewed inside the exterior algebra, is generated by the exterior product of a basis.

theorem Module.Basis.map_ι_span_pow_eq_span_exteriorAlgebra {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_3} [LinearOrder I] (b : Basis I R M) (s : Finset I) : Submodule.map (ExteriorAlgebra.ι R) (Submodule.span R (⇑b '' ↑s)) ^ s.card = R ∙ b.ExteriorAlgebra s

The top exterior power of a coordinate summand is its exterior basis line.

theorem Submodule.finrank_topExteriorLine {k : Type u_1} {V : Type u_2} [Field k] [AddCommGroup V] [Module k V] [Module.Finite k V] (W : Submodule k V) : Module.finrank k ↥(map (ExteriorAlgebra.ι k) W ^ Module.finrank k ↥W) = 1

The top exterior image of a subspace is a line, including when the subspace is zero.

theorem Submodule.nonempty_basis_topExteriorLine_baseChange {k : Type u_1} {V : Type u_2} [Field k] [AddCommGroup V] [Module k V] [Module.Finite k V] (W : Submodule k V) (A : Type u_3) [CommRing A] [Algebra k A] : Nonempty (Module.Basis Unit A ↥(map (ExteriorAlgebra.ι A) (baseChange A W) ^ Module.finrank k ↥W))

After arbitrary scalar extension, the top exterior image of a subspace has a basis indexed by a singleton, including over the zero value algebra.

theorem Submodule.map_topExteriorLine_baseChange_eq_iff {k : Type u_1} {V : Type u_2} [Field k] [AddCommGroup V] [Module k V] [Module.Finite k V] (W : Submodule k V) (A : Type u_3) [CommRing A] [Algebra k A] (f : TensorProduct k A V ≃ₗ[A] TensorProduct k A V) : map (ExteriorAlgebra.map ↑f).toLinearMap (map (ExteriorAlgebra.ι A) (baseChange A W) ^ Module.finrank k ↥W) = map (ExteriorAlgebra.ι A) (baseChange A W) ^ Module.finrank k ↥W ↔ map (↑f) (baseChange A W) = baseChange A W

Over any commutative value algebra, an automorphism stabilizes the top exterior line of an extended subspace if and only if it stabilizes that subspace. The exponent is the dimension over the original field, so this also applies to the zero value algebra.