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 exterior_algebra.graded_algebra, which says that the exterior algebra is a
ℕ-graded algebra.
def
exterior_algebra.graded_algebra.ι
(R : Type u_1)
(M : Type u_2)
[comm_ring R]
[add_comm_group M]
[module R M] :
M →ₗ[R] direct_sum ℕ (λ (i : ℕ), ↥(linear_map.range (exterior_algebra.ι R) ^ i))
A version of exterior_algebra.ι that maps directly into the graded structure. This is
primarily an auxiliary construction used to provide exterior_algebra.graded_algebra.
Equations
- exterior_algebra.graded_algebra.ι R M = (direct_sum.lof R ℕ (λ (i : ℕ), ↥(linear_map.range (exterior_algebra.ι R) ^ i)) 1).comp (linear_map.cod_restrict (linear_map.range (exterior_algebra.ι R) ^ 1) (exterior_algebra.ι R) _)
theorem
exterior_algebra.graded_algebra.ι_apply
(R : Type u_1)
(M : Type u_2)
[comm_ring R]
[add_comm_group M]
[module R M]
(m : M) :
⇑(exterior_algebra.graded_algebra.ι R M) m = ⇑(direct_sum.of (λ (i : ℕ), ↥(linear_map.range (exterior_algebra.ι R) ^ i)) 1) ⟨⇑(exterior_algebra.ι R) m, _⟩
theorem
exterior_algebra.graded_algebra.ι_sq_zero
(R : Type u_1)
(M : Type u_2)
[comm_ring R]
[add_comm_group M]
[module R M]
(m : M) :
⇑(exterior_algebra.graded_algebra.ι R M) m * ⇑(exterior_algebra.graded_algebra.ι R M) m = 0
def
exterior_algebra.graded_algebra.lift_ι
(R : Type u_1)
(M : Type u_2)
[comm_ring R]
[add_comm_group M]
[module R M] :
exterior_algebra R M →ₐ[R] direct_sum ℕ (λ (i : ℕ), ↥(linear_map.range (exterior_algebra.ι R) ^ i))
exterior_algebra.graded_algebra.ι lifted to exterior algebra. This is
primarily an auxiliary construction used to provide exterior_algebra.graded_algebra.
Equations
- exterior_algebra.graded_algebra.lift_ι R M = ⇑(exterior_algebra.lift R) ⟨exterior_algebra.graded_algebra.ι R M _inst_3, _⟩
theorem
exterior_algebra.graded_algebra.lift_ι_eq
(R : Type u_1)
(M : Type u_2)
[comm_ring R]
[add_comm_group M]
[module R M]
(i : ℕ)
(x : ↥(linear_map.range (exterior_algebra.ι R) ^ i)) :
⇑(exterior_algebra.graded_algebra.lift_ι R M) ↑x = ⇑(direct_sum.of (λ (i : ℕ), ↥(linear_map.range (exterior_algebra.ι R) ^ i)) i) x
@[protected, instance]
def
exterior_algebra.graded_algebra
(R : Type u_1)
(M : Type u_2)
[comm_ring R]
[add_comm_group M]
[module R M] :
The exterior algebra is graded by the powers of the submodule (exterior_algebra.ι R).range.