Recovering a subspace from its exterior line

A finite subset of a basis spans a direct summand. Its top exterior product recovers that summand: a vector belongs to it exactly when its exterior product with the top product vanishes. Consequently a linear automorphism stabilizes the summand exactly when its induced exterior algebra automorphism stabilizes the line of the top product. All results hold over arbitrary commutative rings, so they apply after scalar extension to nonreduced value algebras as well.

This is the linear algebra in the passage from subspace stabilizers to line stabilizers in Chevalley's theorem; see J. S. Milne, Algebraic Groups (2017), Lemma 4.28 and Theorem 4.27. The recovery argument uses the contraction formulas in TauCeti.LinearAlgebra.ExteriorAlgebra.Contraction.

theorem ExteriorAlgebra.ιMulti_mem_span_of_mem_span {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (v w : Fin n → M) (hw : ∀ (i : Fin n), w i ∈ Submodule.span R (Set.range v)) : (ιMulti R n) w ∈ R ∙ (ιMulti R n) v

The exterior product of a family in the span of another family of the same length belongs to the line generated by the exterior product of that family.

@[simp]

theorem Module.Basis.ι_mul_exteriorAlgebra_eq_zero_iff {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) (v : M) : (ExteriorAlgebra.ι R) v * b.ExteriorAlgebra s = 0 ↔ v ∈ Submodule.span R (⇑b '' ↑s)

A vector belongs to the span of a finite subset of a basis exactly when wedging it with the exterior product of that subset gives zero. This includes the empty subset.

@[simp]

theorem Module.Basis.map_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) {N : Type u_4} [AddCommGroup N] [Module R N] (f : M ≃ₗ[R] N) : (ExteriorAlgebra.map ↑f) (b.ExteriorAlgebra s) = (b.map f).ExteriorAlgebra s

Exterior products are natural under a change of basis induced by a linear equivalence.

theorem Module.Basis.map_span_exteriorAlgebra_le {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) (f : M →ₗ[R] M) (hf : Submodule.map f (Submodule.span R (⇑b '' ↑s)) ≤ Submodule.span R (⇑b '' ↑s)) : Submodule.map (ExteriorAlgebra.map f).toLinearMap (R ∙ b.ExteriorAlgebra s) ≤ R ∙ b.ExteriorAlgebra s

Preserving a coordinate summand preserves its top exterior line.

@[simp]

theorem Module.Basis.map_span_exteriorAlgebra_eq_iff {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) (f : M ≃ₗ[R] M) : Submodule.map (ExteriorAlgebra.map ↑f).toLinearMap (R ∙ b.ExteriorAlgebra s) = R ∙ b.ExteriorAlgebra s ↔ Submodule.map (↑f) (Submodule.span R (⇑b '' ↑s)) = Submodule.span R (⇑b '' ↑s)

A linear automorphism stabilizes the top exterior line of a coordinate summand exactly when it stabilizes that summand. No field or reducedness assumption on the scalars is needed.

@[simp]

theorem Module.Basis.map_span_exteriorPower_eq_iff {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) {n : ℕ} (t : ↑(Set.powersetCard I n)) (f : M ≃ₗ[R] M) : Submodule.map (exteriorPower.map n ↑f) (R ∙ (exteriorPower n b) t) = R ∙ (exteriorPower n b) t ↔ Submodule.map (↑f) (Submodule.span R (⇑b '' ↑↑t)) = Submodule.span R (⇑b '' ↑↑t)

Stabilizing a coordinate summand is equivalent to stabilizing its top exterior line in the corresponding exterior power. This is the form used for finite-dimensional representations.