Results about the grading structure of the exterior algebra #
Many of these results are copied with minimal modification from the tensor algebra.
The main result is ExteriorAlgebra.gradedAlgebra
, which says that the exterior algebra is a
ℕ-graded algebra.
def
ExteriorAlgebra.GradedAlgebra.ι
(R : Type u_1)
(M : Type u_2)
[CommRing R]
[AddCommGroup M]
[Module R M]
:
M →ₗ[R] ⨁ (i : ℕ), { x // x ∈ LinearMap.range (ExteriorAlgebra.ι R) ^ i }
A version of ExteriorAlgebra.ι
that maps directly into the graded structure. This is
primarily an auxiliary construction used to provide ExteriorAlgebra.gradedAlgebra
.
Instances For
theorem
ExteriorAlgebra.GradedAlgebra.ι_apply
(R : Type u_1)
(M : Type u_2)
[CommRing R]
[AddCommGroup M]
[Module R M]
(m : M)
:
↑(ExteriorAlgebra.GradedAlgebra.ι R M) m = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ExteriorAlgebra.ι R) ^ i }) 1)
{ val := ↑(ExteriorAlgebra.ι R) m,
property := (_ : ↑(ExteriorAlgebra.ι R) m ∈ LinearMap.range (ExteriorAlgebra.ι R) ^ 1) }
theorem
ExteriorAlgebra.GradedAlgebra.ι_sq_zero
(R : Type u_1)
(M : Type u_2)
[CommRing R]
[AddCommGroup M]
[Module R M]
(m : M)
:
↑(ExteriorAlgebra.GradedAlgebra.ι R M) m * ↑(ExteriorAlgebra.GradedAlgebra.ι R M) m = 0
def
ExteriorAlgebra.GradedAlgebra.liftι
(R : Type u_1)
(M : Type u_2)
[CommRing R]
[AddCommGroup M]
[Module R M]
:
ExteriorAlgebra R M →ₐ[R] ⨁ (i : ℕ), { x // x ∈ LinearMap.range (ExteriorAlgebra.ι R) ^ i }
ExteriorAlgebra.GradedAlgebra.ι
lifted to exterior algebra. This is
primarily an auxiliary construction used to provide ExteriorAlgebra.gradedAlgebra
.
Instances For
theorem
ExteriorAlgebra.GradedAlgebra.liftι_eq
(R : Type u_1)
(M : Type u_2)
[CommRing R]
[AddCommGroup M]
[Module R M]
(i : ℕ)
(x : { x // x ∈ LinearMap.range (ExteriorAlgebra.ι R) ^ i })
:
↑(ExteriorAlgebra.GradedAlgebra.liftι R M) ↑x = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ExteriorAlgebra.ι R) ^ i }) i) x
instance
ExteriorAlgebra.gradedAlgebra
(R : Type u_1)
(M : Type u_2)
[CommRing R]
[AddCommGroup M]
[Module R M]
:
GradedAlgebra fun x => LinearMap.range (ExteriorAlgebra.ι R) ^ x
The exterior algebra is graded by the powers of the submodule (ExteriorAlgebra.ι R).range
.