Basis for ExteriorAlgebra

@[implicit_reducible]

instance ExteriorAlgebra.instDecompositionNatSubmoduleExteriorPower {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] : DirectSum.Decomposition fun (n : ℕ) => ⋀[R]^n M

The direct sum decomposition of the exterior algebra from the graded algebra structure.

Equations

• ExteriorAlgebra.instDecompositionNatSubmoduleExteriorPower = (ExteriorAlgebra.gradedAlgebra R M).toDecomposition

noncomputable def Module.Basis.ExteriorAlgebra {R : Type u_1} {M : Type u_2} {I : Type u_3} [LinearOrder I] [CommRing R] [AddCommGroup M] [Module R M] (b : Basis I R M) : Basis (Finset I) R (_root_.ExteriorAlgebra R M)

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

Equations

• b.ExteriorAlgebra = (⋯.collectedBasis fun (n : ℕ) => Module.Basis.exteriorPower n b).reindex Set.powersetCard.prodEquiv

theorem ExteriorAlgebra.basis_apply {R : Type u_1} {M : Type u_2} {I : Type u_3} [LinearOrder I] [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis I R M) (s : Finset I) : b.ExteriorAlgebra s = ιMulti_family R s.card (⇑b) (Set.powersetCard.prodEquiv.symm s).snd

theorem ExteriorAlgebra.basis_apply_ofCard {R : Type u_1} {M : Type u_2} {n : ℕ} {I : Type u_3} [LinearOrder I] [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis I R M) {s : Finset I} (s_card : s.card = n) : b.ExteriorAlgebra s = ιMulti_family R n (⇑b) (Set.powersetCard.ofCard s_card)

theorem ExteriorAlgebra.basis_apply_powersetCard {R : Type u_1} {M : Type u_2} {m : ℕ} {I : Type u_3} [LinearOrder I] [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I m)) : b.ExteriorAlgebra ↑s = ιMulti_family R m (⇑b) s

theorem ExteriorAlgebra.basis_eq_coe_basis {R : Type u_1} {M : Type u_2} {m : ℕ} {I : Type u_3} [LinearOrder I] [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I m)) : b.ExteriorAlgebra ↑s = ↑((Module.Basis.exteriorPower m b) s)

theorem ExteriorAlgebra.basis_mul_of_not_disjoint {R : Type u_1} {M : Type u_2} {m n : ℕ} {I : Type u_3} [LinearOrder I] [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I m)) (t : ↑(Set.powersetCard I n)) (h : ¬Disjoint ↑s ↑t) : b.ExteriorAlgebra ↑s * b.ExteriorAlgebra ↑t = 0

theorem ExteriorAlgebra.basis_mul_of_disjoint {R : Type u_1} {M : Type u_2} {m n : ℕ} {I : Type u_3} [LinearOrder I] [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I m)) (t : ↑(Set.powersetCard I n)) (h : Disjoint ↑s ↑t) : b.ExteriorAlgebra ↑s * b.ExteriorAlgebra ↑t = Equiv.Perm.sign (Set.powersetCard.permOfDisjoint h) • b.ExteriorAlgebra ↑(Set.powersetCard.disjUnion h)