Constructs a basis for exterior powers

Finiteness of the exterior power.

instance exteriorPower.instFinite {R : Type u_1} {M : Type u_3} {n : ℕ} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] : Module.Finite R ↥(⋀[R]^n M)

The nth exterior power of a finite module is a finite module.

We construct a basis of ⋀[R]^n M from a basis of M.

noncomputable def exteriorPower.ιMultiDual (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I n)) : Module.Dual R ↥(⋀[R]^n M)

If b is a basis of M indexed by a linearly ordered type I and s is a finset of I of cardinality n, then we get a linear form on the nth exterior power of M by applying the exteriorPower.linearForm construction to the family of linear forms given by the coordinates of b indexed by elements of s (ordered using the given order on I).

@[simp]

theorem exteriorPower.ιMultiDual_apply_ιMulti (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I n)) (v : Fin n → M) : (ιMultiDual R n b s) ((ιMulti R n) v) = (Matrix.of fun (i j : Fin n) => (b.coord ((Set.powersetCard.ofFinEmbEquiv.symm s) j)) (v i)).det

theorem exteriorPower.ιMultiDual_apply_diag (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I n)) : (ιMultiDual R n b s) (ιMulti_family R n (⇑b) s) = 1

Let b be a basis of M indexed by a linearly ordered type I and s be a finset of I of cardinality n. If we apply the linear form on ⋀[R]^n M defined by b and s to the exterior product of the b i for i ∈ s, then we get 1.

theorem exteriorPower.ιMultiDual_apply_nondiag (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Module.Basis I R M) (s t : ↑(Set.powersetCard I n)) (hst : s ≠ t) : (ιMultiDual R n b s) (ιMulti_family R n (⇑b) t) = 0

Let b be a basis of M indexed by a linearly ordered type I and s be a finset of I of cardinality n. Let t be a finset of I of cardinality n such that s ≠ t. If we apply the linear form on ⋀[R]^n M defined by b and s to the exterior product of the b i for i ∈ t, then we get 0.

theorem exteriorPower.ιMulti_family_linearIndependent_ofBasis (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Module.Basis I R M) : LinearIndependent (ι := ↑(Set.powersetCard I n)) R (ιMulti_family R n ⇑b)

If b is a basis of M (indexed by a linearly ordered type), then the family exteriorPower.ιMulti R n b of the n-fold exterior products of its elements is linearly independent in the nth exterior power of M.

noncomputable def Module.Basis.exteriorPower {R : Type u_1} {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Basis I R M) : Basis (↑(Set.powersetCard I n)) R ↥(⋀[R]^n M)

If b is a basis of M (indexed by a linearly ordered type), the basis of the nth exterior power of M formed by the n-fold exterior products of elements of b.

@[simp]

theorem exteriorPower.coe_basis (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Module.Basis I R M) : ⇑(Module.Basis.exteriorPower n b) = ιMulti_family R n ⇑b

theorem exteriorPower.basis_apply (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I n)) : (Module.Basis.exteriorPower n b) s = ιMulti_family R n (⇑b) s

theorem exteriorPower.basis_coord (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I n)) : (Module.Basis.exteriorPower n b).coord s = ιMultiDual R n b s

If b is a basis of M indexed by a linearly ordered type I and B is the corresponding basis of the nth exterior power of M, indexed by the set of finsets s of I of cardinality n, then the coordinate function of B at s is the linear form on the nth exterior power defined by b and s in exteriorPower.ιMultiDual.

theorem exteriorPower.basis_repr_apply (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Module.Basis I R M) (x : ↥(⋀[R]^n M)) (s : ↑(Set.powersetCard I n)) : ((Module.Basis.exteriorPower n b).repr x) s = (ιMultiDual R n b s) x

@[simp]

theorem exteriorPower.basis_repr_self (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I n)) : ((Module.Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) s)) s = 1

@[simp]

theorem exteriorPower.basis_repr_ne (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Module.Basis I R M) {s t : ↑(Set.powersetCard I n)} (hst : s ≠ t) : ((Module.Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) s)) t = 0

theorem exteriorPower.basis_repr (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I n)) : (Module.Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) s) = fun₀ | s => 1

Freeness and dimension of `⋀[R]^n M.

instance exteriorPower.instFree (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] : Module.Free R ↥(⋀[R]^n M)

If M is a free module, then so is its nth exterior power.

theorem exteriorPower.finrank_eq (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial R] [Module.Free R M] [Module.Finite R M] : Module.finrank R ↥(⋀[R]^n M) = (Module.finrank R M).choose n

If R is non-trivial and M is finite free of rank r, then the nth exterior power of M is of finrank Nat.choose r n.

Results that only hold over a field.

theorem exteriorPower.ιMulti_family_linearIndependent_field {K : Type u_2} {E : Type u_4} (n : ℕ) [Field K] [AddCommGroup E] [Module K E] {I : Type u_5} [LinearOrder I] {v : I → E} (hv : LinearIndependent K v) : LinearIndependent (ι := ↑(Set.powersetCard I n)) K (ιMulti_family K n v)

If v is a linearly independent family of vectors (indexed by a linearly ordered type), then the family of its n-fold exterior products is also linearly independent.