Documentation

Mathlib.LinearAlgebra.ExteriorAlgebra.Basis

Basis for ExteriorAlgebra #

source
๐Ÿ”ธ coverage
@[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.

source
๐Ÿ”ธ coverage
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.

Instances For
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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)